Handling Left-Quadratic Rules When Completing Tree Automata
Yohan Boichut, Roméo Courbis, Pierre‐Cyrille Héam, Olga Kouchnarenko · Electronic Notes in Theoretical Computer Science · 2008
This paper addresses the following general problem of tree regular model-checking: decide whether R ∗ ( L ) ∩ L p = ∅ where R ∗ is the reflexive and transitive closure of a successor relation induced by a term rewriting system R , and L and L p are both regular tree languages. We develop an automatic approximation-based technique to handle this – undecidable in general – problem in the case when term rewriting system rules are left-quadratic. The most common practical case is handled this way.