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.
Original languageUndefined
Title of host publicationProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016)
Place of PublicationUSA
PublisherACM
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 - New York, United States

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

Fingerprint

Model checking
Distributed computer systems

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: ACM. 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 : ACM, 2016. p. 31-45.

Research output: ScientificConference contribution

@inbook{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",
isbn = "978-1-4503-4391-6",
publisher = "ACM",
pages = "31--45",
booktitle = "Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016)",

}

Katoen, JP 2016, The Probabilistic Model Checking Landscape. in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016). ACM, USA, pp. 31-45, 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, New York, United States, 5-8 July. 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 : ACM, 2016. p. 31-45.

Research output: ScientificConference contribution

TY - CHAP

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 - ACM

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: ACM. 2016. p. 31-45. Available from, DOI: 10.1145/2933575.2934574