Skip to Main content Skip to Navigation
Conference papers

Advances and Challenges of Probabilistic Model Checking

Abstract : Probabilistic model checking is a powerful technique for formally verifying quantitative properties of systems that exhibit stochastic behaviour. Such systems are found in many domains: probabilistic behaviour may arise, for example, due to failures of unreliable components, communication across lossy media, or through the use of randomisation in distributed protocols. In this paper, we give a short overview of probabilistic model checking and of PRISM (www.prismmodelchecker.org), currently the leading software tool in this area. We then mention some of the limitations of these techniques, describe some of the advances that are being made to overcome them, and outline key challenges that remain in this research area.
Document type :
Conference papers
Complete list of metadata

Cited literature [38 references]  Display  Hide  Download

https://hal.inria.fr/hal-00767474
Contributor : Hongyang Qu <>
Submitted on : Wednesday, December 19, 2012 - 10:51:21 PM
Last modification on : Wednesday, November 25, 2020 - 5:06:03 PM
Long-term archiving on: : Wednesday, March 20, 2013 - 11:38:25 AM

File

allerton10.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00767474, version 1

Collections

Citation

Marta Kwiatkowska, Gethin Norman, David Parker. Advances and Challenges of Probabilistic Model Checking. 48th Annual Allerton Conference on Communication, Control and Computing, Sep 2010, Monticello, United States. pp.1691-1698. ⟨hal-00767474⟩

Share

Metrics

Record views

172

Files downloads

509