Abstract
In this paper, we study combining equational tree automata in two different senses: (1) whether decidability results about equational tree automata over disjoint theories \({\mathcal{E}}_1\) and \({\mathcal{E}}_2\) imply similar decidability results in the combined theory \({\mathcal{E}}_1 \cup {\mathcal{E}}_2\); (2) checking emptiness of a language obtained from the Boolean combination of regular equational tree languages. We present a negative result for the first problem. Specifically, we show that the intersection-emptiness problem for tree automata over a theory containing at least one AC symbol, one ACI symbol, and 4 constants is undecidable despite being decidable if either the AC or ACI symbol is removed. Our result shows that decidability of intersection-emptiness is a non-modular property even for the union of disjoint theories. Our second contribution is to show a decidability result which implies the decidability of two open problems: (1) If idempotence is treated as a rule f(x,x) →x rather than an equation f(x,x) = x, is it decidable whether an AC tree automata accepts an idempotent normal form? (2) If \({\mathcal{E}}\) contains a single ACI symbol and arbitrary free symbols, is emptiness decidable for a Boolean combination of regular \({\mathcal{E}}\)-tree languages?
Keywords
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.
Research supported by ONR Grant N00014-02-1-0715.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2007), http://www.grappa.univ-lille3.fr/tata
Comon, H., Jacquemard, F.: Ground reducibility is EXPTIME-complete. Information and Computation 187(1), 123–153 (2003)
Devienne, P., Talbot, J.-M., Tison, S.: Solving classes of set constraints with tree automata. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 62–76. Springer, Heidelberg (1997)
Feuillade, G., Genet, T., Viet Triem Tong, V.: Reachability analysis over term rewriting systems. J. Autom. Reasoning 33(3–4), 341–383 (2004)
Genet, T., Klay, F.: Rewriting for cryptographic protocol verification. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 271–290. Springer, Heidelberg (2000)
Hendrix, J., Meseguer, J.: On the completeness of context-sensitive order-sorted specifications. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 229–245. Springer, Heidelberg (2007)
Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 151–155. Springer, Heidelberg (2006)
Hendrix, J., Ohsaki, H.: Combining equational tree automata over AC and ACI theories. Technical Report UIUCDCS-R-2008-2940, University of Illinois (2008)
Hendrix, J., Ohsaki, H., Viswanathan, M.: Propositional tree automata. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 50–65. Springer, Heidelberg (2006)
Hopkins, M.W., Kozen, D.: Parikh’s theorem in commutative kleene algebra. In: Proc. of LICS 1999, pp. 394–401. IEEE Computer Society, Los Alamitos (1999)
Jacquemard, F., Rusinowitch, M., Vigneron, L.: Tree automata with equality constraints modulo equational theories. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 557–571. Springer, Heidelberg (2006)
Kapur, D., Narendran, P., Rosenkrantz, D., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Inf. 28(4), 311–350 (1991)
Klarlund, N., Møller, A.: MONA Version 1.4 User Manual. BRICS, Department of Computer Science, University of Aarhus, Notes Series NS-01-1. Revision of BRICS NS-98-3 (January 2001), http://www.brics.dk/mona/
Lugiez, D.: Multitree automata that count. Theoretical Comput. Sci. 333(1–2), 225–263 (2005)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)
Ohsaki, H.: Beyond regularity: Equational tree automata for associative and commutative theories. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 539–553. Springer, Heidelberg (2001)
Ohsaki, H., Seki, H.: Languages modulo normalization. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 221–236. Springer, Heidelberg (2007)
Ohsaki, H., Takai, T.: Decidability and closure properties of equational tree languages. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 114–128. Springer, Heidelberg (2002)
Ohsaki, H., Talbot, J.-M., Tison, S., Roos, Y.: Monotone AC-tree automata. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 337–351. Springer, Heidelberg (2005)
Parikh, R.J.: On context-free languages. J. ACM 13(4), 570–581 (1966)
Shostak, R.E.: Deciding combinations of theories. J. ACM 31(1), 1–12 (1984)
Slutzki, G.: Alternating tree automata. Theoretical Comput. Sci. 41, 305–318 (1985)
Verma, K.N.: On closure under complementation of equational tree automata for theories extending AC. In: Vardi, M.Y., Voronkov, A. (eds.) LPAR 2003. LNCS, vol. 2850, pp. 183–197. Springer, Heidelberg (2003)
Verma, K.N.: Two-way equational tree automata for AC-like theories: Decidability and closure properties. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 180–196. Springer, Heidelberg (2003)
Verma, K.N., Goubault-Larrecq, J.: Alternating two-way AC-tree automata. Information and Computation 205(6), 817–869 (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hendrix, J., Ohsaki, H. (2008). Combining Equational Tree Automata over AC and ACI Theories. In: Voronkov, A. (eds) Rewriting Techniques and Applications. RTA 2008. Lecture Notes in Computer Science, vol 5117. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70590-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-70590-1_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70588-8
Online ISBN: 978-3-540-70590-1
eBook Packages: Computer ScienceComputer Science (R0)