Skip to Main content Skip to Navigation
Conference papers

On Positive TAGED with a Bounded Number of Constraints

Pierre-Cyrille Heam 1, 2 Vincent Hugot 1, 2 Olga Kouchnarenko 1, 2
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : 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.
Document type :
Conference papers
Complete list of metadata
Contributor : Pierre-Cyrille Heam <>
Submitted on : Friday, November 23, 2012 - 11:54:09 AM
Last modification on : Thursday, November 12, 2020 - 9:42:08 AM



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⟩



Record views