×

Reachability, confluence, and termination analysis with state-compatible automata. (English) Zbl 1362.68137

Summary: Regular tree languages are a popular device for reachability analysis over term rewrite systems, with many applications like analysis of cryptographic protocols, or confluence and termination analysis. At the heart of this approach lies tree automata completion, first introduced by Genet for left-linear rewrite systems. Korp and Middeldorp introduced so-called quasi-deterministic automata to extend the technique to non-left-linear systems. In this paper, we introduce the simpler notion of state-compatible automata, which are slightly more general than quasi-deterministic, compatible automata. This notion also allows us to decide whether a regular tree language is closed under rewriting, a problem which was not known to be decidable before.
The improved precision has a positive impact in applications which are based on reachability analysis, namely termination and confluence analysis.
Our results have been formalized in the theorem prover Isabelle/HOL. This allows to certify automatically generated proofs that are using tree automata techniques.

MSC:

68Q45 Formal languages and automata
68Q42 Grammars and rewriting systems
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press
[2] Boyer, B.; Genet, T.; Jensen, T. P., Certifying a tree automata completion checker, (Proc. 4th International Joint Conference on Automated Reasoning. Proc. 4th International Joint Conference on Automated Reasoning, Lect. Notes Comput. Sci., vol. 5195 (2008)), 523-538 · Zbl 1165.68400
[3] Comon, H.; Dauchet, M.; Gilleron, R.; Jacquemard, F.; Lugiez, D.; Löding, C.; Tison, S.; Tommasi, M., Tree automata techniques and applications (2007), available at
[4] Endrullis, J.; de Vrijer, R. C.; Waldmann, J., Local termination, (Proc. 20th International Conference on Rewriting Techniques and Applications. Proc. 20th International Conference on Rewriting Techniques and Applications, Lect. Notes Comput. Sci., vol. 5595 (2009)), 270-284 · Zbl 1242.68130
[5] Felgenhauer, B.; Thiemann, R., Reachability analysis with state-compatible automata, (Proc. 8th International Conference on Language and Automata Theory and Applications. Proc. 8th International Conference on Language and Automata Theory and Applications, Lect. Notes Comput. Sci., vol. 8370 (2014)), 347-359 · Zbl 1362.68136
[6] Feuillade, G.; Genet, T.; Tong, V. V.T., Reachability analysis over term rewriting systems, J. Autom. Reason., 33, 341-383 (2004) · Zbl 1075.68038
[7] Genet, T., Decidable approximations of sets of descendants and sets of normal forms, (Proc. 9th International Conference on Rewriting Techniques and Applications. Proc. 9th International Conference on Rewriting Techniques and Applications, Lect. Notes Comput. Sci., vol. 1379 (1998)), 151-165
[8] Genet, T.; Tang-Talpin, Y.-M.; Tong, V. V.T., Verification of copy-protection cryptographic protocol using approximations of term rewriting systems, (Proc. WITS’03 (Workshop on Issues in the Theory of Security) (2003))
[9] Geser, A.; Hofbauer, D.; Waldmann, J.; Zantema, H., On tree automata that certify termination of left-linear term rewriting systems, Inf. Comput., 205, 4, 512-534 (2007) · Zbl 1112.68077
[10] Haftmann, F.; Nipkow, T., Code generation via higher-order rewrite systems, (Proc. 10th International Symposium on Functional and Logic Programming. Proc. 10th International Symposium on Functional and Logic Programming, Lect. Notes Comput. Sci., vol. 6009 (2010)), 103-117 · Zbl 1284.68131
[11] Hirokawa, N.; Middeldorp, A., Tyrolean termination tool, (Proc. 16th International Conference on Rewriting Techniques and Applications. Proc. 16th International Conference on Rewriting Techniques and Applications, Lect. Notes Comput. Sci., vol. 3467 (2005)), 175-184 · Zbl 1078.68656
[12] Korp, M., Termination analysis by tree automata completion (2010), University of Innsbruck, Ph.D. thesis
[13] Korp, M.; Middeldorp, A., Match-bounds revisited, Inf. Comput., 207, 11, 1259-1283 (2009) · Zbl 1192.68399
[15] Lammich, P.; Lochbihler, A., The Isabelle collections framework, (Proc. 1st International Conference on Interactive Theorem Proving. Proc. 1st International Conference on Interactive Theorem Proving, Lect. Notes Comput. Sci., vol. 6172 (2010)), 339-354 · Zbl 1291.68357
[16] Lochbihler, A., Light-weight containers for Isabelle: efficient, extensible, nestable, (Proc. 4th International Conference on Interactive Theorem Proving. Proc. 4th International Conference on Interactive Theorem Proving, Lect. Notes Comput. Sci., vol. 7998 (2013)), 116-132 · Zbl 1317.68219
[17] Nipkow, T.; Paulson, L.; Wenzel, M., Isabelle/HOL - a Proof Assistant for Higher-Order Logic, Lect. Notes Comput. Sci., vol. 2283 (2002), Springer · Zbl 0994.68131
[18] Thiemann, R.; Sternagel, C., Certification of termination proofs using CeTA, (Proc. 22nd International Conference on Theorem Proving in Higher Order Logics. Proc. 22nd International Conference on Theorem Proving in Higher Order Logics, Lect. Notes Comput. Sci., vol. 5674 (2009)), 452-468 · Zbl 1252.68265
[19] Zankl, H.; Felgenhauer, B.; Middeldorp, A., CSI - a confluence tool, (Proc. 23rd International Conference on Automated Deduction. Proc. 23rd International Conference on Automated Deduction, Lect. Notes Artif. Intell., vol. 6803 (2011)), 499-505 · Zbl 1341.68199
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.