Skip to Main content Skip to Navigation
New interface
Conference papers

Expressiveness of a spatial logic for trees

Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
Contributor : Iovka Boneva Connect in order to contact the contributor
Submitted on : Tuesday, November 16, 2010 - 5:32:11 PM
Last modification on : Friday, February 4, 2022 - 3:18:56 AM
Long-term archiving on: : Thursday, February 17, 2011 - 3:07:21 AM


Files produced by the author(s)


  • HAL Id : inria-00536696, version 1



Iovka Boneva, Jean-Marc Talbot, Sophie Tison. Expressiveness of a spatial logic for trees. 20th Annual IEEE Symposium on Logic in Computer Science, 2005, Chicago, United States. pp.280--289. ⟨inria-00536696⟩



Record views


Files downloads