On Positive TAGED with a Bounded Number of Constraints

Pierre-Cyrille Heam (1, 2) , 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 With Global Equality Constraints (aka. positive TAGED, or TAGE) are a variety of Bottom-Up Tree Automata, with added expressive power. While there is interest in using this formalism to extend existing regular model-checking frameworks -- built on vanilla tree automata -- such a project can only be practical if the algorithmic complexity of common decision problems is kept tractable. Unfortunately, useful TAGE decision problems sport very high complexities: Membership is NP-complete, Emptiness and Finiteness are both EXPTIME-complete, Universality and Inclusion are undecidable. It is well-known that restricting the kind of equality constraints can have a dramatic effect on complexity, as evidenced by Rigid Tree Automata. However, the influence of the number of constraints on complexity has yet to be examined. In this paper, we focus on three common decision problems: Emptiness, Finiteness and Membership, and study their algorithmic complexity under a bounded number of equality constraints.

Domaines: Théorie et langage formel [cs.FL]

Pierre-Cyrille Heam, Vincent Hugot, Olga Kouchnarenko. On Positive TAGED with a Bounded Number of Constraints. CIAA - 17th International Conference on Implementation and Application of Automata 2012, Jul 2012, Porto, Portugal. pp.329-336, ⟨10.1007/978-3-642-31606-7_29⟩. ⟨hal-00756564⟩