Faster Statistical Model Checking for Unbounded Temporal Properties

Cite This

Files in this item

Checksum: MD5:facae91249bd47954b8e3ee20569b4f3

DACA, Przemysław, Thomas A. HENZINGER, Jan KŘETÍNSKÝ, Tatjana PETROV, 2017. Faster Statistical Model Checking for Unbounded Temporal Properties. In: ACM Transactions on Computational Logic. 18(2), 12. ISSN 1529-3785. eISSN 1557-945X. Available under: doi: 10.1145/3060139

@article{Daca2017-06-23Faste-42125, title={Faster Statistical Model Checking for Unbounded Temporal Properties}, year={2017}, doi={10.1145/3060139}, number={2}, volume={18}, issn={1529-3785}, journal={ACM Transactions on Computational Logic}, author={Daca, Przemysław and Henzinger, Thomas A. and Křetínský, Jan and Petrov, Tatjana}, note={Article Number: 12} }

<rdf:RDF xmlns:dcterms="" xmlns:dc="" xmlns:rdf="" xmlns:bibo="" xmlns:dspace="" xmlns:foaf="" xmlns:void="" xmlns:xsd="" > <rdf:Description rdf:about=""> <dc:contributor>Daca, Przemysław</dc:contributor> <bibo:uri rdf:resource=""/> <dcterms:available rdf:datatype="">2018-04-20T12:56:51Z</dcterms:available> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dcterms:isPartOf rdf:resource=""/> <dc:date rdf:datatype="">2018-04-20T12:56:51Z</dc:date> <dc:rights>terms-of-use</dc:rights> <dcterms:title>Faster Statistical Model Checking for Unbounded Temporal Properties</dcterms:title> <dcterms:rights rdf:resource=""/> <dc:creator>Křetínský, Jan</dc:creator> <dc:creator>Petrov, Tatjana</dc:creator> <dc:contributor>Henzinger, Thomas A.</dc:contributor> <dc:language>eng</dc:language> <dc:contributor>Křetínský, Jan</dc:contributor> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dspace:hasBitstream rdf:resource=""/> <dc:creator>Henzinger, Thomas A.</dc:creator> <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> <dspace:isPartOfCollection rdf:resource=""/> <dcterms:issued>2017-06-23</dcterms:issued> <dc:contributor>Petrov, Tatjana</dc:contributor> <dcterms:hasPart rdf:resource=""/> <dc:creator>Daca, Przemysław</dc:creator> </rdf:Description> </rdf:RDF>

Downloads since Apr 20, 2018 (Information about access statistics)

Daca_2-16l0jts3wgeoz5.pdf 137

This item appears in the following Collection(s)

Search KOPS


My Account