Information Technology Reference
In-Depth Information
Equations :
(P1)
P
p
↕
P
=
P
(P2)
P
p
↕
Q
=
Q
1
−
p
↕
P
(P3)
(
P
p
↕
Q
)
q
↕
R
=
P
p
·
q
↕
(
Q
(
1
−
p
)
·
q
1
↕
R
)
−
p
·
q
(I1)
P P
=
P
(I2)
P Q
=
Q P
(I3)
(
P Q
)
R
=
P
(
Q R
)
(E1)
P
=
P
0
(E2)
P Q
=
Q P
(E3)
(
P Q
)
R
=
P
(
Q R
)
(EI)
a
P
a
Q
=
a
P a
Q
.
.
.
.
(D1)
P
(
Q
p
↕
R
)=(
P Q
)
p
↕
(
P
R
)
(D2)
a
P
(
Q R
)=(
a
P Q
)
(
a
P
R
)
.
.
.
(D3)
(
P
1
P
2
)
(
Q
1
Q
2
)=(
P
1
(
Q
1
Q
2
))
(
P
2
(
Q
1
Q
2
))
((
P
1
P
2
)
Q
1
)
((
P
1
P
2
)
Q
2
)
May :
(May0)
a
P
b
Q
=
a
P b
Q
.
.
.
.
(May1)
P
P Q
(May2)
0
P
(May3)
a
.
(
P
p
↕
Q
)
a
P
p
↕
a
Q
.
.
Must :
(Must1)
P Q
Q
(Must2)
R
p
j
·
(
a
i
Q
ij
P
ij
)
I
a
i
J
i
p
j
·
Q
ij
.
.
,
i
∈
j
∈
∈
I
j
∈
J
i
i
provided
inits
(
R
)
ↆ
{
a
i
}
i
∈
I
Fig. 5.8
Equations and inequations. (©[2007] IEEE. Reprinted, with permission, from [
16
])
The axiom (
Must2
) can equivalently be formulated as follows:
a
i
.
j
∈
J
i
a
k
.R
k
p
j
·
(
a
i
.Q
ij
P
ij
)
p
j
·
Q
ij
,
k
∈
K
∈
L
k
i
∈
I
j
∈
J
i
i
∈
I
{
a
k
|
k
∈
K
,
∈
K
k
}ↆ{
a
i
|
i
∈
I
}
.
This is the case because a term
R
satisfies
inits
(
R
)
provided
ↆ{
a
i
}
i
∈
I
iff it can be converted
into the form
k
∈
K
a
k
.R
k
by means of axioms (
D1
), (
P1
)-(
P3
) and (
E1
)-(
E3
)
∈
L
k
of Fig.
5.8
. This axiom can also be reformulated in an equivalent but more semantic
style:
(
Must2
)
R
i
∈
I
P
i
i
∈
I
a
i
.Q
i
,
a
i
−ₒ
X
−ₒ
provided
[[
P
i
]]
[[
Q
i
]]
and
[[
R
]]
with
X
=
Act
\{
a
i
}
i
∈
I
.
a
−ₒ
This is the case because [[
P
]]
[[
Q
]] iff, up to the axioms in Fig.
5.8
,
P
has the
form
j
∈
J
p
j
·
P
j
) and
Q
has the form
j
∈
J
p
j
·
(
a.Q
j
Q
j
for certain
P
j
,
Q
j
and
p
j
, for
j
∈
J
.
Search WWH ::
Custom Search