--- res: bibo_abstract: - 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. @eng bibo_authorlist: - foaf_Person: foaf_givenName: Przemyslaw foaf_name: Daca, Przemyslaw foaf_surname: Daca foaf_workInfoHomepage: http://www.librecat.org/personId=49351290-F248-11E8-B48F-1D18A9856A87 - foaf_Person: foaf_givenName: Thomas A foaf_name: Henzinger, Thomas A foaf_surname: Henzinger foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87 orcid: 0000−0002−2985−7724 - foaf_Person: foaf_givenName: Jan foaf_name: Kretinsky, Jan foaf_surname: Kretinsky foaf_workInfoHomepage: http://www.librecat.org/personId=44CEF464-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0002-8122-2881 - foaf_Person: foaf_givenName: Tatjana foaf_name: Petrov, Tatjana foaf_surname: Petrov foaf_workInfoHomepage: http://www.librecat.org/personId=3D5811FC-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0002-9041-0905 bibo_doi: 10.1145/3060139 bibo_issue: '2' bibo_volume: 18 dct_date: 2017^xs_gYear dct_isPartOf: - http://id.crossref.org/issn/15293785 dct_language: eng dct_publisher: ACM@ dct_title: Faster statistical model checking for unbounded temporal properties@ ...