Faster Statistical Model Checking for Unbounded Temporal Properties

DACA, Przemyslaw; Thomas A HENZINGER; Jan KŘETÍNSKÝ a Tatjana PETROV. Faster Statistical Model Checking for Unbounded Temporal Properties. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. UNITED STATES: ASSOC COMPUTING MACHINERY, 2017, roč. 18, č. 2, s. 1-25. ISSN 1529-3785. Dostupné z: https://doi.org/10.1145/3060139.

Základní údaje

Originální název

Faster Statistical Model Checking for Unbounded Temporal Properties

Autoři

DACA, Przemyslaw; Thomas A HENZINGER; Jan KŘETÍNSKÝ a Tatjana PETROV

Vydání

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, UNITED STATES, ASSOC COMPUTING MACHINERY, 2017, 1529-3785

---

Další údaje

Typ výsledku

Článek v odborném periodiku

Impakt faktor

Impact factor: 0.731

Označené pro přenos do RIV

Ne

Organizační jednotka

Fakulta informatiky

DOI

https://doi.org/10.1145/3060139

---

Anotace

V originále

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.