Information Technology Reference
In-Depth Information
Definition 14 (Strong simulation).
For AIMC
I
=(
S,
Act
,L,
P
l
,
P
u
,λ,s
0
)
,
S
is a
simulation relation
, iff for any
(
s, s
)
R
⊆
S
×
∈
R
it holds:
1a. for all
α
∈ Act
and
u
∈
S
with
L
(
s, α, u
)
⊥
there exists
u
∈
S
with
=
L
(
s
,α,u
)
⊥
and
(
u, u
)
∈
R
,
=
and
u
∈
S
with
L
(
s
,α,u
)=
1b. for all
α ∈ Act
there exists
u
∈
S
with
and
(
u, u
)
L
(
s, α, u
)=
∈
R
,and
T
(
s
)
there exists
μ
∈
T
(
s
)
2.
L
(
s, τ, u
)
=
for all
u
∈
S
,impliesforall
μ
∈
[0
,
1]
such that for all
u, u
∈
and
Δ
:
S
×
S
→
S
:
(a)
Δ
(
u, u
)
>
0=
uRu
(c)
Δ
(
S, u
)=
μ
(
u
)
⇒
(b)
Δ
(
u, S
)=
μ
(
u
)
s
if (
s, s
)
II
for AIMCs
We write
s
∈
R
for some simulation
R
and
I
I
.
Let us briefly explain this definition. Item 1a requires that any may- or must-
transition of
s
must be reflected in
s
. Item 1b requires that any must-transition
of
s
must match some must-transition of
s
, i.e., all required behavior of
s
stems
from
s
. Note that this allows a must-transition of
s
to be mimicked by a may-
transition of
s
. Condition (2) is the same as in the defininition of simulation for
IMCs, except that the set of distributions in a state in an IMC is a singleton,
whereas for AIMCs this set can be infinite.
I
with initial states
s
0
and
s
0
,if
s
0
s
0
in the disjoint union of
and
I
and
Theorem 12.
[49] For any AIMC
I
and abstraction function
α
,
I
α
(
I
)
.
As this abstraction is coarser than bisimulation, a significantly larger state-
space reduction may be achieved and peak memory consumption is even further
reduced. The notion of parallel composition and hiding, as defined for IMCs can
now be lifted to AIMCs in a natural manner, and it can be shown that
Theorem 13.
[49]
is a pre-congruence wrt. parallel composition and hiding.
This result provides us the means to carry out abstraction on (A)IMCs in a fully
compositional manner. 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. Let
α
(
I
i
)betheabstractionofIMC
I
i
,
for 0
<i
N
. Thanks to the property that strong simulation is substitutive
wrt. parallel composition, it follows from the fact that
≤
I
i
α
(
I
i
), for 0
<i
≤
N
,
that:
I
1
||
A
1
I
2
||
A
2
...
||
A
N
I
N
α
(
I
1
)
||
A
1
α
(
I
2
)
||
A
2
...
||
A
N
α
(
I
N
)
.
5 IMCsasSemanticalModel
Much of computer science is about specification formalisms. Domain specific
languages as well as universal notations are being promoted by various interest
groups and taken up by standardization bodies. Some of them appeal due to their
graphical notation convenience, such as the UML, others appeal because they
