Faster Statistical Model Checking for Unbounded Temporal Properties

Daca, Przemysław; Henzinger, Thomas A.; Křetínský, Jan; Petrov, Tatjana

Faster Statistical Model Checking for Unbounded Temporal Properties

Dateien

Daca_2-16l0jts3wgeoz5.pdfGröße: 281.29 KBDownloads: 289

Datum

2017

Autor:innen

Daca, Przemysław

Henzinger, Thomas A.

Křetínský, Jan

Petrov, Tatjana

Open Access-Veröffentlichung

Open Access Green

Sammlungen

Informatik und Informationswissenschaft

Publikationstyp

Zeitschriftenartikel

Publikationsstatus

Published

Erschienen in

ACM Transactions on Computational Logic. 2017, 18(2), 12. ISSN 1529-3785. eISSN 1557-945X. Available under: doi: 10.1145/3060139

Zusammenfassung

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.

Fachgebiet (DDC)

004 Informatik

Schlagwörter

Languages; Theory; Answer set programming;expressiveness; complexity; nonmonotonic reasoning; second-order logic

Zitieren

ISO 690

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. 2017, 18(2), 12. ISSN 1529-3785. eISSN 1557-945X. Available under: doi: 10.1145/3060139

BibTex

@article{Daca2017-06-23Faste-42125,
  year={2017},
  doi={10.1145/3060139},
  title={Faster Statistical Model Checking for Unbounded Temporal Properties},
  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: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/server/rdf/resource/123456789/42125">
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2018-04-20T12:56:51Z</dcterms:available>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:rights>terms-of-use</dc:rights>
    <dcterms:title>Faster Statistical Model Checking for Unbounded Temporal Properties</dcterms:title>
    <dc:creator>Daca, Przemysław</dc:creator>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/42125"/>
    <dc:creator>Petrov, Tatjana</dc:creator>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:creator>Henzinger, Thomas A.</dc:creator>
    <dc:contributor>Daca, Przemysław</dc:contributor>
    <dc:contributor>Křetínský, Jan</dc:contributor>
    <dcterms:issued>2017-06-23</dcterms:issued>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:creator>Křetínský, Jan</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>
    <dc:contributor>Petrov, Tatjana</dc:contributor>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/42125/1/Daca_2-16l0jts3wgeoz5.pdf"/>
    <dc:language>eng</dc:language>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2018-04-20T12:56:51Z</dc:date>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/42125/1/Daca_2-16l0jts3wgeoz5.pdf"/>
    <dc:contributor>Henzinger, Thomas A.</dc:contributor>
  </rdf:Description>
</rdf:RDF>

Universitätsbibliographie

Ja