27/10/2005
Jean-Marc Talbot (Laboratoire d'Informatique Fondamentale de Lille)
Model-checking, Satisfiability and Expressiveness for the TQL Logic

We study the TQL logic introduced 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. We will address three issues for this logic: first, we investigate the complexity of model-checking, ie deciding whether a tree is a model of a formula. Then, we study the satisfiability problem for this logic (ie deciding whether a given formula admits a model) as well as its expressiveness; in particular, we will compare various fragments of the TQL logic with the monadic second-order logic.