<title>On Complexity of Model-Checking for the TQL Logic</title>

<author>Iovka Boneva</author>

<author>Jean-Marc Talbot</author>

<comment>3rd IFIP International Conference on Theoretical Computer Science.</comment>

<abstract><p>In this paper we study the complexity of the model-checking problem for the tree logic introduced as the basis for the query language TQL [Cardelli, Ghelli 01: Query Language Based on the Ambient Logic]. We define two distinct fragments of this logic: TL containing only spatial connectives and TLe containing spatial connectives and quantification. We show that the combined complexity of TL is PSPACE-hard. We also study data complexity of model-checking and show that it is linear for TL, hard for all levels of the polynomial hierarchy for TLe and PSPACE-hard for the full logic. Finally we devise a polynomial space model-checking algorithm showing this way that the model-checking problem for the TQL logic is PSPACE-complete.</p></abstract>

<comment>A previous version has been presented at the 19th International Workshop on Unification.</comment>

<abstract><p>N-ary queries in trees select sets of n-tuples of nodes. We propose and investigate representation formalisms for n-ary queries by tree automata, both for ranked and unranked trees. We show that existential run-based queries capture MSO in the \nary case as well as universal run-based queries. We then investigate queries by unambiguous tree automata that are relevant for query induction. We characterize queries by unambiguous automata by a natural fragment of MSO, show how to decide whether regular queries are definable in that fragment, and how to answer them efficiently in linear time. </p></abstract>

<title>On Complexity of Model-Checking for the TQL Logic</title>

<author>Iovka Boneva</author>

<author>Jean-Marc Talbot</author>

<comment>3rd IFIP International Conference on Theoretical Computer Science.</comment>

<abstract><p>In this paper we study the complexity of the model-checking problem for the tree logic introduced as the basis for the query language TQL [Cardelli, Ghelli 01: Query Language Based on the Ambient Logic]. We define two distinct fragments of this logic: TL containing only spatial connectives and TLe containing spatial connectives and quantification. We show that the combined complexity of TL is PSPACE-hard. We also study data complexity of model-checking and show that it is linear for TL, hard for all levels of the polynomial hierarchy for TLe and PSPACE-hard for the full logic. Finally we devise a polynomial space model-checking algorithm showing this way that the model-checking problem for the TQL logic is PSPACE-complete.</p></abstract>