Partial-order reduction for general state exploring algorithms

Lade...
Vorschaubild
Dateien
OpenProvisoSTTT.pdf
OpenProvisoSTTT.pdfGröße: 239.21 KBDownloads: 264
Datum
2009
Autor:innen
Bo nački, Dragan
Lluch-Lafuente, Alberto
Herausgeber:innen
Kontakt
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
ArXiv-ID
Internationale Patentnummer
EU-Projektnummer
DFG-Projektnummer
Angaben zur Forschungsförderung (Freitext)
Projekt
Open Access-Veröffentlichung
Gesperrt bis
Titel in einer weiteren Sprache
Forschungsvorhaben
Organisationseinheiten
Zeitschriftenheft
Publikationstyp
Zeitschriftenartikel
Publikationsstatus
Published
Erschienen 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
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.

Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Konferenz
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690BO 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>
Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Kontakt
URL der Originalveröffentl.
Prüfdatum der URL
Prüfungsdatum der Dissertation
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Ja
Begutachtet
Diese Publikation teilen