Completeness of Tree Automata Completion
We consider rewriting of a regular language with a left-linear term rewriting system. We show a completeness theorem on equational tree automata completion stating that, if there exists a regular over-approximation of the set of reachable terms, then equational completion can compute it (or safely under-approximate it). A nice corollary of this theorem is that, if the set of reachable terms is regular, then equational completion can also compute it. This was known to be true for some term rewriting system classes preserving regularity, but was still an open question in the general case. The proof is not constructive because it depends on the regularity of the set of reachable terms, which is undecidable. To carry out those proofs we generalize and improve two results of completion: the Termination and the Upper-Bound theorems. Those theoretical results provide an algorithmic way to safely explore regular approximations with completion. This has been implemented in Timbuk and used to verify safety properties, automatically and efficiently, on first-order and higher-order functional programs.
term rewriting systems
regularity preservation
over-approximation
completeness
tree automata
tree automata completion
Theory of computation~Semantics and reasoning
Theory of computation~Rewrite systems
16:1-16:20
Regular Paper
https://hal.inria.fr/hal-01501744
Thomas
Genet
Thomas Genet
Univ Rennes/Inria/IRISA, Campus de Beaulieu, 35042 Rennes Cedex, France
10.4230/LIPIcs.FSCD.2018.16
A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.-C. Héam, O. Kouchnarenko, J. Mantovani, S. Mödersheim, D. von Oheimb, M. Rusinowitch, J. Santos Santiago, M. Turuani, L. Viganò, and L. Vigneron. The AVISPA Tool for the automated validation of internet security protocols and applications. In CAV'2005, volume 3576 of LNCS, pages 281-285. Springer, 2005.
F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
Y. Boichut, R. Courbis, P.-C. Héam, and O. Kouchnarenko. Handling non left-linear rules when completing tree automata. IJFCS, 20(5), 2009.
Y. Boichut, T. Genet, T. Jensen, and L. Leroux. Rewriting Approximations for Fast Prototyping of Static Analyzers. In RTA'07, volume 4533 of LNCS, pages 48-62. Springer, 2007.
Y. Boichut, P.-C. Héam, and O. Kouchnarenko. Automatic Approximation for the Verification of Cryptographic Protocols. In Proc. AVIS'2004, joint to ETAPS'04, Barcelona (Spain), 2004.
H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, C. Löding, S. Tison, and M. Tommasi. Tree Automata Techniques and Applications. http://tata.gforge.inria.fr, 2008.
B. Felgenhauer and R. Thiemann. Reachability Analysis with State-Compatible Automata. In LATA'14, volume 8370 of LNCS, pages 347-359. Springer, 2014.
G. Feuillade, T. Genet, and V. Viet Triem Tong. Reachability Analysis over Term Rewriting Systems. Journal of Automated Reasonning, 33 (3-4):341-383, 2004. URL: http://people.irisa.fr/Thomas.Genet/publications.html.
http://people.irisa.fr/Thomas.Genet/publications.html
T. Genet. Decidable Approximations of Sets of Descendants and Sets of Normal Forms. In RTA'98, volume 1379 of LNCS, pages 151-165. Springer, 1998.
T. Genet. Termination Criteria for Tree Automata Completion. Journal of Logical and Algebraic Methods in Programming, 85, Issue 1, Part 1:3-33, 2016.
T. Genet. Automata Completion and Regularity Preservation. Technical report, INRIA, 2017. URL: https://hal.inria.fr/hal-01501744.
https://hal.inria.fr/hal-01501744
T. Genet, Y. Boichut, B. Boyer, T. Gillard, T. Haudebourg, and S. Lê Cong. Timbuk 3.2 - a Tree Automata Library. IRISA / Université de Rennes 1, 2017. URL: http://people.irisa.fr/Thomas.Genet/timbuk/.
http://people.irisa.fr/Thomas.Genet/timbuk/
T. Genet, T. Gillard, T. Haudebourg, and S. Lê Cong. Extending timbuk to Verify Functional Programs. In WRLA'18, LNCS. Springer, 2018. To be published.
T. Genet, T. Haudebourg, and T. Jensen. Verifying higher-order functions with tree automata. In FoSSaCS'18, LNCS. Springer, 2018. To be published.
T. Genet and R. Rusu. Equational tree automata completion. Journal of Symbolic Computation, 45:574-597, 2010.
A. Geser, D. Hofbauer, J. Waldmann, and H. Zantema. On tree automata that certify termination of left-linear term rewriting systems. In RTA'05, volume 3467 of LNCS, pages 353-367. Springer, 2005.
F. Jacquemard. Decidable approximations of term rewriting systems. In H. Ganzinger, editor, Proc. of RTA'96, volume 1103 of LNCS, pages 362-376. Springer, 1996.
Dexter Kozen. On the Myhill-Nerode theorem for trees. Bull. Europ. Assoc. Theor. Comput. Sci., 47:170-173, June 1992.
Y. Matsumoto, N. Kobayashi, and H. Unno. Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs. In APLAS'15, volume 9458 of LNCS, pages 295-312. Springer, 2015.
A. Middeldorp. Approximations for strategies and termination. ENTCS, 70(6):1-20, 2002.
L. Ong and S. Ramsay. Verifying higher-order functional programs with pattern-matching algebraic data types. In POPL'11. ACM, 2011.
W. Snyder. Efficient Ground Completion: An O(n log n)lgorithm for Generating Reduced Sets of Ground Rewrite Rules Equivalent to a Set of Ground Equations E. In RTA'89, volume 355 of LNCS, pages 419-433. Springer, 1989.
T. Takai. A Verification Technique Using Term Rewriting Systems and Abstract Interpretation. In RTA'04, volume 3091 of LNCS, pages 119-133. Springer, 2004.
T. Takai, Y. Kaji, and H. Seki. Right-linear finite-path overlapping term rewriting systems effectively preserve recognizability. In RTA'11, volume 1833 of LNCS. Springer, 2000.
T. Genet
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode