On Complexity of Model-Checking for the TQL Logic

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 and Ghelli, 2001]. We define two distinct fragments of this logic: TL containing only spatial connectives and TL∃ 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 TL∃ 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.

• Type: Conference
• Year: 2004
• Where: IFIP
• Authors: Iovka Boneva, Jean-Marc Talbot
• Keywords: Communications, IFIPTCS 2004, Model-checking Problem, Query Language Tql, Spatial Connectives