{SAT} Solvers for Queries over Tree Automata with Constraints

Pierre-Cyrille Héam (1) , Vincent Hugot (1, 2) , Olga Kouchnarenko (1, 2)

1 FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174)
2 CASSIS - Combination of approaches to the security of infinite states systems

Tree automata turned out to be a very convenient framework for modeling and proving properties on infinite systems like communication protocols, Java programs and also in the context of XML programming. Unfortunately, these works are not always supported by efficient verification and validation tools. This paper investigates the use of two SAT solvers --- minisat and picosat--- to evaluate queries over tree automata with global equality and disequality constraints (TAGED s for short). Unlike general tree automata, TAGED s allow to express constraints useful for e.g., evaluating queries over XML documents, like "in the document, two nodes do not have the same key". These queries being based on the membership problem which is NP-complete for TAGEDs, we propose an efficient SAT encoding of the membership problem for TAGEDs and we show its correctness and soundness. The paper reports on the experimental results, and implementation details are given.

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

Pierre-Cyrille Héam, Vincent Hugot, Olga Kouchnarenko. {SAT} Solvers for Queries over Tree Automata with Constraints. CSTVA'10, 2nd Int. Workshop on Constraints in Software Testing Verification and Analysis - co-located with ICST'2010, 2010, France. ⟨hal-00563313⟩