Fixpoint Logics on 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 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 modelchecking problem for the modal µ-calculus and (monadic) least fixpoint logic on hierarchically defined graphs is investigated. In order to analyze the modal µ-calculus, parity games on hierarchically defined graphs are studied.

• Type: Conference
• Year: 2005
• Where: FSTTCS
• Authors: Stefan Göller, Markus Lohrey
• Keywords: Exponential Size, FSTTCS 2005, Hierarchical Graph Definitions, Polynomial Size Descriptions