Issue No. 06 - June (2003 vol. 29)
<p><b>Abstract</b>—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 <it>state explosion problem</it>: 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.</p>
State explosion, model checking, heuristic search, temporal logic, local model checking, AND/OR graph.
Antonella Santone, "Heuristic Search + Local Model Checking in Selective mu-Calculus", IEEE Transactions on Software Engineering, vol. 29, no. , pp. 510-523, June 2003, doi:10.1109/TSE.2003.1205179