Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation

Aljazzar, Husain; Kuntz, Matthias; Leitner-Fischer, Florian; Leue, Stefan

Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation

Dateien

12845.pdfGröße: 640.82 KBDownloads: 318

Datum

2010

Projekt

DiRePro: Directed Model Checking in the Analysis of Real-Time and Probabilistic Systems

Open Access-Veröffentlichung

Open Access Green

Sammlungen

Informatik und Informationswissenschaft

Publikationstyp

Beitrag zu einem Konferenzband

Publikationsstatus

Published

Erschienen in

Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems - QUOVADIS '10. New York, New York, USA: ACM Press, 2010, pp. 25-32. ISBN 978-1-60558-972-5. Available under: doi: 10.1145/1808877.1808883

Zusammenfassung

The generation of counterexamples for probabilistic model checking has been an area of active research over the past five years. Tangible outcome of this research are novel directed and heuristic algorithms for efficient generation of probabilistic counterexamples, such as K* and XBF. In this paper we present an empirical evaluation of the efficiency of these algorithms and the well-known Eppstein's algorithm. We will also evaluate the effect of optimizations applied to Eppstein, K* and XBF. Additionally, we will show, how information produced during model checking can be used to guide the search for counterexamples. This is a first step towards automatically generating heuristic functions. The experimental evaluation of the various algorithms is done by applying them to one case study, known from the literature on probabilistic model checking and one case study taken from the automotive industry.

Fachgebiet (DDC)

004 Informatik

Schlagwörter

Algorithms, Reliability, Verification

Konferenz

The 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems - QUOVADIS '10, 3. Mai 2010 - 3. Mai 2010, Cape Town, South Africa

Zitieren

ISO 690

ALJAZZAR, Husain, Matthias KUNTZ, Florian LEITNER-FISCHER, Stefan LEUE, 2010. Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation. The 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems - QUOVADIS '10. Cape Town, South Africa, 3. Mai 2010 - 3. Mai 2010. In: Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems - QUOVADIS '10. New York, New York, USA: ACM Press, 2010, pp. 25-32. ISBN 978-1-60558-972-5. Available under: doi: 10.1145/1808877.1808883

BibTex

@inproceedings{Aljazzar2010Direc-6116,
  year={2010},
  doi={10.1145/1808877.1808883},
  title={Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation},
  isbn={978-1-60558-972-5},
  publisher={ACM Press},
  address={New York, New York, USA},
  booktitle={Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems - QUOVADIS '10},
  pages={25--32},
  author={Aljazzar, Husain and Kuntz, Matthias and Leitner-Fischer, Florian and Leue, Stefan}
}

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/6116">
    <dc:format>application/pdf</dc:format>
    <dcterms:bibliographicCitation>First publ. in: QUOVADIS '10 : Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems May 3, 2010, Cape Town, South Africa / Carlo Ghezzi. New York, NY : ACM, 2010. pp. 25-32</dcterms:bibliographicCitation>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dcterms:abstract xml:lang="eng">The generation of counterexamples for probabilistic model checking has been an area of active research over the past five years. Tangible outcome of this research are novel directed and heuristic algorithms for efficient generation of probabilistic counterexamples, such as K* and XBF. In this paper we present an empirical evaluation of the efficiency of these algorithms and the well-known Eppstein's algorithm. We will also evaluate the effect of optimizations applied to Eppstein, K* and XBF. Additionally, we will show, how information produced during model checking can be used to guide the search for counterexamples. This is a first step towards automatically generating heuristic functions. The experimental evaluation of the various algorithms is done by applying them to one case study, known from the literature on probabilistic model checking and one case study taken from the automotive industry.</dcterms:abstract>
    <dc:contributor>Kuntz, Matthias</dc:contributor>
    <dcterms:issued>2010</dcterms:issued>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:09:38Z</dc:date>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/6116"/>
    <dcterms:title>Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation</dcterms:title>
    <dc:language>eng</dc:language>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6116/1/12845.pdf"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:contributor>Leitner-Fischer, Florian</dc:contributor>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Kuntz, Matthias</dc:creator>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6116/1/12845.pdf"/>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:contributor>Aljazzar, Husain</dc:contributor>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:09:38Z</dcterms:available>
    <dc:creator>Leue, Stefan</dc:creator>
    <dc:creator>Aljazzar, Husain</dc:creator>
    <dc:rights>terms-of-use</dc:rights>
    <dc:creator>Leitner-Fischer, Florian</dc:creator>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
  </rdf:Description>
</rdf:RDF>

Universitätsbibliographie

Ja