Partial-order reduction for general state exploring algorithms

D. Bosnacki, S. Leue, A. Lluch Lafuente

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

12 Citations (Scopus)

Abstract

An important component of partial-order based reduction algorithms is the condition that prevents action ignoring, commonly known as the cycle proviso. In this paper we give a new version of this proviso that is applicable to a general search algorithm skeleton also known as the General State Expanding Algorithm (GSEA). GSEA maintains a set of open (visited but not expanded) states from which states are iteratively selected for exploration and moved to a closed set of states (visited and expanded). Depending on the open set data structure used, GSEA can be instantiated as depth-first, breadth-first, or a directed search algorithm. The proviso is characterized by reference to the open and closed set of states in GSEA. As a result the proviso 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, which is an extension of the model checker SPIN for directed model checking. We evaluate the state space reduction achieved by partial-order reduction according to the proviso that we propose by comparing it on a set of benchmark problems to other reduction approaches. We also compare the use of breadth-first search and A*, two algorithms ensuring that counterexamples of minimal length will be found, together with the proviso that we propose.
Original languageEnglish
Title of host publicationModel Checking Software (Proceedings 13th International SPIN Workshop, Vienna, Austria, March 30-April 1, 2006)
EditorsA. Valmari
Place of PublicationBerlin
PublisherSpringer
Pages271-287
ISBN (Print)978-3-540-33102-5
DOIs
Publication statusPublished - 2006

Publication series

NameLecture Notes in Computer Science
Volume3925
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'Partial-order reduction for general state exploring algorithms'. Together they form a unique fingerprint.

Cite this