Partial-Order Reduction for General State Exploring Algorithms

Dragan Bošnački, Stefan Leue, Alberto Lluch Lafuente

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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 : 13th International SPIN Workshop, Vienna, Austria, March 30 - April 1, 2006. Proceedings
PublisherSpringer Berlin Heidelberg
Publication date2006
Pages271-287
ISBN (Print)978-3-540-33102-5
ISBN (Electronic)978-3-540-33103-2
DOIs
Publication statusPublished - 2006
Externally publishedYes
Event13th International SPIN Workshop on Model Checking Software - Vienna, Austria
Duration: 30 Mar 20061 Apr 2006
Conference number: 13

Conference

Conference13th International SPIN Workshop on Model Checking Software
Number13
CountryAustria
CityVienna
Period30/03/200601/04/2006
SeriesLecture Notes in Computer Science
Volume3925
ISSN0302-9743

Cite this