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 metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/inria-00536696
Contributor : Iovka Boneva <>
Submitted on : Tuesday, November 16, 2010 - 5:32:11 PM
Last modification on : Thursday, July 25, 2019 - 8:50:03 AM
Long-term archiving on : Thursday, February 17, 2011 - 3:07:21 AM

File

lics2005.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00536696, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

228

Files downloads

246