Statistical Verification of Probabilistic Properties with Unbounded Until - Formal Methods: Foundations and Applications - page 144

Statistical Verification of Probabilistic
Properties with Unbounded Until

H akan L.S. Younes 1 , Edmund M. Clarke 2 , and Paolo Zuliani 2

1 Google Inc
2 Computer Science Department, Carnegie Mellon University, USA

Abstract. We consider statistical (sampling-based) solution methods
for verifying probabilistic properties with unbounded until. Statistical
solution methods for probabilistic verification use sample execution tra-
jectories for a system to verify properties with some level of confidence.
The main challenge with properties that are expressed using unbounded
until is to ensure termination in the face of potentially infinite sample ex-
ecution trajectories. We describe two alternative solution methods, each
one with its own merits. The first method relies on reachability analy-
sis, and is suitable primarily for large Markov chains where reachability
analysis can be performed eciently using symbolic data structures, but
for which numerical probability computations are expensive. The second
method employs a termination probability and weighted sampling. This
method does not rely on any specific structure of the model, but er-
ror control is more challenging. We show how the choice of termination
probability—when applied to Markov chains—is tied to the subdomi-
nant eigenvalue of the transition probability matrix, which relates it to
iterative numerical solution techniques for the same problem.

1 Introduction

Probabilistic model checking deals with verification of stochastic systems, such
as a queuing system with random arrivals and departures. Temporal stochas-
tic logics, e.g., PCTL [12] and CSL [1], exist for expressing properties of such
stochastic systems. Our focus is on time-unbounded properties of stochastic sys-
tems. For a queuing system, for instance, an interesting property could be: “the
probability is at most 0 . 1 that the queue eventually becomes full.” In PCTL,
such properties are expressed using the formula

full].
We present two statistical algorithms for solving such model-checking prob-
lems that are based on unbiased sampling. Sampling is said to be unbiased if the
expectation of the sample distribution is the same as the expectation of the true
distribution. The use of unbiased sampling distinguishes our methods from most
recent efforts to devise sampling-based algorithms for time-unbounded proper-
ties, which are based on biased sampling [21,18,27,3] (see Sect. 4).
Statistical algorithms for probabilistic model checking use discrete-event sim-
ulation to generate sample trajectories, and verify some temporal formula over
each generated trajectory. This is combined with hypothesis testing or statistical

P ≤ 0 . 1 [ U