Partial-order reduction for general state exploring algorithms |
| |
Authors: | Dragan Bo?na?ki Stefan Leue Alberto Lluch Lafuente |
| |
Affiliation: | (1) Department of Biomedical Engineering, Eindhoven University of Technology, Den Dolech 2, P.O. Box 513, 5612 MB Eindhoven, The Netherlands;(2) Department of Computer and Information Science, University of Konstanz, 78457 Constance, Germany;(3) Department of Computer Science, University of Pisa, Largo B. Pontecorvo 3, 56127 Pisa, Italy |
| |
Abstract: | Partial-order reduction is one of the main techniques used to tackle the combinatorial state explosion problem occurring in
explicit-state model checking of concurrent systems. The reduction is performed by exploiting the independence of concurrently
executed events, which allows portions of the state space to be pruned. An important condition for the soundness of partial-order-based
reduction algorithms is a condition that prevents indefinite ignoring of actions when pruning the state space. This condition
is commonly known as the cycle proviso. In this paper, we present a new version of this proviso, which is applicable to a general search algorithm skeleton that
we refer to as the general state exploring algorithm (GSEA). GSEA maintains a set of open states from which states are iteratively
selected for expansion and moved to a closed set of states. Depending on the data structure used to represent the open set,
GSEA can be instantiated as a depth-first, a breadth-first, or a directed search algorithm such as Best-First Search or A*.
The proviso is characterized by reference to the open and closed set of states of the search algorithm. As a result, it can
be computed in an efficient manner during the search based on local information. We implemented partial-order reduction for
GSEA based on our proposed proviso in the tool HSF-SPIN, an extension of the explicit-state model checker SPIN for directed
model checking. We evaluate the state space reduction achieved by partial-order reduction using the proposed proviso by comparing
it on a set of benchmark problems to the use of other provisos. We also compare the use of breadth-first search (BFS) and
A*, two algorithms ensuring that counterexamples of minimal length will be found, together with the proviso that we propose. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|