Comple e s a e encoding based
on
he heo y
o
egions
Jo di Co adella* Michael Kishine sky Alex Kond a ye
The Uni e si y
o
Aizu
Ca alunya,
08071
Aizu- Wakama su, Aizu-Wakama su,
Ba celona, Spain 965-80 Japan 965-80 Japan
Uni e si a Poli hcnica de The Uni e si y
o
Aizu
Lucian0 La agnoj Alex Yako le s
Poli ecnico di
To ino
10129 To ino, I aly Uni e si y
o
Newcas le upon Tyne
NE1
7RU
England
Abs ac
Syn hesis o asynch onous ci cui s om Signal
T ansi ion G aphs
in ol es sol ing
example
o
such p oblems is ha o Comple e S a e
,
which happens when
a
pai
o
di le en
has he same bina y encoding.
A
sian-
da d way o app oach s a e coding con lic s is o
add
new s a e signals in o he o iginal speci ica ion in such
a
way ha he o iginal beha iou emains in ac . Ex-
is ing me hods ha e no
ye
been
able
o p o ide such
heo e ical ounda ion
o
e en inse ion, ha could
yield e icien p ac ical esul s when applied o
la ge
models.
This
pape
aims
a
p esen ing such
a
gene al ame-
wo k, which is based on wo undamen al concep s.
One is
a
egion
o s a es in an abs ac labelled
SG
(called
a
T ansi ion Sys em
.
Regions co espond
o
places in he associa ed
STd!
The second concep
is
a
speed-independence p ese ing se ,
which is s ongly
ela ed o he implemen abili y
o
he model in logic.
Regions and hei in e sec ions o e “nice” s uc-
u al p ope ies ha make hem e icien “cons uc ion
blocks”
o
e en inse ion. The applica ion
o
ou
he-
o y, h ough he so wa e ool
pe i y,
o s a e g aphs
o
la ge size has p o ed
o
be
success ul.
1
In oduc ion
The p oblem o
Comple e S a e Coding
(CSC)
is
a undamen al p oblem in syn hesis o asynch onous
con ol ci cui s om Signal T ansi ion G aphs
(STGs)
and S a e G aphs
(SGs
[2]. This p oblem a ises when
a pai o seman ically di e en s a es in an
SG
has he
same bina y encoding. Such s a es a e said o be in
CSC
con lic .
To esol e
CSC
con lic s, he syn hesis
*This
wo k
has been pa ly suppo ed by he Minis y
o
Educa ion
o
Spain (CICYT TIC 95-0419).
This
wo k
has been pa ly suppo ed by EPSRC g an
GR/
J78334.
This
wo k
has been pa ly suppo ed by
he
U.K.
SERC
GR/J72486
and by MURST esea ch p ojec
“VLSI
a chi ec u es”.
§This
wo k
has been pa ly suppo ed by he
U.K.
SERC
GR/ J52327.
p ocedu e mus inse one o mo e new signals in o he
STG
(o
SG)
speci ica ion. The alue o hese new sig-
nals ha e o be di e en in all pai s o s a es in ol ed
in a
CSC
con lic . S a e signal inse ion mus usually
sa is y a se
o
impo an equi emen s: p ese ing
equi alence o he speci ica ions and implemen abili y
o he new and he o iginal non-inpu signals wi hou
haza ds (speed-independence p ese a ion). The o -
me equi emen e e s o he language gene a ed by
he
STG.
The la e implies ha he implemen abili y
condi ions (de e minism, commu a i i y, pe sis ency,
deadlock- eedom and consis ency) mus be p ese ed
in he ans o med speci ica ion.
Rela ed
Wo k.
A
numbe o me hods o sol ing
he
CSC
p oblem a e known o da e
[6,
8,
9,
10,
13,
14,
15,
18, 22,
23,
24, 26,
27,
301. Repo ed ex-
pe imen al esul s and ou own expe ience wi h he
a ailable ools o sol ing
CSC
ensu ed he au ho s
o his pape ha none o he published me hods ap-
pea s o be success ul when applied o gene al
SGs
o
STGs
wi h mo e han a ew housand s a es. Me h-
ods om
[13,
15,
18,
22,
24, 271 wo k a he
STG
le el
wi hou doing s a e a e sal. They allow o a oid
s a e explosion and he e o e can p ocess la ge speci-
ica ions i some addi ional cons ain s on an
STG
a e
gi en. Such cons ain s (no choice is allowed, o ex-
ac ly one ising and alling ansi ion €o each signal is
allowed, e c.) se e ely limi he design space and do
no allow o ge a solu ion o many p ac ical speci ica-
ions. [14] sol es
CSC
p oblem by mapping an ini ial
SG
in o a low able syn hesis p oblem and hen using
classical low able minimiza ion and s a e assignmen
me hods. This me hod
is
es ic ed wi h li e and sa e
ee-choice
STGs
and
canno p ocess la ge
SGs
due o
limi a ions o classical s a e assignmen me hods.
In [23,
261
a
e y gene al amewo k o s a e
as-
signmen is p esen ed. The
CSC
p oblem is o mula ed
as
s a e a iable assignmen on he s a e g aph. The
co ec ness condi ions o such assignmen a e o mu-
la ed as a se o Boolean cons ain s. The solu ion
can be ound using a Boolean sa is iabili y
sol e .
Un-
o una ely, his app oach allows o handle only ela-
i ely small speci ica ions (hund eds o s a es) because
0-8186-7298-6/96
$5.00
0
1996
IEEE
36
he compu a ional complexi y o his me hod is dou-
ble exponen ial om he numbe o signals in he
SG.
Al hough
[6]
p esen ed a me hod o imp o e he es-
olu ion
o
he me hod based on a p elimina y decom-
posi ion o he sa is iabili y p oblem, decomposi ion
may p oduce sub-op imal solu ions due o he loss o
in o ma ion incu ed du ing he pa i ioning p ocess.
Mo eo e , he ne con ac ion p ocedu e used o de-
compose he p oblem has ne e been o mally de ined
o non- ee-choice
STGs.
In
[8,
9,
IO]
ano he me hod based on s a e signals
inse ion a he
SG
le el was gi en. A i s he exci-
a ion egions a e dis inguished in he
SG.
These a e
se s o s a es, which co espond o ansi ions o
STG.
Then he g aph o CSC-con lic s be ween exci a ion e-
gions is cons uc ed and colo ed wi h bina y encoded
colo s. Each bi o his code co esponds o a new
s a e signal. A e ha new s a e signals a e inse ed
in o he
SG
using exci a ion egions o he o iginal
o
p e iously inse ed signals. The main d awback o his
app oach was i s limi a ion o
STGs
wi hou choices.
The me hod desc ibed in de ail in
[29, 301
is p oba-
bly he mos e icien and gene al published
so
a . I
is based on pa i ioning o he s a e space in o blocks
which con ain no in e nal CSC-con lic s. Simila o
[9]
a
colo ing p ocedu e is used o ind he op imal
numbe o s a e signals o esol e all he CSC-con lic s
be ween blocks o pa i ioning. Each o hese s a e
signals can be inse ed using
as
exci a ion egion he
se s o s a es ha immedia ely ollow exci a ion e-
gions (swi ching egions).
Con ibu ion
o
his
pape .
This pape p o ides
a gene al heo e ical amewo k o inse ion-based
esolu ion o coding con lic s. The ans o ma ions de-
sc ibed he e a e applied o abs ac
SGs,
called T an-
si ion Sys ems
(TSs
and o bina y encoded
SGs.
This
o con lic s be ween s a es o be esol ed, he e o e i s
applica ion o
CSC
con lic s is only
a
special case. An-
o he applica ion o he me hod may be, e.g., sol ing
Mono onous Co e con lic s
[12],
o echnology map-
ping o asynch onous ci cui s in he basis
o
simple
ga es
(AND,
OR,
NAND, NOR).
I
is essen ial ha he heo y p esen ed in his pa-
pe is based on he concep o
egions
in a
TS.
I
ende s an e icien amewo k o such ans o ma-
ions due o he wo ollowing majo easons. Fi s ly,
egions a e subse s o s a es which ha e a uni o m
“c ossing” (exi -en y) ela ionship wi h e en s in a
TS
(see Sec ion
3).
They can be easily manipula ed in
in e sec ions and unions, hus p o iding a good le el
o
g anula i y in sec ioning he
TS
( o example he
exci a ion and swi ching egions a e ob ained
as
in-
e sec ion o p e- and pos - egions o he same ansi-
ion). Secondly, egions in a
TS
di ec ly co espond o
places in an
STG
wi h a eachabili y g aph isomo phic
o he
TS.
This allows econs uc ing an
STG
o he
TS
wi h all CSC con lic s esol ed
-
an op ion much
mo e sui able
o
he designe han iewing he
TS.
The concep o egions
was
i s ly p esen ed in
[17]
and u he applied o e icien gene a ion o Pe i Ne s
amewo k
is
aime
d
a being independen o he so
and Signal T ansi ion G aphs om s a e-based mod-
els
[4].
The p ac ical implemen a ion
o
ou me hod,
which is only b ie ly ou lined in his pape ( hose de-
ails equi e a sepa a e p esen a ion), uses symbolic
BDD ep esen a ion o he main objec s in he inse -
ion p ocedu e. I has enabled us o sol e CSC p ob-
lem o s a e g aphs wi h hund eds o housands o
s a es while he quali y o he solu ions ob ained o
smalle s a e g aphs has been qui e compa able wi h
o he known me hods.
Ou me hod di e s om p e ious wo k
as
ollows:
0
Ou echnique o s a e signal inse ion is mo e
gene al and allows o explo e mo e solu ions han
ha o
[29]
and
[30],
since ou me hod uses e-
gions, hei in e sec ions and unions o in e sec-
ions o inse ion. On he o he hand,
[29]
and
[30]
used exci a ion egions and swi ching egions,
which a e jus pa icula cases o egion in e -
sec ions. E en hough he au ho s o hose pa-
pe s admi ed ha in e sec ions and unions o
in e sec ions o exci a ion and swi ching egions
“could” be used o inse ion, hey claimed ha
“ his does no seem necessa y in p ac ice”, and
did no p o ide any me hod
o
educing he com-
plexi y o he esul ing huge sea ch space.
The no ion o speed-independence p ese ing se
(SIP-se ) by which he inse ion o s a e sig-
nals can be. done wi hou iola ion o speed-
independence p ope ies is gene alized in compa -
ison o
[26],
as will be shown in de ail when dis-
cussing Theo em
4.1.
e
Ou me hod is p o en o be comple e o a ai ly
gene al class o
SGs.
An addi ional ad an age o he heo y p esen ed
in his pape is back-anno a ion a he
STG
le el.
The esul o CSC esolu ion is shown o he use
as a modi ied
STG,
so
ha he impac o s a e
signal inse ion on, e.g., he concu ency o he
speci ica ion, can be mo e easily analyzed.
F om he p ac ical side we obse ed ha al hough
he ool
assassin
[28]
which implemen s me hods
om
[24, 26,
301
o en allows be e solu ions han
o he p e iously known ools,
i
has di icul ies in han-
dling la ge speci ica ions.
Fo
example, a
mas e - ead
STG
wi h
8932
s a es an o mo e han
24
hou s
o
CPU ime a SPARC-10 machine wi hou ha ing
sol ed CSC. Ou ool
pe i y
sol ed his example in
15
min o CPU ime. We also sol ed examples wi h
10l1
s a es using a ew hou s o CPU ime. I is wo h
o men ion ha on he basis
o
he egion app oach
pe i y
succeeded in handling examples ha we e
adi ionally di icul o
CSC
solu ion by any o he
ool (see Sec ion
8
o mo e de ails).
The pape is u he o ganized as ollows. Sec ion
2
in oduces bo h s a e-based and e en -based models.
Sec ion
3
p esen s he basics o he heo y o egions.
Sec ion
4
is dedica ed o p ope y-p ese ing e en in-
se ion,
which
uses
he
no ion
o
speed-independence-
p ese ing se s (SIP-se s) o s a es. Sec ion
5
discusses
37
he issue o selec ion o SIP-se s, based on egions.
Sec ion
6
applies he e en inse ion echnique o bi-
na y encoded
TSs.
Sec ion
7
cha ac e izes he
se
o
STGs
o which
CSC
can be sol ed using he p oposed
me hod. Sec ion
8
ou lines some expe imen al esul s.
Finally, Sec ion
9
d aws conclusions.
2
S a e and E en
models
T ansi ion sys ems.
A
ansi ion sys em
(TS)
migh be iewed
as
an abs ac s a e g aph and is
o -
mally de ined as a quad uple [17]
A
=
(S,E,T,si,,),
whe e
S
is a
ini e non-emp y
se
o
s a es,
E
is a se
o
e en s,
T
c
S
x
E
x
S
is a
ansi ion
ela ion, and
Sin
is an
ini ial s a e.
The elemen s o
T
a e called he
ansi ions
o
TS
and will be o en deno ed by
s
5
s’
ins ead o
(s,
e,
s’).
The
eachabili y ela ion
be ween s a es is he an-
si i e closu e
o
he ansi ion ela ion
T.
A
easible
sequence
is a (possibly emp y) sequence o ansi ions
U
be ween s a es
s
and
SI
(deno ed by
s
5
s’
o
sim-
ply by
s
si.)
A
easible ace
is ob ained om a
easible sequence by emo ing s a es.
I
s1
3
s2,
s2
4
s3, s3
3
s4
is
a easible sequence, hen
el,
e2,
e3
is he
co esponding easible ace. We also w i e
s
5,
5
s‘,
and
s
5,
4
s
i
s
-5
s’
o
s
-41,
SI,
co espondingly.
No e ha each s a e
is
eachable om i sel . A s a e
o a
TS
is called a
deadlock
i he e is no e en
e
E
E
such ha
s
$.
Fu he mo e, a TS mus sa is y he ollowing ou
basic axioms:
No
sel -loops,
No
mul iple a cs be ween a pai o s a es,
E e y e en has an occu ence,
E e y s a e is eachable om he ini ial s a e.
s a e
=
c ,b,c,d>
(a)
@)
(e)
Figu e
1:
An example
o
T ansi ion Sys em (a), he
co esponding
SG
(b),
and
STG
(c)
A
TS
is called
de e minis ic
i o each s a e
s
and
each label
a
he e can be a mos one s a e
s’
such ha
s
5
SI.
O he wise, a
TS
is called
nonde e minis ic.
In he ollowing we a e in e es ed only in de e minis ic
TSs.
An example o a de e minis ic
TS
is shown in
Figu e 1,a.
S a e
G aph.
Fo
he pu pose o logic syn hesis
TSs
mus be bina y encoded. A
s a e g aph,
SG,
is
a bina y
encoded
TS.
A
SG
is gi en by
(A,X,
As,
AE),
whe e
signals, and
XO
is he se o
ou pu
signals1, such ha
Each s a e
s
E
S
in he
SG
is labelled wi h a
bi-
na y ec o
(s(l),
.(a),
.
. .
,
s(n))
acco ding o he sig-
nals
X
=
(21,
z2,.
. .
,x,}
o he sys em. The labeling
is gi en by a
s a e assignmen unc ion
AS
:
S
x
X
cs
{0,1}.
Fo a gi en s a e
s
E
S,
s(i
deno es he i- h
xi
EX.
Each e en
e
E
E
in he
SG
is labelled wi h a
signal
ansi ion.
The labeling is gi en by an
e en assign-
men unc ion
AE
:
E
H
X
x
{+,
-}.
Each signal
ansi ion can be ep esen ed as
za+
o
za-
o
he
ising
(0
.--i
1)
o
alling
(1
---$
0)
ansi ion o signal
i.
zi*
is used
o
depic ei he a
“2i+”
ansi ion
o
a
“ii-”
ansi ion. Fu he , i no con usion a ises,
we will deno e di e en signal names by di e en le -
e s
a,
b,
.
. .
ins ead o
zl,
22,.
. .
Also,
(s,
zi*,
s’)
E
T
s ands o
(s,
e,
s’)
E
T
A
AE(e)
=
$a*.
An
SG
has a
consis en s a e assignmen
(we call
such an
SG
consis en ) i he ollowing condi ions o
assignmen unc ions a e me : le
(s,
e,
s’)
E
T
hen
(1)
i
AE(e)
=
zi+,
hen
s(i)
=
0
and
s’(i)
=
1;
(2)
i .AE(e)
=
zi-,
hen
s(i)
=
1
and
s‘(i)
=
0;
(3)
in all o he cases
s(i)
=
s’(i).
Consis en s a e assignmen is a necessa y condi-
ion o de i ing logic unc ions o signals encoding a
SG
[2]. Figu e 1,b shows a consis en
SG
which is ob-
ained by bina y encoding o he
TS
om Figu e 1,a.
A e bina y encoding, o example, e en
c
is mapped
in o signal ansi ion
b-
and s a e
sl
is mapped in o
bina y code
<
a,
b,
c,
d
>=
0010.
is a ansi ion sys em,
X
=
XI
U
ina y signals,
XI
is
he se o
inpu
xInxo
=O.
componen
o
s
co esponding o
h
e alue o signal
Comple e
S a e
Coding.
An unambiguous s a e
assignmen is equi ed o de i ing logic o encoding
bina y signals. Logic mus be de i ed only o ou pu
signals and he e o e he unambiguous s a e assign-
men mus conce n only ou pu signals. This equi e-
men is called
Comple e S a e
Coding
(CSC,
[2]):
A
SG
is said
o
sa is y he Comple e S a e Codang
equi emen
i
o any wo s a es
sl
and
s2
which a e
assigned he same bina y ec o s he se s
o
enabled
ou pu signals a e iden ical.
Le
a
and
b
be ou pu and
c
and
d
be inpu signals
o he
SG
in Figu e 1,b. S a es
SO
and
s2
ha e he
same bina y code 0110. Ou pu signal
b
is enabled in
nal
signals
o
he modeled ci cui .
’The ou pu signals include
bo h
ex e nal ou pu
and
in e -
38
sl
and is no enabled in
s2,
he e o e
CSC
is iola ed
and we say ha s a es
SO
and
92
a e in
CSC
con lic .
Al hough s a es
s5
and
s7
a e also assigned he same
bina y code
1111,
hey a e no in
CSC
con lic , since
no ou pu signals a e enabled in
s5
and
s7.
Pe i Ne s
and
Signal T ansi ion
G aphs.
A
Pe i Ne is o en
a
mo e compac model o ep esen
sys ems wi h concu ency han
a
TS.
A Pe i Ne
[20]
is
a
quad uple
N
=
(P,
T,
F,
mo),
whe e
P
is a
ini e
se o places,
T
is a
ini e
se o
ansi ions,
F
C
(P
x
T)
U
T
x
P)
is he low ela ion,
is enabled a ma king
ml
i all i s inpu places a e
ma ked. An enabled ansi ion
may i e, p oducing
a new ma king
m2
wi h one less oken in each inpu
place and one mo e oken-in each ou pu place
(ml
4
m2).
The se s o inpu and ou pu places o ansi ion
a e deno ed by
o
and
o.
The Reachabili y G aph
(RG)
o
a
PN
is
a
g aph
wi h:
a
e ex o each eachable ma king o he
PN
and
0
an a c
(ml,
mz)
i and only i
ml
+
m2
in some
A ne is called
sa e
i no mo e han one oken can
appea in
a
place. Sa e ne s a e used in many applica-
ions, since hey ha e simple e i ica ion algo i hms
[5]
and simple seman ics. A
labeled
PN
is a
PN
wi h
a
labeling unc ion
X
:
T
-+
A
which pu s in o co e-
spondence e e y ansi ion o he ne wi h
a
symbol
(called label) om he alphabe
A.
A
Signal T an-
si ion G aph
(STG)
is
a
PN
whose ansi ions a e la-
belled wi h signal ansi ions
(a+,
a-,
...).
Places
wi h one inpu and one ou pu ansi ion a e called
implici places and a e depic ed
as
an a c connec ing
hese wo ansi ions. An
STG
exp essing he same
beha io as he
SG
om Figu e 1,b is shown in Fig-
u e 1,c.
3
In his sec ion we will b ie ly e iew he heo y o
egions and will show how his heo y allows o pe -
o m ans o ma ions be ween
TSs
and
PNs
(hence,
be ween
SGs
and
STGs).
and
mo
is he ini ial ma
k
ing.
A
ansi ion
E
T
i ing sequence o he
PN.
Basics
o
he heo y
o
egions
Regions.
Regions a e se s o s a es which co e-
spond o places in Pe i Ne s. Le
S1
be
a
subse o
he s a es o
a
TS,
SI
&
S.
I s
S1
and
s'
E
SI,
hen
we say ha ansi ion
s
-%
s'
en e s
SI.
I s
E
S1
and
s'
SI,
hen ansi ion
s
5
s'
exi s
SI.
O he wise,
ansi ion
s
5
s'
does no c oss
5'1.
In pa icula , i
s
E
SI
and
s'
E
SI,
hen he ansi ion is said o be
in e nal
o
SI,
and i
s
#
SI
and
s'
$!
SI,
hen he
ansi ion is
ex e nal
o
SI.
A
subse o s a es,
,
is a
egion
i o each e en
e
exac ly
one
o he ollowing condi ions holds: all
ansi ions labelled wi h
e
(1) exi
,
(2)
en e
,
o
(3)
do no c oss
.
Le
us
conside he
TS
shown in Figu e
1,a.
The
se o s a es
1
=
{
s5,
se,
sg}
is
a
egion, since all an-
si ions labeled wi h
a
and wi h
d
exi
l,
and all an-
si ions labeled wi h
b
and wi h
g
en e
1.
On he
o he hand,
{sg,sg}
is
no
a
egion since ansi ion
sg
5
SO
exi s his se , while ano he ansi ion also
labeled wi h
a
sg
5
s4,
does no .
Le
and
'
be egions o
a
TS.
A
egion
'
is said
o be
a
sub egion
o
i
'
C
.
A egion
'
is
a
minimal
egion
i
'
is no
a
sub egion o
any
o he
egion o he
TS.
A egion
is a
p e- egion
o
e en
e
i he e is a ansi ion labeled wi h
e
which exi s
.
A
egion
is
a
pos - egion
o e en
e
i he e is
a
ansi ion labeled wi h
e
which en e s
.
The se o
all p e- egions and pos - egions
o
e
is deno ed wi h
'e
and
eo
espec i ely. By de ini ion
i
ollows ha
i
E
Oe,
hen all ansi ions labeled wi h
e
exi
.
Simila ly, i
E
eo,
hen all ansi ions labeled wi h
e
en e
.
The e a e wo p e- egions o e en
a
in
Figu e
1:
1
=
{S~,SS,S~}
and
2
=
{sg,s7,sg}.
Bo h
o hem a!e minimal egions, since no subse o
1
o
2
is
a
egion.
The ollowing p oposi ions s a e
a
ew impo an
p ope ies o egions
[l,
4,
171.
P ope y
3.1
1.
I
and
'
a e wo di e en egions such ha
l
is a sub egion
o
,
hen
T
-
'
is a egion.
2.
A
se
o
s a es
is a egion i and only i
i s
cose
P
=
S- is a egion, whe e
S
is
Q
se
o
all s a es
o
he
TS.
3.
E e y egion can be ep esen ed as
a
union
o
dis-
join minimal egions.
Exci a ion egions.
While egions in a
TS
a e e-
la ed o places in he co esponding
PN,
an exci a ion
egion
191
o e en
a
is
a
maximal se o s a es in which
ansi ion
a
is enabled. The e o e, exci a ion egions
a e ela ed o ansi ions o he
PN.
A
se o s a es
S1
is called a
gene alized exci a ion
egion
an
exci a ion egion)
o
e en
a,
deno ed by
GER(a
(by
ERj(a)),
i i is
a
maximal
(a
maximal
connec ed)
se o s a es such ha
o
e e y s a e
s
E
SI
he e is
a
ansi ion
s
%.
The
GER
o
a
is he union
o all
ERs
o
a.
In he
TS
om Figu e
1,a
he e a e
wo exci a ion egions o e en
a: ER1
a)
=
{sg}
and
.
The co esponding
G
L
R
o
e en
a
De i ing Pe i Ne s
om
T ansi ion Sys ems.
The p ocedu e o syn hesize
a
PN
om an elemen a y
TS
is as ollows:
Fo
each e en
a
a
ansi ion labeled wi h
a
is
gene a ed in he
PN;
0
Fo
each minimal egion
i
a
place
pi
is gene a ed;
Place
pi
con ains
a
oken
in
he
ini ial
ma king
mo
i
sin
E
j;
39
The low ela ion is
as
ollows:
a
E
pp
i
i
is a
p e- egion o
a
and
a
E
bpi
i
j
is a pos - egion
o
a.
This p ocedu e allows o ob ain a sa e
PN
wi h a
RG
isomo phic o he ini ial
TS
o
o i s minimized
e sion i he ini ial
TS
is
elemen a y
[17].
As
shown
in
[4]
elemen a i y o minimal
TS
can be de ined by
he ollowing wo condi ions.
b
Exci a ion closu e.
Fo
each e en
a:
n,.,
oa
=
GER(a);
b
E en e ec i eness.
FQ
each e en
a:
GER(a)
#
8;
As
shown in Figu e
1,
egion
1
is mapped in o place
TI
o he
STG.
I a
TS
is no elemen a y, hen i is always possible
o ans o m i o an elemen a y one by label spli -
ing (one label
a
which causes iola ions o elemen-
a i y is subs i u ed in he
TS
by a ew independen
labels
al,
a2,
. .
.)
o
by inse ing dummy ansi ions.
The e o e, o any
TS
an equi alen sa e
PN
can be
syn hesized.
4
Cons ained ans o ma ions o
TSs
In his sec ion we desc ibe cons ained ans o ma-
ions o
TSs
which p ese e equi alence and o he im-
po an p ope ies. In pa icula , we o malize he no-
ion o beha io al equi alence o
TSs,
and we de ine
speed-independence.
Speed-Independen T ansi ion Sys ems.
A
de-
sign is speed-independen i i s beha io does no de-
pend on he speed o i s componen s (ga es).
As
shown
in
[7],
wo p ope ies ensu e ha a de e minis ic
TS
allows o a speed-independen implemen a ion:
pe -
sis ency
and
commu a i i y.
The pe sis ency p ope y
s a es ha no e en can be disabled by any o he
e en . The commu a i i y p ope y gua an ees ha
he same s a e o he
TS
is eached unde any o de
o enabled e en i ing.
De ini ion
4.1
(E en pe sis ency)
Le
A
=
(S,
E,T)
be
a
ansi ion sys em. An e en
a
E
E
as
said o
be
pe sis en in
C
S
i :
Vsl
E
:
[sl
5
A
(sl
A
s2)
ET]
=j
s2
-%
An e en
a
E
E
2s
saad
o
be
pe sis en
i
a
as
pe -
sis en
$12
S.
De ini ion
4.2
(Commu a i i y)
A
ansi ion
sys em
A
is
called
commu a i e i
o
any aces
ab
and
ba
ha a e easible om some s a e
SI
E
S
bo h
uces
lead
o he same s a e, i.e., i
sl
-%
s2, s2
-+
s4
and
sl
+
s3,
$3
%
s5
hen
s4
=
s5.
b
b
T ace equi alence.
The se o easible aces o a
TS
A
is called he
language
accep ed by
A
and is de-
no ed
as
L(A).
I
p
is a easible ace o
A,
hen i s
p ojec ion on a subse o e en s
E1
C
E,
deno ed
as
p
J.
El,
is a sequence o e en s
p‘
ob ained om
p
by
dele ing all e en s om
E
-
El.
I
L(A)
is he lan-
guage accep ed by
A,
hen i s p ojec ion
L(A)
1
El
is
he se o sequences
{p
1
El
:
p
E
L(A)}.
Le
A’
=
(S‘,
E‘,
TI)
and
A
=
(S,
E,T)
be wo
TSs
such ha
E
c
E’.
Then,
TSs
A
and
A’
a e
ace equi alen
i
L(A’)
1
E
=
L(A).
Addi ionally
o ace equi alence, he ollowing p ope ies mus be
p ese ed a e ans o ming a
TS:
pe sis ency, com-
mu a i i y, de e minism, and deadlock eedom. The
i s h ee p ope ies gua an ee ha he new
TS
al-
lows o a speed-independen implemen a ion. The
la e p ope y gua an ees ha li eness o he ini ial
TS
is p ese ed. I is de ined
as
ollows: i s a e
s’
is a
deadlock in
A’
and is eachable om he ini ial s a e
si,,
by a easible ace
p’,
hen s a e
s
o he o iginal
TS
eachable om
sin
by a easible ace
p
=
p’
j.
E
is
a
deadlock in
A.
E en inse ion.
The basic ans o ma ion is he
inse ion
o
a
single e en
in o a
TS.
The e can be
di e en schemes o e en inse ion ha p ese e ace
equi alence
[3].
In his pape we will ely on a simple
one which consis s o wo s eps and is simila o
[9,
26,
301
:
Choosing in he o iginal
TS
a se o s a es
in
which he new e en
x
will be enabled.
co e-
sponds o a gene alized exci a ion egion o e en
x
in he new
TS
and he e o e is deno ed
as
ER(x)
in Figu e
2.
un il e en
x
i es.
0
Delaying all ansi ions ha exi he se o s a es
De ini ion
4.3
(E en inse ion)
Le A
=
(S,
E,T)
be
a
ansi ion sys em and
x
4
E
be
a
new e en . Assume ha
C
S
is an a bi a
y
subse
o
s a es. Le
‘,
‘nS
=
0,
be
a
se
o
new s a es such
ha o each
s
E
he e is one s a e
s’
E
’
and ace
e sa. The inse ion o
x
in
A
by
p oduces ano he
ansi ion sys em
A’
=
(S‘,
E’,
TI)
de ined as ollows:
S’
=
S
U
’
E‘
=
EU
{x}
T’
=
TU
{(s
5
s’)Is
E
A
s’
E
’}U
{(sl’
-%
s2’)(sl,
s2
E
T
A
(sl
5
s2)
E
T}U
{(SI’
5
s2)lsl
E
A
s2
{(SI
Z
s2)lsl
E
A
s2
6
}
A
(SI
5
s2)
E
T}-
By De ini ion
4.3
ans o ming
A
o
A’
ia adding
he new e en
x
by a se o s a es
leads o spli in
all s a es
s
E
in
S
in o wo s a es
s
and
s‘
in
SI.
AB
o he s a es
s
6
a e in co espondence wi h only one
s a e in
SI.
Figu e
2
illus a es how e en inse ion is
pe o med.
40

S-ER(x) S-ER(x)
Figu e 2: Inse ion o e en
x
om
ER(x)
Speed-independence p ese ing se s.
I is easy
o show ha he inse ion o e en
2
by De ini ion 4.3
always p ese es ace equi alence, de e minism and
deadlock- eedom
[3]. Pe sis ency and commu a i i y,
on
he o he hand, a e no au oma ically p ese ed,
and need a mo e ca e ul analysis.
De ini ion
4.4
(SIP-se )
Le
A
=
(S,
E,T)
be
a
ansi ion sys em, x
e
E
be
a
new e en and
E
S.
Le
A‘
=
(S’,
E’,T’)
be
a
ansi ion sys em ob ained
a e inse ing x
by
.
is said o
be
a
speed-
independence p ese ing se (SIP-se )
i :
1.
Va
E
E
:
a
is pe sis en in
A
=$-
a
is
pe sis en in
A’
2.
A
is commu a i e
I
sa is ies only condi ion
1
hen
is
a
pe sis ency
p ese ing
se .
The ollowing heo em de e mines wo condi ions o
p ese ing pe sis ency and commu a i i y.
A’
is commu a i e
A’:
s4
Y
s4
s3’
s2’
bQ
s4
(b)
Figu e 3: Se
o
s a es
is no pe sis ency p ese ing.
Theo em
4.1
Le
A
=
(S,
E,”)
be
a
TS
and
C
S
a
subse
o
s a es.
is
a
pe sis ency-p ese ing se
i
[(sl
5
s3),(s2
5
s4),(sl
5
$2)
E
T
A
s2
E
Le
A
=
(S,
E,
T)
be
a
commu a i e ansi ion
sys-
em and
c
S
be
a
pe sis ency p ese ing se . Then
is
a
SIP-se i :
,s4# ]
a
slE
A
s39
(1)
b
b
sl
s2, s2
--$
$4,
sl
+
s3, s3
5
s4
E
TA
This heo em e ines condi ions
o
speed-indepen-
dence om [23]. I allows o handle co ec ly he
so
called asymme ic “ ake” con lic s be ween signals
(kl]).
Conside , o example, Figu e 3.(a), whe e
e e is no a c be ween s3 and
s4.
On he o he hand,
SIP condi ions we e de ined in [23] only wi h espec
o comple e diamonds o s a es. Hence, he condi ions
s a ed in [23] a e no su icien o ind he iola ion
o
pe sis ency in cases like ha
o
Figu e 3,a.
Figu e 3 shows wo possible cases o iola ion o
he pe sis ency p ese ing condi ion
(1)
om Theo-
em 4.1. In bo h cases e en
b
becomes non-pe sis en .
No e ha e en
x
is pe sis en by cons uc ion in he
TS
ob ained a e he inse ion. Hence, i a pe sis-
ency p ese ing se is used o signal inse ion, hen
no new non-pe sis encies can a ise.
(sl,
s2
E
A
s3
$2
)
s4
#
(2)
s4’
Figu e
4:
Commu a i i y iola ion a e signal inse -
ion
Figu e 4 shows a iola ion o commu a i i y when
a se o s a es
does no mee condi ion (2) o Theo-
em
4.1.
Figu e
5
shows allowable co ec in e sec ions
o a SIP-se wi h all s a e diamonds in a
SG.
5
Selec ing
SIP-se s
This sec ion p esen s a ew basic p ope ies which al-
low
us
o o mula e imp o ed s a egies o selec ion
o SIP-se s. In 123, 26 SIP-se s a e
selec ed
by sol -
he sea ch space o SIP-se s is p oblema ic since in
he educ ion o he sa is iabili y p oblem each s a e
in
SG
is conside ed sepa a ely (i is encoded by wo
bina y signals) ha quickly leads o unmanageable
complexi y when sol ing he sa is iabili y ins ance.
In
[8,
9,
101
SIP-se s a e
cons uc ed
om exci a ion
egions
o
he o iginal signals and p e iously in o-
duced s a e signals. [30] gene alized his me hod in
such way ha bo h ERs and swi ching egions
(SRS)
a e used o SIP-se s. In his pape we u he gen-
e alize his me hod: SIP-se s a e
cons uc ed
as
e-
gions, hei in e sec ions and union
o
in e sec ions.
We will show below ha e ions ensu e o
au oma i-
cally
ind alid SIP-se s, a %e han checking
o
SIP
a
pos e io i,
which is conside ably less e icien . No e
ha Eh and
SRs
a e pa icula cases o egion in-
e sec ions.
The e o e,
ou
me hod allows o explo e
a la ge sea ch space o SIP-se s and o ind mo e
e icien solu ions.
ing a sa is iabili y p o
lb
lem. E icien ly cons aining
41
sl
2
ySia
AA2
s3
s4
s4
Figu e 5: SIP-se s o a s a e diamond
P ope y
5.1
I
is
a
egion in
a
commu a i e ele-
men a y ansi ion sys em, hen
is
a
SIP-se .
The p oo
o
his p ope y is i ial. A he
PN
le el his p ope y co esponds o a ollowing s uc-
u al ans o ma ion: place
is subs i u ed by wo
places
and
’
wi h a new in e media e ansi ion la-
belled wi h
x.
Place
has only one ou pu ansi ion,
x,
and all ansi ions which belong o
e
in he ini-
ial
PN
belong o
’o
in he new
PN.
Ob iously, such
ans o ma ions canno iola e pe sis ency
o
commu-
a i i y o any e en .
P ope y
5.2
I
is an exci a ion egion
o
e en
c
in
a
commu a i e ansi ion sys em
A
and
c
is
pe sis-
en in
,
hen
is
a
SIP-se .
In ui i ely, his p ope y can be s a ed
as
ollows:
delaying a pe sis en e en canno c ea e iola ions
o pe sis ency
o
commu a i i y. A he
PN
le el his
means ha subs i u ing a pe sis en ansi ion by a se-
quen ial composi ion o wo ansi ions p ese es pe -
sis ency and commu a i i y. A he ci cui le el his
p ope y co esponds o a well-known ac : inse ing
delays a he ga e ou pu s be o e a wi e o k does no
iola e semi-modula i y
o
he ci cui
[16].
Mos o
he p e ious me hods o
CSC
used a ia ions o p op-
e y 5.2 [2,
9,
14, 23,
301.
De ini ion
5.1
(Exi and inpu bo de )
Le
A
=
(S,
E,T)
be
a
ansi ion sys em. Gi en
a
subse
o
s a es
C
S,
he
exi bo de
o
(deno ed as
EB( ))
and he
inpu bo de
o
(deno ed as
IB( ))
a e
de-
ined as ollows:
EB( )
=
{s
E
13a
E
E,
s’
E
S
:
s
3
s’
E
T
A
s‘
#
)
IB( )
=
(s
E
[3a
E
E,
s’
E
S
:
s’
5
s
E
T
A
s’
g‘
}
Exi bo de s
o
egions and in e sec ion o p e-
egions o he same e en can also be sa ely used
as
SIP-se s unde he ollowing condi ions.
P ope y
5.3
Le
A
=
(S,
E,
T)
be
a
commu a i e
elemen a y ansi ion sys em and le
be
Q
egion in
A.
I all he exi e en s
o
a e pe sis en hen
EB( )
as
a
SIP-se .
P oo :
I Condi ion
1
o a SIP-se is iola ed, hen
s2
E
EB( )
and s4
6
EB( ).
Hence, he e exis s e en
c
such ha
s2
5
s5, s5
$Z
.
Clea ly
c
is an exi e en
o
and om he p ope ies
o
a egion any s a e in
which
c
is enabled belongs o
.
I
c
#
b
hen om
s4
EB( )
ollows ha e en
c,
which
is
enabled
in s2, becomes disabled in
s4.
This con adic s he
assump ion ha all exi e en s o
a e pe sis en .
I
c
=
b
hen sl-belongs o
EB( )
con adic ion
wi h Figu e 3,a) and
93
mus be ou o
I
con adic ion
wi h Figu e 3,b).
2.
Viola ions o Condi ion
2
(Figu e 4). By he
same conside a ion i
c
#
b
hen
c
becomes disabled
in
s3.
I
c
=
b
hen s4 canno be in
EB( ).
0
A se o s a es
S
is called
o wa d connec ed
i o
any pai o s a es
s1
,
s2
E
S
he e is a s a e
s3
E
S
(s3
may coincide wi h
SI
o wi h
s2)
such ha
si
273,
s2
2
s3
and all s a es o
U
and
a1
belong o
S.
P ope y
5.4
Le
A
=
(S, E,T)
be
a
commu a i e
elemen a y ansi ion sys em and le
l,
2
be
p e-
egions
o
he same e en .
I
1
n
2
is
o wa d con-
nec ed and
all
exi e en s
o
ln z
a e pe sis en , hen
1
n
2
4s
a
SIP-se .
P oo :
Assume ha
A
=
(S,
E,
T)
is a commu a i e
elemen a y ansi ion sys em. Assume also ha
1
,
2
a e p e- egions o he same e en
b
E
E,
1
n
7-2
is
o wa d connec ed, and all exi e en s o
1
n
9-2
a e
pe sis en . Le us p o e ha
1
n
2
is a SIP se , i.e.,
l
n
2
is pe sis ency-p ese ing and commu a i i y-
p ese ing.
Assume ha
A’
is
he
TS
ob ained a e inse ing
a new e en
x
by
1
n
2.
We need o p o e ha
pe sis ency and commu a i i y a e p ese ed in
A’.
Pe sis ency
p ese a ion.
(1)
A new e en
x
and all e en s om
E
which
do
no exi
1
n
2
a e pe sis en in
A‘
by cons uc ion.
(2)
Conside e en
b.
Le us e e o condi ion
(1)
om
Theo em 4.1 and Figu e 3. Since
l, 2
E
ob,
all
ansi ions labelled wi h
b
mus exi bo h
1
and
2.
Hence, sl
-+
s3
exi s bo h
1
and
z
and he e o e,
1. Viola ions
o
Condi ion
1
(Figu e
3).
b
b
sl
4
s3
exi s
1
n
2.
Condi ion
sl
E
1
n
2
A
s3
6
1
n
2
is sa is ied and pe sis ency holds by Theo em
4.1.
42
(3)
Conside e en
b’
o he han
b
such ha
b’
exi s
1n 2
bu
l
o
2
a e no p e- egions
o
b’.
T ansi ion
92
5
s4
om condi ion
(1)
o Theo em
4.1
exi s
1
n
2.
Hence,
s2
--+
s4
exi s ei he
1
o
2.
Le us
assume, o example, ha
s2
+
s4 exi s
1.
Then
ansi ion
sl
-+
s3
also exi s
1.
Le
s2
E
GER(b).
Since
b
is pe sis en and
s2
5
94,
s a e
s4
E
GER(b)
and
s2
-%
s4
is in e nal o
GER(b).
In an elemen a y
TS
he in e sec ion o p e- egions
o
he same e en
b
gi es he exci a ion egion o
b.
Hence,
s2
--+
s4
is in e nal o
1
and we ha e eached
a con adic ion.
Le
s2
E
( ln Z)-GER(b).
Since
ln 2
is o wa d
connec ed h ee cases a e possible:
(2)
3s’
E
GER(b)
:
s’
5
s2,
and
(3)
3s’
E
GER(b),
SI’
E
( 1
n
a)
-
GER(b)
:
s2
b’
b’
b’
b’
(1)
3s‘
E
GER(b)
:
~2
Z.
s‘,
A
01
I’
+s.
Le us conside he i s case. E en
b’
is pe sis en
and since
b’
exi s
1,
he ollowing condi ion holds:
6’
U.
The e o e, he e is a s a e
s5
such ha
s‘
---
s5.
Since
s’
E
GER(b)
and
b
is pe sis en he ollowing
holds:
s5
+.
The e o e,
s5
E
GER(b)
and
s’
+
s5
is in e nal o
GER(b)
ansi ion. Hence,
s’
+
s5
is in e nal o
1
and we ha e eached a con adic ion
wi h he assump ion ha
b’
exi s
1.
Le us conside he second case. Since
b
is pe sis-
en ,
1
n
1-2
is o wa d connec ed and bo h
1
and
~2
a e p e- egions o
b,
hen e en
b
$
U.
The e o e,
s a e
s2
E
GER(b)
and bo h
b
and
b’
a e enabled in
62.
Since
b
is pe sis en we may conclude ha ansi ion
s2
+
is in e nal o
GER(b)
and hence is also in e nal
o
7-1.
We again ha e eached a con adic ion.
Le us conside he hi d case. Since
b
is pe sis en ,
1
n
1-2
is
o wa d connec ed and bo h
1
and
2
a e
p e- e ions o
6,
e en
b
is enabled in
s”
which implies
hi d case o he i s case, which has been al eady
conside ed.
Commu a i i y p ese a ion.
Le us e e o
condi ion
(2)
om Theo em
4.1
and Figu e
4.
Gi en
a diamond
sl
5
s2,
s2
-+
s4, 61
s3, s3
s4,
he
commu a i i y p ope y may be iola ed only in one
case: i s a e
s3
$
ln 2
and s a es
sl,
92,
s4
E
ln 2.
In such case ansi ion
sl
A
s3
exi s
n
2
and
he e o e mus exi
1
o
2.
Assume o example
ha
sl
-+
s3 exi s
1.
On he o he hand, ansi-
ion
s2
+
s4
is in e nal
o
l
n
2
and hence does
no exi
1.
We ha e eached a con adic ion wi h he
de ini ion
o
a egion.
0
A
signi ican consequence o hese p ope ies is
ha he good candida es o inse ion can be buil
b’
b
b’
b’
b’
ha
s
$1
E
GER(b).
The e o e, we ha e educed he
b
b
b
b
on he basis
o
egions and hei in e sec ions, since
hey gua an ee o p ese e equi alence and speed-
independence. One
may
also conclude ha SIP-se s
o e en inse ion can be buil e y e icien ly om
egions a he han s a es.
6
T ans o ma ions
o
S a e G aphs
The bina y encoding
o
a
TS
o ob ain an
SG
im-
plies addi ional cons ain s o inse ing new e en s:
each inse ed e en has o be in e p e ed
as
a signal
ansi ion and he e o e consis ency o s a e assign-
men mus be p ese ed. Any e en inse ion scheme
which p ese es ace equi alence (like hose in De i-
ni ion 4.3)
also
p ese es consis ency o he o iginal
signals. Special ca e mus be aken o ensu e consis-
ency
o
he new signals ( ha a e usually called
s a e
signals).
A speci ic class o
SGs
ans o ma ions can be de-
ined
as
ollows:
1.
Inse ion is made by signals no by e en s. The e-
o e, ins ead
o
inse ing a single e en wo signal
ansi ions o a new signal a e inse ed a each
s ep:
z+
and
z-.
Two se s o s a es o inse ion,
GER(z+)
and
GER(z-),
a e de ined simul ane-
ously such ha
GER(z+)
n
GER(z-)
=
0.
2.
Simila o
TSs
ans o ma ions, bo h se s o in-
se ion,
GER(z+)
and
GER(z-),
mus be SIP-
se s. In addi ion, consis ency o s a e assignmen
o signal
x
is equi ed.
Gi en an
SG
wi h a se o bina y s a es
S,
a pa -
i ion o he inse ion o signal
x,
called
I-pa i ion,
is
a pa i ion o
S
in o ou blocks
([25]):
So,
6,
S+
and
S-.
So(S1)
de ines he s a es in which
x
will
ha e he s able alue
0
(1).
S+(S-)
de ines
GER(z+)
Le
A
be
a
consis en
SG
and
le
I
=
{So,
S1,
S+ S-}
be
an I-pa i ion
o
A.
SG
A‘
ob ained
by
inse ing signal
x
by
pa i ion
I
is
consis en
i
he
only
allowed
a cs c ossing bounda ies
o
he pa i ion
blocks a e he ollowing:
So
+.
S+
--+
S1
+
S-
--i
So,
S+
+
S-
and
S-
-+
S+,
S+
-+
So
and
S-
--.*
S1.
A cs like hose shown in Figu e
6
a e o bidden.
The p oo
o
his p ope y i ially ollows om he
ules o inse ion o e en s
z+
and
z-
(see De ini ion
(GER(
z-)).
4.3).
SO
I
h
J,
S’
Figu e
6:
Illegal ansi ions in an I-pa i ion
An I-pa i ion can be ound in wo s eps:
43
0
Find
a
bipa i ion
{b,
b},
(6
=
S
-
b)
o
S.
The
alue o signal
2
is cons an inside blocks
b
and
6.
0
Choose
GER(x+)
and
GER(x-)
a he bound-
a ies o blocks
b
and
5
espec i ely.
The bounda ies migh be de ined in wo ways:
as
exi bo de s
o
as inpu bo de s. Figu e 7,a shows
inse ion by exi bo de s: gi en a bipa i ion
(b,&},
GER(z+)
=
EB(b)
and
GER(x-)
=
EB(5)
(o
ice e sa). Figu e 7,b illus a es inse ion by in-
pu bo de s. In his case
GER(x+)
=
IB(b)
and
GER(x-)
=
IB(6)
(o
ice e sa).
/
x=l
/
x=
1
S-
b)
Figu e
7:
Signal inse ion by exi (a) and inpu (b)
bo de s
In gene al, using exi and inpu bo de s
as
inse -
ion se s o new signal ansi ions does no always
gua an ee he consis ency o he new signal. I may
be necessa y o enla ge he exi bo de
EB(b)
wi h
hose s a es o he block
b
which a e di ec ly each-
able om
EB(b).
Simila ly, o inpu bo de
IB(b)
an enla gemen is equi ed wi h hose s a es o
b
om
which
IB(b
can be en e ed. Such enla gemen is no
De ini ion
6.1
Le
{b,T}
be
a
bipa i ion
o
a
SG
s a es.
1.
The exz bo de EB(b) is called well- o med i Vs
EB(b)
:
[ /s
5
s’
:
s‘
E
6
U
EB(b)] (simila ly
o
necessa y i
2
a bo de
is
well- o med.
inpu bo de IB(b) is called well- o med
i
Vs
E
IB(b)
:
[Vs’
1
s
:
s’
E
TU
IB(b)] (simila ly o
IB(~))
.
Le us e e o Figu e
6.
I
well- o med exi bo -
de s a e chosen o inse ing new signal ansi ions,
hen he I-pa i ion is de ined
as
ollows:
So
=
b
-
EB(b),
S+
=
EB(b),
S1
=
b-
El?($),
S-
=
EB
6
.
Since a ansi ion can exi
b
only h ough he
EB[b),
no a cs
So
-+
6
and
So
S-
in Figu e
6
a e pos-
sible. Due o he well- o medness o
EB(b)
i is no
possible o e u n om
EB(b)
o
b-EB(b),
hence a cs
S+
3
So
a e no possible ei he . A simila easoning
holds o
EB(b),
hence none o he illegal ansi ions
om Figu e
6
can occu .
P ope y
6.1
Le
A
be
a
consis en
SG
wi h
a
se
o
s a es
S
pa i ioned in o
{b,&}.
The
SG
A‘
ob ained
by
inse ing signal
x
by
exi
(inpu )
bo de s
o
{b,b)
is consis en
i
hese bo de s a e well- o med.
I he bo de s o a gi en pa i ion
{b,6}
o
S
a e no well- o med, we can s ill use i by conside -
ing
la ge
se s o s a es ha gua an ee consis ency.
Namely, gi en
{b,T;),
we
can de ine minimal well-
o med
ex ended
EB
and IB (deno ed
MWFEEB(b)
and
MWFEIB(
b))
as
minimal well- o med enla gemen s
o
exi and inpu bo de s espec i ely.
MWFEEB(b)
can
be calcula ed
as
he leas ix poin o he ollowing
ecu sion:
1.
MWFEEB(b)
=
EB(b)
2.
[s
E
MWFEEB(b)
A
s’
E
b
A
s
-s’]
j
s’
E
MWFEEB(b)
A
simila ecu sion can be applied o calcula ing
M
W
FEEB(z),
M
W
FE
I
B(
b)
,
and
M
W
F
El
B(6).
Minimal
well- o med ex ended bo de s hence a e minimal se s
o s a es o signal ansi ion inse ion which gua an-
ee consis ency.
7
Comple eness
o
he me hod
In his sec ion we will show ha he me hod o
CSC
solu ion using egion-based signal inse ion is com-
ple e, i.e. i allows o sol e all
CSC
con lic s,
o
a
ai ly gene al class o
SGs.
A
di ec syn hesis me hod o speed-independen
implemen a ion
o
STGs
wi hou choice has been p o-
posed in
[9].
I sol es all
CSC
con lic s by cons uc-
ion. This me hod can be gene alized o any sa e
STG
[3]
which is pe sis en wi h espec o he an-
si ions o ou pu signals
(so
called
ou pu -pe sis en
STGs).
Hence, his di ec me hod can be applied o
any
SG
o which
a
sa e and ou pu -pe sis en
STG
can
be gene a ed using egions
as
desc ibed in Sec ion
2.
Gene a ing such an
STG
is possible i an
SG
sa -
is ies he ollowing condi ions:
(1)
i is de e minis ic,
consis en , commu a i e and pe sis en by ou pu sig-
nals, and
(2)
i
is
elemen a y
a e spli ing all
GERs
in o
E%.
This esul implies ha o each
SG
which
mee s hese condi ions, he p ocedu e o signal inse -
ions based on in e sec ion o egions will e en ually
con e ge.
Le us ha e a close
look
a an I-pa i ion, in o de
o es ima e an uppe bound on he numbe
o
s a e
signals needed o sol e all CSC con lic s. Assume ha
(b,
6}
is a bipa i ion
o
a se
o
s a es. Assume ha an
I-pa i ion is cons uc ed om
{b,
6}
by exi bo de s,
i.e.,
S+
=
MWFEEB(b),
S-
=
MWFEEB(8)
and
So
=
b
-
S+
,
S1
=
b
-
5’-
(see Figu e 7,a).
Clea ly, all he s a es om
So
and
S1
will di e in
he new
SG
ob ained a e he ans o ma ion by he
44