Efficient algorithms for hard problems in nondeterministic tree automata
View/ Open
Date
30/11/2017Author
Almeida, Ricardo Manuel de Oliveira
Metadata
Abstract
We present PTIME language-preserving techniques for the reduction of non-deterministic
tree automata, both for the case of finite trees and for infinite trees.
Our techniques are based on new transition removing and state merging results,
which rely on binary relations that compare the downward and upward behaviours
of states in the automaton. We use downward/upward simulation preorders and the
more general but EXPTIME-complete trace inclusion relations, for which we introduce
good under-approximations computable in polynomial time. We provide a complete
picture of combinations of downward and upward simulation/trace inclusions which
can be used in our reduction techniques.
We define an algorithm that puts together all the reduction results found for finite
trees, and implemented it under the name minotaut, a tool built on top of the well-known
tree automata library libvata. We tested minotaut on large collections of
automata from program verification provenience, as well as on different classes of
randomly generated automata. Our algorithm yields substantially smaller and sparser
automata than all previously known reduction techniques, and it is still fast enough to
handle large instances.
Taking reduction of automata on finite trees one step further, we then introduce
saturation, a technique that consists of adding new transitions to an automaton while
preserving its language. We implemented this technique on minotaut and we show
how it can make subsequent state-merge and transition-removal operations more
effective. Thus we obtain a PTIME algorithm that reduces the number of states of
tree automata even more than before.
Additionally, we explore how minotaut alone can play an important role when
performing hard operations like complementation, allowing to obtain smaller complement
automata and at lower computation times overall. We then show how saturation
can extend this contribution even further. An overview of the tool, highlighting some
of its implementation features, is presented as well.