Hardware Reference
In-Depth Information
Defns.
2.1.16
and
2.1.17
characterize compositions that do not fall into a deadlock
or a livelock.
When clear from the context, instead of A-
compositionally
we will write more
simply
compositionally
.
2.2
Solution of Equations Over Languages
2.2.1
Language Equations Under Synchronous Composition
Given the alphabets I; U; O, a language A over alphabet I
U and a language C
over alphabet I
O, consider the language equations
A
X
C;
(2.1)
or,
A
X
D
C:
(2.2)
Definition 2.2.1.
Given the alphabets I; U; O, a language A over alphabet I
U
and a language C over alphabet I
O, language B over alphabet U
O is called
a
solution
of the equation A
X
C iff A
B
C .
Given the alphabets I; U; O, a language A over alphabet I
U and a language
C over alphabet I
O, language B over alphabet U
O is called a
solution
of the
equation A
X
D
C iff A
B
D
C .
A solution is called the
largest solution
if it contains any other solution. B
D;
is the trivial solution.
Theo
rem 2
.12.
The largest solution of the equation
A
X
C
is the language
S
D
A
C
.
If
A
A
C
D
S
then
A
C
is the largest solution of the equation
A
X
D
C
.
O/
?
;then˛ is in the largest solution of
Proof.
Consider a string ˛
2
.U
A
X
C iff A
f
˛
g
C and the following chain of equivalences follows:
A
f
˛
g
C
,
.A
"
O
\f
˛
g
"
I
/
#
I
O
\
C
D;,
by
Prop
:2:1.a/C
D
.C
"
U
/
#
I
O
.A
"
O
\f
˛
g
"
I
/
#
I
O
\
.C
"
U
/
#
I
O
D;,
by
Prop
:2:3.d/
since
..C
"
U
/
#
I
O
/
"
U
D
C
"
U
.A
"
O
\f
˛
g
"
I
\
C
"
U
/
#
I
O
D;,
by
Prop
:2:7.b/
A
"
O
\f
˛
g
"
I
\
C
"
U
D;,
by
Prop
:2:7.b/
Search WWH ::
Custom Search