Algorithms for guided tree automata
When reading an input tree, a bottom-up tree automaton is] “unaware” of where it is relative to the root. This problem is important to the efficient implementation of decision procedures for the Monadic Second-order Logic (M2L) on finite trees. In [KS97], it is shown how exponential state space blow-ups may occur in common situations. The analysis of the problem leads to the notion of guided tree automaton for combatting such explosions. The guided automaton is equipped with separate state spaces that are assigned by a top-down automaton, called the guide.
In this paper, we explore the algorithmic and practical problems arising from this relatively complicated automaton concept.
Our solutions are based on a BDD representation of automata [HJJ+96], which allows the practical handling of automata on very large alphabets. In addition, we propose data structures for avoiding the quadratic size of transition tables associated with tree automata.
We formulate and analyze product, projection (subset construction), and minimization algorithms for guided tree automata. We show that our product algorithm for certain languages are asymptotically faster than the usual algorithm that relies on transition tables.
Also, we provide some preliminary experimental results on the use of guided automata vs. standard tree automata.
KeywordsTransition Function Decision Procedure Binary Decision Diagram Input Tree Default Representation
Unable to display preview. Download preview PDF.
- Bry86.R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, Aug 1986.Google Scholar
- CC82.A. Cardon and M. Crochemore. Partitioning a graph in O(¦A¦log2¦V¦). TCS, 19:85–98, 1982.Google Scholar
- HJJ+96.J.G. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS '95, LNCS 1019, 1996. Also available through http://www.brics.dk/klarlund/papers.htrnl.Google Scholar
- KKS96.N. Klarlund, J. Koistinen, and M. Schwartzbach. Formal design constraints. In Proc. OOPSLA '96, 1996. to appear.Google Scholar
- Kla96.N Klarlund. An n log n algorithm for online bdd refinement. Technical report, BRIGS Report Series RS-96-, Department of Computer Science, University of Aarhus, 1996.Google Scholar
- Koz92.D. Kozen. On the Myhill-Nerode theorem for trees. EATCS Bulletin, 47, 1992.Google Scholar
- KS97.N. Klarlund and M. Schwartzbach. Regularity=logic + recursive data types. Technical report, BRICS, 1997. To appear.Google Scholar
- PT87.R. Paige and R. Tarjan. Three efficient algorithms based on partition refinement. SIAM Journal of Computing, 16(6), 1987.Google Scholar
- Tho90.W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133–191. MIT Press/Elsevier, 1990.Google Scholar