Sciweavers

Share
MST
2011

Fixpoint Logics over Hierarchical Structures

8 years 8 months ago
Fixpoint Logics over Hierarchical Structures
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 µ-calculus and (monadic) least fixpoint logic on hierarchically defined input graphs is investigated. In order to analyze the modal µ-calculus, parity games on hierarchically defined input graphs are investigated. Precise upper and lower complexity bounds are derived. A restriction on hierarchical graph definitions that leads to more efficient model-checking algorithms is presented.
Stefan Göller, Markus Lohrey
Added 14 May 2011
Updated 14 May 2011
Type Journal
Year 2011
Where MST
Authors Stefan Göller, Markus Lohrey
Comments (0)
books