<comment>Submitted to a conference.. 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>First-Order Theory of Subtyping Constraints</title>
<author>Zhendong Su</author>
<author>Alexander Aiken</author>
<author>Joachim Niehren</author>
<author>Tim Priesnitz</author>
<author>Ralf Treinen</author>
<comment>TOPLAS. Extended Version of POPL 2002.</comment>
<abstract><p>We investigate the first-order theory of subtyping constraints. We show that the first-order theory of non-structural subtyping is undecidable, and we show that in the case where all constructors are either unary or nullary, the first-order theory is decidable for both structural and non-structural subtyping.
Our results hold for both simple and recursive types. The undecidability result is shown by a reduction from the Post's Correspondence Problem, and
the decidability results are shown by a reduction to a decision problem on tree automata. In addition, we introduce the notion of a constrained tree automaton to express non-structural subtype entailment.
This work is a step towards resolving long-standing open problems of the decidability of entailment for non-structural subtyping.</p></abstract>
<comment>20th International Conference on Automated Deduction.</comment>
<abstract><p>
Context unification (CU) is the famous open problem of
solving context equations for trees. We distinguish
a new decidable fragment of CU - well-nested CU -
and present a new unification algorithm that solves
well-nested context equations in non-deterministic
polynomial time. We show that minimal
well-nested solutions of context equations can be
composed from the material present in the equation.
This surprising property is highly wishful when
modeling natural language ellipsis in CU.
</p></abstract>
</paper>
</li>
<li>
<paperfile="">
<title>Automata and Logics for Unranked and Unordered Trees</title>
<author>Iovka Boneva</author>
<author>Jean-Marc Talbot</author>
<comment>Rewriting Techniques and Applications, RTA 2005.</comment>
<abstract><p>In this paper, we consider the monadic second order logic (MSO) and two of its extensions, namely Counting MSO (CMSO) and Presburger MSO (PMSO), interpreted over unranked and unordered trees. We survey classes of tree automata introduced for the logics PMSO and CMSO as well as other related formalisms; we gather results from the literature and sometimes clarify or fill the remaining gaps between those various formalisms. Finally, we complete our study by adapting these classes of automata for capturing precisely the expressiveness of the logic MSO.</p></abstract>
<title>Extraction and Implication of Path Constraints</title>
<author>Yves André</author>
<author>Anne-Cécile Caron</author>
<author>Denis Debarbieux</author>
<author>Yves Roos</author>
<author>Sophie Tison</author>
<comment>Proceedings of the 29th Symposium on Mathematical Foundations of Computer Science.</comment>
<abstract><p>We consider semistructured data as rooted edge-labeled directed graphs, and path inclusion
constraints on these graphs.
In this paper, we give a new decision algorithm
for the implication problem of a constraint
$p \preceq q$ by a set of constraints $p_i \preceq u_i$ where $p$, $q$, and the $p_i$'s are regular
path expressions and the $u_i$'s are non-empty paths, improving in this particular case, the
more general algorithms of S. Abiteboul and V. Vianu, and Alechina et al.
Moreover, in the case of a set of word equalities $u_i \equiv v_i$, we give a more efficient
decision algorithm for the implication of a word equality $u \equiv v$, improving the
more general algorithm of P. Buneman et al., and
we prove that, in this case, the implication problem for non-deterministic models or
for (complete) deterministic models are equivalent.</p></abstract>
</paper>
</li>
<li>
<paperfile="">
<title>Expressiveness of a spatial logic for trees</title>
<author>Iovka Boneva</author>
<author>Jean-Marc Talbot</author>
<author>Sophie Tison</author>
<comment>Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005).</comment>
<abstract><p>In this paper we investigate the quantifier-free fragment of the TQL logic proposed by Cardelli and Ghelli. The TQL logic, inspired from the ambient logic, is the core of a query language for semistructured data represented as unranked and unordered trees. The fragment we consider here, named STL, contains as main features spatial composition and location as well as a fixed point construct. We prove that satisfiability for STL is undecidable.We show also that STL is strictly more expressive that the Presburger monadic second-order logic (PMSO) of Seidl, Schwentick and Muscholl when interpreted over unranked and unordered edge-labeled trees. We define a class of tree automata whose transitions are conditioned by arithmetical constraints; we show then how to compute from a closed STL formula a tree automaton accepting precisely the models of the formula. Finally, still using our tree automata framework, we exhibit some syntactic restrictions over STL formulae that allow us to capture precisely the logics MSO and PMSO.</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>
