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 statespace 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 twophase process: (a) the first phase is concerned with identifying the bound k_{0}; (b) the second phase computes the probability of satisfying the k_{0}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
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, PRISMU2B, 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 modeldependent way followed by the second phase where this is used to estimate the probability of satisfying the original property within prespecified 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 prespecified error bounds. PRISMU2B 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 userinterface modules.
Quicklinks: Case Studies (Illustrative Example, Queue, Zeroconf, Dining Philosopher)
How to use the tool
 Download and install modified PRISM distribution.
 Commandline usage: Modified command line arguments are listed below.
 sim 12: 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 rightclicking 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.
Illustrative Example from the Paper: Download Illustrative Example
Input Property File: Download Illustrative Example property
Nbuffer Queue Example: Download Queue Example
Input Property File: Download Queue Example property
Zeroconf Protocol: Download Zeroconf Example
Input Property File: Download Zeroconf Example property
Dining Philosopher DTMC: Download Phil10 Example
Input Property File: Download Phil10 Example property