Improved Model Checking of Hierarchical Systems
===============================================
We present a unified game-based approach for branching-time model checking of
hierarchical systems. Such systems are exponentially more succinct than standard
state-transition graphs, as repeated sub-systems are described only once. Early work on
model checking of hierarchical systems shows that one can do better than a naive
algorithm that "flattens" the system and removes the hierarchy.
Given a hierarchical system $\S$ and a branching-time specification $\psi$ for it, we
reduce the model-checking problem (does $\S$ satisfy $\psi$?) to the problem of solving
a {\em hierarchical game\/} obtained by taking the product of $\S$ with an alternating
tree automaton $\A_\psi$ for $\psi$. Our approach leads to clean, uniform, and improved
model-checking algorithms for a variety of branching-time temporal logics. In
particular, by improving the algorithm for solving hierarchical parity games, we are
able to solve the model-checking problem for the $\mu$-calculus in {\sc Pspace} and time
complexity that is only polynomial in the depth of the hierarchy. Our approach also
leads to an abstraction-refinement paradigm for hierarchical systems. The abstraction
maintains the hierarchy, and is obtained by merging both states and sub-systems into
abstract states.