Sciweavers

Share
KBSE
2010
IEEE

A bounded statistical approach for model checking of unbounded until properties

9 years 2 months ago
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].
Ru He, Paul Jennings, Samik Basu, Arka P. Ghosh, H
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where KBSE
Authors Ru He, Paul Jennings, Samik Basu, Arka P. Ghosh, Huaiqing Wu
Comments (0)
books