Information Technology Reference
In-Depth Information
3.1
Sampling-Based Method with Reachability Analysis
The first method uses reachability analysis to avoid infinite sample trajectories.
For an unbounded until formula Φ
U
Ψ to hold over a single sample trajectory
σ
for model
M
, it is necessary (although not sucient) that
M
,σ
[
i
]
|
=Ψforsome
i
≥
0. If after the generation of a finite prefix
σ
↑
n
it becomes evident that
¬
Ψ
invariably holds along all possible extensions of
σ
↑
n
, then we can determine that
Φ
Ψdoesnotholdover
σ
without generating a complete (possibly infinite)
sample trajectory.
This condition for early termination can be expressed formally as the
non-
probabilistic
CTL [6] formula
AG
U
¬
Ψ, or equivalently
¬
EF
Ψ. Hence, if we first
verify
EF
Ψforamodel
, which amounts to reachability analysis, then we
can terminate the generation of any sample trajectory entering a state of
M
M
that does not satisfy
EF
Ψ. This pre-processing step requires that we construct
the full model, so it may seem counter to the appeal of sampling-based methods,
which usually avoid model construction. We show, however, in Sect. 5 that this
approach that combines symbolic reachability analysis and statistical sampling
can work very well in practice. It scales better with the size of the model than nu-
merical solution methods, which enables us to verify time-unbounded properties
for larger models.
Let
M
R
be the model we get by removing all outgoing transitions from all
states in
that do not satisfy
EF
Ψ. We can now define the Bernoulli random
variable
X
R
:
Path
R
(
s
)
M
as follows:
X
R
(
σ
)=
1 f
→{
0
,
1
}
M
R
,σ
|
=Φ
U
Ψ
.
(9)
0 f
M
R
,σ
|
=Φ
U
Ψ
Theorem 1.
Let
X
be the random variable defined in (6) and let
X
R
be the ran-
dom variable defined in (9). The expectation of
X
R
is the same as the expectation
of
X
:
E[
X
R
]=E[
X
]
.
This theorem is a standard result in Markov chain theory (see, e.g., [2]), and
a consequence of it is that we can use statistical hypothesis testing with obser-
vations of
X
R
instead of
X
to verify
. The benefit of using
observations of
X
R
instead of
X
is that certain trajectories that are infinite in
P
θ
[Φ
U
Ψ] in
M
M
have been made finite in
M
R
.Since
X
R
still represents a Bernoulli trial, the ex-
act same techniques as for formulae with time-bounded until (described in detail
by Younes and Simmons [26]) can be used to verify formulae with unbounded
until for model
M
R
, satisfying conditions (4) and (5).
We illustrate this solution method on the discrete-time Markov chain in Fig. 1.
The original model is shown in Fig. 1(a). After performing reachability analysis,
we obtain the model in Fig. 1(b). The gray states have been made absorbing
because they do not satisfy
EF
Ψ. Trajectories generated from the modified
model will almost surely (with probably 1) eventually terminate.
We assume here that reachability analysis can be performed eciently on
the model
M
. For Markov chains, we can ignore the actual values of transition
Search WWH ::
Custom Search