Draft:Probabilistic Model Checking
Formal verification approach
From Wikipedia, the free encyclopedia
In computer science, Probabilistic Model Checking is a technique for the formal verification of systems that exhibit probabilistic behavior. It extends traditional model checking approaches to verify probabilistic notions of correctness in Markov Automata such as Markov decision processes, discrete-time Markov chains, and continuous-time Markov chains.[1] This technique is commonly used to analyze systems where uncertainty is inherent, such as communication protocols, randomized algorithms, and engineered biological systems. It provides proofs of exact solutions to a specification.
 | Review waiting, please be patient.
This may take 8 weeks or more, since drafts are reviewed in no specific order. There are 3,266 pending submissions waiting for review.
Where to get help
How to improve a draft
You can also browse Wikipedia:Featured articles and Wikipedia:Good articles to find examples of Wikipedia's best writing on topics similar to your proposed article. Improving your odds of a speedy review To improve your odds of a faster review, tag your draft with relevant WikiProject tags using the button below. This will let reviewers know a new draft has been submitted in their area of interest. For instance, if you wrote about a female astronomer, you would want to add the Biography, Astronomy, and Women scientists tags. Editor resources
Reviewer tools
|
Specification
Algorithmic solutions rely on the formulation of the probabilistic system's specification in a precise mathematical language. Probabilistic Model Checking enables the automated verification of properties specified in probabilistic temporal logics. By rigorously analyzing these models, one can determine whether a model satisfies given conditions with a specified probability.
Models
The foundational model structures for Probabilistic Model Checking are Markov Automata, including Markov chains (discrete-time and continuous-time) and Markov decision processes.
Properties
Probabilistic Model Checking relies on logics including PCTL (Probabilistic Computation Tree Logic) for property specifications on discrete-time models and CSL (Continuous Stochastic Logic) for property specification on continuous-time models.
Algorithms and Tools
Probabilistic model checking relies on several algorithms that enable the analysis of probabilistic computational systems.
Symbolic Approaches
For applications that are suited to it, symbolic representations such as Binary Decision Diagrams (BDDs) are used to efficiently represent large or infinite state spaces.[2] Symbolic representations apply to many models, but transient reachability analysis for continuous-time models requires an explicit state space representation.[3] Once a BDD is constructed for the state space, a Breadth-first or Depth-first Search is used to traverse the state space and evaluate a specification.[4]
Approximate Solutions
Monte Carlo methods leverage random sampling to estimate probabilities across state spaces. These algorithms are particularly useful in scenarios where the state space is too large for exhaustive enumeration. These approaches can include weighted ensemble,[5] the weighted Stochastic Simulation Algorithm,[6] Importance Sampling,[7] and Importance Splitting.[8]
Numeric Methods
Numeric techniques involve the direct computation of probability distributions over states. These methods include Linear Programming techniques for Markov decision processes and matrix exponentiation for continuous-time Markov chains.[9]
Tools
Publicly-available tools for Probabilistic Model Checking include PRISM,[10] Storm,[3] and Modest.[11]