Statistical Model Checking: Black or White?

Pranav Ashok; Przemysław Daca; Jan Křetínský; Maximilian Weininger

doi:10.1007/978-3-030-61362-4_19

Statistical Model Checking: Black or White?

Pranav Ashok, Przemysław Daca, Jan Křetínský, Maximilian Weininger

Informatics 7 - Associate Professorship of Formal Methods for Software Reliability

Technical University of Munich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

3 Scopus citations

Abstract

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.

Original language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation
Subtitle of host publication	Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings
Editors	Tiziana Margaria, Bernhard Steffen
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	331-349
Number of pages	19
ISBN (Print)	9783030613617
DOIs	https://doi.org/10.1007/978-3-030-61362-4_19
State	Published - 2020
Event	9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020 - Rhodes, Greece Duration: 20 Oct 2020 → 30 Oct 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12476 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020
Country/Territory	Greece
City	Rhodes
Period	20/10/20 → 30/10/20

Access to Document

10.1007/978-3-030-61362-4_19

Cite this

Ashok, P., Daca, P., Křetínský, J., & Weininger, M. (2020). Statistical Model Checking: Black or White? In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings (pp. 331-349). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12476 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-61362-4_19

Ashok, Pranav ; Daca, Przemysław ; Křetínský, Jan et al. / Statistical Model Checking : Black or White?. Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. editor / Tiziana Margaria ; Bernhard Steffen. Springer Science and Business Media Deutschland GmbH, 2020. pp. 331-349 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{8000f5bb97574d0f858bc90bf865f9e7,

title = "Statistical Model Checking: Black or White?",

abstract = "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.",

author = "Pranav Ashok and Przemys{\l}aw Daca and Jan K{\v r}et{\'i}nsk{\'y} and Maximilian Weininger",

note = "Publisher Copyright: {\textcopyright} 2020, Springer Nature Switzerland AG.; 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020 ; Conference date: 20-10-2020 Through 30-10-2020",

year = "2020",

doi = "10.1007/978-3-030-61362-4_19",

language = "English",

isbn = "9783030613617",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "331--349",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation",

}

Ashok, P, Daca, P, Křetínský, J & Weininger, M 2020, Statistical Model Checking: Black or White? in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12476 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 331-349, 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020, Rhodes, Greece, 20/10/20. https://doi.org/10.1007/978-3-030-61362-4_19

Statistical Model Checking: Black or White? / Ashok, Pranav; Daca, Przemysław; Křetínský, Jan et al.
Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. ed. / Tiziana Margaria; Bernhard Steffen. Springer Science and Business Media Deutschland GmbH, 2020. p. 331-349 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12476 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Statistical Model Checking

T2 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020

AU - Ashok, Pranav

AU - Daca, Przemysław

AU - Křetínský, Jan

AU - Weininger, Maximilian

PY - 2020

Y1 - 2020

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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85097381928&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-61362-4_19

DO - 10.1007/978-3-030-61362-4_19

M3 - Conference contribution

AN - SCOPUS:85097381928

SN - 9783030613617

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 331

EP - 349

BT - Leveraging Applications of Formal Methods, Verification and Validation

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer Science and Business Media Deutschland GmbH

Y2 - 20 October 2020 through 30 October 2020

ER -

Ashok P, Daca P, Křetínský J, Weininger M. Statistical Model Checking: Black or White? In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. Springer Science and Business Media Deutschland GmbH. 2020. p. 331-349. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-61362-4_19

Statistical Model Checking: Black or White?

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this