WIA 1996: Automata Implementation pp 6-25

# Algorithms for guided tree automata

• Morten Biehl
• Nils Klarlund
• Theis Rauhe
Contributed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1260)

## Abstract

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.

## Keywords

Transition Function Decision Procedure Binary Decision Diagram Input Tree Default Representation
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

## References

1. Bry86.
R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, Aug 1986.Google Scholar
2. CC82.
A. Cardon and M. Crochemore. Partitioning a graph in O(¦A¦log2¦V¦). TCS, 19:85–98, 1982.Google Scholar
3. 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
4. KKS96.
N. Klarlund, J. Koistinen, and M. Schwartzbach. Formal design constraints. In Proc. OOPSLA '96, 1996. to appear.Google Scholar
5. 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
6. Koz92.
D. Kozen. On the Myhill-Nerode theorem for trees. EATCS Bulletin, 47, 1992.Google Scholar
7. KS97.
N. Klarlund and M. Schwartzbach. Regularity=logic + recursive data types. Technical report, BRICS, 1997. To appear.Google Scholar
8. PT87.
R. Paige and R. Tarjan. Three efficient algorithms based on partition refinement. SIAM Journal of Computing, 16(6), 1987.Google Scholar
9. 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

## Authors and Affiliations

• Morten Biehl
• 1
• Nils Klarlund
• 2
• Theis Rauhe
• 1
1. 1.BRICS, Department of Computer ScienceUniversity of AarhusAarhusDenmark
2. 2.AT&T Labs - ResearchMurray Hill