Information Technology Reference
In-Depth Information
mapped onto
s
.
α
is called the abstraction function whereas
γ
=
α
−
1
is known
as the concretization function.
Definition 13 (Abstraction).
For an AIMC
I
=(
S,
Act
,L,
P
l
,
P
u
,λ,s
0
)
,the
S
induces the AIMC
α
(
)=(
S
,
,L
,
P
l
,
P
u
,λ,
abstraction function
α
:
S
→
I
Act
α
(
s
0
))
,where:
⎧
⎨
if
u∈γ
(
u
)
L
(
s, β, u
)=
γ
(
s
)
for all
s
∈
if
u∈γ
(
u
)
L
(
s, β, u
)=
-
L
(
s
,β,u
)=
⊥
⊥
for all
s
∈
γ
(
s
)
⎩
?
otherwise
-P
l
(
s
,u
)=min
s∈γ
(
s
)
u∈γ
(
u
)
P
l
(
s, u
)
-P
u
(
s
,u
)=min(1
,
max
s∈γ
(
s
)
u∈γ
(
u
)
P
u
(
s, u
))
There is a must-transition
s
γ
(
s
) exhibits
such transition to some state in
γ
(
u
). There is no transition between
s
and
u
if
there is no such transition from
s
α
u
if any concrete version
s
−−→
∈
γ
(
s
)to
γ
(
u
). In all other cases, we obtain
∈
a may-transition
s
α
u
.
−−→
Example 4.
Consider the uniform IMC depicted in the figure below on the left,
and ket
S
=
be the abstract state space. Assume the abstraction is
defined by
α
(
u
0
)=
α
(
u
1
)=
u
,and
α
(
s
0
)=
α
(
s
1
)=
s
. This yields the abstract
IMC depicted on the right. As
s
0
{
s, u
}
α
α
−−→
u
0
and
s
1
−−→
u
1
, there is a must-transition
β
−−→
labeled by
α
from
s
to
u
. Although
s
0
u
0
,
s
1
has no
β
-transition to
u
0
or
u
1
. Accordingly, we obtain a may-transition labeled with
β
between
s
and
u
.As
P
(
u
0
,s
1
)=
2
and
P
(
u
1
,s
1
)=
3
, we obtain that
P
l
(
u, s
)=
3
and
P
u
(
u, s
)=
2
.
The other probability intervals are justified in a similar way.
β
may
β
α
s
0
u
0
α
s
u
1
2
2
3
1
2
1
[
3
,
2
]
[
2
,
3
]
[1
,
1]
s
1
u
1
α
1
1
3
The formal relationship between an AIMC and its abstraction is given by a
simulation relation which is in fact a combination of probabilistic simulation on
IMCs as defined before (with a slight adaptation to deal with intervals) and the
concept of refinement on modal transition systems [52]. Let
T
(
s
)denotetheset
of probability distributions that exist in state
s
and that satisfy all bounds of
the probability intervals of the outgoing Markovian interval transitions of
s
.
