Faster Statistical Model Checking for Unbounded Temporal
Properties

D 2016

Faster Statistical Model Checking for Unbounded Temporal Properties

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

Základní údaje

Originální název

Faster Statistical Model Checking for Unbounded Temporal Properties

Autoři

DACA, Przemyslaw (616 Polsko), Thomas A. HENZINGER (40 Rakousko), Jan KŘETÍNSKÝ (203 Česká republika, garant, domácí) a Tatjana PETROV (688 Srbsko)

Vydání

Berlin Heidelberg, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, od s. 112-129, 18 s. 2016

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/16:00088469

Organizační jednotka

Fakulta informatiky

ISBN

978-3-662-49673-2

ISSN

DOI

http://dx.doi.org/10.1007/978-3-662-49674-9_7

UT WoS

000406428000007

Klíčová slova anglicky

statistical model checking; verification; temporal logic

Štítky

core_A, firank_A, formela-conference

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 1. 6. 2022 12:34, RNDr. Pavel Šmerk, Ph.D.

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.

Návaznosti

GBP202/12/G061, projekt VaV

Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)

Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky

Citovat

DACA, Przemyslaw, Thomas A. HENZINGER, Jan KŘETÍNSKÝ a Tatjana PETROV. Faster Statistical Model Checking for Unbounded Temporal Properties. In Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016. Berlin Heidelberg: Springer, 2016, s. 112-129. ISBN 978-3-662-49673-2. Dostupné z: https://dx.doi.org/10.1007/978-3-662-49674-9_7.

@inproceedings{1365646,
   author = {Daca, Przemyslaw and Henzinger, Thomas A. and Křetínský, Jan and Petrov, Tatjana},
   address = {Berlin Heidelberg},
   booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016},
   doi = {http://dx.doi.org/10.1007/978-3-662-49674-9_7},
   keywords = {statistical model checking; verification; temporal logic},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Berlin Heidelberg},
   isbn = {978-3-662-49673-2},
   pages = {112-129},
   publisher = {Springer},
   title = {Faster Statistical Model Checking for Unbounded Temporal Properties},
   year = {2016}
}

TY  - JOUR
ID  - 1365646
AU  - Daca, Przemyslaw - Henzinger, Thomas A. - Křetínský, Jan - Petrov, Tatjana
PY  - 2016
TI  - Faster Statistical Model Checking for Unbounded Temporal Properties
PB  - Springer
CY  - Berlin Heidelberg
SN  - 9783662496732
KW  - statistical model checking
KW  - verification
KW  - temporal logic
N2  - 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.
ER  -

DACA, Przemyslaw, Thomas A. HENZINGER, Jan KŘETÍNSKÝ a Tatjana PETROV. Faster Statistical Model Checking for Unbounded Temporal Properties. In \textit{Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016}. Berlin Heidelberg: Springer, 2016, s.~112-129. ISBN~978-3-662-49673-2. Dostupné z: https://dx.doi.org/10.1007/978-3-662-49674-9\_{}7.

Podrobný výpis o publikaci