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 for it, we reduce the model-checking problem (does S satisfy ?) to the problem of solving a hierarchical game obtained by taking the product of S with an alternating tree automaton A for . 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 ?-calculus in Pspace and time complexity that is only polynomial in the depth o...

• Type: Conference
• Year: 2010
• Where: VMCAI
• Authors: Benjamin Aminof, Orna Kupferman, Aniello Murano
• Keywords: Branching-time Model Checking, Branching-time Temporal Logics, Hierarchical Parity Games, Software Engineering, VMCAI 2010