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

probabilistic model checking, PRISM [17], relies on iterative methods to verify
properties with unbounded until. Each iteration involves a matrix-vector multi-
plication, which in the worst case is O ( n 2 ), but often O ( n )(forsparsemodels),
where n is the size of the state space. This dependence on the size of the state
space make numerical solution methods impractical for very large models, in
which case sampling-based solution become an attractive alternative.
The number of iterations ( k ) required to achieve some numerical precision
is related to the subdominant eigenvalue ( ρ )of P as follows [22, p. 156]:
k =

log

log ρ . Since computing eigenvalues is no easier than solving the model-
checking problem, heuristics must be employed to bound the number of itera-
tions, but this means that no formal correctness guarantees can be made. This
is similar to the situation for the second sampling-based method we described.
The reachability-based sampling approach, in contrast, does not suffer from this
weakness as the precision of the result is independent of any property of the
model.
John von Neumann and Stanislaw Ulam, as early as the 1940s, devised a
Monte Carlo method for solving systems of linear equations of the type in (12).
It is this algorithm, first published by Forsythe and Leibler [10], that we use in
the second of our solution methods. It should come as no surprise that both the
iterative numerical solution methods, and the Monte Carlo approach that uses
a termination probability, have a dependency on the subdominant eigenvalue to
provide some prescribed precision. The method of von Neumann and Ulam is
essentially a Monte Carlo version of a numerical iterative algorithm.
Sampling-based solution methods for time-unbounded formulae have received
some attention recently [21,18,3,7], but these authors appear unaware of the
method devised by von Neumann and Ulam.
Sen et al. [21] propose a solution method that on the surface looks similar
to our second approach (the one based on the method by von Neumann and
Ulam). They use a termination probability p T in the same way as we to ensure
terminating sample trajectories. Instead of using weighted sampling with the
random variable X T , however, they use the following Bernoulli random variable:
Y T ( σ )= 1 f

M T ,σ | =Φ U Ψ

.

(13)

0 f M T ,σ | =Φ U Ψ

The problem with Y T is that its expectation does not match that of the random
variable X . Sen et al. recognize this problem and provide a bound on the expec-
tation E[ X ]expressedintermsofE[ Y T ]. The bound depends on the size of the
model, however, and is too loose to be useful in practice.
In other work [18,27,3], it is proposed to use the results from verifying time-
bounded properties to obtain a probability estimate for unbounded properties.
These methods essentially boil down to estimating the expected value of the
following random variable:
Z k ( σ )= 1 f

M ,σ ↑ k | =Φ U Ψ

. (14)

0 f M ,σ ↑ k | =Φ U Ψ