Abstract
We present a tool for checking the sufficient completeness of left-linear, order-sorted equational specifications modulo associativity, commutativity, and identity. Our tool treats this problem as an equational tree automata decision problem using the tree automata library CETA, which we also introduce in this paper. CETA implements a semi-algorithm for checking the emptiness of a class of tree automata that are closed under Boolean operations and an equational theory containing associativity, commutativity and identity axioms. Though sufficient completeness for this class of specifications is undecidable in general, our tool is a decision procedure for subcases known to be decidable, and has specialized techniques that are effective in practice for the general case.
Research supported by ONR Grant N00014-02-1-0715.
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.
References
Bouhoula, A., Jacquemard, F.: Automatic verification of sufficient completeness for conditional constrained term rewriting systems. Technical Report LSC-05-17, ENS de Cachan (2006), available at http://www.lsv.ens-cachan.fr/Publis/
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications, (1997) (release October 1, 2002), available at: http://www.grappa.univ-lille3.fr/tata
Comon, H., Jacquemard, F.: Ground reducibility is EXPTIME-complete. Information and Computation 187(1), 123–153 (2003)
Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica 10, 27–52 (1978)
Hendrix, J., Clavel, M., Meseguer, J.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165–174. Springer, Heidelberg (2005)
Hendrix, J., Ohsaki, H., Meseguer, J.: Sufficient completeness checking with propositional tree automata. Technical Report UIUCDCS-R-2005-2635, University of Illinois at Urbana-Champaign (2005), available at: http://maude.cs.uiuc.edu/tools/scc/
Hendrix, J., Ohsaki, H., Viswanathan, M.: Propositional Tree Automata. Technical Report UIUCDCS-R-2006-2695, University of Illinois at Urbana-Champaign (2006), available at: http://maude.cs.uiuc.edu/tools/scc/
Kapur, D., Narendran, P., Rosenkrantz, D.J., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Informatica 28(4), 311–350 (1991)
Kapur, D., Narendran, P., Zhang, H.: On sufficient-completeness and related properties of term rewriting systems. Acta Informatica 24(4), 395–415 (1987)
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., 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., Takai, T.: ACTAS: A system design for associative and commutative tree automata theory. In: Proc. of RULE. ENTCS, vol. 124, pp. 97–111. Elsevier, Amsterdam (2005)
Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science 285(2), 487–517 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hendrix, J., Meseguer, J., Ohsaki, H. (2006). A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms. In: Furbach, U., Shankar, N. (eds) Automated Reasoning. IJCAR 2006. Lecture Notes in Computer Science(), vol 4130. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814771_14
Download citation
DOI: https://doi.org/10.1007/11814771_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37187-8
Online ISBN: 978-3-540-37188-5
eBook Packages: Computer ScienceComputer Science (R0)