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 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, 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 exploration of the search space in order to avoid construction of the complete state graph.