Publikation:

DiPro : A Tool for Probabilistic Counterexample Generation

Lade...
Vorschaubild

Dateien

Leitner-Fischer_DiPro.pdf
Leitner-Fischer_DiPro.pdfGröße: 437.67 KBDownloads: 844

Datum

2011

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

ArXiv-ID

Internationale Patentnummer

Angaben zur Forschungsförderung

Projekt

Directed model checking in the analysis of real-time
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

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.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

probabilistic model checking, counterexamples

Konferenz

Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

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

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