Information Technology Reference
In-Depth Information
Definition 11 (Uniform IMC).
An IMC is
uniform
if for any state
s
we have
that
∈
R
>
0
.
The residence time in any state with at least one Markovian transition is thus
governed by the same exponential distribution. Although this seems a rather
severe restriction, there is an important class of systems for which this applies,
viz. IMCs in which delays are imposed in a compositional manner using the
constraint-oriented specification style. The point is that any CTMC can be
transformed by a simple linear-time procedure into a weak bisimilar uniform
CTMC [3]. Consider the specification
P
MT
(
s
)
=
∅
implies
E
(
s
)=
λ
for a given fixed
λ
||
A
D
p
where
P
is an IMC with only
interactive transitions, i.e.,
P
is an LTS, and
D
p
is a CTMC, probably enhanced
with a start action
α
and end action
β
as explained before. The purpose of
D
p
is to impose a random delay between the occurrence of
α
and
β
in
P
.Thisis
modeled as an arbitrary, finite-state CTMC. We can now transform
D
into its
uniform counterpart
D
p
,say.As
D
p
≈ D
p
and
is substitutive wrt. parallel
composition, it follows that the non-uniform IMC
P ||
A
D
p
is weak bisimilar to
the uniform IMC
P
≈
||
A
D
p
. (Several operators are preserving uniformity, see [38].)
is a natural mixture of
abstraction of labeled transition systems by
modal
transition systems [51,52] and
abstraction of probabilities by
intervals
[27,48]. This combination yields
abstract
IMCs.
Let IMC
I
be uniform. Our abstraction technique for
I
Definition 12 (Abstract IMC).
An
abstract
IMC is a tuple
I
=(
S,
Act
,L,
P
l
,
P
u
,λ,s
0
)
with
S
,
s
0
and
Act
as before, and
-
L
:
S × Act × S →
B
3
,a
three-valued labeled
transition function
-P
l
,
P
u
:
S
×
S
→
[0
,
1]
, lower/upper transition
probability bounds
s.t.
P
l
(
s, S
)
≤
1
≤
P
u
(
s, S
)
and
-
λ
∈
R
>
0
,anexitrate.
B
3
=
{⊥
,
?
,
}
⊥
<
?
<
Here
is the complete lattice with the ordering
and
) operations. The labeling
L
(
s, α, s
) identifies the transition
“type”:
indicates a must-transition, ? a may-transition, and
⊥
the absence of
a transition.
P
l
(
s, s
) is the minimal one-step probability to move from
s
to
s
,whereas
P
u
(
s, s
) is the maximal one-step probability between these states.
Given these bounds, the IMC can move from
s
to
s
with any probability in
the interval [
P
l
(
s, s
)
,
P
u
(
s, s
)]. Any uniform IMC is an AIMC without may-
transitions and for which
P
l
(
s, s
)=
P
u
(
s, s
). The requirement
P
l
(
s, S
)
meet (
)andjoin(
≤
P
u
(
s, S
) ensures that in any state
s
, a distribution
μ
over the direct successor
states of
s
can be chosen such that for any
s
≤
1
we have:
P
l
(
s, s
)
μ
(
s
)
≤
≤
P
u
(
s, s
).
Let us now describe how to perform abstraction of an (A)IMC. As stated
above, the principle is to partition the state space by grouping concrete states
to abstract states. For concrete state space
S
and abstract state space
S
,let
α
:
S
S
map states to their corresponding abstract ones, i.e.,
α
(
s
) denotes
the abstract state of
s
and
α
−
1
(
s
)=
γ
(
s
)isthesetofconcretestatesthatare
→
