Completeness of Tree Automata Completion

Thomas Genet (1)

1 CELTIQUE - Software certification with semantic analysis

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.

Mots clés: tree automata; tree automata completion; regularity preservation; Other Rewriting Systems; over-approximation; completeness

Domaines: Génie logiciel [cs.SE]; Informatique et langage [cs.CL]; Théorie et langage formel [cs.FL]

Thomas Genet. Completeness of Tree Automata Completion. FSCD 2018 - 3rd International Conference on Formal Structures for Computation and Deduction, Jul 2018, Oxford, United Kingdom. pp.1-20, ⟨10.4230/LIPIcs.FSCD.2018.15⟩. ⟨hal-01778407⟩