Partial-order reduction for general state exploring algorithms

Bo nački, Dragan; Leue, Stefan; Lluch-Lafuente, Alberto

Partial-order reduction for general state exploring algorithms

Dateien

OpenProvisoSTTT.pdfGröße: 239.21 KBDownloads: 248

Datum

2009

Autor:innen

Bo nački, Dragan

Leue, Stefan

Lluch-Lafuente, Alberto

Publikationstyp

Zeitschriftenartikel

unikn.publication.listelement.citation.prefix.version.undefined

International Journal on Software Tools for Technology Transfer (STTT). 2009, 11(1), pp. 39-51. ISSN 1433-2779. eISSN 1433-2787. Available under: doi: 10.1007/s10009-008-0093-y

Zusammenfassung

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.

Fachgebiet (DDC)

004 Informatik

Zitieren

ISO 690

BO NAČKI, Dragan, Stefan LEUE, Alberto LLUCH-LAFUENTE, 2009. Partial-order reduction for general state exploring algorithms. In: International Journal on Software Tools for Technology Transfer (STTT). 2009, 11(1), pp. 39-51. ISSN 1433-2779. eISSN 1433-2787. Available under: doi: 10.1007/s10009-008-0093-y

BibTex

@article{Bonacki2009Parti-6195,
  year={2009},
  doi={10.1007/s10009-008-0093-y},
  title={Partial-order reduction for general state exploring algorithms},
  number={1},
  volume={11},
  issn={1433-2779},
  journal={International Journal on Software Tools for Technology Transfer (STTT)},
  pages={39--51},
  author={Bo nački, Dragan and Leue, Stefan and Lluch-Lafuente, Alberto}
}

RDF

<rdf:RDF
    xmlns:dcterms="http://purl.org/dc/terms/"
    xmlns:dc="http://purl.org/dc/elements/1.1/"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:bibo="http://purl.org/ontology/bibo/"
    xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
    xmlns:foaf="http://xmlns.com/foaf/0.1/"
    xmlns:void="http://rdfs.org/ns/void#"
    xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > 
  <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/6195">
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/6195"/>
    <dc:creator>Lluch-Lafuente, Alberto</dc:creator>
    <dc:format>application/pdf</dc:format>
    <dcterms:abstract xml:lang="eng">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.</dcterms:abstract>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Bo nački, Dragan</dc:creator>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:rights>terms-of-use</dc:rights>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6195/1/OpenProvisoSTTT.pdf"/>
    <dc:language>eng</dc:language>
    <dcterms:title>Partial-order reduction for general state exploring algorithms</dcterms:title>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:10:06Z</dc:date>
    <dcterms:issued>2009</dcterms:issued>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dcterms:bibliographicCitation>First publ. in: International Journal on Software Tools for Technology Transfer (STTT) 11 (2009), 1, pp. 39-51</dcterms:bibliographicCitation>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6195/1/OpenProvisoSTTT.pdf"/>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:contributor>Lluch-Lafuente, Alberto</dc:contributor>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:10:06Z</dcterms:available>
    <dc:creator>Leue, Stefan</dc:creator>
    <dc:contributor>Bo nački, Dragan</dc:contributor>
  </rdf:Description>
</rdf:RDF>

Universitätsbibliographie

Ja