Faster Statistical Model Checking for Unbounded Temporal Properties

Cite This

Files in this item

Files Size Format View

There are no files associated with this item.

PRZEMYSŁAW, Daca, Thomas A. HENZINGER, Jan KŘETÍNSKÝ, Tatjana PETROV, 2016. Faster Statistical Model Checking for Unbounded Temporal Properties. TACAS 2016 : 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Eindhoven, Apr 2, 2016 - Apr 8, 2018. In: CHECHIK, Marsha, ed., Jean-François RASKIN, ed.. Tools and algorithms for the construction and analysis of systems : 22nd International Conference, TACAS 2016, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Berlin:Springer, pp. 112-129. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-662-49673-2. Available under: doi: 10.1007/978-3-662-49674-9_7

@inproceedings{Przemysaw2016Faste-42171, title={Faster Statistical Model Checking for Unbounded Temporal Properties}, year={2016}, doi={10.1007/978-3-662-49674-9_7}, number={9636}, isbn={978-3-662-49673-2}, issn={0302-9743}, address={Berlin}, publisher={Springer}, series={Lecture notes in computer science}, booktitle={Tools and algorithms for the construction and analysis of systems : 22nd International Conference, TACAS 2016, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings}, pages={112--129}, editor={Chechik, Marsha and Raskin, Jean-François}, author={Przemysław, Daca and Henzinger, Thomas A. and Křetínský, Jan and Petrov, Tatjana} }

<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/42171"> <dcterms:abstract xml:lang="eng">We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds.</dcterms:abstract> <dc:contributor>Petrov, Tatjana</dc:contributor> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2018-04-25T12:47:41Z</dcterms:available> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:language>eng</dc:language> <dc:contributor>Henzinger, Thomas A.</dc:contributor> <dc:contributor>Przemysław, Daca</dc:contributor> <dcterms:title>Faster Statistical Model Checking for Unbounded Temporal Properties</dcterms:title> <dc:creator>Henzinger, Thomas A.</dc:creator> <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/42171"/> <dcterms:issued>2016</dcterms:issued> <dc:creator>Petrov, Tatjana</dc:creator> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2018-04-25T12:47:41Z</dc:date> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:creator>Křetínský, Jan</dc:creator> <dc:contributor>Křetínský, Jan</dc:contributor> <dc:creator>Przemysław, Daca</dc:creator> </rdf:Description> </rdf:RDF>

This item appears in the following Collection(s)

Search KOPS


Browse

My Account