Approximate Probabilistic Model Checking

By Thomas Hérault, Richard Lassaigne, Frédéric Magniette, Sylvain Peyronnet. International Conference on Verification, Model Checking and Abstract Interpretation, 2004

340 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Uppaal SMC tutorial (2015, background): “Probability estimation The probability estimation algorithm [30] computes the number of runs needed to produce an approximation interval [p − ε, p + ε] for p = Pr(ψ) with a confidence 1 − α.”
Statistical Model Checking: An Overview (2010, background): “The interested reader is redirected to [13,15,19] for more details.”
PRISM 4.0: Verification of Probabilistic Real-Time Systems (2011, methodology): “It also incorporates several new components, including engines for quantitative abstraction-refinement [9] and statistical model checking [14,5].”
Stochastic Model Checking (2007, methodology): “Related topic include: probabilistic generalisations of bisimulation and simulation relations for DTMCs [49,57] and for CTMCs [17,11]; and approximate methods for stochastic model checking based on discrete event simulation [33,63].”
Statistical Model Checking of Black-Box Probabilistic Systems (2004, background): “[7], which can model-check discrete-time Markov chains against properties expressed in an expressively weak logic (“positive LTL”).”