Please use this identifier to cite or link to this item: http://dx.doi.org/10.18419/opus-2546
Authors: Lohrey, Markus
Title: Model checking hierarchical structures
Issue Date: 2005
metadata.ubs.publikation.typ: Arbeitspapier
Series/Report no.: Technischer Bericht / Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik;2005,1
URI: http://nbn-resolving.de/urn:nbn:de:bsz:93-opus-22419
http://elib.uni-stuttgart.de/handle/11682/2563
http://dx.doi.org/10.18419/opus-2546
Abstract: 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.
Appears in Collections:05 Fakultät Informatik, Elektrotechnik und Informationstechnik

Files in This Item:
File Description SizeFormat 
TR_2005_01.pdf345,37 kBAdobe PDFView/Open


Items in OPUS are protected by copyright, with all rights reserved, unless otherwise indicated.