Type of Publication: | Contribution to a conference collection |
URI (citable link): | http://nbn-resolving.de/urn:nbn:de:bsz:352-opus-105327 |
Author: | Aljazzar, Husain; Leue, Stefan |
Year of publication: | 2009 |
Conference: | 2009 Sixth International Conference on the Quantitative Evaluation of Systems (QEST), Sep 13, 2009 - Sep 16, 2009, Budapest, Hungary |
Published in: | 2009 Sixth International Conference on the Quantitative Evaluation of Systems. - IEEE, 2009. - pp. 197-206. - ISBN 978-0-7695-3808-2 |
DOI (citable link): | https://dx.doi.org/10.1109/QEST.2009.10 |
Summary: |
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.
|
Subject (DDC): | 004 Computer Science |
Link to License: | In Copyright |
Bibliography of Konstanz: | Yes |
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, Sep 13, 2009 - Sep 16, 2009. In: 2009 Sixth International Conference on the Quantitative Evaluation of Systems. IEEE, pp. 197-206. ISBN 978-0-7695-3808-2. Available under: doi: 10.1109/QEST.2009.10
@inproceedings{Aljazzar2009-09Gener-6192, title={Generation of Counterexamples for Model Checking of Markov Decision Processes}, year={2009}, doi={10.1109/QEST.2009.10}, 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 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/rdf/resource/123456789/6192"> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6192/1/3808a197.pdf"/> <dcterms:issued>2009-09</dcterms:issued> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/6192"/> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:10:05Z</dcterms:available> <dc:creator>Leue, Stefan</dc:creator> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:language>eng</dc:language> <dc:contributor>Aljazzar, Husain</dc:contributor> <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> <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:rights>terms-of-use</dc:rights> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6192/1/3808a197.pdf"/> <dc:creator>Aljazzar, Husain</dc:creator> <dc:contributor>Leue, Stefan</dc:contributor> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:10:05Z</dc:date> <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:title>Generation of Counterexamples for Model Checking of Markov Decision Processes</dcterms:title> <dc:format>application/pdf</dc:format> </rdf:Description> </rdf:RDF>
3808a197.pdf | 426 |