
Hierarchical graph definitions allow a modular description of graphs using modules for the specification of repeated substructures. Beside this modularity, hierarchical graph definitions also allow to specify graphs of exponential size using polynomial size descriptions. In many cases, this succinctness increases the computational complexity of decision problems when input graphs are defined hierarchical. 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 graphs is investigated. It is shown that in general these model-checking problems are exponentially harder than their non-hierarchical counterparts, where the input graphs 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.
Hierarchical structures, Model checking, Specification and verification (program logics, model checking, etc.), Computer Networks and Communications, Analysis of algorithms and problem complexity, Model checking , Berechnungskomplexität, Mathematical Logic (CR F.4.1), 511, model-checking, Theoretical Computer Science, Complexity Measures and Classes (CR F.1.3), Complexity classes (hierarchies, relations among complexity classes, etc.), logic in computer science, logic, Logic in computer science, Applied Mathematics, Berechnungskomplexität, Complexity, 004, hierarchical structures, Model-checking, Computational Theory and Mathematics, complexity
Hierarchical structures, Model checking, Specification and verification (program logics, model checking, etc.), Computer Networks and Communications, Analysis of algorithms and problem complexity, Model checking , Berechnungskomplexität, Mathematical Logic (CR F.4.1), 511, model-checking, Theoretical Computer Science, Complexity Measures and Classes (CR F.1.3), Complexity classes (hierarchies, relations among complexity classes, etc.), logic in computer science, logic, Logic in computer science, Applied Mathematics, Berechnungskomplexität, Complexity, 004, hierarchical structures, Model-checking, Computational Theory and Mathematics, complexity
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 8 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
