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

estimation to verify probabilistic properties [26,18]. The challenge for statistical
algorithms with time-unbounded properties is to determine the truth-value of
Φ

Ψ without generating infinite sample trajectories.
The first method (see Sect 3.1) combines reachability analysis with statistical
sampling. This approach has been used in the past for program analysis [20],
and more recently for model checking [27] using biased sampling. The algorithm
is ensured termination for any finite-state homogeneous discrete-time Markov
chain, although it is potentially applicable for any model for which we can per-
form reachability. The use of reachability analysis requires that we construct the
full model, so it may seem counter to the appeal of statistical methods, which
usually avoid model construction. The real cost in probabilistic model checking,
however, lies in the numerical computation of probabilities, which we replace
with sampling. We show in Sect. 5 that the combination of reachability analysis
and statistical sampling scales better with the size of the model than standard
numerical solution methods. As a result, we can verify time-unbounded prop-
erties for larger models than possible with existing numerical algorithms. By
using unbiased sampling, we can also make strong guarantees regarding error
bounds. Other sampling-based methods, as well as iterative numerical solution
methods, do not give the same strong guarantees as they depend on heuristics
for bounding sample trajectory lengths or number of iterations.
The second method (see Sect. 3.2) is based on a Monte Carlo method devised
in the 1940s by John von Neumann and Stanislaw Ulam for computing the in-
verse of a matrix [10]. This method uses a termination probability p T that is
applied in each state along a trajectory to ensure finite sample trajectories. To
account for the change in sample distribution, we weigh satisfying trajectories
more heavily the longer the trajectory is. This way, we obtain an unbiased esti-
mator of the probability that Φ

U

Ψ holds over the set of trajectories that start
in some state s . The second method does not rely on reachability analysis, so
it has minimal memory requirements. It generally requires a larger number of
sample trajectories to achieve the same precision as the first method, so it can
be slower than the first method when reachability analysis is fast. It also suffers
from the same problem as iterative numerical solution methods in that accuracy
can be hard to guarantee. Still, the second method is potentially applicable for
a much larger class of models.
We limit our attention to discrete-time Markov chains. The results extend
trivially to continuous-time Markov chains and semi-Markov processes, as veri-
fication of time-unbounded properties for such models is done on an embedded
discrete-time Markov chain.

U

2 Probabilistic Model Checking

This section describes discrete-time Markov chains (without nondeterminism),
which is the class of models that we consider for probabilistic model checking.
We present a temporal stochastic logic (a subset of PCTL) and discuss realistic
error control for statistical model-checking algorithms.