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~(exist) 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~(exist) 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.
展开▼
机译：在本文中，我们研究了作为查询语言TQL的基础而引入的树逻辑的模型检查问题的复杂性[Cardelli and Ghelli，2001]。我们定义了这种逻辑的两个截然不同的片段：仅包含空间连接词的TL和包含空间连接词和量化的TL_（exist）。我们证明了TL的综合复杂性是PSPACE困难的。我们还研究了模型检查的数据复杂性，并表明它对于TL是线性的，对于TL〜（exist）的多项式层次结构的所有级别来说是困难的，而对于完整逻辑而言则是PSPACE-hard。最后，我们设计了一种多项式空间模型检查算法，该算法显示了TQL逻辑的模型检查问题是PSPACE完全的。
展开▼
