Statistical Model Checking: An Overview
By Axel Legay, Benoît Delahaye, Saddek Bensalem. Runtime Verification, 2010
499 citations recorded by the source corpus.
Quantitative properties of stochastic systems are usually specified in logics that allow one to compare the measure of executions satisfying certain temporal properties with thresholds. The model checking problem for stochastic systems with respect to such logics is typically solved by a numerical approach [31,8,35,22,21,5] that iteratively computes (or approximates) the exact measure of paths satisfying relevant subformulas; the algorithms themselves depend on the class of systems being analyzed as well as the logic used for specifying the properties. Another approach to solve the model checking problem is to simulate the system for finitely many executions, and use hypothesis testing to infer whether the samples provide a statistical evidence for the satisfaction or violation of the specification. In this tutorial, we survey the statistical approach, and outline its main advantages in terms of efficiency, uniformity, and simplicity.
Subfields: Computational Theory and Mathematics, Software
View Paper: https://www.semanticscholar.org/paper/eda3115c50ef33b36d77cc867b792e8486e17fe8
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Computational Theory and Mathematics
Citations in the corpus
- Probably Approximately Correct MDP Learning and Control With Temporal Logic Constraints (2014, background): “…and the time, space, and sample complexity of achieving this policy is polynomial in the size of the MDP, in the size of the automaton expressing the temporal logic specification and other quantities that measure the accuracy of, and the confidence in, the learned MDP with respect to the true one.”
- Approximate Computing: A Survey (2016, unknown): “Probabilistic model checking is an automatic procedure for establishing whether a desired property holds in a probabilistic system (see Legay and Delahaye_s survey [32]).”