Information Technology Reference
In-Depth Information
Theorem 8.
[56] 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
The above result opens the way to generate —prior to any (time-consuming)
analysis— an IMC that is bisimilar to the IMC under consideration, but prefer-
ably much smaller. This is called the quotient IMC. For equivalence relation
R
on state space
S
and
s
∈
S
,let[
s
]
R
denote the equivalence class of
s
under
R
,
and let
S/R
=
{
[
s
]
R
|
s
∈
S
}
denote the quotient space of
S
under
R
.
Definition 10 (Quotient IMC).
Let
I
=(
S,
Act
,
−→
,
⇒
,s
0
)
be an IMC
/R
=
S/R,
−→
,
and
R
a strong bisimulation on
S
.The
quotient IMC
I
Act
,
⇒
,
[
s
0
]
R
where
−→
and
⇒
are the smallest relations satisfying:
α
s
implies
[
s
]
R
−−→
[
s
]
R
,and
α
1.
s
−−→
R
(
s,
[
s
]
R
)
⇒
[
s
]
R
.
λ
⇒
s
implies
[
s
]
R
2.
s
I
I∼I
/R
.
It now follows that for any IMC
and strong bisimulation, it holds
∼
≈
(A similar result holds for weak bisimulation, replacing
).
The next question is how to obtain the bisimulation quotient of a given IMC,
and preferably even the quotient with respect to the coarsest bisimulation, as
this yields an IMC of minimal size which is strong bisimilar to the original one.
Using a variant of Paige-Tarjan's partition-refinement algorithm for computing
strong bisimulation on labeled transition systems we obtain:
by
Theorem 9.
[35] For any IMC
I
with state space
S
and strong bisimulation
R
on
S
, the quotient IMC
I
/R
can be computed in time complexity
O
(
m
log
n
)
where
m
and
n
are the number of transitions and states of the IMC
I
.
The results so far suggest to compute the quotient IMC prior to the analysis
of, e.g., time-bounded reachability probabilities. This leads to significant state-
space reductions and eciency gains in computation times, as e.g., is shown
in [47] for CTMCs. But, as the bisimulation minimisation is not an on-the-fly
algorithm, it requires the entire state space of the original, i.e., non-minimised
IMC up front. For realistic systems, this requirement is a significant burden.
Fortunately, as IMCs are compositional —they can be put in parallel in a simple
manner— and as bisimulation is a congruence wrt. parallel composition, bisim-
ulation minimisation can be applied in a
component-wise manner
. This works as
follows. Suppose the system-to-be-analysed is of the form:
I
=
I
1
||
A
1
I
2
||
A
2
...
||
A
N
I
N
,
i.e., a parallel composition of
N
IMCs. For the sake of our argument, let us
assume that the size of
is too large to be handled, and therefore bisimulation
minimisation cannot be applied. However, each component is of a moderate
size that can be subject to minimisation. Let
I
I
i
be the quotient of IMC
I
i
,for
0
<i
N
. Each such quotient can be obtained by the aforementioned partition-
refinement algorithm. Thanks to the property that bisimulation is substitutive
≤
