Publikation: Generation of Counterexamples for Model Checking of Markov Decision Processes
Lade...
Dateien
Datum
2009
Autor:innen
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
DOI (zitierfähiger Link)
Internationale Patentnummer
Link zur Lizenz
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
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.
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Konferenz
2009 Sixth International Conference on the Quantitative Evaluation of Systems (QEST), 13. Sept. 2009 - 16. Sept. 2009, Budapest, Hungary
Rezension
undefined / . - undefined, undefined
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. Sept. 2009 - 16. Sept. 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.10BibTex
@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>Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Prüfungsdatum der Dissertation
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Ja
