Probabilistic Model Checking

The goal of this project is to investigate and develop statistical methods for probabilistic model checking (specifically for unbounded until temporal properties).

Members

Faculty: Samik Basu and Arka Ghosh.

Students

Paul Jennings (MS): MoSys
Ru He

Tools in this page are based on PRISM Model Checker.

Perl Implementation: Analyzing PRISM Model Checker Output

Supplementary material for ICFEM 2009 paper on Approximate Probabilistic Model Checking involving Unbounded Until Properties.

Abstract: We study the problem of applying statistical methods for approximate model checking of probabilistic systems against properties encoded as PCTL formulas. Such approximate methods have been proposed primarily to deal with state-space explosion that makes the exact model checking by numerical methods practically infeasible for large systems. However, the existing statistical methods consider a restricted subset of PCTL, specifically, the subset that can only express bounded until properties. We propose a new method that does not rely on such restriction and can be effectively used to reason about unbounded until properties. We approximate probabilistic characteristics of an unbounded until property by that of a bounded until property for suitably chosen value of the bound. In essence, our method is a two-phase process: (a) the first phase is concerned with identifying the bound k₀; (b) the second phase computes the probability of satisfying the k₀-bounded until property as an estimate for the probability of satisfying the corresponding unbounded until property. In both phases, it is sufficient to verify bounded until properties which can be effectively done using existing statistical techniques. We prove the correctness of our technique and present a prototype implementation based on widely used PRISM model checker. We empirically show the practical applicability of our method by considering different case studies including IPv4 zeroconf protocol and dining philosopher protocol modeled as Discrete Time Markov chain.

Paper at Springer Site.
Preliminary results and prototype tool are available here

PRISM-U2B

This tool is developed by Paul Jennings as part of his MS thesis work. The tool modifies PRISM implementation to incorporate a new simulation technique and GUI.

Download Journal Version

We present a tool, PRISM-U2B, for approximate probabilistic model checking of unbounded until PCTL properties for DTMC models. This tool broadens the scope of statistical model checking by allowing verification of such properties for complex models where PRISM's existing method fails to provide a result. Furthermore, this tool provides results more efficiently (with respect to time), even for the models where PRISM successfully completes the verification, as shown in the case studies. This tool attempts to verify an unbounded property in two phases. In the first phase, an optimal bounded until property is obtained automatically in a model-dependent way followed by the second phase where this is used to estimate the probability of satisfying the original property within pre-specified error bound. In contrast, PRISM requires users to specify a similar bound (a bound on simulation path length) and uses that to estimate the probability of satisfying the original property. In general, it is not possible for a user to specify such a bound to guarantee the correctness of the estimation within the pre-specified error bounds. PRISM-U2B is an extension of PRISM model checking engine and leverages on PRISM's parsers for reading input DTMC models and PCTL properties in PRISM's specification language, and extends PRISM's simulation path generation and graphical user-interface modules.

Quicklinks: Case Studies (Illustrative Example, Queue, Zeroconf, Dining Philosopher)

How to use the tool

Download and install modified PRISM distribution.
Command-line usage: Modified command line arguments are listed below.
- -sim 1|2: 1 invokes standard PRISM simulator; 2 invokes modified simulator
- -simepsilon x [x x]: Specifies error bound(s) on simulation (Default 0.025)
- -simdelta x [x]: Specifies confidience interval(s) for simulation (Default 0.01)
Sample invocations:
- prism ./illus/illus.pm ./illus/illus.pctl -sim 2
- prism ./illus/illus.pm ./illus/illus.pctl -sim 2 -simapprox 0.02
- prism ./illus/illus.pm ./illus/illus.pctl -sim 2 -simapprox 0.0025 0.0125 0.01
- prism ./illus/illus.pm ./illus/illus.pctl -sim 2 -simdelta 0.02
- prism ./illus/illus.pm ./illus/illus.pctl -sim 2 -simdelta 0.01 0.01
- prism ./illus/illus.pm ./illus/illus.pctl -sim 2 -const "q=0.9,r=0.9,n=10"
Example:The property file contains

label "phi1" = ( s=0 | s=1 | (s>10 & s<=10000)); label "phi2" = ((s=4) | (s=3)); P=?[ "phi1" U "phi2" ]
The simulator can be invoked by:
prism ./illus/illus.pm ./illus/illus.pctl -sim 2
Sample output:

bash$ bin/prism ./examples/illus.pm ./examples/illus.pctl -sim 2
PRISM

GUI interface The standard PRISM GUI can be invoked by:
xprism
The model and properties file can be loaded into the interface as usual. The simulator can be invoked by right-clicking on a property and clicking Simulate, as shown below.

The modified simulator can be invoked by selecting "Automatic bound calculation". The fields allow entry of the parameters for the modified simulator, as shown below.