Heuristic Search + Local Model Checking in Selective mu-Calculus

Many tools for the automatic analysis or verification of finite-state distributed systems are based on the construction of the global state graph of the system under consideration. Thus, they often fail because of the state explosion problem: The state space of a distributed system potentially increases exponentially in the number of its parallel components. To overcome this problem in this paper, we present a model checking procedure, based on the combination of heuristic searches with ideas taken from local model checking. We use heuristic mechanisms for the exploration of the search space in order to avoid the construction of the complete state graph.