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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, Aug 1986.
A. Cardon and M. Crochemore. Partitioning a graph in O(¦A¦log2¦V¦). TCS, 19:85–98, 1982.
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.
N. Klarlund, J. Koistinen, and M. Schwartzbach. Formal design constraints. In Proc. OOPSLA '96, 1996. to appear.
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.
D. Kozen. On the Myhill-Nerode theorem for trees. EATCS Bulletin, 47, 1992.
N. Klarlund and M. Schwartzbach. Regularity=logic + recursive data types. Technical report, BRICS, 1997. To appear.
R. Paige and R. Tarjan. Three efficient algorithms based on partition refinement. SIAM Journal of Computing, 16(6), 1987.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Biehl, M., Klarlund, N., Rauhe, T. (1997). Algorithms for guided tree automata. In: Raymond, D., Wood, D., Yu, S. (eds) Automata Implementation. WIA 1996. Lecture Notes in Computer Science, vol 1260. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63174-7_2
Download citation
DOI: https://doi.org/10.1007/3-540-63174-7_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63174-3
Online ISBN: 978-3-540-69205-8
eBook Packages: Springer Book Archive