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

<author>Laurent Planque</author>

<author>Iovka Boneva</author>

<author>Jean-Marc Talbot</author>

<author>Sophie Tison</author>

<comment>Submitted to a conference.. 19th International Workshop on Unification.</comment>

<comment>3rd IFIP International Conference on Theoretical Computer Science.</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>

<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>TOPLAS. Extended Version of POPL 2002.</comment>

<author>Sophie Tison</author>

<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>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>

</paper>

</li>

...

...

@@ -72,17 +63,38 @@ This work is a step towards resolving long-standing open problems of the decidab

<title>Automata and Logics for Unranked and Unordered Trees</title>

<title>Indexes and path constraints in semistructured data</title>

<author>Iovka Boneva</author>

<author>Yves Andre</author>

<author>Jean-Marc Talbot</author>

<author>Anne-Cecile Caron</author>

<comment>Rewriting Techniques and Applications, RTA 2005.</comment>

<author>Denis Debarbieux</author>

<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>

<author>Yves Roos</author>

<comment>Workshop on Logical Aspects and Applications of Integrity Constraints.</comment>

<abstract><p>In this paper, we study semistructured data and indexes preserving

inclusion constraints.

A semistructured datum is modelled by multi-rooted edge-labeled

directed graphs.

We consider regular path queries and inclusion constraints other these data.

These constraints are binary relations over regular

path expressions q and r, and are interpreted on a datum as

``for this datum, the answer to query q is included in the answer to query r''.

We study how to represent inclusion constraints that are common to several data.

Our work is based on two existing indexes: dataguide and 1-index.

Given a set of data S, we extract from the

dataguide of S a finite set C(S) of (finite) inclusion constraints

such that an inclusion constraint is satisfied by a datum of S if

and only if it is implied by C(S).

We use 1-index which are covering indexes preserving inclusion

constraints.

Experiments

compare the different ways of using the 1-index to index a set of data.</p></abstract>

</paper>

</li>

...

...

@@ -118,23 +130,6 @@ 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>Indexes and path constraints in semistructured data</title>

<author>Yves Andre</author>

<title>Expressiveness of a spatial logic for trees</title>

<author>Anne-Cecile Caron</author>

<author>Iovka Boneva</author>

<author>Denis Debarbieux</author>

<author>Jean-Marc Talbot</author>

<author>Yves Roos</author>

<author>Sophie Tison</author>

<comment>workshop on Logical Aspects and Applications of Integrity Constraints (DEXA 2005).</comment>

<comment>20th Annual IEEE Symposium on Logic in Computer Science.</comment>

<abstract><p>In this paper, we study semistructured data and indexes preserving

inclusion constraints.

A semistructured datum is modelled by multi-rooted edge-labeled

directed graphs.

We consider regular path queries and inclusion constraints other these data.

These constraints are binary relations over regular

path expressions q and r, and are interpreted on a datum as

``for this datum, the answer to query q is included in the answer to query r''.

We study how to represent inclusion constraints that are common to several data.

Our work is based on two existing indexes: dataguide and 1-index.

Given a set of data S, we extract from the

dataguide of S a finite set C(S) of (finite) inclusion constraints

such that an inclusion constraint is satisfied by a datum of S if

and only if it is implied by C(S).

We use 1-index which are covering indexes preserving inclusion

constraints.

Experiments

compare the different ways of using the 1-index to index a set of data.</p></abstract>

<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>Automata and Logics for Unranked and Unordered Trees</title>

<author>Iovka Boneva</author>

<author>Jean-Marc Talbot</author>

<comment>20th International Conference on Rewriting Techniques and Applications.</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>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 ACM 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>

<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>