Journal article
Partial-order reduction and trail improvement in directed model checking
In this paper we present work on trail improvement and partial-order reduction in the context of directed explicit-state model checking. Directed explicit-state model checking employs directed heuristic search algorithms such as A* or best-first search to improve the error-detection capabilities of explicit-state model checking.
We first present the use of directed explicit-state model checking to improve the length of already established error trails. Second, we show that partial-order reduction, which aims at reducing the size of the state space by exploiting the commutativity of concurrent transitions in asynchronous systems, can coexist well with directed explicit-state model checking.
Finally, we illustrate how to mitigate the excessive length of error trails produced by partial-order reduction in explicit-state model checking. In this context we also propose a combination of heuristic search and partial-order reduction to improve the length to already provided counterexamples.
Language: | English |
---|---|
Publisher: | Springer Berlin Heidelberg |
Year: | 2004 |
Pages: | 277-301 |
ISSN: | 14332787 and 14332779 |
Types: | Journal article |
DOI: | 10.1007/s10009-004-0151-z |