Technical Report TR-2005-04

BibliographyGöller, Stefan; Lohrey, Markus: Fixpoint logics on hierarchical structures.
University of Stuttgart, Faculty of Computer Science, Electrical Engineering, and Information Technology, Technical Report Computer Science No. 2005/04.
38 pages, english.
CR-SchemaF.1.3 (Complexity Measures and Classes)
F.4.1 (Mathematical Logic)
Keywordsparity games; mu-calculus; hierarchical structures; lfp; mlfp; model checking
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. In this paper, the model-checking problem for the modal $\mu$-calculus and (monadic) least fixpoint logic on hierarchically defined input graphs is investigated. In order to analyze the modal $\mu$-calculus, parity games on hierarchically defined input graphs are investigated. In most cases precise upper and lower complexity bounds are derived. A restriction on hierarchical graph definitions that leads to more efficient model-checking algorithms is presented.

Full text and
other links
PDF (321585 Bytes)
PostScript (702529 Bytes)
Contactgoeller@informatik.uni-stuttgart.de lohrey@informatik.uni-stuttgart.de
Department(s)University of Stuttgart, Institute of Formal Methods in Computer Science, Theoretical Computer Science
Entry dateJune 24, 2005
   Publ. Computer Science