Counterexamples for Model Checking of Markov Decision Processes

Zitieren

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:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:bibo="http://purl.org/ontology/bibo/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:dcterms="http://purl.org/dc/terms/" xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > <rdf:Description rdf:about="https://kops.uni-konstanz.de/rdf/resource/123456789/5540"> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:18Z</dc:date> <dc:contributor>Leue, Stefan</dc:contributor> <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> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5540"/> <dc:creator>Aljazzar, Husain</dc:creator> <dc:contributor>Aljazzar, Husain</dc:contributor> <dcterms:rights rdf:resource="http://nbn-resolving.org/urn:nbn:de:bsz:352-20140905103416863-3868037-7"/> <dcterms:title>Counterexamples for Model Checking of Markov Decision Processes</dcterms:title> <dc:language>eng</dc:language> <dc:format>application/pdf</dc:format> <dc:creator>Leue, Stefan</dc:creator> <dc:rights>deposit-license</dc:rights> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">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 160

Das Dokument erscheint in:

KOPS Suche


Stöbern

Mein Benutzerkonto