Handling Left-Quadratic Rules When Completing Tree Automata

Yohan Boichut (1, 2) , Roméo Courbis (2, 3) , Pierre-Cyrille Héam (2) , Olga Kouchnarenko (2, 3)

1 LIFO - Laboratoire d'Informatique Fondamentale d'Orléans
2 FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174)
3 CASSIS - Combination of approaches to the security of infinite states systems

This paper addresses the following general problem of tree regular model-checking: decide whether the intersection of R*(L) and Lp is empty, where R* is the reflexive and transitive closure of a successor relation induced by a term rewriting system R, and L and Lp 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.

Domaines: Génie logiciel [cs.SE]; Modélisation et simulation

Yohan Boichut, Roméo Courbis, Pierre-Cyrille Héam, Olga Kouchnarenko. Handling Left-Quadratic Rules When Completing Tree Automata. 2nd Workshop on Reachability Problems in Computational Models - RP'08, Sep 2008, Liverpool, United Kingdom. pp.61--70, ⟨10.1016/j.entcs.2008.12.031⟩. ⟨hal-00563293⟩