Information Technology Reference
In-Depth Information
I
i
∼ I
i
,for0
<i
wrt. parallel composition, it follows from the fact that
≤
N
,
that:
||
A
N
I
N
.
The worst case time complexity to obtain this reduced system is determined
by the largest IMC
I
1
||
A
1
I
2
||
A
2
I
1
||
A
1
I
2
||
A
2
...
||
A
N
I
N
∼
...
(max
i
(
m
i
log
n
i
)) where
m
i
and
n
i
are the
number of transitions and states in IMC
I
i
. Similar reasoning applies to weak
bisimulation, with the exception that the time complexity for determining the
quotient under weak bisimulation requires the computation of a transitive clo-
sure which is in
I
i
and equals
O
(
n
2
.
376
). As weak bisimulation also preserves maximal time-
bounded reachability probabilities, and is substitutive, an IMC can be minimised
compositionally before any analysis:
Theorem 10.
For any finitely-branching IMC with state space
S
, states
s, s
∈
S
,
G
O
⊆
S
and time interval
I
:
s
p
max
(
s, I
)=
p
max
(
s
,I
)
.
s
≈
implies
Finally, for simulation preorders we obtain a slightly other preservation result.
Intuitively speaking, whenever
II
,then
I
can mimic all behaviours of
I
,
but perhaps can do more (and faster). This yields:
Theorem 11.
For any finitely-branching IMC with state space
S
, states
s, s
∈
S
,
G
⊆
S
and time interval
I
:
s
p
max
(
s, I
)
p
max
(
s
,I
)
.
s
implies
≤
One may now be tempted to first minimise an IMC wrt. simulation preorder or
its corresponding equivalence
∩
−
1
, but it turns out that checking a sim-
ulation relation between probabilistic models such as IMCs is computationally
involved [1,67]. In the sequel, we will see that simulation preorders are nonethe-
less crucial to obtain more aggressive abstraction techniques for IMCs.
Interval abstraction.
Compositional bisimulation minimisation has been applied
to several examples yielding substantial state-space reductions. It allowed the
analysis of IMCs (in fact, CTMCs) that could not be analysed without composi-
tional minimisation [39,30,32]. With the advent of increasingly complex systems,
more radical reduction techniques are needed. In the sequel, we present a recent
framework to perform aggressive abstraction of IMCs in a compositional man-
ner [49]. The key idea is to (again) partition the state space, but rather requiring
that each partition solely consists of equivalent (strong or weak bisimilar) states,
we are more liberal, and in fact allow for any state space partitioning. As a re-
sult, a state
s
is not bisimilar to its partition (as for bisimulation), but instead
its partition
simulates
s
. Intuitively speaking, this means that all behaviour of
s
can be mimicked, but perhaps that the partition exhibits more behaviours
than
s
. As the partition is aimed to be coarser than in the case of bisimulation,
a central question is which measures are preserved, i.e., what does a maximal
(time-bounded) reachability probability computed on the minimised IMC imply
for the original IMC?
In the remainder of this section, we assume that IMCs are
uniform
.
