Type of Publication:  Contribution to a conference 
Author:  Aljazzar, Husain; Leue, Stefan 
Year of publication:  2006 
Published in:  Formal Modeling and Analysis of Timed Systems / Asarin, Eugene; Bouyer, Patricia (ed.).  Berlin, Heidelberg : Springer Berlin Heidelberg, 2006.  (Lecture Notes in Computer Science ; 4202).  pp. 3351.  ISBN 9783540450269 
DOI (citable link):  https://dx.doi.org/10.1007/11867340_4 
Summary: 
Current numerical model checkers for stochastic systems can efficiently analyse stochastic models. However, the fact that they are unable to provide debugging information constrains their practical use. In precursory work we proposed a method to select diagnostic traces, in the parlance of functional model checking commonly referred to as failure traces or counterexamples, for probabilistic timed reachability properties on discretetime and continuoustime Markov chains. We applied directed explicitstate search algorithms, like Z ∗ , to determine a diagnostic trace which carries large amount of probability. In this paper we extend this approach to determining sets of traces that carry large probability mass, since properties of stochastic systems are typically not violated by single traces, but by collections of those. To this end we extend existing heuristics guided search algorithms so that they select sets of traces. The result is provided in the form of a Markov chain. Such diagnostic Markov chains are not just essential tools for diagnostics and debugging but, they also allow the solution of timed reachability probability to be approximated from below. In particular cases, they also provide real counterexamples which can be used to show the violation of the given property. Our algorithms have been implemented in the stochastic model checker PRISM. We illustrate the applicability of our approach using a number of case studies.

Subject (DDC):  004 Computer Science 
Bibliography of Konstanz:  Yes 
Files  Size  Format  View 

There are no files associated with this item. 
ALJAZZAR, Husain, Stefan LEUE, 2006. Extended directed search for probabilistic timed reachability. In: ASARIN, Eugene, ed., Patricia BOUYER, ed.. Formal Modeling and Analysis of Timed Systems. Berlin, Heidelberg:Springer Berlin Heidelberg, pp. 3351. ISBN 9783540450269. Available under: doi: 10.1007/11867340_4
@inproceedings{Aljazzar2006Exten21297, title={Extended directed search for probabilistic timed reachability}, year={2006}, doi={10.1007/11867340_4}, number={4202}, isbn={9783540450269}, address={Berlin, Heidelberg}, publisher={Springer Berlin Heidelberg}, series={Lecture Notes in Computer Science}, booktitle={Formal Modeling and Analysis of Timed Systems}, pages={3351}, editor={Asarin, Eugene and Bouyer, Patricia}, 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/22rdfsyntaxns#" xmlns:bibo="http://purl.org/ontology/bibo/" xmlns:dspace="http://digitalrepositories.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.unikonstanz.de/rdf/resource/123456789/21297"> <bibo:uri rdf:resource="http://kops.unikonstanz.de/handle/123456789/21297"/> <dc:creator>Aljazzar, Husain</dc:creator> <dc:contributor>Aljazzar, Husain</dc:contributor> <dspace:isPartOfCollection rdf:resource="https://kops.unikonstanz.de/rdf/resource/123456789/36"/> <dcterms:abstract xml:lang="eng">Current numerical model checkers for stochastic systems can efficiently analyse stochastic models. However, the fact that they are unable to provide debugging information constrains their practical use. In precursory work we proposed a method to select diagnostic traces, in the parlance of functional model checking commonly referred to as failure traces or counterexamples, for probabilistic timed reachability properties on discretetime and continuoustime Markov chains. We applied directed explicitstate search algorithms, like Z ∗ , to determine a diagnostic trace which carries large amount of probability. In this paper we extend this approach to determining sets of traces that carry large probability mass, since properties of stochastic systems are typically not violated by single traces, but by collections of those. To this end we extend existing heuristics guided search algorithms so that they select sets of traces. The result is provided in the form of a Markov chain. Such diagnostic Markov chains are not just essential tools for diagnostics and debugging but, they also allow the solution of timed reachability probability to be approximated from below. In particular cases, they also provide real counterexamples which can be used to show the violation of the given property. Our algorithms have been implemented in the stochastic model checker PRISM. We illustrate the applicability of our approach using a number of case studies.</dcterms:abstract> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">20130131T08:44:32Z</dc:date> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">20130131T08:44:32Z</dcterms:available> <dcterms:title>Extended directed search for probabilistic timed reachability</dcterms:title> <dcterms:rights rdf:resource="https://kops.unikonstanz.de/page/termsofuse"/> <dcterms:issued>2006</dcterms:issued> <dc:language>eng</dc:language> <dc:rights>termsofuse</dc:rights> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dcterms:isPartOf rdf:resource="https://kops.unikonstanz.de/rdf/resource/123456789/36"/> <dc:contributor>Leue, Stefan</dc:contributor> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dc:creator>Leue, Stefan</dc:creator> <dcterms:bibliographicCitation>Formal modeling and analysis of timed systems : 4th International Conference, FORMATS 2006, Paris, France, September 25  27, 2006; proceedings / Eugene Asarin ... (eds.).  Berlin [u.a.] : Springer.  S. 3351.  (Lecture notes in computer science ; 4202).  ISBN 9783540450269</dcterms:bibliographicCitation> </rdf:Description> </rdf:RDF>