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

Hence, Ψ] has a positive answer if and only if E[ X ] θ .

If we could sample observations of X , then we could use statistical hypothesis
testing or estimation to verify

M ,s | = P θ [Φ U

Ψ]. To sample an observation of X ,we
would sample a trajectory from Path ( s ) (e.g., using discrete-event simulation)
and verify Φ

P θ [Φ U

U

Ψ over the sample trajectory. A single sample trajectory would
be extended incrementally until we reach a state that satisfies either Ψ (positive
observation; the path formula holds over the sample trajectory) or

Φ (negative
observation; the path formula does not hold over the sample trajectory). The
problem with this naive approach is that we are not guaranteed to ever reach
a state that satisfies either Ψ or

¬

Φ. It works well for probabilistic properties
with time-bounded until, as demonstrated by Younes and Simmons [26], because
we can stop extending a sample trajectory if the time bound is exceeded. This
ensures termination (with probability 1) provided that the model is time diver-
gent. For unbounded until, however, there is no finite time bound to stop us
from going on indefinitely, so we can no longer guarantee termination.
Consider, for example, the model in Fig. 1(a), with a single state satisfying
some state formula Ψ. Assume that we want to verify

¬

Ψ]
(i.e., the probability of eventually reaching the state satisfying Ψ is at least 0 . 15
if we start in state s 0 at time 0). Note that the state satisfying Ψ is shown as
absorbing—i.e., it has no outgoing transitions. This is to reflect that sample-
trajectory generation ends in that state. For all other states, the outgoing tran-
sition probabilities sum to 1. Any trajectory that starts in s 0 and does not satisfy
U

M ,s 0 | = P ≥ 0 . 15 [ U

Ψ is infinite. For this simple model, the probability measure of the set of
satisfying trajectories that start in s 0 at time 0 can be computed as:

∞

1
6

0 . 4 i = μ ( { σ ∈ Path ( s 0 ): M ,σ | = U Ψ } )=0 . 1 · . (8)

i =0

Thus the stated model-checking problem has a positive answer, but a naive
sampling-based approach does not work due to the positive probability ( 6 )for
the set of infinite trajectories.
Next, we describe two sampling-based solution methods that aim to avoid
infinite sample trajectories.

1 0. 9

1 0. 9

0. 5 0. 5 0. 45

1 0. 1 1 0. 1 0. 9 0. 09

s 0 Ψ s 0 Ψ s 0 Ψ

0. 4 0. 4

(b) M R

0. 36

(a) M (c) M T ( p T =0 . 1)

Fig. 1. Three variations of a simple discrete-time Markov chain