Counterexamples for Model Checking of Markov Decision Processes


Dateien zu dieser Ressource

Prüfsumme: MD5:61141ef9df0a7454fc38bcba1fd99780

ALJAZZAR, Husain, Stefan LEUE, 2007. Counterexamples for Model Checking of Markov Decision Processes

@techreport{Aljazzar2007Count-5540, series={Technical Report, Chair for Software Engineering, University of Konstanz}, title={Counterexamples for Model Checking of Markov Decision Processes}, year={2007}, number={soft-08-01}, author={Aljazzar, Husain and Leue, Stefan} }

<rdf:RDF xmlns:dcterms="" xmlns:dc="" xmlns:rdf="" xmlns:bibo="" xmlns:dspace="" xmlns:foaf="" xmlns:void="" xmlns:xsd="" > <rdf:Description rdf:about=""> <dc:date rdf:datatype="">2011-03-24T15:56:18Z</dc:date> <dc:contributor>Leue, Stefan</dc:contributor> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dcterms:abstract xml:lang="eng">The debugging of stochastic system models relies on the availability of diagnostic information. Classic probabilistic model checkers, which are based on iterated numerical probability matrix operations, do not provide such diagnostic information. In precursory work, we have devised counterexample generation methods for continuous- and discrete-time Markov Chains based on heuristics guided explicit state space search. In this paper we address the problem of generating diagnostic information, or counterexamples, for Markov Decision Processes (MDPs), which are a convenient formalism for modelling concurrent stochastic systems. We define the notion of counterexamples for MDPs in relation to an upwards-bounded PCTL formula. Next we present our approach to counterexample generation. We first use an adoption of Eppstein's algorithm for k-shortest paths in order to collect the most probable MDP execution traces contributing to a violation of the PCTL formula. We then use the data structure of AND/OR trees in order to adequately extract from the collected execution sequences the most informative counterexample and to compute its probability. In our experimental evaluation we show that our approach scales to models of realistic size, and that the collected diagnostic information is helpful in system debugging.</dcterms:abstract> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dspace:isPartOfCollection rdf:resource=""/> <dspace:hasBitstream rdf:resource=""/> <dcterms:rights rdf:resource=""/> <dcterms:isPartOf rdf:resource=""/> <bibo:uri rdf:resource=""/> <dc:creator>Aljazzar, Husain</dc:creator> <dc:contributor>Aljazzar, Husain</dc:contributor> <dc:language>eng</dc:language> <dcterms:title>Counterexamples for Model Checking of Markov Decision Processes</dcterms:title> <dc:format>application/pdf</dc:format> <dcterms:hasPart rdf:resource=""/> <dc:rights>terms-of-use</dc:rights> <dc:creator>Leue, Stefan</dc:creator> <dcterms:available rdf:datatype="">2011-03-24T15:56:18Z</dcterms:available> <dcterms:issued>2007</dcterms:issued> </rdf:Description> </rdf:RDF>

Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)

AljazzarLeue_TechRep08.pdf 188

Das Dokument erscheint in:

KOPS Suche


Mein Benutzerkonto