Automata Completion and Regularity Preservation
Thomas Genet · HAL (Le Centre pour la Communication Scientifique Directe) · 2017
We consider rewriting of a regular language with a left-linear term rewriting system. We showtwo completeness theorems. The first one shows that, if the set of reachable terms is regular, thenthe equational tree automata completion can compute it. This was known to be true for someterm rewriting system classes preserving regularity, but was still an open question in the generalcase. The proof is not constructive because it depends on regularity of the set of reachable terms,which is undecidable. The second theorem states that, if there exists a regular over-approximationof the set of reachable terms then completion can compute it (or safely under-approximate it).This theorem also provides an algorithmic way to safely explore regular approximations withcompletion. This has been implemented and used to verify safety properties, automatically, onfirst-order and higher-order functional programs. To carry out the proof, we also generalize andimprove two results of completion: the Termination and the Upper-Bound theorems.