Tree automata with equality constraints modulo equational theories. (English) Zbl 1137.68035
Summary: This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have a good potential for application in e.g. software verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formulas.
MSC:
| 68Q45 | Formal languages and automata |
| 03B25 | Decidability of theories and sets of sentences |
| 03B35 | Mechanization of proofs and logical operations |
| 03D05 | Automata and formal grammars in connection with logical questions |
Keywords:
first-order theorem proving; tree automata; basic paramodulation; splitting; verification of infinite state systemsReferences:
| [1] | M. Abadi, C. Fournet, Mobile values, new names, and secure communication, in: 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2001.; M. Abadi, C. Fournet, Mobile values, new names, and secure communication, in: 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2001. · Zbl 1323.68398 |
| [2] | Bachmair, L.; Ganzinger, H.; Lynch, C.; Snyder, W., Basic paramodulation, Inform. Comput., 121, 2, 172-192 (1995) · Zbl 0833.68115 |
| [3] | Bogaert, B.; Tison, S., Equality and disequality constraints on direct subterms in tree automata, (9th Symp. on Theoretical Aspects of Computer Science, STACS. 9th Symp. on Theoretical Aspects of Computer Science, STACS, LNCS, vol. 577 (1992), Springer) · Zbl 1493.68183 |
| [4] | J.A. Bull, D.J. Otway, The authentication protocol, Tech. Rep., Defence Research Agency, Malvern, UK, 1997.; J.A. Bull, D.J. Otway, The authentication protocol, Tech. Rep., Defence Research Agency, Malvern, UK, 1997. |
| [5] | Caron, A.-C.; Comon, H.; Coquidé, J.-L.; Dauchet, M.; Jacquemard, F., Pumping, cleaning and symbolic constraints solving, (21st Int. Coll. on Automata, Languages and Programming, ICALP. 21st Int. Coll. on Automata, Languages and Programming, ICALP, LNCS, vol. 820 (1994), Springer) · Zbl 1418.68114 |
| [6] | H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, M. Tommasi, Tree Automata Techniques and Applications, 1997, <http://www.grappa.univ-lille3.fr/tata>.; H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, M. Tommasi, Tree Automata Techniques and Applications, 1997, <http://www.grappa.univ-lille3.fr/tata>. |
| [7] | Dauchet, M.; Caron, A.-C.; Coquidé, J.-L., Automata for reduction properties solving, J. Symbolic Comput., 20, 2, 215-233 (1995) · Zbl 0843.68071 |
| [8] | Denning, D. E.; Sacco, G. M., Timestamps in key distribution protocols, Commun. ACM (1981) |
| [9] | Dershowitz, N.; Jouannaud, J.-P., Rewrite systems, Handbook of Theoretical Computer Science, vol. B (1990), Elsevier, pp. 243-320 · Zbl 0900.68283 |
| [10] | Devienne, P.; Talbot, J.-M.; Tison, S., Set-based analysis for logic programming and tree automata, (Hentenryck, P. V., Static Analysis, 4th International Symposium, SAS. Static Analysis, 4th International Symposium, SAS, Lecture Notes in Computer Science, vol. 1302 (1997), Springer) |
| [11] | T. Frühwirth, E. Shapiro, M. Vardi, E. Yardeni, Logic programs as types for logic programs, in: Proc. of the 6th IEEE Symposium on Logic in Computer Science, 1991.; T. Frühwirth, E. Shapiro, M. Vardi, E. Yardeni, Logic programs as types for logic programs, in: Proc. of the 6th IEEE Symposium on Logic in Computer Science, 1991. |
| [12] | Genet, T.; Klay, F., Rewriting for cryptographic protocol verification, (Proc. of 17th Int. Conf. on Automated Deduction, CADE. Proc. of 17th Int. Conf. on Automated Deduction, CADE, LNCS, vol. 1831 (2000), Springer) · Zbl 0963.94016 |
| [13] | Goubault-Larrecq, J., Deciding \(H_1\) by resolution, Inform. Process. Lett., 95, 3, 401-408 (2005) · Zbl 1185.68620 |
| [14] | Jacquemard, F.; Meyer, C.; Weidenbach, C., Unification in extensions of shallow equational theories, (9th Int. Conf. on Rewriting Techniques and Applications, RTA. 9th Int. Conf. on Rewriting Techniques and Applications, RTA, LNCS, vol. 1379 (1998), Springer) · Zbl 0903.03008 |
| [15] | Jacquemard, F.; Rusinowitch, M.; Vigneron, L., Tree automata with equality constraints modulo equational theories, (Furbach, U.; Shankar, N., Proceedings of 3rd International Joint Conference on Automated Reasoning, IJCAR. Proceedings of 3rd International Joint Conference on Automated Reasoning, IJCAR, Lecture Notes in Artificial Intelligence, vol. 4130 (2006), Springer: Springer Seattle, WA) · Zbl 1137.68035 |
| [16] | Küsters, R.; Wilke, T., Automata-based analysis of recursive cryptographic protocols, (21st Annual Symp. on Theoretical Aspects of Computer Science, STACS. 21st Annual Symp. on Theoretical Aspects of Computer Science, STACS, LNCS, vol. 2996 (2004), Springer) · Zbl 1122.94383 |
| [17] | Lynch, C.; Meadows, C., On the relative soundness of the free algebra model for public key encryption, Electr. Notes Theor. Comput. Sci., 125, 1, 43-54 (2005) · Zbl 1272.94049 |
| [18] | Nielson, F.; Riis Nielson, H.; Seidl, H., Normalizable Horn Clauses, strongly recognizable relations, and Spi, (Static Analysis, 9th Int. Symp., SAS. Static Analysis, 9th Int. Symp., SAS, LNCS, vol. 2477 (2002), Springer) · Zbl 1015.68042 |
| [19] | Nieuwenhuis, R.; Rubio, A., Paramodulation-based theorem proving, (Handbook of Automated Reasoning, vol. I (2001), Elsevier Science and MIT Press), 371-443, (Chapter 7) · Zbl 0997.03012 |
| [20] | Ohsaki, H.; Takai, T., Decidability and closure properties of equational tree languages, (13th Int. Conf. on Rewriting Techniques and Applications, RTA. 13th Int. Conf. on Rewriting Techniques and Applications, RTA, LNCS, vol. 2378 (2002), Springer) · Zbl 1045.68083 |
| [21] | Riazanov, A.; Voronkov, A., Splitting without backtracking, (Proc. of the 17th Int. Joint Conf. on Artificial Intelligence, IJCAI (2001), Morgan Kaufmann) |
| [22] | Seidl, H., Haskell overloading is dexptime-complete, Inform. Process. Lett., 52, 2, 57-60 (1994) · Zbl 0835.68008 |
| [23] | Seki, H.; Takai, T.; Fujinaka, Y.; Kaji, Y., Layered transducing term rewriting system and its recognizability preserving property, (Int. Conf. on Rewriting Techniques and Applications, RTA. Int. Conf. on Rewriting Techniques and Applications, RTA, LNCS, vol. 2378 (2002), Springer) · Zbl 1045.68076 |
| [24] | S. Tison, Tree automata and term rewrite systems, Invited Tutorial at the 11th Int. Conf. on Rewriting Techniques and Applications, RTA, 2000.; S. Tison, Tree automata and term rewrite systems, Invited Tutorial at the 11th Int. Conf. on Rewriting Techniques and Applications, RTA, 2000. |
| [25] | Truderung, T., Selecting theories and recursive protocols, (Abadi, M.; de Alfaro, L., CONCUR. CONCUR, Lecture Notes in Computer Science, vol. 3653 (2005), Springer) · Zbl 1134.94368 |
| [26] | K.N. Verma, Two-way equational tree automata, Ph.D. thesis, ENS Cachan, September 2003.; K.N. Verma, Two-way equational tree automata, Ph.D. thesis, ENS Cachan, September 2003. · Zbl 1038.03047 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
