Information Technology Reference
In-Depth Information
IMC,
I
=[0
,d
] a time interval with rational
d
,
G
be a set of goal states, and
A
a set of states that need to be avoided before reaching
G
. The measure-of-
interest now is to maximise the probability to reach
G
at some time point in
the interval
I
while avoiding any state in
A
prior to reaching
G
. Formally, the
event-of-interest is:
=
π ∈ Paths
ω
(
∈ A
U
[0
,d
]
G
|∃t ≤ d. ∃s
∈ π
t. s
∈ G ∧∀s
∈ pref
(
s
)
.s
A
s
)
@
(
s
) is the set of states along
π
that are reached before reaching
s
and
A
is the complement of
A
, i.e.,
A
=
S
where
pref
A
. The maximal probability of this event
can be computed in the following way. The IMC is first transformed by making
all states in
G
absorbing, i.e., for any state
s
\
G
, the outgoing transitions are
removed. This is justified by the fact that it is not of importance what happens
once a state in
G
has been reached (via a
A
-path); in addition, if a
G
-state is
reached before the deadline
d
, this does not matter, as it will still be in
G
at
time
d
since it is made absorbing. In addition, all states in
A
∈
G
are made
absorbing as the probability of a path that reaches an
A
-state which is also a
G
-state to satisfy the event-of-interest is zero. The resulting structure is thus an
IMC in which only the states in
A
∩
G
are unaffected; all other states are made
absorbing. It now follows in a similar way as in [2]:
\
A
U
[0
,d
]
G
[0
,d
]
G
Theorem 7.
sup
D
Pr
s,D
=sup
D
Pr
s,D
.
in the IMC I
in the IMC I'
I
is obtained from
Here, IMC
G
absorbing. As
a result of the above theorem, computing time-bounded reach-avoid probabilities
is reduced to determining time-bounded reachability probabilities, which can be
determined in the way described earlier. It goes without saying that a similar
strategy can be applied to (unbounded) reach-avoid probabilities.
I
by making all states outside
A
\
4 Abstraction
As for any state-based technique, the curse of dimensionality is a major limitation
for IMCs. Although its approximate analysis algorithms as described above are
polynomial (with relatively low degree) in the state space size, state spaces of
realistic systems easily consist of millions or even billions of states. In order
to deal with such systems, aggressive abstraction techniques are required. In
the following, we consider abstraction techniques that are based on partitioning
the state space into groups of states. A possibility to achieve this, is to apply
bisimulation minimisation.
Compositional bisimulation minimisation.
An important property that provides
the basis for such abstraction is the fact that for bisimilar states time-bounded
(as well as unbounded) reachability probabilities are preserved:
