Emptiness and Finiteness for Tree Automata with Global Reflexive Disequality Constraints

Carles Creus, Adria Gascón, Guillem Godoy

Research output: Contribution to journalArticlepeer-review

Abstract

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.
Original languageEnglish
Pages (from-to)371-400
Number of pages30
JournalJournal of Automated Reasoning
Volume51
Issue number4
DOIs
Publication statusPublished - 2013

Fingerprint

Dive into the research topics of 'Emptiness and Finiteness for Tree Automata with Global Reflexive Disequality Constraints'. Together they form a unique fingerprint.

Cite this