IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Twentieth Annual IEEE Symposium on

Logic in Computer Science (LICS 2005)

Paper: Model-Checking Hierarchical Structures (at LICS 2005)

Authors: Markus Lohrey


Hierarchical graph definitions allow a modular description of graphs using modules for the specification of repeated substructures. Beside this modularity, hierarchical graph definitions 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 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 graphs is investigated. Several new complete problems for the levels of the polynomial time hierarchy and the exponential time hierarchy are obtained. Two restrictions on the structure of hierarchical graph definitions that lead to more efficient model-checking algorithms are presented.


    author = 	 {Markus Lohrey},
    title = 	 {Model-Checking Hierarchical Structures},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)},
    year =	 {2005},
    month =	 {June}, 
    pages =      {168--177},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}

Last modified: 2017-04-0512:37
Andrzej Murawski