Information Technology Reference
In-Depth Information
Inv
S
A
S
0
Inv
T
A
T
0
Inv
A
∧
Inv
B
A
S
0
T
0
h
l
v
m
g
i
∧
u
j
h
l
∧ v
m
u
j
g
i
o!
o!
p
m
s
l
···
a?
o!
···
···
···
a?
a?
r
i
∪
t
j
s
l
∪
p
m
r
i
t
j
A
S
2
A
T
2
A
S
1
A
T
1
A
S
1
T
1
A
S
2
T
2
Fig. 8.
Two states of TIOAs
A
S
and
A
T
are combined into one TIOA
A
with the
conjunctionoperatorforonestep.Thisprocessistheniterated.
-
If
(
q
S
,a,ϕ
S
,c
S
,q
S
)
∈
E
S
and
(
q
T
,a,ϕ
T
,c
T
,q
T
)
∈
E
T
this gives rise to
c
T
,
(
q
S
,q
T
))
∈
((
q
S
,q
T
)
,a,ϕ
S
∧
ϕ
T
,c
S
∪
E
.
AnexampleofhowtheconjunctionoftwospecificstatesfromtwodifferentTIOA
withexampleinputandoutputtransitionswilllookisgiveninFigure4.1.
Conjunction mayintroducelocallyinconsistentstates.For example, assume
that
A
S
reachesastatefrom
s
wheretheonlyavailableactionistheoutput
a
and
A
T
reachesastate
t
fromwheretheonlyavailableactionis the output
b
.
Assumealsothat
A
S
and
A
T
cannotdelayin
s
and
t
.In
(
s, t
)
,theconjunction
willnotissueanyoutputandwillnotbeabletodelay,whichviolatesthe
inde-
pendentprogress
property.AsstatedinSection2,locallyinconsistentstatescan
be removedwith the help ofa pruning operation.In the restof the paper,we
assumethateachconjunctionisimmediatelyfollowedbyapruning.
In[12],wehaveshownthefollowingresults:
-
Thesetofimplementationssatisfyingaconjunctionistheintersectionofthe
implementationsetsoftheoperands:
[[ (
A
S
∧
A
T
)]]
mod
= [
A
S
]]
mod
∩
[[
A
T
]]
mod
.
-
Theconjunctionof
A
S
and
A
T
correspondstothegreatestlowerboundof
theirimplementationssets:if
A
A
T
.
-
Theconjunctionoperation(alsoifcombinedwithpruning)isassociativeand
commutative,soamongothers:
[[ (
A
S
∧
≤
A
S
and
A
≤
A
T
wehavethat
A
≤
A
S
∧
A
T
)
∧
A
U
]]
mod
=[
A
S
∧
(
A
T
∧
A
U
)]]
mod
.
4.2 Composition
Weshallnowdefine
structuralcomposition
,alsocalled
parallel composition
,be-
tween specifications. Roughly speaking, this operation computes the classical
product between timed specifications[21], where components synchronise on
common inputs/outputs. Two components are
composable
iff the intersection
between their output alphabets is empty. Formally the
parallel composition
of
A
S
with
A
T
,denoted
A
S
||
A
T
,istheTIOA
A
=(
Loc
,q
0
,
Clk
,E,Act,
Inv
)
given
Loc
T
,
q
0
=(
q
0
,q
0
)
,
Clk
=
Clk
S
by:
Loc
=
Loc
S
×
Clk
T
,
Inv
((
q
S
,q
T
)) =
Inv
(
q
S
)
∧
Inv
(
q
T
)
and the set of actions
Act
=
Act
i
Act
o
is given by
Act
i
=
