The Probabilistic Model Checking Landscape

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 13 Citations

Abstract

Randomization is a key element in sequential and distributed computing. Reasoning about randomized algorithms is highly nontrivial. In the 1980s, this initiated first proof methods, logics, and model-checking algorithms. The field of probabilistic verification has developed considerably since then. This paper surveys the algorithmic verification of probabilistic models, in particular probabilistic model checking. We provide an informal account of the main models, the underlying algorithms, applications from reliability and dependability analysis—and beyond—and describe recent developments towards automated parameter synthesis.
LanguageUndefined
Title of host publicationProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016)
Place of PublicationUSA
PublisherAssociation for Computing Machinery
Pages31-45
Number of pages15
ISBN (Print)978-1-4503-4391-6
DOIs
StatePublished - Jul 2016
Event31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016 - Columbia University, New York, United States
Duration: 5 Jul 20168 Jul 2016
Conference number: 31

Publication series

Name
PublisherACM

Conference

Conference31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016
Abbreviated titleLICS
CountryUnited States
CityNew York
Period5/07/168/07/16

Keywords

  • EC Grant Agreement nr.: FP7/2007-2013
  • EC Grant Agreement nr.: FP7/318490
  • IR-100650
  • METIS-317201
  • EWI-27009

Cite this

Katoen, J. P. (2016). The Probabilistic Model Checking Landscape. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016) (pp. 31-45). USA: Association for Computing Machinery. DOI: 10.1145/2933575.2934574
Katoen, Joost P./ The Probabilistic Model Checking Landscape. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016). USA : Association for Computing Machinery, 2016. pp. 31-45
@inproceedings{565c4afed48243b6833b6ff4605c5420,
title = "The Probabilistic Model Checking Landscape",
abstract = "Randomization is a key element in sequential and distributed computing. Reasoning about randomized algorithms is highly nontrivial. In the 1980s, this initiated first proof methods, logics, and model-checking algorithms. The field of probabilistic verification has developed considerably since then. This paper surveys the algorithmic verification of probabilistic models, in particular probabilistic model checking. We provide an informal account of the main models, the underlying algorithms, applications from reliability and dependability analysis—and beyond—and describe recent developments towards automated parameter synthesis.",
keywords = "EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/318490, IR-100650, METIS-317201, EWI-27009",
author = "Katoen, {Joost P.}",
note = "eemcs-eprint-27009",
year = "2016",
month = "7",
doi = "10.1145/2933575.2934574",
language = "Undefined",
isbn = "978-1-4503-4391-6",
publisher = "Association for Computing Machinery",
pages = "31--45",
booktitle = "Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016)",
address = "United States",

}

Katoen, JP 2016, The Probabilistic Model Checking Landscape. in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016). Association for Computing Machinery, USA, pp. 31-45, 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, New York, United States, 5/07/16. DOI: 10.1145/2933575.2934574

The Probabilistic Model Checking Landscape. / Katoen, Joost P.

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016). USA : Association for Computing Machinery, 2016. p. 31-45.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - The Probabilistic Model Checking Landscape

AU - Katoen,Joost P.

N1 - eemcs-eprint-27009

PY - 2016/7

Y1 - 2016/7

N2 - Randomization is a key element in sequential and distributed computing. Reasoning about randomized algorithms is highly nontrivial. In the 1980s, this initiated first proof methods, logics, and model-checking algorithms. The field of probabilistic verification has developed considerably since then. This paper surveys the algorithmic verification of probabilistic models, in particular probabilistic model checking. We provide an informal account of the main models, the underlying algorithms, applications from reliability and dependability analysis—and beyond—and describe recent developments towards automated parameter synthesis.

AB - Randomization is a key element in sequential and distributed computing. Reasoning about randomized algorithms is highly nontrivial. In the 1980s, this initiated first proof methods, logics, and model-checking algorithms. The field of probabilistic verification has developed considerably since then. This paper surveys the algorithmic verification of probabilistic models, in particular probabilistic model checking. We provide an informal account of the main models, the underlying algorithms, applications from reliability and dependability analysis—and beyond—and describe recent developments towards automated parameter synthesis.

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - EC Grant Agreement nr.: FP7/318490

KW - IR-100650

KW - METIS-317201

KW - EWI-27009

U2 - 10.1145/2933575.2934574

DO - 10.1145/2933575.2934574

M3 - Conference contribution

SN - 978-1-4503-4391-6

SP - 31

EP - 45

BT - Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016)

PB - Association for Computing Machinery

CY - USA

ER -

Katoen JP. The Probabilistic Model Checking Landscape. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016). USA: Association for Computing Machinery. 2016. p. 31-45. Available from, DOI: 10.1145/2933575.2934574