Fixpoint logics over hierarchical structures

Hierarchical graph definitions allow a modular description of graphs using mod-ules for the specification of repeated substructures. Beside this modularity, hierarchi-cal graph definitions also allow to specify graphs of exponential size using polynomial size descriptions. In many cases, this succinctness increases the computational com-plexity 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 hierar-chically 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.