HANDLING NON LEFT-LINEAR RULES WHEN COMPLETING TREE AUTOMATA
Yohan Boichut, Roméo Courbis, Pierre‐Cyrille Héam, Olga Kouchnarenko · International Journal of Foundations of Computer Science · 2009
This paper addresses the following general problem of tree regular model-checking: decide whether [Formula: see text] where [Formula: see text] is the reflexive and transitive closure of a successor relation induced by a term rewriting system [Formula: see text], and [Formula: see text] and [Formula: see text] 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 non left-linear.