Generation of Counterexamples for Model Checking of Markov Decision Processes

Aljazzar, Husain; Leue, Stefan

Generation of Counterexamples for Model Checking of Markov Decision Processes

Dateien

3808a197.pdfGröße: 477.39 KBDownloads: 314

Datum

2009

Open Access-Veröffentlichung

Open Access Green

Sammlungen

Informatik und Informationswissenschaft

Publikationstyp

Beitrag zu einem Konferenzband

Publikationsstatus

Published

Erschienen in

2009 Sixth International Conference on the Quantitative Evaluation of Systems. IEEE, 2009, pp. 197-206. ISBN 978-0-7695-3808-2. Available under: doi: 10.1109/QEST.2009.10

Zusammenfassung

The practical usefulness of a model checker as a debugging tool relies on its ability to provide diagnostic information, sometimes also referred to as a counterexample. Current stochastic model checkers do not provide such diagnostic information. In this paper we address this problem for Markov Decision Processes. First, we define the notion of counterexamples in this context. Then, we discuss three methods to generate informative counterexamples which are helpful in system debugging. We point out the advantages and drawbacks of each method. We also experimentally compare all three methods. Our experiments demonstrate the conditions under which each method is appropriate to be used.

Fachgebiet (DDC)

004 Informatik

Konferenz

2009 Sixth International Conference on the Quantitative Evaluation of Systems (QEST), 13. Sep. 2009 - 16. Sep. 2009, Budapest, Hungary

Zitieren

ISO 690

ALJAZZAR, Husain, Stefan LEUE, 2009. Generation of Counterexamples for Model Checking of Markov Decision Processes. 2009 Sixth International Conference on the Quantitative Evaluation of Systems (QEST). Budapest, Hungary, 13. Sep. 2009 - 16. Sep. 2009. In: 2009 Sixth International Conference on the Quantitative Evaluation of Systems. IEEE, 2009, pp. 197-206. ISBN 978-0-7695-3808-2. Available under: doi: 10.1109/QEST.2009.10

BibTex

@inproceedings{Aljazzar2009-09Gener-6192,
  year={2009},
  doi={10.1109/QEST.2009.10},
  title={Generation of Counterexamples for Model Checking of Markov Decision Processes},
  isbn={978-0-7695-3808-2},
  publisher={IEEE},
  booktitle={2009 Sixth International Conference on the Quantitative Evaluation of Systems},
  pages={197--206},
  author={Aljazzar, Husain 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/6192">
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:10:05Z</dc:date>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:rights>terms-of-use</dc:rights>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6192/1/3808a197.pdf"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:10:05Z</dcterms:available>
    <dcterms:abstract xml:lang="eng">The practical usefulness of a model checker as a debugging tool relies on its ability to provide diagnostic information, sometimes also referred to as a counterexample. Current stochastic model checkers do not provide such diagnostic information. In this paper we address this problem for Markov Decision Processes. First, we define the notion of counterexamples in this context. Then, we discuss three methods to generate informative counterexamples which are helpful in system debugging. We point out the advantages and drawbacks of each method. We also experimentally compare all three methods. Our experiments demonstrate the conditions under which each method is appropriate to be used.</dcterms:abstract>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:format>application/pdf</dc:format>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:title>Generation of Counterexamples for Model Checking of Markov Decision Processes</dcterms:title>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/6192"/>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dcterms:issued>2009-09</dcterms:issued>
    <dc:language>eng</dc:language>
    <dc:contributor>Aljazzar, Husain</dc:contributor>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6192/1/3808a197.pdf"/>
    <dc:creator>Leue, Stefan</dc:creator>
    <dcterms:bibliographicCitation>Publ. in: Proceedings of 6th International Conference on the Quantitative Evaluation of SysTems (QEST '09), IEEE Computer Society Press, 2009</dcterms:bibliographicCitation>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:creator>Aljazzar, Husain</dc:creator>
  </rdf:Description>
</rdf:RDF>

Universitätsbibliographie

Ja