Publikation:

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

Lade...
Vorschaubild

Dateien

12845.pdf
12845.pdfGröße: 640.82 KBDownloads: 329

Datum

2010

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

ArXiv-ID

Internationale Patentnummer

Angaben zur Forschungsförderung

Projekt

DiRePro: Directed Model Checking in the Analysis of Real-Time and Probabilistic Systems
Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz

Gesperrt bis

Titel in einer weiteren Sprache

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.

Zusammenfassung in einer weiteren Sprache

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
Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690ALJAZZAR, 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>

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