Sciweavers

ICFEM
2009
Springer

Approximate Model Checking of PCTL Involving Unbounded Path Properties

14 years 4 months ago
Approximate Model Checking of PCTL Involving Unbounded Path 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 either consider a restricted subset of PCTL, specifically, the subset that can only express bounded until properties; or rely on user-specified finite bound on the sample path length. We propose a new method that does not have such restrictions 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 a 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 phas...
Samik Basu, Arka P. Ghosh, Ru He
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where ICFEM
Authors Samik Basu, Arka P. Ghosh, Ru He
Comments (0)