DiPro : A Tool for Probabilistic Counterexample Generation

Aljazzar, Husain; Leitner-Fischer, Florian; Leue, Stefan; Simeonov, Dimitar

DiPro : A Tool for Probabilistic Counterexample Generation

Dateien

Leitner-Fischer_DiPro.pdfGröße: 437.67 KBDownloads: 777

Datum

2011

Projekt

Directed model checking in the analysis of real-time

Open Access-Veröffentlichung

Open Access Green

Sammlungen

Informatik und Informationswissenschaft

Publikationstyp

Beitrag zu einem Konferenzband

Publikationsstatus

Published

Erschienen in

GROCE, Alex, ed., Madanlal MUSUVATHI, ed.. Model Checking Software. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 183-187. Lecture Notes in Computer Science. 6823. ISBN 978-3-642-22305-1. Available under: doi: 10.1007/978-3-642-22306-8_13

Zusammenfassung

The computation of counterexamples for probabilistic model checking has been an area of active research over the past years. In spite of the achieved theoretical results in this field, there is no freely available tool that allows for the computation and representation of probabilistic counterexamples. We present an open source tool called DiPro that can be used with the PRISM and MRMC probabilistic model checkers. It allows for the computation of probabilistic counterexamples for discrete time Markov chains (DTMCs), continuous time Markov chains (CTMCs) and Markov decision processes (MDPs). The computed counterexamples can be rendered graphically.

Fachgebiet (DDC)

004 Informatik

Schlagwörter

probabilistic model checking, counterexamples

Zitieren

ISO 690

ALJAZZAR, Husain, Florian LEITNER-FISCHER, Stefan LEUE, Dimitar SIMEONOV, 2011. DiPro : A Tool for Probabilistic Counterexample Generation. In: GROCE, Alex, ed., Madanlal MUSUVATHI, ed.. Model Checking Software. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 183-187. Lecture Notes in Computer Science. 6823. ISBN 978-3-642-22305-1. Available under: doi: 10.1007/978-3-642-22306-8_13

BibTex

@inproceedings{Aljazzar2011DiPro-14780,
  year={2011},
  doi={10.1007/978-3-642-22306-8_13},
  title={DiPro : A Tool for Probabilistic Counterexample Generation},
  number={6823},
  isbn={978-3-642-22305-1},
  publisher={Springer Berlin Heidelberg},
  address={Berlin, Heidelberg},
  series={Lecture Notes in Computer Science},
  booktitle={Model Checking Software},
  pages={183--187},
  editor={Groce, Alex and Musuvathi, Madanlal},
  author={Aljazzar, Husain and Leitner-Fischer, Florian and Leue, Stefan and Simeonov, Dimitar}
}

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/14780">
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-12-07T07:33:59Z</dc:date>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:bibliographicCitation>First publ. in: Model checking software : proceedings ; 18th International SPIN Workshop, Snowbird, UT, USA, July 14 - 15, 2011 / Alex Groce ; Madanlal Musuvathi (ed.). - Berlin ; Heidelberg : Springer, 2011. - pp. 183-187. - (Lecture notes in computer science ; 6823). -  ISBN 978-3-642-22305-1</dcterms:bibliographicCitation>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:issued>2011</dcterms:issued>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/14780/1/Leitner-Fischer_DiPro.pdf"/>
    <dc:rights>terms-of-use</dc:rights>
    <dc:language>eng</dc:language>
    <dc:contributor>Aljazzar, Husain</dc:contributor>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2012-08-31T22:25:04Z</dcterms:available>
    <dc:contributor>Leitner-Fischer, Florian</dc:contributor>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/14780/1/Leitner-Fischer_DiPro.pdf"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:creator>Simeonov, Dimitar</dc:creator>
    <dc:creator>Leue, Stefan</dc:creator>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/14780"/>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:contributor>Simeonov, Dimitar</dc:contributor>
    <dc:creator>Leitner-Fischer, Florian</dc:creator>
    <dc:creator>Aljazzar, Husain</dc:creator>
    <dcterms:title>DiPro : A Tool for Probabilistic Counterexample Generation</dcterms:title>
    <dcterms:abstract xml:lang="eng">The computation of counterexamples for probabilistic model checking has been an area of active research over the past years. In spite of the achieved theoretical results in this field, there is no freely available tool that allows for the computation and representation of probabilistic counterexamples. We present an open source tool called DiPro that can be used with the PRISM and MRMC probabilistic model checkers. It allows for the computation of probabilistic counterexamples for discrete time Markov chains (DTMCs), continuous time Markov chains (CTMCs) and Markov decision processes (MDPs). The computed counterexamples can be rendered graphically.</dcterms:abstract>
  </rdf:Description>
</rdf:RDF>

Universitätsbibliographie

Ja