The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.06 - June (2003 vol.29)
pp: 510-523
ABSTRACT
<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>
INDEX TERMS
State explosion, model checking, heuristic search, temporal logic, local model checking, AND/OR graph.
CITATION
Antonella Santone, "Heuristic Search + Local Model Checking in Selective mu-Calculus", IEEE Transactions on Software Engineering, vol.29, no. 6, pp. 510-523, June 2003, doi:10.1109/TSE.2003.1205179
28 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool