Logics for unranked and unordered trees and their use for querying semistructured data
Expressivité, satisfiabilité et model checking d'une logique spatiale pour arbres non ordonnés
Résumé
Trees are said to be unordered if the order between successor nodes of a given node is not important. Unranked trees are trees which do not have a priori bound on the number of successors of each node of the tree. Unranked and unordered trees are a possible model for semistructured data. The advantage of this model is that it is less dependant on the representation of semistructured data as XML documents, and the drowback is that formalisms (tree automata, logics) for manipulating this kind of trees are generally related with worse complexity results compared with similar formalisms for unranked and ordered trees. Our aim is a theoretical study of some logics for unranked and unordered trees, espetially from the point of view of using it as query languages for semistructured data. Thus, we are interested in the model checking problem and its complexity, in the satisfiability problem and in caracterising the expressive power of these logics. The model checking problem is, given a tree and a logic formula, to decide whether the trees satisfies the formula; model checking is the mecanism used for query evaluation. The satisfiability problem is, given a logic formula, to decide whether this formula admits some models; satisfiability can be used for query optimisation. Finally, caracterisation of the expressive power of a logic is a caracterisation of the kind of properties it can express. We start from a spatial logic which has been introduced as the basis of a query language for semistructured data. This logic is quite expressive and has several kinds of operators. We consider different fragments of this logic. We identify several interesting fragments of the logic for which the satisfiability problem is decidable, when this problem is known to be undecidable for other fragments. We compare fragments of the logic with monadic second order logic on trees and extensions of it. Finally, studying the model checking problem and its complexity allowed us to propose a model checking algorithm and to establish several results on theoretic complexity of model checking for several fragments of the spatial logic.
Loading...