Approximate Probabilistic Model Checking Using Bounded Until Properties
Samik Basu , Department of Computer Science
Arka P. Ghosh, Department of Statistics
Ru He, Department of Computer Science
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 k0; (b) the second phase computes the probability of satisfying the k0-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.
Quicklinks: Tool, Case Studies (Illustrative Example, Queue, Zeroconf, Dining Philosopher), Comments on Optimization
Prototype: Infinite State Model--XSB implementation
Tool
- Download and install Perl.
- Download and install PRISM. All experiments are conducted using Prism v 3.2 on Linux platform.
- Download the scripts below.
twophase-v1.pl: (k0 is obtained by incrementing the value of k by fixed amount.)
In this file, you will have to update the value of $prismexe variable to point to the location of your prism executable.
Usage: The input parameters are listed below. All except the model (model file) and the prop (property file) optional inputs. If the objective is to estimate P=?(φ1 U φ2), then the property file must contain P=?(φ1 U φ2) (i.e., P=?Ψ1) and P=?(!φ2 U (!φ1 /\ !φ2) (i.e., P=?Ψ2). The perl script will read this file and create the corresponding bounded PCTL properties P=?Ψk1 and P=?Ψk2 for different values of k and for each k, P=?Ψk is estimated from the sum of the estimates: P=?Ψk1 + P=?Ψk2.
k0 = initial value of k: default is 1 kmax = maximum value of k: default is 1000 step = steps of increments of k: default is 10 ep = error limit: default is 0.025 de = confidence limit: default is 0.01 model = location of the probabilistic model file prop = location of the property file options = with quots to assign values to model variables: default is ""
Sample invocations:
perl twophase-v1.pl -model ./illus/illus.pm -prop ./illus/illus.pctl
perl twophase-v1.pl -kmax 1000 -model ./illus/illus.pm -prop ./illus/illus.pctl
perl twophase-v1.pl -model ./zeroconf/zeroconf.pm -prop ./zeroconf/zeroconf.pctl -options "q=0.9,r=0.9,n=10"
As per our technique, prism's statistical method will be invoked for each k in our first phase, i.e., prism's statistical method will be invoked repeatedly until a suitable k0 is obtained. However, to obtain the k0 using one invocation to prism, the implementation requires the user to provide a kmax. The perl script will generate a file of all properties (P=?Ψk1 and P=?Ψk2) from the initial value of k till kmax. Prism's statistical method will be invoked once and it will be terminated as soon as a suitable k is obtained for which the estimate of P=?Ψk1 + P=?Ψk2 reaches the required threshold (1-ε0).
User is also provided with the option to change the step by which k will be incremented.
Example: If the property file contains
label "phi1" = ( s=0 | s=1 | (s>10 & s<=10000));
label "phi2" = ((s=4) | (s=3));
P=?[ "phi1" U "phi2" ]
P=?[ !"phi2" U (!"phi2" & !"phi1") ]
and
perl twophase-v1.pl -k0 10 -kmax 1000 -step 20 -model ./illus/illus.pm -prop ./illus/illus.pctl
is invoked, then a file temp.pctl is generated in the current directory containing:
label "phi1" = ( s=0 | s=1 | (s>10 & s<=10000));
label "phi2" = ((s=4) | (s=3)); P=?[ "phi1" U<=10 "phi2" ]
P=?[ !"phi2" U<=10 (!"phi2" & !"phi1") ]
P=?[ "phi1" U<=30 "phi2" ]
P=?[ !"phi2" U<=30 (!"phi2" & !"phi1") ] ...
P=?[ "phi1" U<=1000 "phi2" ]
P=?[ !"phi2" U<=1000 (!"phi2" & !"phi1") ]
Sample output:
bash$ perl twophase-v1.pl -k0 20 -kmax 1000 -step 20 -model ./illus/illus.pm -prop ./illus/illus.pctl
Required target for P(psi_k): 0.9975
N1=19172, N2= 239658 for epsilon=0.025 and delta=0.01
for 20: 0.991176470588235
for 40: 0.993137254901961
for 60: 0.994117647058824
for 80: 0.995098039215686
...
for 200: 0.998039215686275
k0 Bound obtained for P(psi_k)=0.9975 is 200 Time taken for phase 1: 1 sec.
Estimated prob result: 0.6610878835674169 Time taken for phase 2: 51 sec.
twophase-v2.pl: k0 is obtained by incrementing the value of k by Δ.
In this file, you will have to update the value of $prismexe variable to point to the location of your prism executable.
Usage: The input parameters are listed below. In this version, kmax and step are not input parameters.
k0 = initial value of k: default is 1
ep = error limit: default is 0.025
de = confidence limit: default is 0.01
model = location of the probabilistic model file
prop = location of the property file
options = with quots to assign values to model variables: default is ""
Sample invocations:
perl twophase-v2.pl -model ./phil/phil40.pm -prop ./phil/phil40.pctl
perl twophase-v2.pl -k0 20 -model ./phil/phil40.pm -prop ./phil/phil40.pctl
perl twophase-v2.pl -model ./zeroconf/zeroconf.pm -prop ./zeroconf/zeroconf.pctl -options "q=0.9,r=0.9,n=10"
Sample output:
In the output, Mode 0 refers to the case where the increment in k is first done by steps of 10 till the estimate of P(psi_k) is greater than 0.1, after which the increments are done using Δ. Mode 1 refers to the binary search strategy.
bash$ perl twophase-v2.pl -model ./phil/phil40.pm -prop ./phil/phil40.pctl
Required target for P(psi_k): 0.9975
Required upper bound for P(psi_k): 0.99875
N1=19172, N2= 239658 for epsilon=0.025 and delta=0.01
for 1: 0 Mode 0 increment
for 11: 0.0100146046317546 Mode 0 increment
for 21: 0.0665553932818694 Mode 0 increment
for 31: 0.191946588775297 Mode 0 increment
for 95: 0.982943876486543 Mode 0 increment
for 96: 0.990976423951596 Mode 0 increment
for 106: 0.996192363863968 Mode 0 increment
for 108: 0.99775714583768
k0 Bound obtained for P(psi_k)=0.9975 is 108 Time taken for phase 1: 175 sec.
Estimated prob result: 0.019506964090495623 Time taken for phase 2: 400 sec.
Case Studies
Illustrative Example from the Paper: Download Illustrative Example
Input Property File
Download Illustrative Example property
Input Property File
Download Queue Example property
Precision Results
Results of Δ jumps
Input Property File
Download Zeroconf Example property
Precision Results
Results of Δ jumps
Dining Philosopher DTMC: Download Phil10 Example
Input Property File
Download Phil10 Example property
Precision Results
Results of Δ jumps
Some Comments on Optimization (see Section 5.2 of the paper)
The increment-scheme for searching for the bound k (of simulation path length) is based on first-order (linear) approximation. More precisely, for the current value of k, we want to choose Δ such that F(k+Δ) = 1- ε0, where F(.) is as introduced in Section 4 of the paper. Applying Taylor's approximation, we get
F(k+Δ) ≈ F(k) + F'(k)Δ = 1- ε0
Defining p(i)=F(ki) where ki is the value of k in the i-th iteration for i=1,2, ..., we calculate Δ for choosing the next value of k by solving the above equation with F'(k) approximated by the first order difference of the p(i)-sequence:
p(i-1) + [ ( p(i-1) - p(i-2) )⁄( ki-1 - ki-2 ) ] Δ = 1- ε0
This leads to the main part of the iteration scheme to obtain k. Note that the success of the scheme depends on the properties of the F function (see Fig 3, 4 in paper). Specifically, the speed of convergence of the scheme depends on the first derivative F'(k) described above. For examples such as zeroconf and queue (first two examples in Section 5.1) this derivative is monotonically decreasing (See Fig A below), whereas for examples such as Dining Philosopher protocol (third example in Section 5.2) this derivative is not a monotone function (see Figure B below). In the first case (derivative monotonically decreasing), the scheme described above will always produce values smaller or equal to the true k0, and the sequence of ki's will converge to k0 from below. In the other case, it is possible that our scheme ''overshoots'' the true k0: i.e., at some point in the iteration, Δ-value became so large that the bound (1-ε0) is reached, but we ended up with a k0 value that is larger than the minimum possible value (that attains the bound). Since the second phase of our method depends on the bound k, it is in our interest to obtain as small value of k0 as possible. This prompted us to introduce the second part of the optimization, where this ''overshooting'' problem is addressed by a binary search of smaller k values.
 |
 |
| Fig A | Fig B |
Handling Infinite State Models: XSB Implementation
- Download and install XSB logic programming system. All experiments are conducted using XSB v 3.1 on Linux platform.
- Download xsbi.P: XSB implementation of two-phase sampling based technique.
This is a prototype implementation used to show that our technique can handle models with infinite state-space. The property must be of p U q.
Usage: The implementation includes PRISM's statistical method and our two-phase method. Each method has been set up to work with the typical (default) settings of error (ε) and confidence parameters, and sample path length (for PRISM's statistical method). These values can be updated if needed (refer to commented sections in the xsbi.P).
The model is described using three predicates:
- trans(Source, Probability, Destination): transition from Source to Destination with some Probability.
- sat(State, Proposition): Proposition is satisfied State.
- startstate(State): the start state of the model is State.
-
Given a model file inf.P, PRISM statistical method can be applied using XSB implementation as follows. Commands appear in the lines starting with $ prompt and |?-
Start XSB environment and compile the implementation file.
$ [your XSB Executable Dir/]xsb [xsb_configuration loaded] [sysinitrc loaded] XSB Version 3.1 (Incognito) of August 10, 2007 [i686-pc-linux-gnu; mode: optimal; engine: slg-wam; gc: indirection; scheduling: local] | ?- [xsbi]. [Compiling ./xsbi] % Specialising partially instantiated calls to satisfies/2 % Specialising partially instantiated calls to tsimu/4 [xsbi compiled, cpu time used: 0.0210 seconds] [xsbi loaded] yes
Load the model file| ?- load(inf). [inf.P dynamically loaded, cpu time used: 0.0010 seconds]
Invocation for PRISM statistical method| ?- prismsim.
Invocation for two-phase method| ?- twophase.