Statistical Model Checking: Black or White?

D 2020

Statistical Model Checking: Black or White?

ASHOK, Pranav; Przemyslaw DACA; Jan KŘETÍNSKÝ a Maximilian WEININGER

Základní údaje

Originální název

Statistical Model Checking: Black or White?

Autoři

ASHOK, Pranav; Przemyslaw DACA; Jan KŘETÍNSKÝ a Maximilian WEININGER

Vydání

Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part I, od s. 331-349, 19 s. 2020

Nakladatel

Springer

Další údaje

Typ výsledku

Stať ve sborníku

Označené pro přenos do RIV

Organizační jednotka

Fakulta informatiky

ISBN

9783030613617

ISSN

DOI

https://doi.org/10.1007/978-3-030-61362-4_19

Změněno: 17. 3. 2025 14:43, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

One of the advantages of statistical model checking (SMC) is its applicability to black-box systems. In this paper, we discuss the advantages gained when SMC is applied to white-box systems, utilizing the knowledge of their internals. We focus on the setting of unbounded-horizon properties such as reachability or LTL. We compare our approach to other statistical and numerical techniques both conceptually as instantiations of the same framework, and experimentally. It not only clearly preserves scalability advantages of black-box SMC compared to classical model checking (while providing high level of guarantees), but it also scales yet better than either of the two for a wide class of models.

Citovat

ASHOK, Pranav; Przemyslaw DACA; Jan KŘETÍNSKÝ a Maximilian WEININGER. Statistical Model Checking: Black or White? In Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part I. Springer, 2020, s. 331-349. ISBN 9783030613617. Dostupné z: https://doi.org/10.1007/978-3-030-61362-4_19.

@inproceedings{2484795,
   author = {Ashok, Pranav and Daca, Przemyslaw and Křetínský, Jan and Weininger, Maximilian},
   booktitle = {Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part I},
   doi = {https://doi.org/10.1007/978-3-030-61362-4_19},
   isbn = {9783030613617},
   pages = {331-349},
   publisher = {Springer},
   title = {Statistical Model Checking: Black or White?},
   year = {2020}
}

TY  - CONF
ID  - 2484795
AU  - Ashok, Pranav - Daca, Przemyslaw - Křetínský, Jan - Weininger, Maximilian
PY  - 2020
TI  - Statistical Model Checking: Black or White?
PB  - Springer
SN  - 9783030613617
N2  - One of the advantages of statistical model checking (SMC) is its applicability to black-box systems. In this paper, we discuss the advantages gained when SMC is applied to white-box systems, utilizing the knowledge of their internals. We focus on the setting of unbounded-horizon properties such as reachability or LTL. We compare our approach to other statistical and numerical techniques both conceptually as instantiations of the same framework, and experimentally. It not only clearly preserves scalability advantages of black-box SMC compared to classical model checking (while providing high level of guarantees), but it also scales yet better than either of the two for a wide class of models.
ER  -

ASHOK, Pranav; Przemyslaw DACA; Jan KŘETÍNSKÝ a Maximilian WEININGER. Statistical Model Checking: Black or White? In \textit{Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part I}. Springer, 2020, s.~331-349. ISBN~9783030613617. Dostupné z: https://doi.org/10.1007/978-3-030-61362-4\_{}19.

Přehled o publikaci