Partial-order reduction for general state exploring algorithms

Cite This

Files in this item

Checksum: MD5:a420522229824fba610a07a2538590a0

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). 11(1), pp. 39-51. ISSN 1433-2779. eISSN 1433-2787. Available under: doi: 10.1007/s10009-008-0093-y

@article{Bonacki2009Parti-6195, title={Partial-order reduction for general state exploring algorithms}, year={2009}, doi={10.1007/s10009-008-0093-y}, 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 xmlns:dcterms="" xmlns:dc="" xmlns:rdf="" xmlns:bibo="" xmlns:dspace="" xmlns:foaf="" xmlns:void="" xmlns:xsd="" > <rdf:Description rdf:about=""> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:rights>terms-of-use</dc:rights> <dc:contributor>Lluch-Lafuente, Alberto</dc:contributor> <dc:creator>Bo nački, Dragan</dc:creator> <dcterms:available rdf:datatype="">2011-03-24T16:10:06Z</dcterms:available> <bibo:uri rdf:resource=""/> <dc:creator>Lluch-Lafuente, Alberto</dc:creator> <dcterms:issued>2009</dcterms:issued> <dspace:isPartOfCollection rdf:resource=""/> <dc:format>application/pdf</dc:format> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <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> <dc:language>eng</dc:language> <dc:contributor>Bo nački, Dragan</dc:contributor> <dcterms:rights rdf:resource=""/> <dc:creator>Leue, Stefan</dc:creator> <dcterms:title>Partial-order reduction for general state exploring algorithms</dcterms:title> <dc:contributor>Leue, Stefan</dc:contributor> <dc:date rdf:datatype="">2011-03-24T16:10:06Z</dc:date> <dcterms:isPartOf rdf:resource=""/> <dcterms:bibliographicCitation>First publ. in: International Journal on Software Tools for Technology Transfer (STTT) 11 (2009), 1, pp. 39-51</dcterms:bibliographicCitation> <dspace:hasBitstream rdf:resource=""/> <dcterms:hasPart rdf:resource=""/> </rdf:Description> </rdf:RDF>

Downloads since Oct 1, 2014 (Information about access statistics)

OpenProvisoSTTT.pdf 203

This item appears in the following Collection(s)

Search KOPS


My Account