Model-checking hierarchical structures

作     者：Lohrey, Markus 

作者机构：Univ Stuttgart FMI D-7000 Stuttgart Germany 

出 版 物：《JOURNAL OF COMPUTER AND SYSTEM SCIENCES》 (计算机与系统科学杂志)

年 卷 期：2012年第78卷第2期

页      面：461-490页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：Model-checking Hierarchical structures Logic in computer science Complexity 

摘      要：Hierarchical graph definitions allow a modular description of structures using modules for the specification of repeated substructures. Beside this modularity, hierarchical graph definitions allow us to specify structures of exponential size using polynomial size descriptions. In many cases, this succinctness increases the computational complexity of decision problems when input structures are defined hierarchically. In this paper, the model-checking problem for first-order logic (FO), monadic second-order logic (MSO), and second-order logic (SO) on hierarchically defined input structures is investigated. It is shown that in general these model-checking problems are exponentially harder than their non-hierarchical counterparts, where the input structures are given explicitly. As a consequence, several new complete problems for the levels of the polynomial time hierarchy and the exponential time hierarchy are obtained. Based on classical results of Gaifman and Courcelle, two restrictions on the structure of hierarchical graph definitions that lead to more efficient model-checking algorithms are presented. (C) 2011 Elsevier Inc. All rights reserved.