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...

• Type: Conference
• Year: 2009
• Where: ICFEM
• Authors: Samik Basu, Arka P. Ghosh, Ru He
• Keywords: ICFEM 2009, Model Checking, Software Engineering, Statistical Methods, Such Approximate Methods