Document Open Access Logo

Completeness of Tree Automata Completion

Author Thomas Genet

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2018.16.pdf
  • Filesize: 0.6 MB
  • 20 pages

Document Identifiers

Author Details

Thomas Genet
  • Univ Rennes/Inria/IRISA, Campus de Beaulieu, 35042 Rennes Cedex, France

Cite AsGet BibTex

Thomas Genet. Completeness of Tree Automata Completion. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSCD.2018.16

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Semantics and reasoning
  • Theory of computation → Rewrite systems
Keywords
  • term rewriting systems
  • regularity preservation
  • over-approximation
  • completeness
  • tree automata
  • tree automata completion

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. 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. Google Scholar
  2. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  3. Y. Boichut, R. Courbis, P.-C. Héam, and O. Kouchnarenko. Handling non left-linear rules when completing tree automata. IJFCS, 20(5), 2009. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. B. Felgenhauer and R. Thiemann. Reachability Analysis with State-Compatible Automata. In LATA'14, volume 8370 of LNCS, pages 347-359. Springer, 2014. Google Scholar
  8. 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.
  9. 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. Google Scholar
  10. T. Genet. Termination Criteria for Tree Automata Completion. Journal of Logical and Algebraic Methods in Programming, 85, Issue 1, Part 1:3-33, 2016. Google Scholar
  11. T. Genet. Automata Completion and Regularity Preservation. Technical report, INRIA, 2017. URL: https://hal.inria.fr/hal-01501744.
  12. 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/.
  13. 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. Google Scholar
  14. T. Genet, T. Haudebourg, and T. Jensen. Verifying higher-order functions with tree automata. In FoSSaCS'18, LNCS. Springer, 2018. To be published. Google Scholar
  15. T. Genet and R. Rusu. Equational tree automata completion. Journal of Symbolic Computation, 45:574-597, 2010. Google Scholar
  16. 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. Google Scholar
  17. 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. Google Scholar
  18. Dexter Kozen. On the Myhill-Nerode theorem for trees. Bull. Europ. Assoc. Theor. Comput. Sci., 47:170-173, June 1992. Google Scholar
  19. 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. Google Scholar
  20. A. Middeldorp. Approximations for strategies and termination. ENTCS, 70(6):1-20, 2002. Google Scholar
  21. L. Ong and S. Ramsay. Verifying higher-order functional programs with pattern-matching algebraic data types. In POPL'11. ACM, 2011. Google Scholar
  22. 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. Google Scholar
  23. T. Takai. A Verification Technique Using Term Rewriting Systems and Abstract Interpretation. In RTA'04, volume 3091 of LNCS, pages 119-133. Springer, 2004. Google Scholar
  24. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact