Partial-order reduction and trail improvement in directed model checking

Stefan Edelkamp, Stefan Leue, Alberto Lluch Lafuente

Research output: Contribution to journalJournal articleResearchpeer-review

Abstract

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.
Original languageEnglish
JournalInternational Journal on Software Tools for Technology Transfer
Volume6
Issue number4
Pages (from-to)277-301
Number of pages25
ISSN1433-2779
DOIs
Publication statusPublished - 2004
Externally publishedYes

Keywords

  • Heuristic search
  • HSF-SPIN
  • Model checking
  • Partial-order reduction
  • Trail improvement
  • Modular robots
  • Asynchronous system
  • Best first search
  • Explicit-state model checking
  • Heuristic search algorithms
  • Heuristic algorithms

Fingerprint Dive into the research topics of 'Partial-order reduction and trail improvement in directed model checking'. Together they form a unique fingerprint.

Cite this