Abstract
Equational tree automata provide a powerful tree language framework that facilitates to recognize congruence closures of tree languages. In the paper we show the emptiness problem for AC-tree automata and the intersection-emptiness problem for regular AC-tree automata, each of which was open in our previous work [20], are decidable, by a straightforward reduction to the reachability problem for ground AC-term rewriting. The newly obtained results generalize decidability of so-called reachable property problem of Mayr and Rusinowitch [17]. We then discuss complexity issue of AC-tree automata. Moreover, in order to solve some other questions about regular A- and AC-tree automata, we recall the basic connection between word languages and tree languages.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
B. Bogaert and S. Tison: Equality and Disequality constraints on Direct Subterms in Tree Automata, Proc. of 9th STACS, Cachan (France), LNCS 577, pp. 161–171 1992.
H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison and M. Tommasi: Tree Automata Techniques and Applications, draft, 1999. Available on http://www.grappa.univ-lille3.fr/tata/
A. Deruyver and R. Gilleron: The Reachability Problem for Ground TRS and Some Extensions, Proc. of 14th CAAP, Barcelona (Spain), LNCS 351, pp. 227–243, 1989.
J. Esparza: Petri Nets, Commutative Context-Free Grammars, and Basic Parallel Processes, Fundamenta Informaticae 31(1), pp. 13–25, 1997.
M.R. Garey and D.S. Johnson: Computers and Intractability: A Guide to the Theory of NP-Completeness, W.H. Freeman & Company, New York, 1979.
F. Gécseg and M. Steinby: Tree Automata, Akadémiai Kiadó, Budapest, 1984.
T. Genet and F. Klay: Rewriting for Cryptographic Protocol Verification, Proc. of 17th CADE, Pittsburgh (PA), LNCS 1831, pp. 271–290, 2000.
J.E. Hopcroft and J.D. Ullman: Introduction to Automata Theory, Languages, and Computation, Addison-Wesley Publishing Company, 1979.
H. Hosoya, J. Vouillon and B.C. Pierce: Regular Expression Types for XML, Proc. of 5th ICFP, Montreal (Canada), SIGPLAN Notices 35(9), pp. 11–22, 2000.
Y. Kaji, T. Fujiwara and T. Kasami: Solving a Unification Problem under Constrained Substitutions Using Tree Automata, JSC 23(1), pp. 79–117, 1997.
M. Kudlek and V. Mitrana: Normal Forms of Grammars, Finite Automata, Abstract Families, and Closure Properties of Macrosets, Multiset Processing, LNCS 2235, pp. 135–146, 2001.
S. LaTorre and M. Napoli: Timed Tree Automata with an Application to Temporal Logic, Acta Informatica 38(2), pp. 89–116, 2001.
D. Lugiez: A Good Class of Tree Automata and Application to Inductive Theorem Proving, Proc. of 25th ICALP, Aalborg (Denmark), LNCS 1443, pp. 409–420, 1998.
D. Lugiez and J.L. Moysset: Tree Automata Help One to Solve Equational Formulae in AC-Theories, JSC 18(4), pp. 297–318, 1994.
E.W. Mayr: An Algorithm for the General Petri Net Reachability Problem, SIAM J. Comput. 13(3), pp. 441–460, 1984.
R. Mayr and M. Rusinowitch: Reachability is Decidable for Ground AC Rewrite Systems, Proc. of 3rd INFINITY, Aalborg (Denmark), 1998. Draft available from http://www.informatik.uni-freiburg.de/~mayrri/ac.ps
R. Mayr and M. Rusinowitch: Process Rewrite Systems, Information and Computation 156, pp. 264–286, 1999.
J. Millen and V. Shmatikov: Constraint Solving for Bounded-Process Cryptographic Protocol Analysis, Proc. of 8th CCS, Philadelphia (PA), pp. 166–175, 2001.
D. Monniaux: Abstracting Cryptographic Protocols with Tree Automata, Proc. of 6th SAS, Venice (Italy), LNCS 1694, pp. 149–163, 1999.
H. Ohsaki: Beyond Regularity: Equational Tree Automata for Associative and Commutative Theories, Proc. of 15th CSL, Paris (France), LNCS 2142, pp. 539–553, 2001.
R.J. Parikh: On Context-Free Languages, JACM 13(4), pp. 570–581, 1966.
X. Rival and J. Goubault-Larrecq: Experiments with Finite Tree Automata in Coq, Proc. of 14th TPHOLs, Edinburgh (Scotland), LNCS 2152, pp. 362–377, 2001.
B. Schneier: Applied Cryptography: Protocols, Algorithms, and Source Code in C, Second Edition, John Wiley & Sons, 1996.
H. Seki, T. Takai, Y. Fujinaka and Y. Kaji: Layered Transducing Term Rewriting System and Its Recognizability Preserving Property, Proc. of 13th RTA, Copenhagen (Denmark), 2002. To appear in LNCS.
T. Takai, Y. Kaji and H. Seki: Right-Linear Finite-Path Overlapping Term Rewriting Systems Effectively Preserve Recognizability, Proc. of 11th RTA, Norwich (UK), LNCS 1833, pp. 246–260, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ohsaki, H., Takai, T. (2002). Decidability and Closure Properties of Equational Tree Languages. In: Tison, S. (eds) Rewriting Techniques and Applications. RTA 2002. Lecture Notes in Computer Science, vol 2378. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45610-4_9
Download citation
DOI: https://doi.org/10.1007/3-540-45610-4_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43916-5
Online ISBN: 978-3-540-45610-0
eBook Packages: Springer Book Archive