Name
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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1145/3060139 | ACM Transactions on Computational Logic (TOCL) |
Keywords | Field | DocType |
Markov chains,mean payoff,simulation,statistical model checking,temporal logic | Discrete mathematics,Combinatorics,Model checking,Second-order logic,A priori and a posteriori,Markov chain,Algorithm,Linear temporal logic,Temporal logic,Strongly connected component,State space,Mathematics | Journal |
Volume | Issue | ISSN |
18 | 2 | 1529-3785 |
Citations | PageRank | References |
4 | 0.40 | 20 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Przemyslaw Daca | 1 | 36 | 3.32 |
| Thomas A. Henzinger | 2 | 14827 | 1317.51 |
| Jan Kretínský | 3 | 159 | 16.02 |
| Tatjana Petrov | 4 | 90 | 7.06 |