A bounded statistical approach for model checking of unbounded until properties

We study the problem of statistical model checking of probabilistic systems for PCTL unbounded until property P1p(ϕ1 U ϕ2) (where 1 ∈ {<, ≤, >, ≥}) using the computation of P≤0(ϕ1 U ϕ2). The approach is first proposed by Sen et al. [13] but their approach suffers from two drawbacks. Firstly, the computation of P≤0(ϕ1 U ϕ2) requires for its validity, a user-specified input parameter δ2 which the user is unlikely to correctly provide. Secondly, the validity of computation of P≤0(ϕ1 U ϕ2) is limited only to probabilistic models that do not contain loops. We present a new technique which addresses both problems described above. Essentially our technique transforms the hypothesis test for the unbounded until property in the original model into a new equivalent hypothesis test for bounded until property in our modified model. We empirically show the effectiveness of our technique and compare our results with those using the method proposed in [13].

• Type: Journal
• Year: 2010
• Where: KBSE
• Authors: Ru He, Paul Jennings, Samik Basu, Arka P. Ghosh, Huaiqing Wu
• Keywords: Computation, Hypothesis Test, KBSE 2010, Software Engineering, User-specified Input Parameter