On complexity of model-checking for the TQL logic

Abstract

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 TL3 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 TL3 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. © 2004 Springer Science + Business Media, Inc.