TY - JOUR
T1 - Emptiness and Finiteness for Tree Automata with Global Reflexive Disequality Constraints
AU - Creus, Carles
AU - Gascón, Adria
AU - Godoy, Guillem
PY - 2013
Y1 - 2013
N2 - In recent years, several extensions of tree automata have been considered. Most of them are related with the capability of testing equality or disequality of certain subterms of the term evaluated by the automaton. In particular, tree automata with global constraints are able to test equality and disequality of subterms depending on the state to which they are evaluated. The emptiness problem is known decidable for this kind of automata, but with a non-elementary time complexity, and the finiteness problem remains unknown. In this paper, we consider the particular case of tree automata with global constraints when the constraint is a conjunction of disequalities between states, and the disequality predicate is forced to be reflexive. This restriction is significant in the context of XML definitions with monadic key constraints. We prove that emptiness and finiteness are decidable in triple exponential time for this kind of automata.
AB - In recent years, several extensions of tree automata have been considered. Most of them are related with the capability of testing equality or disequality of certain subterms of the term evaluated by the automaton. In particular, tree automata with global constraints are able to test equality and disequality of subterms depending on the state to which they are evaluated. The emptiness problem is known decidable for this kind of automata, but with a non-elementary time complexity, and the finiteness problem remains unknown. In this paper, we consider the particular case of tree automata with global constraints when the constraint is a conjunction of disequalities between states, and the disequality predicate is forced to be reflexive. This restriction is significant in the context of XML definitions with monadic key constraints. We prove that emptiness and finiteness are decidable in triple exponential time for this kind of automata.
U2 - 10.1007/s10817-012-9270-5
DO - 10.1007/s10817-012-9270-5
M3 - Article
SN - 1573-0670
VL - 51
SP - 371
EP - 400
JO - Journal of Automated Reasoning
JF - Journal of Automated Reasoning
IS - 4
ER -