Induc ion-based Ve i ica ion
o Timed Sys ems
Disse a ion
zu E langung des akademischen G ades eines
Dok o s de Na u wissenscha en
an de
Fakul ä ü Elek o echnik, In o ma ik und Ma hema ik
de
Uni e si ä Pade bo n
o geleg on
Tobias Isenbe g, M.Sc.
Pade bo n, Feb ua 2016
iii
Abs ac
Compu e con olled sys ems a e a ounda ion o oday’s mode n socie y.
Thei use and impac a e e e -g owing, in pa icula when conside ing ends like
sma homes and Indus y 4.0. The de elopmen o such sys ems is non- i ial.
Co ec ness o he unc ionali y p o ided by hese sys ems is o impo ance, since
hey a e o en deployed in sa e y-c i ical scena ios, whe e a ailu e could lead o
a loss in p oduc ion alue o he isk o li e. Many o hese sys ems a e eal- ime
sys ems o include some kind o imed beha io .
In o de o ensu e a ce ain quali y o hese sys ems, model-based design
app oaches can be employed. Wi hin hese s uc u ed p ocedu es, he sys ems
unde de elopmen a e designed using models ha speci y ce ain aspec s o
hem. This s uc u ed p ocedu e p o ides o ewe e o s being made. In
combina ion wi h o mal me hods, he absence o e oneous beha io can be
ensu ed. To his end, o mal languages wi h a ma hema ically de ined seman ics
a e employed, and o mal e i ica ion, based on his seman ics, is used o eason
abou he absence o e oneous beha io . The e exis se e al o malisms o he
e i ica ion o imed sys ems, e.g., he o malism o ne wo ks o imed au oma a
used in his hesis. Howe e , oday’s echniques and ools o his ask o en
su e om he same de iciency. They easily un ou o memo y when explo ing
la ge, complex models due o he eno mous amoun o s a es (s a e explosion
p oblem) hey need o keep ack o .
An addi ional challenge a ises when conside ing he p ocedu e du ing he
design phase. The models a e epea edly econ igu ed, i.e., changed o e lec
design choices un il a inal design is ound. In addi ion, hey may also be econ-
igu ed du ing li e ime, in pa icula when conside ing sys ems o Indus y 4.0
ha a e sel -op imizing and adap able. In consequence, he espec i e models a e
econ igu ed o e lec hese adap a ions. These econ igu a ions aise he need o
edo e i ica ions since he s a e spaces o he models migh ha e changed. Tech-
niques employed o hese edone e i ica ions ha e o mee speci ic demands, in
pa icula e iciency, since hey migh be employed in a so o online e i ica ion
du ing he li e ime o a sys em.
In his hesis, we app oach bo h o he challenges men ioned abo e. Fi s ,
we p o ide a echnique o he e i ica ion o sa e y p ope ies speci ying he
absence o e oneous beha io o ne wo ks o imed au oma a. Ou echnique
delibe a ely wo ks dis inc om o he s a e-o - he-a app oaches in his ield,
as i employs induc ion and, hus, a oids explici explo a ion and s o age o
s a es. In consequence, i is a aluable complemen o exis ing echnologies as i s
s eng hs and weaknesses di e o hose o o he echnologies. Ou app oach
combines he IC3 algo i hm, well known in he ha dwa e e i ica ion domain,
wi h he Zone abs ac ion, used o imed e i ica ion. The esul , IC3 wi h Zones
is compe i i e and includes he s eng hs o bo h componen s, namely he ime
abs ac ing e iciency o zones and he e iciency on disc e e s uc u ed o IC3.
We show he p ac icali y o i in nume ous expe imen s on di e en aspec s o
scalabili y.
In ou con inued wo k, we employ ou algo i hm o he e i ica ion o
econ igu ed models. To his end, we euse an induc i e in a ian compu ed by
IC3 wi h Zones.
i
This basic idea wo ks pa icula ly well o a special class o sys ems, deno ed
Pa ame e ized Timed Sys ems. They con ain an a bi a y, bu ixed numbe o
ins ances o a p ocess as is he case, e.g., in clien -se e se ings wi h an a bi a y
numbe o clien s. We p opose an app oach o a oid he online e i ica ion
o such sys ems, as would be needed whene e he numbe o p ocesses is
changed, e.g., a clien is added. Ou echnique enables an a p io i e i ica ion o
he en i e sys em, i espec i e o he ac ual numbe o ins ances. To his end,
we e i y he sa e y p ope y o he smalle models o he amily and euse he
compu ed induc i e in a ian s. These a e adap ed using he symme y inhe en
in Pa ame e ized Timed Sys ems, and employed o he easoning abou he
en i e sys em. Fo his pu pose, we p opose and p o e a Te mina ion Theo em
ha enables his easoning. The p ac icali y o ou app oach is shown using
se e al expe imen s.
In addi ion, we examine he eusabili y o he induc i e in a ian o gene al
models and econ igu a ions wi h he aim o speed up he e i ica ion o econ-
igu ed models. To his end, he same accele a ion echnique is employed as in
he special case o Pa ame e ized Timed Sys ems. We discuss in de ail, why i
is ha dly easible o adap he induc i e in a ian o e lec a econ igu a ion in
gene al. As a esul , we gi e a bes -guess app oach ha adap s he in a ian whe e
possible. Nume ous expe imen s show ha his echnique is o alue e en so, in
pa icula when he econ igu a ions a e small.
Zusammen assung
Rechne ges eue e Sys eme bilden den G unds ein de heu igen Gesellscha .
Ih Einsa z und ih e Ve b ei ung wachsen s e ig, un e s ü z du ch T ends wie
Sma Homes und Indus ie 4.0. Die En wicklung solche Sys eme is jedoch
schwie ig. Ih e ko ek e Funk ionali ä is on g oße Wich igkei , da diese
Sys eme o mals in siche hei sk i ischen Szena ios eingese z we den, in denen
eine Fehl unk ion zu inanziellem Schaden ode soga zu Ge ah ü Leib und
Leben üh en kann. Viele diese Sys eme sind Ech zei sys eme ode besi zen
zei ges eue es Ve hal en.
Um die Quali ä de Sys eme siche zus ellen, können Modell-basie e Design-
Ansä ze e wende we den. In diesen s uk u ie en Vo gehensweisen we den die
zu e s ellenden Sys eme mi hil e on Modellen en wo en, die ein Sys em un e
bes imm en Gesich spunk en spezi izie en. Ein solch s uk u ie e Ansa z so g
da ü , dass wenige Fehle gemach we den. Du ch die zusä zliche Nu zung o -
male Me hoden kann die Abwesenhei on ehle ha em Ve hal en siche ges ell
we den. Hie zu we den o male Sp achen mi ma hema isch de inie e Seman ik
genu z , sowie o male Ve i ika ion, die basie end au de o malen Seman ik
übe die Abwesenhei on ehle ha em Ve hal en schluss olge . E liche Fo mal-
ismen exis ie en ü die Ve wendung zu Ve i ika ion zei liche Sys eme, zum
Beispiel die Ne zwe ke on zei lichen Au oma en, die in diese A bei e wen-
de we den. Die meis en de heu igen Techniken ü die Ve i ika ion zei liche
Sys eme leiden jedoch un e dem gleichen P oblem. Bei de Explo a ion g oße ,
komplexe Modelle benö igen sie ein eno mes Maß an Speiche , um die besuch en
Zus ände zu speiche n. Du ch das eno me Anwachsen de Anzahl an Zus änden
(Zus andsexplosionsp oblem) schläg die Ve i ika ion o ehl.
Eine zusä zliche He aus o de ung en s eh du ch den Ablau de Design-
Phase. Bis das inale Design en schieden is , können die Modelle wiede hol
ekon igu ie , d.h. geände , we den um Designen scheidungen umzuse zen.
Zusä zlich kann dies auch zu Lau zei de Sys eme au e en, insbesonde e bei
Sys emen de Indus ie 4.0, die selbs op imie end und anpassungs ähig sind.
Demen sp echend können sich die en sp echenden Modelle zu Lau zei ände n.
Diese Rekon igu a ionen e langen eine e neu e Ve i ika ion, da sich de Zus and-
s aum geände haben kann. An die Techniken, die ü diese e neu en Ve i ika-
ionen eingese z we den, we den spezielle An o de ungen ges ell , insbesonde e
E izienz, da sie wäh end de Lau zei als Online-Ve i ika ionen du chge üh
we den.
In diese A bei we den beide zu o genann en He aus o de ungen ange-
gangen. Es wi d eine Technik zu Ve i ika ion on Siche hei seigenscha en,
die die Abwesenhei on ehle ha em Ve hal en de inie en, in Ne zwe ken on
zei lichen Au oma en o ges ell . Diese Technik ha ein g undlegend ande es
Funk ionsp inzip als ande e ak uelle Ansä ze, da sie Induk ion nu z und somi
die explizi e Explo a ion und Speiche ung on Zus änden umgeh . Hie du ch
is sie eine we olle E gänzung zu den bes ehenden Ansä zen, da die S ä ken
und Schwächen un e schiedlich aus allen. De Ansa z kombinie den IC3 Al-
go i hmus, de in de Ha dwa e Ve i ika ion e olg eich eingese z wi d, mi
de Zonen-Abs ak ion, die G undlage iele zei liche Ve i ika ions e ah en is .
De esul ie ende Algo i hmus IC3 mi Zonen is we bewe bs ähig und en häl

i
S ä ken on beiden genann en Komponen en. Dies sind insbesonde e die gu e
Fähigkei zu Zei -Abs ak ion on Zonen und die E izienz au disk e en S uk-
u en on IC3. Die Anwendba kei und Skalie ba kei de Technik wi d in ielen
Expe imen en gezeig .
Au bauend au diese Technik we den Ansä ze o ges ell , die au die Ve i-
ika ion on ekon igu ie en Modellen abzielen. Sie nu zen dazu die induk i e
In a ian e, die on IC3 mi Zonen be echne wi d.
Die Idee de Wiede e wendung de In a ian e is besonde s gu einse zba
bei eine speziellen A on Sys emen, genann Pa ame isie e Zei liche Sys eme.
Diese en hal en eine beliebige, abe es e Anzahl an Ins anzen eines P ozesses, wie
beispielsweise in einem Clien -Se e Sys em mi beliebige Anzahl Clien s. Unse
Ansa z umgeh die No wendigkei eine Online-Ve i ika ion ü solche Sys eme,
die beispielsweise no wendig wä e, wenn die Anzahl an Clien s geände wü de.
Die Technik basie au eine Ve i ika ion de gesam en Familie an Modellen,
die on o nhe ein ausge üh wi d. Hie zu wi d die Siche hei seigenscha ü
die kleine en Modelle e i izie . Die dabei be echne en induk i en In a ian en
we den anhand de Symme ie, die du ch die Pa ame isie ung gegeben is ,
angepass und danach e wende , um übe die gesam e Familie an Modellen zu
u eilen. Hie ü wi d ein Te minie ungs heo em gegeben und bewiesen. E liche
Expe imen e zeigen den Nu zen de Technik.
Zusä zlich wi d un e such , wie man die induk i en In a ian en ü allge-
meine Rekon igu a ionen und Modelle nu zen kann, so dass die Ve i ika ion ü
ekon igu ie e Modelle schnelle wi d. Es we den die gleichen Techniken zu
Beschleunigung on Ve i ika ionen mi hil e de In a ian en benu z , wie in de
A bei zu pa ame isie en Sys emen. De aillie wi d da geleg , wa um diese
In a ian en im allgemeinen Fall kaum an die Rekon igu a ion angepass we den
können. Schließlich wi d ein Ansa z o ges ell , de die In a ian e sowei wie
möglich anpass . Expe imen e zeigen, dass diese Technik eine Be eiche ung im
Kon ex de Online-Ve i ika ion da s ell .
ii
Acknowledgmen s
Mos impo an ly, I would like o exp ess my since e g a i ude o my supe -
iso P o . D . Heike Weh heim o he guidance and suppo . The las h ee
yea s ha e been a ewa ding, in e es ing ime and I am e y hank ul o he
oppo uni y o wo k in he esea ch g oup and o w i e my hesis. I also wan o
exp ess my g a i ude o my second supe iso P o . D . Oli e Niggemann o
his suppo .
Since e hanks go o P o . D . Hans Kleine Büning, Jun.-P o . D . Heiko
Hamann and D . Theodo Le mann o being pa o my PhD commi ee.
In addi ion, I wan o hank all cu en and o me membe s o he esea ch
g oup ha ha e c ossed my pa h: S e en Be inge , D . Galina Beso a, Ma ie-
Ch is ine Jakobs, Julia K äme , D . Thomas Ruh o h, Elisabe h Schla , Alexande
Sch emme , D . Dominik S eenken, D . Nils Timm, Manuel Töws, Oleg T a kin,
S en Wal he and S e en Ziege . They p o ided o a pleasan a mosphe e and
a g ea ime.
Fu he mo e, I owe special g a i ude o Dennis Wol e s and Anna Lena
Isenbe g o p oo eading pa s o his hesis.
Finally, I wan o hank my pa en s, We ne and Ul ike Isenbe g, o always
encou aging me and p o iding, oge he wi h my win b o he Flo ian and my
sis e Anna Lena, o an amazing childhood ha made me who I am.
Las , bu no leas , I wan o exp ess my lo ing g a i ude o my gi l iend
Nadja. She knows how o make me smile and she has always been he e o
suppo me.
Con en s
Lis o Figu es xiii
Lis o Tables x
1 In oduc ion 1
1.1 P oblemDe ini ion .............................. 3
1.2 Con ibu ion.................................. 5
1.3 ThesisOu line................................. 9
2 Backg ound 11
2.1 TimedAu oma a ............................... 11
2.1.1 Decidabili y and Abs ac ions . . . . . . . . . . . . . . . . . . . 19
2.1.2 Rela edwo k ............................. 20
2.2 SAT-&SMT-Sol ing ............................. 23
2.2.1 SAT-Sol ing.............................. 23
2.2.2 SMT-Sol ing.............................. 24
2.3 Induc ion based Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.4 IC3 ....................................... 28
2.4.1 Algo i hm and Explana ion . . . . . . . . . . . . . . . . . . . . . 28
2.4.2 Op imiza ions............................. 35
2.4.3 IC3wi hSMT............................. 37
2.4.4 IC3 o TA............................... 38
3 Timed Au oma a Ve i ica ion ia IC3 wi h Zones 41
3.1 SMT-Encoding................................. 42
3.1.1 Va iables................................ 43
3.1.2 Encoding o he Ini ial S a es . . . . . . . . . . . . . . . . . . . . 44
3.1.3 Encoding o Clock Cons ain s . . . . . . . . . . . . . . . . . . . 45
3.1.4 Encoding o In ege Cons ain s . . . . . . . . . . . . . . . . . . 46
ix
x i Lis o Tables
A.4 Resul s o expe imen s wi h IC3 wi h Zones (Fische _Bmodel) . . . . . . . 164
A.5 Resul s o expe imen s wi h IC3 wi h Zones (Lampo _Bmodel) . . . . . . 164
A.6 Resul s o expe imen s wi h IC3 wi h Zones (Lampo _Smodel) . . . . . . 165
A.7 Resul s o expe imen s wi h IC3 wi h Zones (Sha i Lynch_Bmodel) . . . . 165
A.8 Resul s o expe imen s wi h IC3 wi h Zones (Sha i Lynch_Pmodel) . . . . 166
A.9 Resul s o expe imen s wi h IC3 wi h Zones (FDDIcoun model) . . . . . . 167
A.10 Resul s o expe imen s wi h loca ion iden i ie s (Fische _Umodel) . . . . 168
A.11 Induc i e s eng henings: Valida ion and size (Fische _Umodel) . . . . . 169
A.12
Induc i e s eng henings: Valida ion and size (
Fische _U(swi ched)
model)
170
A.13 Induc i e s eng henings: Valida ion and size (CSMA/CD model) . . . . 171
A.14 Induc i e s eng henings: Valida ion and size (FDDI model) . . . . . . . 171
A.15 Induc i e s eng henings: Valida ion and size (FDDIcoun model) . . . . 172
A.16 Induc i e s eng henings: Valida ion and size (Fische _Bmodel) . . . . . 172
A.17 Induc i e s eng henings: Valida ion and size (Lampo _Bmodel) . . . . . 172
A.18 Induc i e s eng henings: Valida ion and size (Lampo _Smodel) . . . . . 172
A.19 Induc i e s eng henings: Valida ion and size (Sha i Lynch_Bmodel) . . 173
A.20 Induc i e s eng henings: Valida ion and size (Sha i Lynch_Pmodel) . . 173
A.21 Induc i e s eng henings: Valida ion and size (Lemgo model) . . . . . . . 173

1
In oduc ion
Mo e han e e does oday’s socie y ely on he co ec unc ionali y o so wa e and
ha dwa e, as mo e and mo e asks a e ca ied ou by compu e -con olled sys ems.
This end can be obse ed in e e yones pe sonal en i onmen , as well as in he
indus y. Examples o impo ance a e he usage o connec ed con olle s in sma
homes, e.g., o doo s and adia o s, o he pa adigm o Indus y 4.0 ha acili a es he
in e connec ion and adap a ion o all componen s engaged in a p oduc ion sys em.
As a esul , he sys ems and hei in e ac ion g ow mo e and mo e complex.
The inc eased complexi y poses a se ious h ea o he co ec unc ionali y o
he sys ems, as a mis ake migh mo e easily s ay unno iced wi hin a la ge sys em.
Wi h mos o he sys ems being sa e y c i ical, e e y possible e o mus be made
o a oid and ind such mis akes ha esul in unin ended, e oneous beha io .
Conside ing again he abo e examples, a mis ake migh esul in he sma doo
opening e oneously, o a sudden, undesi ed s op in a p oduc ion sys em. The
consequence migh be a loss in p oduc ion alue o he isk o li e.
In esponse o his p oblem, an inc easing e o is made o esea ch and in oduce
s uc u ed app oaches ha a e able o ensu e a ce ain quali y o a sys em. One such
app oach o so wa e is he model d i en so wa e de elopmen (MDSD) [B+05]
ha s a s as ea ly as possible du ing de elopmen , namely in he design phase. In
such s uc u ed app oaches, a sys em is speci ied ia models ha depic di e en
aspec s o i . Fo example, he uni ied modeling language (UML) [RJB04] is ypically
employed o his ask du ing he de elopmen o so wa e sys ems. UML con ains
nume ous ypes o diag ams o speci y di e en aspec s o he sys em, e.g., use case
diag ams o cap u e beha io al equi emen s o class diag ams o cap u e s uc u al
ela ions. These diag ams a e no only employed o speci ica ion, bu a e also used
o documen a ion pu pose and a e o en in ol ed in he cons uc ion o he inal
sys em. To his end, au oma ed ans o ma ions and gene a o s a e employed ha
ully au oma e he ask o ans o ma ion in o o he modeling o malisms, o he
gene a ion o code. This s uc u ed p ocedu e o speci ica ion and gene a ion o
1
2CHAPTER 1. INTRODUCTION
pa s o a so wa e sys em is o en used and helps o achie e a good code quali y and
a chi ec u e. Howe e , e e y manual speci ica ion and modeling migh in oduce
unin ended, e oneous beha io in he models and, using he au oma ed gene a o s
and ans o ma ions, in o he inal sys em. Fo his eason, o mal me hods a e
employed ha a e able o gua an ee he absence o such beha io in he models and,
in consequence, in he inal sys em, p o ided he ans o ma ions a e co ec . These
o mal me hods basically d aw on h ee impo an elemen s. Fi s , he unin ended,
e oneous beha io has o be speci ied. Second, he models ha a e o be checked
need o be speci ied using a o malism based on a igo ous ma hema ical seman ics
in o de o enable easoning abou e oneous beha io . Thi d, he me hods ha
check he absence o he unin ended beha io in he gi en model a e equi ed o be
sound.
The e exis many dis inc o malisms o modeling he sys em unde de elop-
men . Many o hem a e speci ically designed o cap u e ce ain aspec s o he
sys em, e.g., i s s uc u e, communica ion o imed beha io . They a e based on a
igo ous de ined ma hema ical seman ics ha allows he easoning abou p ope ies.
Using he ma hema ical ounda ion, he easoning abou p ope ies o he models
can be done using one o he app oaches o o mal e i ica ion. The e exis se -
e al such echniques, whe e deduc i e e i ica ion and model checking ep esen
he mos well-known ca ego ies. Among he mos common modeling o malisms
a e au oma a, pe i ne s [Mu 89], p ocess calculi [Mil80; Mil99], Z [SA92] and he
B-me hod [AAH05]. In addi ion, he e exis o malisms ha encompass an explici
no ion o ime, e.g., imed au oma a [AD90], hyb id au oma a [Hen00], imed pe i
ne s [Ram73], Timed CSP [RR86], Du a ion Calculus [CHR91] and Timed G aph
T ans o ma ion Sys ems [HHH10]. These a e o special in e es , as eal- ime sys ems
a e o g owing impo ance.
As an example, conside he nume ous embedded eal- ime con olle s ha
ope a e many sa e y-c i ical sys ems, e.g., he ime-c i ical sensing o a ca acciden
wi h almos immedia e in la ion o an ai bag. Addi ionally, in he indus y mo e
and mo e eal- ime sys ems a e employed, as he pa adigm o Indus y 4.0 o en
equi es he componen s o communica e using eal- ime p o ocols in o de o
achie e adap i i y and sel -op imiza ion o all componen s in a plan . The e exis
se e al addi ional examples ha illus a e oday’s impo ance o eal- ime sys ems
and ime based beha io .
In gene al, such beha io is o in e es in many de elopmen scena ios and so
a e he espec i e o malisms and o mal e i ica ion me hods. As in he un imed
case, he o malisms a e employed o model speci ic aspec s o he sys em unde
de elopmen , and e i ica ion is employed o check whe he speci ied p ope ies
hold ue o he model.
As explained abo e, he sys ems and hei in e ac ion g ow mo e and mo e com-
plex. In consequence, he espec i e models o hese sys ems become inc easingly
complex. The o mal e i ica ion ca ied ou o ensu e he quali y o he sys em
needs o be able o handle such la ge models. Bu wi h models g owing in ensely,
he e i ica ion o p ope ies o hem becomes e en mo e challenging due o he
1.1. PROBLEM DEFINITION 3
s a e explosion p oblem. An addi ional p oblem is he ac ha models a e o en
econ igu ed, i.e., changed. In he MDSD p ocess men ioned abo e, econ igu a ions
may occu epea edly in he design phase un il a inal design is ound. A eason
migh be ha equi ed p ope ies a e no me o ha addi ional pa s ha e o be
included.
In addi ion, he e exis scena ios in which a model is econ igu ed a li e ime
o a de eloped sys em. These econ igu a ions, i.e., changes, o he model e lec
changes o he unning sys em. They a e o huge impo ance, in pa icula , when
conside ing he adap i i y and sel -op imiza ion p oposed o Indus y 4.0 plan s.
Examples o such econ igu a ions a un ime a e he adap a ion o a plan
in which i swi ches o ano he ope a ing mode in o de o sa e ene gy, o he
modi ica ion o he plan including new componen s. Fu he mo e, he subs i u ion
o mechanical pa s migh esul in a di e en iming beha io i he pa s possess
dis inc ope a ing cha ac e is ics.
In such cases, he sys em is econ igu ed a li e ime, possibly in ways ha could
no be o eseen wi hin he design-phase. The e exis wo ks ha a e conce ned wi h
in elligen assis an sys ems o such scena ios [JN12], bu hey do no conside he
con ex o o mal e i ica ion. E e y change in he sys em migh lead o unin ended
beha io . Thus, he e exis s a need o e i y he p ope ies, which ha e al eady been
e i ied o he o iginal model, again o he econ igu ed one.
To his end, he econ igu ed model could be p o ided manually by a model
designe , o e en be lea ned au oma ically by machine lea ning algo i hms, e.g as
imed au oma a [Mai14] o hyb id au oma a [Nig+12].
In any case, he e i ica ion should be as e icien as possible, in pa icula , when
conside ing ha he p ope ies ha e al eady been e i ied o he o iginal model ha
migh be e y simila . Mo eo e , when aking in o accoun ha he econ igu ed
sys em migh al eady be unning, he u gency o his ask becomes ob ious.
Ei he way, a econ igu ed model would esul in a enewed need o e i ica ion.
Wi h he g owing complexi y o sys ems and hei models in mind, hese e i ica ions
should be as e icien as possible. I is, hus, no desi able ha hese e i ica ions o
econ igu ed models employ echniques ha s a om sc a ch.
1.1 P oblem De ini ion
Many o oday’s sys ems exhibi imed beha io . They ely on ime in di e se ways,
e.g., using eal- ime communica ion p o ocols as can be ound o example in he
PROFINET s anda d [Fel04]. Fu he mo e, he in e ac ion o se e al componen s
can be seen as imed in e dependency, e.g., since he dis ibu ion o a p oduc
in he plan elies on i s comple ed c ea ion. The quan i y o sys ems wi h such
beha io shows he signi icance o imed e i ica ion. Fo his ask, models a e
c ea ed ha e lec he ime-based aspec s o he sys em. As illus a ed abo e, he
o mal modeling and e i ica ion can be done a design ime o he sys em, e.g., in
he con ex o model-based design p ocesses, o la e on du ing un ime, e.g., using
lea ned models. Ei he way, a o mal modeling language is equi ed in o de o
4CHAPTER 1. INTRODUCTION
model he men ioned imed beha io . The e exis o malisms ha a e capable o
modeling con inuous eal- ime since he ea ly 1990s. They o e a ious le els o
exp essi eness and usabili y.
In his hesis, we employ he o malism o ne wo ks o imed au oma a [AD90].
I is one o he mos well-known o malisms wi h oughly 25 yea s o esea ch.
The modula s uc u e as a ne wo k consis ing o se e al imed au oma a enables
an elabo a e way o modeling indi idual componen s, e.g., ep esen ing so wa e
p ocesses o di e en ha dwa e con olle s. I is, hus, well sui ed o he modeling
o in e connec ed componen s as is he case in Indus y 4.0 plan s o sma homes.
The decidabili y o eachabili y ques ions in his o malism enables he use o o mal
e i ica ion [AD90].
In ne wo ks o imed au oma a, he in e connec ion o he dis inc componen s’
beha io s is gi en implici ly ia ime. In addi ion, he o malism allows an explici
in e ac ion en o ced ia synch oniza ion and sha ed a iables.
Like in o he au oma a o malisms, imed au oma a a e based on a disc e e
s uc u e ha o e s an easy means o speci y dis inc s a es o he a ious compo-
nen s. This disc e e s uc u e cap u es he o e all, un imed beha io o he sys em.
Howe e , in imed sys ems, his beha io highly depends on ime.
To his end, cons ain s a e in oduced ha es ic he allowed beha io as a
unc ion o he elapsed ime. This in ui i e mechanism o obse ing he p og ess
o ime and, in dependence, limi ing he allowed beha io is a basic concep , also
included in se e al o he imed o malisms, e.g., imed pe i ne s o imed g aph
ans o ma ion sys ems.
In his hesis, we a e conce ned wi h he e i ica ion o sa e y p ope ies ha
speci y he non- eachabili y o e o s a es. These e o s a es a e an in ui i e way o
speci y unin ended o undesi ed beha io . The absence o such e oneous beha io
can be gua an eed ia a o mal e i ica ion o he sa e y p ope ies.
Fo he o malism o ne wo ks o imed au oma a, he e al eady exis echniques
and ools o e i y such p ope ies. Conside ing he equi emen s o oday’s sys ems
and Indus y 4.0, hese app oaches a e no well sui ed.
Mos o hem a e op imized o un ime, i.e., hey a e as a he expense o used
memo y, mos ly due o explici explo a ion. Taking in o accoun he inc easing size
o he sys ems and hei in e connec i i y, an app oach is desi able ha is capable o
e i ying la ge models wi hou unning ou o memo y easily. Fu he mo e, mos
o he cu en echniques a e no sui ed o cope wi h econ igu ed models as may
happen o en, e.g., du ing model-based design p ocesses. These app oaches equi e
a e i ica ion o he p ope ies o he econ igu ed model ha s a s om sc a ch.
These a e he wo p oblems we app oach in his hesis. They a e summed up in
he ollowing.
•
The e i ica ion o la ge models, in pa icula hose wi h a la ge se o eachable
s a es, poses a p oblem o many exis ing echniques. Many o hese echniques
ely on an explici explo a ion and ep esen a ion o he o wa d o backwa d
eachable s a es. These s a es ha e o be s o ed in o de o know which s a es
1.2. CONTRIBUTION 5
ha e al eady been explo ed. T i ially, a la ge numbe o such s a es esul s
in huge memo y equi emen s, which is o en he eason ha a e i ica ion is
abo ed. We will ocus on a echnique ha does no equi e he explo a ion o
each eachable s a e. To his end, i employs induc ion. We seek o de elop an
app oach ha handles complex, la ge models well.
•
The second p oblem in he abo e se ing is ha many models migh be e-
con igu ed du ing design ime o li e ime. Cu en e i ica ion echniques o
imed au oma a a e no designed o an e icien e i ica ion o he econ ig-
u ed models. They will s a a e i ica ion om sc a ch and, hus, was e he
chance o euse a p e ious e i ica ion esul . E en i hey would be capable o
eusing a p e ious ou come, hei explici me hod would need o check e e y
such s a e again, as he s a e space has changed. Ou ocus on an induc i e
me hod es ablishes a dis inc chance, as i can be eused in a mo e elabo a e
way. We seek o de elop a echnique ha e icien ly e i ies sa e y p ope ies
o econ igu ed models in o de o suppo epea ed econ igu a ions du ing
design ime, and in o de o enable online e i ica ion, i.e., e i ica ions du ing
li e ime o a sys em.
In he ollowing, we will s a e ou con ibu ions o hese wo p oblems.
1.2 Con ibu ion
This hesis is conce ned wi h bo h o he p oblems poin ed ou abo e. We p opose
a no el echnique o he e i ica ion o sa e y p ope ies o ne wo ks o imed
au oma a. Based on an induc i e in a ian compu ed by his echnique, we accele a e
he e i ica ion o sa e y p ope ies o econ igu ed models.
In de ail, ou con ibu ion is as ollows.
IC3 wi h Zones
As men ioned abo e, many o he e i ica ion echniques o sa e y
p ope ies in ne wo ks o imed au oma a su e om la ge memo y equi emen s.
When handling la ge models wi h a huge se o eachable s a es, he explici explo-
a ion ha is used in many s a e-o - he-a app oaches easily uns ou o memo y.
The eason is ha he algo i hm needs o s o e he al eady explo ed s a es in o de o
de ec whe he a new s a e was al eady disco e ed. Thus, hei memo y need can be
seen as one o he mos impo an weaknesses o he cu en e i ica ion echniques.
We a oid he explici explo a ion and disco e y o e e y eachable s a e. To
his end, we ans e he IC3 algo i hm o he domain o imed e i ica ion in a
compe i i e way. We p esen , implemen and e alua e a concep ha combines he
s eng hs o he ollowing wo elemen s.
•
The IC3 algo i hm [B a11] has p o en o be success ul and e icien , bo h
ega ding un ime and memo y, o he e i ica ion o sa e y p ope ies on
disc e e s uc u es. I is based on induc ion and SAT-sol ing and, hus, wo ks
di e en ly han he explo a ion algo i hms usually employed in imed e i i-
ca ion. I s mechanisms a oid he disco e y and s o age o e e e y eachable

6CHAPTER 1. INTRODUCTION
s a e, bu ins ead compu e an induc i e in a ian s o ed as a compac p oposi-
ional o mula. We employ his e iciency and dis inc i eness in ou app oach
in o de o a oid he common p oblem o s o ing explici ly explo ed s a es.
•
The Zone abs ac ion has been employed nume ous imes o imed e i ica ion.
I is e sa ile in ha i can be e y ine g ained o e y coa se and he e exis
sophis ica ed algo i hms o e icien ly manipula e zones. Using hese e icien
algo i hms and he p ope coa seness, we employ his abs ac ion in o de o
handle he in ini e s a e space imposed by he seman ics o imed au oma a.
By combina ion o hese wo elemen s, we achie e a ans e o he IC3 algo i hm o
he domain o imed e i ica ion, which is compe i i e, unlike p e ious a emp s. The
esul is a echnique ha wo ks in a way dis inc han o he s a e-o - he-a echniques
in imed e i ica ion, namely by using induc ion. I combines he s eng hs o he
wo included elemen s and, hus, a oids he weakness o s o ing explici ly explo ed
s a es, i.e., he eno mous need o memo y.
Ou echnique employs SMT-sol ing [BST10] and is based on induc ion. The
main challenge is he in ini e s a e ansi ion sys em imposed by he seman ics o
imed au oma a. As explained, we employ he Zone abs ac ion in o de o cope
wi h his p oblem and ensu e e mina ion. The in eg a ion o his abs ac ion in o
he IC3 algo i hm is based on he s uc u e o he SMT-que ies. Ou combina ion
achie es e mina ion and e iciency.
We show his e iciency and p ac icali y o ou p oposed echnique in nume -
ous expe imen s. Using s anda d examples om li e a u e, we illus a e ha ou
app oach is able o ou pe o m s a e-o - he-a ools by models up o h ee imes as
la ge. We p esen expe imen s o examine he scalabili y o ou app oach wi h ega d
o he model size, he used loca ion encoding and he usage o in ege a iables.
Summing up, we p esen a combina ion o wo echniques om dis inc domains.
I does, unlike mos o he echniques in he domain, no explici ly explo e and
s o e he eachable s a e space. Ins ead, ou echnique employs induc ion o
he e i ica ion o sa e y p ope ies in imed sys ems modeled as ne wo ks o
imed au oma a. Due o i s dis inc wo king pa adigm, he p esen ed echnique
is well sui ed o be used o la ge, complex models as in oday’s sys ems. I
is a ele an al e na i e o long-es ablished app oaches and migh gi e hough -
p o oking impulses.
Ou echnique yields a aluable addi ional ou come in case o e i ica ion success,
which we employ o he second p oblem de ined abo e (Sec ion 1.1). I compu es
an induc i e in a ian ha we s o e and euse o he e i ica ion o p ope ies o
econ igu ed models.
In he ollowing, we s a e ou con ibu ion in his di ec ion. The i s wo k
deals wi h speci ic econ igu a ions ha add an ins ance o a p ocess o an al eady
exis ing numbe o such ins ances. Doing so nume ous imes c ea es a sys em
wi h an a bi a y la ge, bu ixed numbe o p ocesses. These sys ems a e deno ed
pa ame e ized imed sys ems.
1.2. CONTRIBUTION 7
Pa ame e ized Timed Sys ems
Pa ame e ized Timed Sys ems occu equen ly in
mode n sys ems. Fo example, conside a scena io in which a numbe o obo s
equi es he exclusi e access o a esou ce, e.g., o he op elemen o a pile o aw
ma e ials in o de o s a wo king. In o de o a oid p oblems, he decision which
obo gains access can be nego ia ed by hei con olle s using a mu ual exclusion
algo i hm. To ensu e e o - ee unc ioning, he in ol ed con olle s migh ha e
been modeled and mu ual exclusion has been e i ied. Howe e , i an addi ional
obo is added, e.g., o inc ease he p oduc i i y, he same p ope y needs o be
e i ied again o he econ igu ed sys em including he addi ional con olle . The e
exis many o he scena ios ha also aise he need o a new e i ica ion whene e
he sys em is econ igu ed wi h a new numbe o p ocesses.
We ha e p oposed a no el app oach o he e i ica ion o sa e y p ope ies o
such pa ame e ized imed sys ems ha consis o an a bi a y, bu ixed numbe
o ins an ia ions o a p ocess. Ou echnique enables an a p io i e i ica ion o he
en i e sys em, whe e he ac ual numbe o ins ances du ing un ime does no ma e .
Thus, he sys em can be econ igu ed by addi ion o dele ion o p ocesses wi hou
aising he need o a new e i ica ion. Ins ead, based on he a p io i e i ica ion
one can be su e ha he sa e y p ope y holds i espec i e o he numbe .
This echnique a oids he need o online e i ica ion o sys ems ha can be
modeled as such a pa ame e ized imed sys em. I is compe i i e and able o eason
abou he en i e amily o models in he sys em by conside ing only a ew ixed
ins ances. To his end, i euses e i ica ion esul s ob ained du ing he e i ica ion
o hese ixed ins ances in o de o eason abou all la ge models. This euse is
ex emely e icien .
Ou app oach consis s o se e al impo an pa s. We p opose a wo k low ha
inc emen ally e i ies he sa e y p ope y in ques ion o models wi h inc easing size.
I employs ou algo i hm IC3 wi h Zones p esen ed in he p e ious pa ag aph and,
hus, p o i s om possible imp o emen s in he u u e. The induc i e in a ian s
compu ed by he algo i hm a e adap ed using he symme y inhe en in pa ame e -
ized imed sys ems and la e on used o eason abou he en i e sys em. To his end,
we p opose and p o e a Te mina ion Theo em ha is he basis o his easoning.
Addi ionally, we euse he adap ed induc i e in a ian s in o de o accele a e
subsequen e i ica ions o he sa e y p ope y o econ igu ed models, which
means in his con ex ha hey include an addi ional p ocess.
Bo h euses o p e iously compu ed esul s a e ex emely success ul as shown in
nume ous expe imen s. We we e able o e i y mu ual exclusion o all conside ed
pa ame e ized imed sys ems, i.e., o any numbe o ins ances. This abili y is a
signi ican bene i o e he single e i ica ion o a ixed model. As an example,
conside a model wi h one million imed au oma a, which can be e i ied by ou
echnique in he con ex o pa ame e ized imed sys ems.
Summing up, we p esen an app oach ha en i ely a oid he need o online
e i ica ion in he con ex o pa ame e ized imed sys ems. Using an a p io i
e i ica ion, i allows he econ igu a ion o he sys em in e ms o he numbe o
8CHAPTER 1. INTRODUCTION
p ocesses wi hou aising he need o a new e i ica ion. I is compe i i e and
e icien in ha i euses compu ed induc i e in a ian s.
Reusing p e iously compu ed induc i e in a ian s o accele a e he e i ica ion
o econ igu ed models does no only wo k in he pa ame e ized se ing, bu also
in a gene al one. We deno e his euse as Feedback-mechanism and apply i in he
ollowing wo k o gene al models and econ igu a ions.
Ve i ica ion in he E en o Gene al Recon igu a ions
In he p e ious se ing, he
speci ic kind o sys ems allows an easy es ima ion o he e ec s o a econ igu a ion
based on he inhe en symme y. Fo gene ic econ igu a ions, howe e , he e ec s
can no be es ima ed in gene al.
Fo example, conside a sel adap a ion o a sys em in a plan . Al hough he
u u e beha io mode is de e mined by his adap a ion, i can no be es ima ed how
his beha io will wo k ou conside ing he en i e sys em in he u u e. In gene al, a
econ igu a ion as li le as he change o a iming cons an migh ul ima ely lead o
unin ended beha io .
As he e ec on he en i e sys em can no be es ima ed, we p opose a bes -guess
app oach ha ies o adap he induc i e in a ian as good as possible. A e wa ds
he adap ed in a ian is used in he Feedback-mechanism in o de o accele a e he
e i ica ion o he p ope y o he econ igu ed model.
Based on he econ igu a ions ha ha e been ca ied ou , we adap he in a ian
such ha i is usable in he new e i ica ion and e lec s he changes applied o
he model. Howe e , due o he IC3 algo i hm and he zone compu a ion, his
adap a ion is ex emely limi ed.
E en so, o en he adap ed induc i e in a ian can success ully be applied o
accele a e he e i ica ion o he sa e y p ope y o he econ igu ed model. We
ha e conduc ed se e al expe imen s o show he alue o his echnique. E en wi h
a econ igu a ion ha in oduces a iola ion o he sa e y p ope y, ou eedback
mechanism has shown o be o help.
Clea ly, he alue o his echnique in gene al is limi ed. Recon igu a ions
ha in oduce oo much change in he model will ul ima ely esul in a useless
euse o he induc i e in a ian . Ne e heless, we ha e in oduced and examined
a euse mechanism ha is able o accele a e he e i ica ion o sa e y p ope ies
o econ igu ed imed sys ems in gene al. I is success ul o many ins ances, in
pa icula , when conside ing small econ igu a ions o la ge models as migh o en
be he case in model-based design p ocesses o econ igu a ions o imed sys ems
du ing li e ime. The echnique gi es an impo an impulse o online e i ica ion o
econ igu ed models, as migh be needed inc easingly in he u u e due o pa adigms
like Indus y 4.0.
In summa y, he ollowing con ibu ions a e made. We success ully ans e he
IC3 algo i hm in o he domain o imed sys ems, such ha i is compe i i e. To
his end, we p opose a combina ion wi h he Zone abs ac ion, which wo ks in a
dis inc way han o he echniques and, hus, gi es new impulses and is o alue as
1.3. THESIS OUTLINE 9
a complemen o exis ing app oaches. Nume ous expe imen s show i s alue and
p ac icali y.
Using he induc i e in a ian compu ed by he p oposed app oach, we in oduce
an app oach o a p io i e i ica ion o an en i e pa ame e ized imed sys em. I
allows he e i ica ion o sa e y p ope ies o any numbe o ins an ia ions o a
p ocesses in hese sys ems, such ha he addi ion o dele ion o a p ocess does no
longe aise he need o a new e i ica ion. Se e al expe imen s a e employed o
show he p ac icali y, in pa icula when eusing p e iously compu ed induc i e
in a ian s o he accele a ion o new e i ica ion uns o econ igu ed models.
Finally, we employ his euse in a gene al se ing. We p esen a bes -guess
app oach ha allows an e icien e i ica ion o sa e y p ope ies o econ igu ed
models and, he eby, enables online e i ica ion o econ igu a ions du ing li e ime
o a sys em. Ou expe imen s a e p omising, e en hough gene al econ igu a ions
a e ha d o handle.
Ou wo k is, hus, o alue o he in ended use, namely he e i ica ion o la ge,
complex models in he con ex o econ igu a ions.
The con ibu ions a e p esen ed in he hesis in he ollowing o de .
1.3 Thesis Ou line
Following his in oduc ion, Chap e 2 in oduces he o malism used h oughou
his hesis. We o mally de ine he employed modeling o malism and i s seman ics
be o e speci ying he conside ed sa e y p ope ies. Elabo a ing he ela ed wo k, we
highligh impo an wo k du ing he 25 yea s o esea ch in his ield. A e wa ds,
we s a wi h an in oduc ion o SAT-based e i ica ion, which includes a de ailed
sec ion abou he employed IC3 algo i hm. I s op imiza ions and ela ed wo k a e
gi en subsequen ly. We inish he chap e wi h ele an ela ed wo k ha employs
IC3, e.g., o imed e i ica ion using he egion abs ac ion.
Chap e 3 con ains ou wo k on he combina ion o he IC3 algo i hm wi h he
Zone abs ac ion. We s a wi h he encoding o ou o malism ia SMT- o mulae.
Subsequen ly gi ing a de ailed explana ion o ou in eg a ion o he zone compu a-
ion in IC3, we close he chap e wi h a ho ough sec ion showing he p ac icali y
and alue o ou wo k including nume ous expe imen s.
Chap e 4 p esen s ou wo k on pa ame e ized imed sys ems. I s a s wi h a
gene al in oduc ion o pa ame e ized sys ems, be o e de ining he models consid-
e ed in his wo k. To his end, we in oduce some es ic ions necessa y o yield
he no ion o symme y we in en and exploi in ou app oach. We illus a e he
inc emen al wo k low ha is he hea o ou app oach, be o e gi ing he Te mi-
na ion Theo em ha enables ou easoning abou he en i e pa ame e ized sys em.
Subsequen ly, we in oduce wo p omising op imiza ions ha accele a e he wo k-
low and inc ease he applicabili y o he heo em. Nex , we p esen he nume ous
expe imen s we ha e conduc ed and hei esul s.
In he nex chap e , we p opose an ex ension o he o malism used in ou
inc emen al wo k low o pa ame e ized imed sys ems. I signi ican ly imp o es he
16 CHAPTER 2. BACKGROUND
In addi ion he clock is ese once mo e. To gain access o he c i ical sec ion (loca ion
l3
), he p ocess mus wai o mo e han 1024 ime uni s, o cing o he p ocesses
eques ing access o upda e he alue o
id
. I he e a e no o he p ocesses,
id
s ill
con ains he same iden i ie (1) and he p ocess is allowed o ake he edge leading
om
l2
o
l3
. O he wise, he would ha e o ake he edge leading again o
l1
, which
may only be aken a e he p ocess in he c i ical sec ion le i and ese he sha ed
a iable
id
o 0. No e, ha he a iable
cn
coun s he numbe o p ocesses in he
c i ical sec ion.
The seman ics illus a ed abo e can be o malized as a ansi ion sys em as
was done, e.g., by Beh mann [Beh+04]. I is deno ed as conc e e seman ics due o a
s a e con aining only conc e e alues, meaning a single loca ion, clock and in ege
alua ion.
De ini ion 2.1.10.
Le
A= (L
,
l0
,
C
,
IV
,
Σ
,
In c
,
In i
,
E)
be de ined o e
Cg
,
IV
and
Σ
as in De . 2.1.8. The ansi ion sys em
TS = (S
,
s0
,
→)
de ines he conc e e
seman ics:
•S=L×RC
≥0×ZIV is he se o s a es,
•s0= (l0, c
0, i
0)∈Sis he ini ial s a e,
•→⊆ S×Scon ains delay ansi ions →dand edge ansi ion →e:
–(l, c, i)→d(l, c+δ, i)i ∀0≤δ0≤δ:( c+δ0)|=In c(l)
–(l
,
c
,
i)→e(l0
,
c0
,
i0)
i
∃(le,φ,ψ,ω,R
−−−−−→ l0)∈E
, s. .
c|=φ
,
c0= c[R]
,
c0|=In c(l0), i|=ψ, i0= i[ω], i0|=In i(l0).
As can be seen only unsynch onized edges (wi h synch oniza ion label
e
) can
be aken in a single imed au oma on since no synch oniza ion pa ne is a ailable.
Howe e , one o he mos con enien aspec s in modeling imed au oma a is he
abili y o composi ional modeling. We call a composed model, consis ing o se e al
imed au oma a unning in pa allel, a ne wo k o imed au oma a. These au oma a a e
modeled sepa a ely, bu in e ac wi h each o he ia clocks, in ege a iables and
synch onized edges. The downside, howe e , is he exponen ial blowup o s a es, as
he seman ics o such a ne wo k equals he p oduc au oma on. We o mally de ine
he composi ion o imed au oma a A1,...,Anas ollows.
De ini ion 2.1.11
(Ne wo k o Timed Au oma a)
.
Le
Cg
,
IV
and
Σ
be gi en, as well
as he imed au oma a
A1
o
An
de ined o e hem. Fo dis inc ion, hei pa s a e
ma ked wi h subsc ip s such ha
Aj= (Lj
,
l0j
,
Cj
,
IV
,
Σ
,
In cj
,
In ij
,
Ej)
. All se s o
clocks (
Cg
,
Cl
1
,
. . . Cl
n
) a e equi ed o be mu ually dis inc . The p oduc au oma on
de ining he ne wo k o imed au oma a
NTA =hA1
,...,
Ani
is de ined o e
Cg
,
IV
and
Σas A= (L,l0,C,IV,Σ,In c,In i,E)wi h

2.1. TIMED AUTOMATA 17
•L=L1×... ×Lnwi h ini ial s a e l0= (l01,..., l0n)∈L,
•C=Cg∪Cl
1∪... ∪Cl
nwi h ini ial alua ion acco ding o local alua ions c
0,
•In c(l1, ..., ln) = In c1(l1)∧... ∧In cn(ln),
•In i(l1, ..., ln) = In i1(l1)∧... ∧In in(ln),
•Eis de ined as
–∀i∈ {1, ..., n}:((..., li,...)σ,φ,ψ,ω,R
−−−−−→ (..., li0,...)) ∈E
i (liσ,φ,ψ,ω,R
−−−−−→ li0)∈Ei
–∀i6=j∈ {1, ..., n}:((..., li, ..., lj,...)e,φ,ψ,ω,R
−−−−−→ (..., li0, ..., lj0,...)) ∈E
i (lia!, φ1,ψ1,ω1,R1
−−−−−−−−→ li0)∈Eiand (lja?, φ2,ψ2,ω2,R2
−−−−−−−−→ lj0)∈Ej
wi h φ=φ1∧φ2,ψ=ψ1∧ψ2,ω=ω1;ω2,R=R1∪R2.
The p oduc au oma on con ains a non-synch onized edge (wi h synch oniza ion
label
e
) whe e e wo edges ha e success ully been synch onized, i.e., ha edge
is allowed o be aken. No e, ha he assignmen s o he sende edge (
m!
) a e
applied be o e hose o he ecei e edge (
m?
). Addi ionally, i s ill con ains he
o iginal edges (see he i s bulle poin de ining
E
abo e) including hose equi ing
a synch oniza ion pa ne . These a e included o u he composi ion, bu a e no
allowed o be aken as de ined in he conc e e seman ics in De ini ion 2.1.10 since
hey con ain a synch oniza ion label dis inc om e.
Ve i ica ion o p ope ies o imed au oma a was done igh om he s a
suppo ed by decidabili y esul s o Alu and Dill in 1990 [AD90]. One o he mos
impo an and in e es ing e i ica ion ques ion is eachabili y o a s a e
s
. I asks
whe he he e exis s a ini e numbe o ansi ion s eps leading om an ini ial s a e
o
s
. This e i ica ion ques ion is challenging no only due o he in ini e ansi ion
sys em in oduced by he eal alued clocks, bu also due o he s a e explosion
p oblem in gene al.
The no ion o eachabili y allows o he de ini ion o sa e y p ope ies, which
speci y ha some hing bad should ne e happen. To his end, e o s a e speci ica ions
a e de ined ha desc ibe he bad si ua ion. The sa e y p ope y holds ue, i.e., he
model is sa e w. . . he sa e y p ope y, i no e o s a e is eachable. The e i ica ion
o sa e y p ope ies is o undamen al impo ance [Hal93] as many e i ica ion
ques ions o in e es can be exp essed as sa e y p ope ies.
We o mally de ine eachabili y and sa e y p ope ies as ollows.
De ini ion 2.1.12
(Reachabili y)
.
Le a imed au oma on
A
be gi en wi h conc e e
seman ics
TS = (S
,
s0
,
→)
. A s a e
s∈S
is eachable, i he e exis s a ini e numbe o
ansi ions leading om he ini ial s a e o s, o mally s0→s1→... →sn→s.
When conside ing some s a es as bad, o e o s a es, we employ eachabili y o
de ine sa e y p ope ies ha equi e hese e o s a es o be un eachable. To his end,
18 CHAPTER 2. BACKGROUND
we de ine e o s a e speci ica ions ha a e able o e icien ly cha ac e ize e o s a es.
We employ in ege and clock cons ain s, which allows us o speci y mo e han a
single conc e e s a e a once.
De ini ion 2.1.13
(E o S a e Speci ica ion)
.
Le a ne wo k o imed au oma a
NTA =hA1
,...,
Ani
be gi en as in De . 2.1.11 wi h conc e e seman ics
TS =
(S
,
s0
,
→)
. An e o s a e speci ica ion is an abs ac o maliza ion o a se o undesi ed
s a es. The se o e o s a e speci ica ions is de ined as
ERR = ((L1∪ {∗})× · · · ×
(Ln∪ {∗})) ×Φ(C)×Ψ(IV)
. Each e o s a e speci ica ion
e = (¯
l
,
φ
,
ψ)∈ERR
includes a clock and an in ege cons ain and addi ionally a (pa ial) loca ion ec o
¯
l∈(L1∪ {∗})× · · · × (Ln∪ {∗})
speci ying a mos one loca ion o each imed
au oma on. The elemen
∗
s ands o an unde ined loca ion. To e e o speci ic loca-
ions in he ec o , we deno e he loca ion speci ied o au oma on
Ai
as
¯
l[i]
. A s a e
s= ((l1
,...,
ln)
,
c
,
i)∈S
is included in an e o s a e speci ica ion
e = (¯
l
,
φ
,
ψ)
,
deno ed s|=e , i
•∀i∈ {1, . . . , n}:¯
l[i] = ∗o ¯
l[i] = li,
• c|=φ,
• i|=ψ.
The s a es ha sa is y an e o s a e speci ica ion a e called E o S a es.
The sa e y p ope ies used wi hin his hesis speci y ha no eachable s a e is
allowed o be an e o s a e. We o mally de ine i as ollows.
De ini ion 2.1.14
(Sa e y P ope y)
.
Le a ne wo k o imed au oma a
NTA =
hA1
,...,
Ani
be gi en as in De . 2.1.11 wi h conc e e seman ics
TS = (S
,
s0
,
→)
.
Using he no a ion o o he LTL-ope a o G, we de ine a sa e y p ope y
ρ:=
G(¬e 1∧ ¬e 2. . . )
o be he conjunc ion o he nega ions o e o s a e speci i-
ca ions
e 1
,
e 2
,
. . .
. I holds ue, when no eachable s a e in
S
is an e o s a e,
o mally
∀s∈S:s is eachable ⇒(s2e 1∧s2e 2∧. . . )
. Then, we say he sa e y
p ope y is in a ian . O he wise, a leas one s a e
s∈S
is eachable ia a ini e
numbe o ansi ions
s0→s1→ · · · → sn→s
and sa is ies one o he e o s a e
speci ica ions
s|=e i
. This pa h iola es he sa e y p ope y and is, hus, called a
coun e example ace o he gi en sa e y p ope y.
Usually, he e i ica ion o p ope ies o ne wo ks o imed au oma a is done
on- he- ly wi hou he compu a ion o he p oduc au oma on, due o he eno mous
inc ease in size o s a es. Howe e , i s ill needs o ake in o accoun he in e de-
pendencies o he indi idual au oma a esul ing in eno mous e o . Thus, since
he beginning di e se a emp s ha e been made o es ablish he p ac icali y o
e i ica ion o imed au oma a.
2.1. TIMED AUTOMATA 19
2.1.1 Decidabili y and Abs ac ions
The easibili y o e i ying eachabili y p ope ies o imed au oma a was es ablished
in 1990 by Alu and Dill [AD90]. They p o ed decidabili y, which is no in ui i e due
o he eal alued clocks. To his end, hey p oposed a ini e abs ac ion o he clock
alua ions based on he obse a ion ha some o hem ha e equal cha ac e is ics.
Gi en he ac ha clocks a e only compa ed o in ege cons an s wi hin clock
cons ain s he ac ual ac ional pa o a clock alue does no ma e . This ac ional
pa is only o in e es o iden i y which clock will change i s in eg al pa i s .
Taking in o accoun ha ime p og esses simul aneously o all clocks, Alu e
al. desc ibed he egion abs ac ion, which pa i ioned he clock alua ions in o
equi alence egions.
De ini ion 2.1.15.
Le
A
be a gi en imed au oma on as in De . 2.1.8. Fo e e y
clock
x∈C
le
nx
be he la ges cons an wi h which
x
is compa ed o. Two clock
alua ions cand c0a e in he same egion, i :
•∀x∈C:b c(x)c=b c0(x)co c(x)>nx∧ c0(x)>nx,
•∀x
,
y∈C
wi h
c(x)≤nx
and
c(y)≤ny
:
ac ( c(x)) ≤ ac ( c(y))
i
ac ( c0(x)) ≤ ac ( c0(y)),
•∀x∈Cwi h c(x)≤nx: ac ( c(x)) = 0 i ac ( c0(x)) = 0.
wi h ac meaning he ac ional pa o he alue.
Since he numbe o clocks and he la ges cons an s a e ixed wi hin a imed
au oma on, he numbe o egions is ini e [AD94]. Thus, decidabili y o eachabili y
was shown since e e y eachabili y ques ion o a imed au oma on can be decided
ia his ini e abs ac ion.
Un o una ely, he numbe o egions g ows exponen ially wi h he size o
cons an s and numbe o clocks [AD94]. Hence, decidabili y ia egion abs ac ion is
an in e es ing heo e ical esul , bu no o subs an ial alue o p ac ical e i ica ion
pu poses. This d awback is ackled by he zone abs ac ion.
De ini ion 2.1.16.
AZone
Z
is a con ex se o clock alua ions, speci ied as a
conjunc ion o clock di e ence cons ain s
xi−xj./ n
wi h
xi
,
xj∈C∪ {x0=
0},./ ∈ {<,≤} and n∈Z.
Each zone is a con ex union o egions and can be desc ibed ia uppe and
lowe bounds on single clocks and clock di e ences. I can e icien ly be s o ed as a
Di e ence Bound Ma ix (DBMs) [Dil90], which allows o an e icien compu a ion
o he zones o p edecesso o successo s a es.
Thus, i gi es ise o a signi ican ly coa se symbolic ansi ion sys em ha is o
p ac ical ele ance. I is used wi hin many algo i hms and ools.
In he ollowing, we su ey he esea ch ha was done o es ablish p ac icali y o
he e i ica ion o imed sys ems.
20 CHAPTER 2. BACKGROUND
2.1.2 Rela ed wo k
We s a wi h a discussion o some algo i hms o he e i ica ion o sa e y p ope ies
o imed au oma a, ollowed by special da a s uc u e and ools. The same sequence
was also used in a su ey pape by Yo ine in 1998 [Yo 98].
The e exis a ious app oaches o he eachabili y analysis o imed au oma a.
Gi en ha s anda d exhaus i e explo a ion on he egion abs ac ion is no e icien ,
some ools apply digi iza ion o comple ely abs ac away he ime domain. To his
end, a ini e se o ep esen a i es is compu ed o ep esen each egion [Göl+94].
In gene al, digi iza ion enables he use o un imed e i ica ion algo i hms, which
a e o en mo e sophis ica ed han simple exhaus i e sea ch. Fo some es ic ed
subclasses o imed au oma a, a BDD-based ixpoin analysis [Bey01] has p o en o
be speci ically success ul. Howe e , hese echniques s ill su e om a sea ch space
exponen ially in he size o he used cons an s in he model.
Hence, coa se abs ac ions we e sough a e . One way is o ind an equi alence
ela ion ha is smalle and, hus, be e sui ed o e i ica ion. The e exis a ious
app oaches sea ching he minimal ini e ansi ion sys em equi alen o he egion
g aph up o ime-abs ac ing bisimula ion [Yo 98; TY96; Alu+92]. O he app oaches
y o minimize he imed au oma on i sel , while main aining a simila no ion o
bisimula ion [DY96].
When conside ing basic o wa d o backwa d sea ch, he u iliza ion o clock
cons ain s o desc ibe se s o clock alua ions comes na u ally. Thei conjunc ion,
deno ed a Zone, desc ibes a con ex se o clock alua ions. Due o being closed
unde ime elapse and ansi ion s eps, zones a e op imally sui ed o exhaus i e
explo a ion o he sea ch space. Fu he mo e, he esul ing zones a e e icien ly
compu able.
All hese di e en ways o abs ac ion show he non- i iali y o imed e i ica ion.
In he end, he success o he abs ac ion s ongly depends on i s combina ion wi h
cle e e i ica ion algo i hms and da a s uc u es.
Mos o en, in pa icula in combina ion wi h he egion o zone abs ac ion, a
basic exhaus i e sea ch is pe o med. S a ing om he ini ial s a e, all successo
s a es a e compu ed and added o he queue o unp ocessed s a es. This queue is
wo ked o un il he e a e no s a es le ha ha e no been p ocessed be o e. Upon
disco e y, e e y single s a e is checked o iola ion o he sa e y p ope y. Exhaus i e
sea ch can also be done in a backwa ds-manne , whe e s a es a e disco e ed s a ing
om he e o s a es. Especially when using he zone abs ac ion, his basic algo i hm
p o ides o an easy and e icien analysis. S o ed in DBMs, he memo y usage is
passable, while p o iding easy mechanisms o compu e successo -, p edecesso - o
ime-elapse-zones [Dil90; DT98]. Mo e sophis ica ed app oaches y o minimize
memo y usage by exploi ing he ac , ha mos o en some clock cons ain s in a DBM
a e edundan . The e exis a ious publica ions on how o compu e and main ain
a minimal lis o such cons ain s [YPD94; La +97]. Despi e hese op imiza ions
in memo y e iciency, one majo p oblem o he exhaus i e sea ch app oach in
combina ion wi h zones emains di icul . Each disco e ed s a e is s o ed o be
able o ell whe he a s a e has al eady been explo ed. A sho check i a new s a e
2.1. TIMED AUTOMATA 21
is al eady s o ed su ices o s op u he explo a ion on his s a e. Conside ing
zones, howe e , a simple check whe he a zone ( o a speci ic loca ion and in ege
alua ion) has al eady been s o ed is ine icien . The eason is ha he zone could
be co e ed by he union o se e al p e iously explo ed zones. Hence, a sui able
co e age check migh be needed ha s ops he explo a ion o zones co e ed by
he union o p e iously explo ed zones. Wi h zones no being closed unde union,
se e al da a s uc u es ha e been p oposed o e ing e icien mechanisms o s o e
and main ain non-con ex unions o zones wi h a as inclusion check. Howe e , in
he end hese da a s uc u es only p o ide o a ade-o educing he eno mous
amoun o memo y needed o s o ing each single zone, bu (mos o en) sligh ly
inc easing he un ime.
Mos o hese non-con ex da a s uc u es a e build as decision diag ams. P o-
posed in 1997, nume ical decision diag ams we e he i s da a s uc u e aiming
a a small ep esen a ion o unions o zones [Asa+97]. The app oach is based on
disc e iza ion o ime and employs bina y decision diag ams [Lee59; Ake78] o
s o ing a bi wise encoding o he ime alues. Thus, i hea ily depends on he size o
he encoded cons an s ende ing i ine icien o he e i ica ion o sa e y p ope ies
o mos imed au oma a. The same disad an age is obse ed in egion encoding
diag ams [Wan00]. They ep esen a egion by he in ege pa s o he clock alues
and he o de ing o he ac ional pa s. Gi en all he necessa y algo i hms o da a
manipula ion, i is sui able as a decision diag am, bu as men ioned lacks he capa-
bili y o handle la ge cons an s. La e app oaches a e no ied o a disc e ized ime o
egion encoding and a e, hus, independen o he size o iming cons an s. La sen e
al. in oduced clock di e ence diag ams (CDD) in 1998 [La +98; Beh+99] pu suing
he goal o a da a s uc u e o comple ely BDD-based e i ica ion app oaches. Clock
di e ence diag ams a e de ined o e he eal alued di e ence o clock alues. In
addi ion, hey b anch wi h ega d o in e als o he eals, while p e ious echniques
b anched only o single alues. This makes hem signi ican ly less dependen on
he size o cons an s. Designed o sha e edundan subs uc u es, clock di e ence
diag ams a e well sui ed o space-e icien co e age decisions. O he app oaches
we e no op imized o co e age checks, bu mo e on space e iciency. Reduced
clock es ic ion diag ams [Wan01a] u ilize he small numbe o cons ain s needed
o ep esen a zone [La +97]. Gi en such a minimal cons ain sys em, a compac
ep esen a ion is achie ed, which lacks he capabili y o e icien de e mina ion o
zone con ainmen . Thus, Wang enhanced his app oach esul ing in cascading clock
es ic ion diag ams [Wan02; Wan03]. The echnique is based on he cascading o m
o zones, which may equi e mo e cons ain s han he educed o m, bu s ill less
han a comple e DBM.
All hese da a s uc u es aim o educe he memo y equi ed o e i ica ion,
mos ly as a ade-o o a sligh ly inc eased un ime. While he p esen ed da a
s uc u es we e able o educe memo y consump ion in gene al, hey s ill un
ou o memo y easily when e i ying p ope ies o la ge models. Despi e hese
sho comings, hey ha e been applied in a ious e i ica ion ools, which we show
in he ollowing. The implemen a ions o all he di e en concep s and algo i hms

22 CHAPTER 2. BACKGROUND
ha e been ex emely success ul in he e i ica ion asks bo h o academic and eal
wo ld models.
O e he las 20 yea s, esea ch has led o he c ea ion o se e al ools, mos
o which a e no ac i ely main ained any mo e. The concep s used in hese ools
a e e y di e se esul ing in di e en modeling and e i ica ion capabili ies. In he
ollowing, we gi e a b ie su ey.
The de elopmen o he i s ools s a ed in he ea ly 1990s. K onos [Daw+96;
Boz+98] uses se e al o he echniques p esen ed abo e. I implemen s symbolic
analysis, as well as ime-abs ac ing bisimula ion. I employs se e al da a s uc u es,
e.g., DBMs and NDDs and igge ed a lo o esea ch. The las elease o K onos has
been in 2002 and since hen i has no been de eloped any u he . Ano he ea ly ool
o he e i ica ion o sa e y p ope ies o imed au oma a is called Uppaal [LPY95;
LPY97] de eloped by esea che s om he uni e si ies o Uppsala and Aalbo g. I is
ac i ely de eloped and main ained down o he p esen day. Gi en i s g aphical use
in e ace i o e s an easy mechanism o modeling and e i ica ion, which migh be
one o he easons o i s success e en in comme cial applica ions. The o he eason
o i s huge success is he e icien e i ica ion, which has been applied o se e al
in e es ing eal-wo ld s udies [Ha +97; LPY98; Ben+96]. I is based on cons ain
sol ing wi h DBMs ep esen ed as minimal cons ain sys ems. Fu he mo e, i
can apply CDDs and se e al op ions o op imiza ion and app oxima ion. Wi h
mo e han 15 yea s o de elopmen [Beh+11], i includes a lo o g ea ideas and
has become he mos well known ool and also quasi-s anda d o he e i ica ion o
sa e y p ope ies o imed au oma a.
Thus, la e ools mos o en had o compa e hei pe o mance wi h Uppaal. The
ool Red [Wan01b] ha was i s implemen ed using egion encoding diag ams was
de eloped in he ea ly 2000s. La e i s e i ica ion engine was based on he p esen ed
clock es ic ion diag ams. The de elopmen o Red, howe e , was discon inued in
2003.
O he ools a e based on o he echniques. A pe ec example o his so o
di e si y is he ool Rabbi [BR00], which is based on digi iza ion in o de o apply
BDD-based echniques. Tho ough in es iga ions in o he bes a iable o de ings,
and adjus ed BDD-based algo i hms showed a g ea pe o mance. Howe e , he
app oach is s ill unsa is ying as i highly depends on he size o ime cons an s.
In he las ew yea s, wo new ools ha e been de eloped ha a e capable o
e i ying imed au oma a. Syn hia [PEM11] is one o hese ools, bu has only been
ac i ely de eloped o 2 yea s, being discon inued in 2011.
The ool PAT [Sun+09], howe e , is de eloped and main ained s a ing in 2009 up
o now. I includes a wide a ie y o e i ica ion echniques including digi iza ion
and BDD-based algo i hms.
In summa y, he e has been an eno mous amoun o esea ch in he ield o
imed au oma a o e he las 25 yea s. Many echniques ha e been in es iga ed
and implemen ed in a ious ools. Howe e , oday only wo ools a e le ha a e
ac i ely main ained. These wo ep esen he mos success ul e i ica ion app oaches,
as Uppaal hea ily elies on zone based e i ica ion and PAT u ilized digi iza ion
2.2. SAT- & SMT-SOLVING 23
wi h BDD-based e i ica ion. Wi h he la e being dependen on he size o ime
cons an s, i is concep ually less ele an . Thus, we will examine he echniques
p esen ed in he ollowing chap e s in compa ison wi h Uppaal. E en a e 15
yea s o esea ch, Uppaal can easily be pushed o i s limi s. As a eason o ailed
e i ica ion a emp s, mos o en i s eno mous need o memo y has o be named.
In consequence, o his hesis we a e in e es ed in echniques wi h be e memo y
e iciency.
2.2 SAT- & SMT-Sol ing
In addi ion o he echniques p esen ed be o e, he e exis a ious concep s employ-
ing SAT- o SMT-sol e s o e i ica ion. We p esen a sho o e iew on SAT- and
SMT-sol ing ha migh be help ul o unde s and Chap e s 3 o 6.
2.2.1 SAT-Sol ing
The boolean sa is iabili y p oblem is de ined as ollows:
De ini ion 2.2.1.
Le a boolean o mula be gi en. The boolean sa is iabili y p oblem
(
SAT
) asks whe he he e exis s an in e p e a ion, meaning a consis en assignmen
o u h alues
ue
o
alse
o he p oposi ional a iables, ha e alua es he o mula
o ue. I is called a sa is ying in e p e a ion.
I he e exis s a sa is ying in e p e a ion, he o mula is said o be sa is iable,
o he wise i is called unsa is iable.
Va ious ools, called SAT-sol e s, exis ha y o answe he boolean sa is iabili y
p oblem. The p oblem is undamen al o complexi y heo y and has been subjec o
esea ch o many decades. In 1971 i was p o en o be
NP −comple e
[Coo71], how-
e e , a lo o esea ch on e icien algo i hms and heu is ics build up he p ac icali y
o oday’s ools, e.g., MiniSAT [ES05], PicoSAT [Bie08] o o he s [Bie12; AS12; LP10].
Mos o he ools a e based on con lic -d i en clause lea ning algo i hms building
on he DPLL app oach, named a e he esea che s Ma in Da is, Hila y Pu nam,
Geo ge Logemann and Donald W. Lo eland [DP60; DLL62]. The algo i hm assigns
a u h alue o li e als and a e wa ds p opaga es hem o simpli y he emaining
clauses. Upon disco e y o a con lic , he algo i hm lea ns a clause ep esen ing he
cause o he con lic and back acks. Mos SAT-sol e s equi e he boolean o mula
o be in conjunc i e no mal o m, which is no a p oblem due o algo i hms o
sa is iabili y-p ese ing ans o ma ions [Tse83; PG86] in polynomial ime.
In 1999 he usage o SAT-sol e s ound i s way in o he domain o un imed o mal
modeling and e i ica ion o ini e s a e ansi ion sys ems. The eason was ha
ea lie echniques such as explici model checking o BDD-based app oaches eached
hei limi s due o scalabili y issues. Bie e e al. [Bie+99] in oduced he concep
o Bounded Model Checking in o de o check ansi ion sys ems o coun e example
aces o bounded leng h. The echnique elies on an encoding o a bounded
un olling o he ansi ion ela ion as a boolean o mula o check o an e o pa h o
24 CHAPTER 2. BACKGROUND
ixed leng h in he model. The o mula is issued o a SAT-sol e . In case he sol e
e u ns
unsa is iable
, he e exis s no such pa h. O he wise, he e u ned sa is ying
in e p e a ion embodies he ound e o pa h.
Due o he success o Bounded Model Checking, he applica ion o SAT-based
echniques o o mal e i ica ion ad anced. Concep s we e p esen ed ha we e
no limi ed o a bounded explo a ion o he s a e space, e.g., by McMillan [McM02].
O he wo k ex ended he capabili ies o bounded model checking by compu ing
C aig In e polan s om unsa is iabili y p oo s [McM03]. In eg a ed in an i e a i e
ixpoin compu a ion, hese a e used o compu e an o e -app oxima ion o he
eachable s a es and p o e he absence o coun e example aces.
In addi ion, SAT-sol ing is applied also in abs ac ion-based easoning, called
coun e example-guided abs ac ion e inemen (CEGAR) [Cla+02; Cha+02]. To his
end, abs ac coun e examples a e checked o spu iousness using SAT-que ies and
possible e inemen s a e done based on he esul s o he sol e .
Fu he applica ions o SAT-sol ing include app oaches elying on induc ion. We
discuss hese echniques in mo e de ail in Sec ion 2.3.
Many o he abo e echniques ha e been ans e ed o he domain o imed
sys ems. Howe e , wi h ime being ep esen ed by unbounded eal alued clocks,
an encoding using boolean a iables is non- i ial. Thus, mos app oaches ely on
an ex ension o boolean sa is iabili y, which we p esen in he ollowing.
2.2.2 SMT-Sol ing
The Sa is iabili y Modulo Theo ies-p oblem is a gene aliza ion o he boolean sa is i-
abili y p oblem. I deno es he sea ch o a sa is ying in e p e a ion o a o mula
in i s -o de logic, whe e some symbols ha e ixed in e p e a ions de e mined by
backg ound heo ies. The e exis s a la ge a ie y o such heo ies, some o which
a e speci ically designed o eason abou da a s uc u es like bi ec o s o a ays.
In he con ex o his wo k, howe e , we a e mos in e es ed in he heo y o eals,
which enables he SMT-sol e o handle eal- alued a iables in combina ion wi h
ope a o s, e.g., addi ion and mul iplica ion. Fu he mo e, he heo y o in ege s may
be employed o encode in ege a iables. The use o hese heo ies esul s in an easy
and na u al way o encode imed sys ems as logical o mulae.
These can be issued o an SMT-sol e asking o sa is iabili y. I he SMT-
o mula is sa is iable, he sa is ying in e p e a ion, also called SAT-Model is e u ned.
O he wise, he o mula is unsa is iable and he sol e may e u n an UNSAT-Co e,
which iden i ies hose pa s o he o mula ha ake pa in i s unsa is iabili y.
Va ious SMT-sol e s exis [DB08; Du 14; CHN12; Cim+13b; Ba +11] and al hough
mos o hem accep he same inpu o ma , s anda dized as SMT-Lib [BST10], hey
di e in hei capabili ies and algo i hms. Mos mode n SMT-sol e s use he lazy
app oach, which is based on an ex ension o he DPLL-algo i hm, called DPLL(T)
[NOT06]. In gene al, a un o a SAT-sol e de e mines candida e assignmen s
o he boolean s uc u e whose sa is iabili y would esul in he sa is iabili y o
he whole o mula. A e wa ds, hese assignmen s a e checked by heo y sol e s
2.3. INDUCTION BASED REASONING 25
whe he hey comply wi h he heo ies. A close in eg a ion o hose heo y sol e s
wi hin he DPLL-algo i hm has shown as success ul basis o SMT-sol e s. Fu he
imp o emen s and he ich use o heu is ics led o a huge success o hese ools.
Al hough hei e iciency is a bi behind he one o SAT-sol e s, SMT-sol e s
a e employed e icien ly in many domains and a e capable o sol ing e y di e se
SMT-ins ances. Gi en hei exp essi eness, hey a e an easy and na u al way o
encoding imed sys ems.
Thus, many o he SAT-based model checking app oaches ha e been ans e ed
o he domain o SMT, including hei employmen o he e i ica ion o sa e y
p ope ies o imed au oma a. Bounded Model Checking has been one o he
i s employmen s o SMT-sol e s o he e i ica ion o sa e y p ope ies o imed
au oma a. S a ing in 2002, a la ge numbe o wo ks has been published om
a a ie y o esea che s [PWZ02; Aud+02; So 03; KJN12a]. All hese wo ks use
SMT-encodings o pa hs in he imed sys ems, bu di e in nuances and esea ch
ocus. SMT is he enabling echnique o hese con ibu ions, as hey employ he
heo y o eals o encode he eal- alued clocks.
In e pola ion-based easoning has also been ans e ed o be used wi h in ini e
sys ems [McM05] like imed au oma a. Howe e , apa om he men ioned app oach
o in ini e sys ems in gene al, i was no in he ocus o esea ch.
In addi ion o he p esen ed wo k, a lo o echniques based on induc ion ha e
been ans e ed om he SAT domain o SMT-sol ing.
2.3 Induc ion based Reasoning
Induc ion is a p oo -p inciple o high in e es . Checking whe he a p ope y is
induc i e o no is e icien and i ial since i does no in ol e an un olling o he
ansi ion sys em.
The ollowing explana ions ely on he no ion o a ansi ion sys em, which may
be in ini e, as can be seen in De ini ion 2.1.10.
De ini ion 2.3.1
(T ansi ion Sys em)
.
A ansi ion sys em
A= (S
,
I
,
T)
is de ined
o e a se o s a es
S
wi h ini ial s a es
I⊆S
. A ansi ion ela ion
T⊆S×S
de ines
he passage om s a e o s a e. We deno e a ansi ion sys em o be a ini e s a e
ansi ion sys em (FTS), whene e Sis ini e.
We de ine induc ion and ela ed concep s using SAT- o SMT-encodings. These
encodings usually employ dis inc se s o a iables
x
,
x0
,
x00
,
. . .
o encode he di e -
en s a es occu ing on a pa h. We le
kI(x)k
and
kρ(x)k
deno e he encodings o he
ini ial s a es, and hose s a es ha sa is y he p ope y
ρ
, espec i ely. Addi ionally,
kT(x
,
x0)k
encodes he ansi ion ela ion, whe e he p imed a iables e e o he
nex s a e as explained abo e. Using hese encodings wi hin que ies o SAT- o
SMT-sol e s, hei unsa is iabili y can be used o check whe he ce ain p ope ies
like induc ion a e sa is ied.
32 CHAPTER 2. BACKGROUND
This blocking p ocess can be seen as a sequence o exclusions s a ing om
F0
up o
Fn
. Wi h
s
being no ini ial s a e, i is no a membe o
F0
. The unsa is iabili y
o
kF0k ∧ ¬ksk∧kTk∧ksk0
assu es ha
s
is un eachable in one ansi ion om
F0
and can be excluded in
F1
. The unsa is iabili y o
kF1k ∧ ¬ksk∧kTk∧ksk0
assu es
ha
s
is un eachable in one ansi ion om
F1 {s}
and can be excluded in
F2
. The
sequence goes o h un il scan be excluded om Fn.
Howe e , he que y o induc i e ela i eness migh be sa is iable o some
obliga ions. In ha case, a s a e
(dis inc o
s
) exis s ha is a p edecesso o
s
and
is a membe o
Fn−1
. The s a e
p e en s he exclusion o
s
om
Fn
, since i hinde s
¬s
om being induc i e ela i e o
Fn−1
. I is, hus, a Coun e example o Induc ion
and needs o be excluded om
Fn−1
in o de o be able o e en ually exclude
s
om
Fn
. Line 39 shows he c ea ion o a new obliga ion
(
,
n−
1
)
ha exp esses his ac .
In a e y speci ic case, such an obliga ion does no need o be c ea ed as he
exclusion o
om
Fn−1
is no possible. Line 33 checks whe he
Fn−1=F0
, which
means we need o block a s a e om
F0
, which is no possible since
F0
con ains
exac ly he ini ial s a es (c . line 6). Thus, IC3 ound he p edecesso
o ano he
CTI s, which is i sel a p edecesso .
Following he ound lis o p edecesso s c ea es a pa h om an ini ial s a e o
an e o s a e, meaning a coun e example ace has been ound and IC3 e mina es
(lines 35, 23 and 9). I no such coun e example is ound, e en ually all obliga ions a e
wo ked o (line 31 educes he numbe o obliga ions) and he blocking p ocedu e
inishes. I e u ns o he s eng henClauses p ocedu e, which checks o u he
p edecesso s o e o s a es o be blocked in o de o e en ually c ea e he nex
ame.
One o he mos impo an aspec s o IC3, howe e , is he ac ha i does no
exclude a single s a e
s
. Ins ead, i gene alizes he s a e s in o a se o s a es ha a e
o be blocked (line 32).
To his end, i employs a Gene aliza ion p ocedu e depic ed in Lis ing 2.4.
Lis ing 2.4: Gene aliza ion algo i hm in IC3
44 gene alizeAndBlock ( s,n ) {
45 ind minimal subclause kcko ¬ksk, s . .
46 kF0k ∧ ¬kckis unsa is iable
47 kFn−1k ∧ kck ∧ kTk ∧ ¬kck0is unsa is iable
48 o ( in i =1; i≤n ; i ++)
49 kFik:=kFik ∧ kck;
50 }
Employed p io o blocking he s a e
s
om
Fn
, i sea ches a minimal subclause o
¬ksk
ha is induc i e ela i e o
Fn−1
. Such a minimal subclause always exis s, since
¬s
i sel is induc i e ela i e o
Fn−1
(line 30). Howe e , he sea ch is non- i ial
since mono onici y is no gi en o he consecu ion que y o ela i e induc i eness
o he subclauses. The emo al o a single li e al in he subclause migh des oy he
consecu ion p ope y al hough i held be o e. In addi ion, he emo al migh also

2.4. IC3 33
e-es ablish consecu ion al hough i did no hold o he subclause be o e emo ing
he li e al. The eason is
c
and
¬c0
being al e ed a he same ime, whe e he emo al
o a li e al s eng hens
c
, bu weakens
¬c
. Thus, he sea ch o such a minimal
subclause is ha d. Mos implemen a ions ely on wo o mo e combined app oaches.
On he one hand, he manual d opping o single li e als one by one can be checked
wi h a sho que y o he sol e . I he que y e u ns unsa is iable, he subclause is
s ill induc i e ela i e, o he wise, he d opped li e al is pu back in he clause. This
manual emo al elies on heu is ics o de e mine he o de in which li e als a e ied
o be d opped. While his is a alid app oach, i is only capable o es ing he emo al
o one li e al a a ime. Using ex ended concep s o SAT-sol ing, his d awback
can be educed. In case he subclause is s ill induc i e ela i e a e he emo al o
a li e al, he que y is ound o be unsa is iable, which allows he ex ac ion o an
unsa is iabili y co e (UNSAT-Co e). Such a co e is used o dele e all hose li e als o
he subclause ha a e no needed in p o ing he o mula unsa is iable. The emo al
o hese li e als is a sa e op ion i he ini ia ion p ope y is no iola ed by doing
so. Using his app oach, mos implemen a ions do no ac ually ca e o ind he
minimal subse , bu in con as sea ch o a small one in easonable ime. Due o his
non-op imali y and he emo al o se e al li e als de e mined by he UNSAT-co e,
he heu is ics play an impo an ole in s ee ing o he gene aliza ion.
Ha ing ound a gene alized clause
kck
o
¬ksk
, i is conjoined o e e y o mula
kF0k
up o
kFnk
(lines 48 and 49). This conjunc ion excludes he s a e
s
om he
ames, as well as many mo e s a es (in case cis a s ic subclause).
The bene i o his gene aliza ion p ocedu e is a as e inemen and small clauses
compu ed in a ai ly e icien way.
In addi ion, a second p ocedu e exis s ha p o ides o a as e inemen . The
pseudocode depic ing his P opaga ion s ep is shown in Lis ing 2.5.
Lis ing 2.5: P opaga ion algo i hm in IC3
51 p opaga eClauses( in k){
52 o ( in i =1; i<k ; i ++)
53 o each clause kckin kFik:
54 i (kFik ∧ kTk ∧ ¬kck0unsa is iable)
55 kFi+1k:=kFi+1k ∧ kck;
56 }
The p ocedu e pushes lea ned clauses o subsequen ames whene e possible,
p o iding s eng hened ames o he nex cycle and, hus, a be e guided e ine-
men . To his end, IC3 checks all clauses o each ame o ela i e induc ion. I a
clause
c
is induc i e ela i e o a ame
Fi
, i can be p opaga ed o
Fi+1
, e ining
Fi+1
ia conjunc ion as depic ed in line 55. Since no s a e ou side o
c
can be eached
om Fiwi hin one ansi ion, his e inemen does no des oy he 4 p ope ies.
The p opaga ion p ocedu e is subjec o se e al icks in e icien implemen a ions.
By s o ing clauses in a da a s uc u e ha associa es hem only wi h he la ges
ame wi h which hey a e conjoined, each clause is es ed only once o p opaga ion.
34 CHAPTER 2. BACKGROUND
Fu he mo e, subsump ion checks a e o en applied in his phase in o de o il e
ou obsole e clauses ha a e no needed any longe .
Co ec ness
All hese di e en p ocedu es and phases main ain he ou p ope ies
o he ames, such ha in he end IC3 is a success ul algo i hm o compu ing
induc i e s eng henings. We will sho ly gi e an in ui ion why hese p ope ies
hold du ing all he phases and why he algo i hm e mina es o ini e s a e ansi ion
sys ems. These can be ound in mo e de ail in he wo k o B adley e al. [B a11].
Du ing he ini ial phase o he algo i hm (lines 1 o 6), IC3 ensu es ha he e
exis no e o s a es ha a e ini ial o eachable om an ini ial s a e by a single
ansi ion s ep. Thus, he i s wo ames
F0=I
and
F1=ρ
can be c ea ed and
adhe e o he ou gi en p ope ies. In pa icula , P ope y 1 is ensu ed by
F0
being
equal o he ini ial s a es. P ope y 2 is ensu ed in line 2 since
ρ
includes all ini ial
s a es, while P ope y 3 is ensu ed in line 4. The las p ope y is ob iously ue due
o P ope y 2 and F1being equal o ρ.
These p ope ies a e main ained du ing each cycle o he main algo i hm (lines
7-15). They a e no iola ed by he call o unc ion s eng henClauses and emain
in ac du ing he call o p opaga eClauses as we will see below. Finally, he c ea ion
o a new on ie
Fk+1=ρ
adhe es o he p ope ies. Since i does no al e he
o he ames, i emains o show ha
kFkk ∧ ¬kFk+1k
,
kFkk∧kTk ∧ ¬kFk+1k0
and
kFk+1k ∧ ¬kρk
a e unsa is iable be o e he inc emen a ion o
k
(line 14) and s a ing a
new loop. The la e is ue by de ini ion o
Fk+1
and he i s one is ue by P ope y
4 o all smalle ames. The ac ha
kFkk∧kTk ∧ ¬kFk+1k0
is unsa is iable has
been es ablished by s eng henClauses(), as i ensu ed ha no di ec p edecesso o an
e o s a e is included in Fk(line 18).
We now conside he me hod s eng henClauses(). Du ing i s un, he 4 p ope ies
a e p ese ed and when e u ning ue, he e exis s no s a e in he ame
Fk
ha is a
di ec p edecesso o an e o s a e. The me hod i sel does no al e he ames, bu
howe e calls unc ion blockCTIs({(s,k)}) o block he di ec p edecesso
s
o an e o
s a e in he ame
Fk
. This is done un il no such p edecesso s a e le . Wha emains
o be shown is ha blockCTIs success ully blocks he ound CTIs while p ese ing
he 4 p ope ies.
The unc ion blockCTIs() wo ks o a lis o obliga ions un il none is le . The
ames a e only al e ed when calling he unc ion gene alizeAndBlock(s,
n
). This is
only done when
¬s
was ound o be induc i e ela i e o
Fn−1
in which case i is also
induc i e ela i e o all smalle ames. The unc ion gene alizeAndBlock(s,
n
)sea ches
o a minimal subclause
c
o
¬s
ha is s ill induc i e ela i e. This clause is added o
F1
up o
Fn
al e ing he ames and success ully blocking
s
om
Fn
. The 4 p ope ies,
howe e , a e p ese ed. In pa icula , P ope y 1 s ill holds, as
F0
is un ouched and
P ope y 4 holds due o ames being s eng hened. P ope y 2 s ill holds since
kF0k ∧ ¬kck
is unsa is iable (line 46) and
c
is added o all
F1
up o
Fn
. Since P ope y
3 p e iously held ue and ela i e consecu ion (line 47) o clause
c
holds, he e ined
ames s ill sa is y P ope y 3. Thus, he me hods gene alizeAndBlock, blockCTIs and
s eng henClauses p ese e he 4 p ope ies o he ames.
2.4. IC3 35
In addi ion, he unc ion p opaga eClauses also p ese es hese p ope ies due o
he same easoning o e ela i e induc i eness. Hence, in o al, he 4 p ope ies a e
main ained o he ames a e and du ing he main loop, allowing he algo i hm o
ind an induc i e s eng hening, i one exis s.
Te mina ion
The algo i hm will always e mina e o a ini e s a e ansi ion sys em.
Wi h he ames being a non-dec easing sequence o se s o s a es and he algo i hm
s ill unning, meaning i did no e mina e due o wo ames being equal, each
ame has o include a leas one addi ional s a e compa ed o he nex smalle
ame. Tha means he e can only exis
|S|
ames a he same ime o a ini e
s a e ansi ion sys em as de ined in De ini ion 2.3.1. Thus, he main loop o he
algo i hm will e en ually e mina e, p o ided ha he unc ions s eng henClauses
and p opaga eClauses e mina e.
S eng henClauses will e mina e when no di ec p edecesso o an e o s a e
emains in ame
Fk
. Assuming he unc ion blockCTIs success ully blocks each ound
p edecesso , s eng hen mus e mina e a e a mos
|S|
uns o i s while loop. The
unc ion blockCTIs will always e mina e. The lis o obliga ions can only con ain
|S| × k
obliga ions. P o ided ha he call o gene alizeAndBlock e mina es and indeed
blocks he s a e
s
om ames
F0
o
Fn
, he lis o obliga ions will e en ually be
wo ked o o a coun e example is ound. Due o he blocking, an obliga ion can
no be ound again in he same un o blockCTIs a e being wo ked o . Thus, he
me hod will e mina e.
Each call o unc ion gene alizeAndBlock e mina es and success ully blocks s a e
s
in ames
F0
o
Fn
. The eason is ha only a ini e numbe o subclauses exis and,
hus, he minimal subclause can be ound. Such a minimal subclause always exis s,
since
¬s
i sel is induc i e ela i e o
Fn−1
. In summa y, each call o s eng henClauses
will e mina e.
In addi ion, each call o he unc ion p opaga eClauses e mina es since
k
is ini e
and he numbe o clauses in a ame is ini e.
Summing up, all unc ions called by he main loop e mina e and he main loop
i sel also e mina es due o adding a new ame each cycle, o which he e a e only
ini ely many.
The a gumen a ions abou e mina ion and co ec ness a e ca ied ou o mally
and in mo e de ail in he i s pape on IC3 by Aa on B adley [B a11].
2.4.2 Op imiza ions
As men ioned abo e, he e exis s a la ge communi y o esea che s ying o imp o e
and op imize IC3 o ans e i o di e en domains. Some o he op imiza ions and
imp o emen s a e speci ically ailo ed o he domain o applica ion ( o example
e na y simula ion in ha dwa e e i ica ion), while o he s a e mo e gene al. In he
ollowing, we p esen and discuss some o hem.
Many op imiza ions a ge he me hod o gene aliza ion (Lis ing 2.4). Hassan e al.
[HBS13] p oposed o u ilize Coun e examples o Gene aliza ion, meaning p edecesso
36 CHAPTER 2. BACKGROUND
s a es ound du ing he gene aliza ion p ocedu e. These a e used in o de o
in e addi ional clauses ha adhe e o he ela i e induc i eness p ope y. Thus,
he app oach u ilizes unsuccess ul ies o inding subclauses, howe e , i is no
gua an eed ha he in e ed clauses a e indeed help ul. In gene al, he op imiza ion
is e alua ed as success ul.
Chockle e al. [Cho+11] u ilize an addi ional SAT-que y as a p elimina y
s ep o gene aliza ion. Designed o ha dwa e e i ica ion hey sea ch o pa ial
assignmen s o a CTI by encoding he ansi ion wi h which he CTI is ound, bu
nega ing he successo s a e. Due o being de e minis ic o he speci ic se o inpu
alues, no dis inc successo s a e exis s, ende ing he SAT-que y unsa is iable.
Chockle ex ac s a pa ial assignmen o he CTI om he UNSAT-Co e, he eby
po en ially gene alizing he CTI.
A simila e ec is he esul o e na y simula ion, as p oposed o use in IC3
by Een e al. [EMB11]. Using h ee alued logic, he e ec o emo ing li e als is
p opaga ed h ough he ha dwa e ci cui and in he end de ines whe he he emo ed
li e al is o use o no . The same pape also p oposed se e al o he op imiza ions,
including a a ia ion o he ou p ope ies o he ames and a a ian o he
algo i hm ha does no need he wo basic checks (lines 2-5). In addi ion, hey
p opose cle e ways o o ganizing obliga ions, as well as he clauses in he ames.
The esul ing implemen a ion, called P ope y Di ec ed Reachabili y (PDR) p o ed o
be supe io o he o iginal implemen a ion and, hus, go adap ed as a synonym o
IC3.
O he imp o emen s use he p opaga ion phase as s a ing poin . Suda [Sud13]
p oposed o igge he p opaga ion o clauses only i possible. To his end, he keeps
ack o wi nesses ha hinde he p opaga ion o a clause. Only i such a wi ness is
no alid any mo e, he p opaga ion o he clause is ied. The app oach seems o
wo k well.
O he a ian s, howe e , did no p o e o be o subs an ial alue, as can o
example be seen in he o iginal pape by B adley [B a11]. He p oposed a a ia ion
o he blocking p ocedu e ha sea ches a subclause induc i e ela i e o a la ge
ame han
Fn−1
(c . Lis ings 2.3 and 2.4). I s pe o mance, howe e , was wo se o
speci ic ha dwa e designs due o being unable o use he UNSAT-Co e.
In summa y, a lo o esea ch has been success ul o a ious ex end in imp o ing
and op imizing IC3 i sel .
The e also exis s wo k on he eusage o e i ica ion esul s as is o in e es
in his hesis. Wi h ha dwa e models changing o en du ing he design p ocess,
Chockle e al. [Cho+11] u ilize a p e iously compu ed induc i e s eng hening o
he e- e i ica ion o he changed model. They apply an op imized SAT-encoding
in o de o ind a subse o clauses o he induc i e s eng hening ha a e s ill
induc i e in he changed model. The ound (induc i e) clauses a e hen injec ed in
he e- e i ica ion in o de o speed i up.
In addi ion o his inc emen al way o using IC3, he algo i hm has also been
applied in comple ely di e en con ex s and domains. Some wo k was done on
2.4. IC3 37
ans e ing IC3 o domains dis inc om ha dwa e e i ica ion and on combina ions
o IC3 wi h o he echniques.
Hassan e al. [HBS12] u ilize he idea o IC3 being inc emen al and induc i e o
CTL-model checking. They success ully build a p ope y-di ec ed abs ac ing model
checke o CTL wi h ai ness.
Baumga ne e al. [Bau+12] apply IC3 in he ha dwa e e i ica ion domain in
o de o compu e abs ac ions. They analyze he ames in an incomple e un o IC3
using heu is ics in o de o ob ain p io i ies o s a e a iables. On he basis o hese
p io i ies, a localiza ion abs ac ion e inemen is guided.
Ano he app oach di ec ly combines IC3 wi h abs ac ion and u ilizes CTIs o
e inemen . In con as o he o iginal CEGAR app oach, he echnique o Bi gmeie
e al. [BBW14] u ilizes single s a es ( he CTIs) o e inemen o he abs ac ion,
while he o iginal app oach uses coun e example aces. The ocus on CTIs enables
wo dis inc poin s o igge ing he e inemen o he abs ac ion and, in addi ion,
enables a choice o delaying he e inemen .
Mo e gene al wo k examines IC3 om a b oade pe spec i e. Bayless e al.
[Bay+13] in oduce he concep o SAT modulo SAT, which wo ks simila o lazy
SMT-sol e s. They u ilize he concep o hei implemen a ion o IC3, which p o es
o be success ul.
IC3 is also applied as co e abili y check o well s uc u ed ansi ion sys ems, in
pa icula pe i ne s. Kloos e al. [Klo+13] p opose an IC3-based algo i hm o his
ask. Thei implemen a ion is SAT-based wi h p edecesso and ela i e induc i eness
compu a ions being di ec ly applied on he pe i ne .
The concep s o IC3 ha e also been ans e ed o domains ha equi e o he
concep s han SAT-sol ing. Fo example, he applica ion o IC3 o game sol ing
(Mo gens e n e al. [MGS13]) equi es a QBF-sol e . As a second example, he usage
o IC3 o planning p oblems (Suda [Sud14]) s icks ou wi h he absence o a sol e .
Ins ead, Suda delega es he asks o he sol e o a speci ic planning p ocedu e.
In gene al, mos app oaches ha do no ely on SAT-sol ing apply he concep
o SMT-sol ing.
2.4.3 IC3 wi h SMT
Cima i e al. we e he i s o combine IC3 wi h he concep o SMT-sol ing in o de
o model check so wa e [CG12]. Apa om changes o he algo i hm in o de o
suppo so wa e model checking based on he con ol- low g aph, hey apply a
quan i ie elimina ion p ocedu e in linea eal a i hme ic o cope wi h he po en ial
in ini y o CTIs in a single blocking phase.
O he app oaches y o be less heo y-speci ic. A combina ion o IC3 using
SMT wi h abs ac ion also p oposed by Cima i e al. [Cim+14] allows o handle
a wide ange o backg ound heo ies. Du ing he un o he algo i hm an implici
abs ac ion is compu ed ha is e ined, whene e a spu ious coun e example is
ound. The wo k can, hus, be seen as an ins ance o CEGAR.

38 CHAPTER 2. BACKGROUND
Cima i also applied IC3 wi h SMT in o de o syn hesize pa ame e s [Cim+13a].
Relying on a quan i ie elimina ion p ocedu e, he algo i hm sea ches o pa am-
e e combina ions ha allow coun e example aces. G adually excluding hese
combina ions, he ool in he end e u ns a se o sa e pa ame e combina ions.
Wi h imed sys ems in mind, we a e speci ically in e es ed in applica ions o IC3
using linea eal a i hme ic, o which some exis . Hode e al. [HB12] gene alized
he PDR algo i hm o usage wi h nonlinea ans o me s (used, e.g., o modeling
so wa e wi h p ocedu es), in which coun e examples un old o ees ins ead o
pa hs. In he same wo k hey apply PDR o linea eal a i hme ic. Thei wo k
applies in e pola ion in he gene aliza ion p ocedu e in o de o ensu e decidabili y
o he eachabili y o imed push-down sys ems. Bjø ne e al. ex end he p e ious
concep [BG14]. They p opose h ee a ia ions o he gene alized PDR algo i hm o
linea eal a i hme ic. The i s one is basically a ede ini ion o he pu e gene alized
PDR algo i hm applying quan i ie -elimina ion-based p ojec ion o ex ac CTIs,
while he o he wo es ic hemsel es o ind speci ic induc i e in a ian s. In he
second algo i hm, he ames a e de ined as con ex polyhed a, meaning conjunc ions
o linea inequali ies. Thus, he algo i hm is able o compu e a con ex polyhed on
as induc i e in a ian . Con a y o his app oach, he au ho s also p esen a a ian
o gene alized PDR ha is able o compu e co-con ex in a ian s, deno ing he
complemen o a con ex polyhed on.
The la e wo echniques a e, howe e , no sui ed o imed au oma a e i ica ion
as hey do no eason abou disc e e pa s, e.g., loca ions o a imed au oma on.
The app oaches men ioned p io o hese wo include such capabili ies. Howe e ,
hei usage o in e pola ion and quan i ie elimina ion is a gene ic mechanism. In
con as , we expec mo e speci ic echniques designed o imed au oma a o be
be e sui ed. The combina ion o disc e e and con inuous componen s in a imed
au oma on pe mi s adjus ed mechanisms, which is done in he app oach p esen ed
below.
2.4.4 IC3 o TA
Kinde mann e al. [KJN12b] applied IC3 speci ically ailo ed o imed sys ems. As
explained be o e, his design decision allows se e al gene al op imiza ions o IC3.
His app oach, howe e , was no compe i i e.
The in ini y o clock alua ions inhe en in con inuously imed sys ems poses
he main challenge o IC3. When li ing he algo i hm o SMT by encoding he
sys em ia SMT- o mulae, he s eng hen phase is no longe gua an eed o e mina e.
The blocking phase blocks he CTI, which is a single conc e e s a e o he in ini e
ansi ion sys ems as de ined in De ini ion 2.1.10. Since he e possibly exis in ini ely
many s a es all sa is ying he que y in line 18, he s eng hen phase migh ne e
e mina e o only i he gene aliza ion blocks all o hem by chance. The same
a gumen s can be used in o de o explain a possibly in ini e un o he blocking
phase, whe e also in ini ely many CTIs migh exis .
Thus, modi ica ions o he algo i hm a e needed o ensu e e mina ion. To his
2.4. IC3 39
end, he decidabili y esul o eachabili y p ope ies o imed au oma a migh ha e
led he way o he app oach o Kinde mann e al. [KJN12b]. Wi h decidabili y
being p o en ia a ini e, eachabili y equi alen abs ac ion, he idea o composing
all clock alua ions ha a e indis inguishable o he imed au oma on seemed like
a good candida e. Thus, he egion abs ac ion was employed due o being ini e
and easily compu able o a single s a e.
Kinde mann uses he o iginal IC3 app oach, bu encodes he imed sys em ia
SMT- o mulae. The algo i hm is un as usual, bu whene e a CTI is ex ac ed, a
speci ic echnique is applied. As in he o iginal app oach, he ex ac s he conc e e
s a e om he sa is ying SMT-in e p e a ion. A e wa ds he applies an abs ac ion
p ocedu e ha eplaces he conc e e clock alua ion o he conc e e s a e wi h i s
unique, su ounding egion in o de o o m an abs ac s a e used as CTI. Wi h
only ini ely many egions, he abs ac ion elimina es he isk o possibly ha ing
in ini ely many CTIs, ensu ing he e mina ion o he algo i hm.
Al hough he su ounding egion o a conc e e clock alua ion is e icien ly
compu able, he egion abs ac ion is no well sui ed o be used in p ac ical appli-
ca ion, as has been explained be o e. The abs ac ion is e y ine g ained and he
numbe o egions hea ily depends on he cons an s used in he imed au oma on.
The combina ion o hese wo cha ac e is ics ensu es a huge numbe o egions,
ende ing he algo i hm ine ec i e, in pa icula o la ge cons an s. Kinde mann’s
e alua ion o his app oach showed a good scalabili y in e ms o model size, bu
does no deal well wi h la ge cons an s. While being a nice heo e ical concep , he
combina ion o IC3 wi h he egion abs ac ion o imed sys ems p o ed o be o no
p ac ical alue. Kinde mann p oposed some speci ic op imiza ions gene alizing he
CTI up on be o e he gene aliza ion p ocedu e o IC3 was applied. Howe e , hese
sugges ions could no es ablish p ac icali y.
Ye , he basic idea has shown o be e y in e es ing since i allows o bene i om
u u e, gene al IC3 imp o emen s and op imiza ions. Fo his eason, ou app oach
p esen ed in Chap e 3 builds on i .
Summing up, he wo k closes o ou s is he one o Kinde mann e al. [KJN12b]
p oposing o use IC3 wi h he egion abs ac ion o imed sys em e i ica ion. In
addi ion, he wo k o Chockle e al. [Cho+11] is closely ela ed o ou objec i e o
handling econ igu a ions. In Chap e s 4 o 6 we will pick up his concep in o de
o imp o e he e i ica ion o sa e y p ope ies o econ igu ed imed models.
3
Timed Au oma a Ve i ica ion ia
IC3 wi h Zones
Many o oday’s sys ems a e sa e y c i ical, which exp esses he need o hei
co ec unc ioning a all imes. O he wise, undesi ed beha io could esul in a
loss in alue, e.g., when a p oduc ion is s opped, o e en be a h ead o li e and
physical condi ion. As a coun e measu e, model-based design p ocesses in oduce
a s uc u ed p ocedu e in which models o he sys ems a e buil . Then, o mal
me hods a e employed o check whe he speci ied p ope ies a e ul illed. Wi h
an inc easing numbe o sys ems elying on eal- ime communica ion, o being
eal- ime ope a ing sys em, he e exis s a demand o imed models and e i ica ion.
As de ailed in he p e ious chap e , ne wo ks o imed au oma a a e amongs he
mos impo an modeling o malisms ha inco po a e ime. Wi h oughly 25 yea s
o esea ch, his modeling o malism is well unde s ood and he e exis many
sophis ica ed algo i hm o he e i ica ion o sa e y p ope ies o hese models.
Howe e , hese algo i hms each hei limi s o la ge models, in pa icula due o
an eno mous need o memo y du ing e i ica ion.
In he ollowing, we will employ he IC3 algo i hm o he e i ica ion o sa e y
p ope ies in he domain o imed au oma a. IC3 o igina es om ha dwa e e i i-
ca ion, in which i has p o en o be ex emely e icien , bo h ega ding ime and
memo y equi emen s. We aim o i o be o alue also in he domain o imed
au oma a. I s huge success o ha dwa e e i ica ion has led o a la ge amoun o
op imiza ions and, in addi ion, i has been success ully ans e ed and applied in
many o he , e y di e se domains. I s i s usage in he domain o imed au oma a
by Kinde mann e al. [KJN12b], howe e , emained unsa is ying, as i was no
compe i i e.
In his chap e , we in oduce ou concep combining he IC3 algo i hm wi h he
zone abs ac ion in o de o e i y sa e y p ope ies o ne wo ks o imed au oma a
[IW14]. We i s p esen he basic componen s, i.e., he SMT-encoding and zone
compu a ion, and a e wa ds explain hei in eg a ion in he IC3 algo i hm. Las ly,
we p esen he p omising esul s o nume ous expe imen s. We discuss o which
41
48 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES
In addi ion, he ex ac ion o he aken edges needed o he compu a ion o he
CTIs migh be mo e di icul .
Thus, we compu e he combina ions o edges, as de ined in De . 2.1.11. As
desc ibed in he seman ics, only hose edges o he p oduc au oma on can be aken
ha a e no synch onized (ma ked by he synch oniza ion symbol
e
). We encode
hese edges by en o cing he sou ce and a ge loca ions o hose imed au oma a,
in which he edges a e aken. Fu he mo e, we encode he cons ain s and in ege
assignmen s and ese s o clocks. In addi ion, we ensu e all unused clock, in ege
and loca ion a iables o keep hei alues, meaning hey ha e he same alue in
hei unp imed and p imed e sions.
We i s desc ibe how in ege assignmen s and ese s o clocks a e encoded.
3.1.6 Encoding o Clock and In ege Upda es
Encoding upda es on he clocks and in ege a iables inhe en ly makes use o bo h
he unp imed and p imed e sions o he a iables, ep esen ing he cu en and he
nex s a e alues, espec i ely. Fi s , we de ine he encoding o in ege assignmen s.
Encoding o In ege Assignmen s
As men ioned be o e, we can combine each
sequence o assignmen s (De ini ion 2.1.5) in o a sequence, in which he o de does
no ma e , since each in ege a iable exis s a mos once in a le hand side o an
assignmen . This ac esul s in a simple encoding using conjunc ion o combine
he assignmen s wi hou he need o in e media e s eps. No e, howe e , ha he
encoding o a sequence, in which he o de is essen ial, can easily be done using
auxilia y a iables and in e media e s eps. The ollowing de ini ion shows he
simple encoding.
De ini ion 3.1.10.
Le an in ege assignmen
ω
be gi en as de ined in De . 2.1.5. The
SMT- o mula kωkencoding i depends on he assignmen . I ωequals
•i :=n o some in ege a iable i ∈ IV and n∈Z, hen
kωk:=ki k0=n,
•i :=i +n o some in ege a iable i ∈ IV and n∈Z, hen
kωk:=ki k0=ki k+n,
•ω1;ω2 o some in ege assignmen s ω1and ω2, hen
kωk:=kω1k ∧ kω2k,
• ue, hen
kωk:= ue.
Fo an assignmen
ue
, he same a gumen s applies as o an in a ian
ue
. I
is igno ed and, hus, all in ege a iables a e o keep hei alue. This p ocess o
keeping he alue is encoded sepa a ely (as
ki k0=ki k
) in each o he edges o all
in ege a iables i ∈ IV ha a e no changed by he assignmen .
We illus a e he encoding wi h he ollowing example.

3.1. SMT-ENCODING 49
Example 3.1.11.
Conside again he Fische model as depic ed in Figu e 3.1. The
in ege assignmen
id :=
0;
cn :=cn −
1 can be seen on he edge be ween loca ion
l3
and
l0
in each o he au oma a. Wi h in ege a iable
id
ha ing iden i ie 0 and
cn ha ing iden i ie 1, he in ege assignmen is encoded as
kωk:= (in 0
0=0)∧(in 0
1= (in 1−1)).
The encoding is s aigh - o wa d o he in ege assignmen s. Howe e , clock
upda es can no be encoded his way due o always conside ing he combina ion
o an edge- ansi ion wi h a subsequen ime elapse s ep. To his end, we c ea e an
addi ional eal- alued a iable
δ
deno ing he ime elapse a e he edge has been
aken.
Encoding o Clock Rese s
Gi en he se
R⊆C
o clocks o be ese , he upda e o
each clock is encoded dependen on i being an elemen o
R
o no . All membe s
a e ese o alue 0, while he emaining clocks keep hei alue. A e wa ds all
clock alues a e inc eased by a ime delay s ep, encoded as he addi ion o a eal
alued a iable δ. Fo mally, he upda e o each clock c∈Cis encoded as
kck0=δi c∈R,
kck0= (kck+δ)else.
Using he abo e encodings, we can inally o malize he encoding o edges.
3.1.7 Encoding o Edges
When encoding he edges o an NTA, we dis inguish be ween he encoding o edges
ha o igina e om synch oniza ion and hose ha don’ . We s a wi h he la e ,
deno ing such edges ha can be ound in single imed au oma a in he ne wo k,
ma ked by symbol e, meaning no synch oniza ion akes place.
Unsynch onized Edges
These edges a e ela ed only o a single imed au oma on
Ai
(
i∈ {
1,...,
n}
) in he ne wo k
NTA =hA1
,...,
Ani
. Thus, hey do no conside he
loca ions o he o he imed au oma a, as well as hei local clocks. These alues do
no ma e , as hey a e unchanged when he edge is aken (no aking in o accoun
successi e ime elapse). Hence, ou encoding does no need o compu e he p oduc
au oma on wi h all i s combina ions o loca ions. Ins ead, we demand
Ai
o be in
he sou ce loca ion be o e aking he edge and o be in he a ge loca ion a e wa ds.
In addi ion, he clock and in ege cons ain s ha e o be me , as well as he ese o
clocks and he in ege assignmen s. The encoding is p esen ed in de ail below.
De ini ion 3.1.12.
Le a ne wo k o imed au oma a
NTA =hA1
,...,
Ani
be gi en as
in De . 2.1.11. Each unsynch onized edge
e= (l1e,φ,ψ,ω,R
−−−−−→ l2)∈Ei
o each imed
au oma on Ai(i∈ {1, . . . , n}) is encoded as ollows.
50 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES
kek:=kl1ki∧ kl2ki0
∧ kφk ∧ kψk ∧ kωk
^
c∈R
kck0=δ^
c∈C R
kck0=kck+δ
^
j∈{1,...,n}
j6=i
mx(Aj)
^
m=0
lj
m
0=lj
m
^
i ∈IV,i /∈ω
ki k0=ki k
We explain he encoding in he ollowing. The i s line encodes he au oma on
Ai
being in loca ion
l1
be o e he edge is aken and in
l2
a e wa ds, which is encoded
ia he p imed a iables. The nex line demands he cons ain s
ψ
and
φ
o hold
be o e he edge is aken and he assignmen
ω
being applied o he in ege a iables.
The hi d line demands he clocks in
R
o be ese , while all o he s keep hei alue.
In addi ion, a ime elapse o
δ
is encoded, whe e he equi emen o he delay
being nonnega i e (
δ≥
0) is encoded sepa a ely, oge he o all edges. Finally, he
loca ions o he imed au oma a o he han
Ai
a e p ese ed, as well as he alues o
he in ege a iables ha a e no upda ed in he assignmen ω.
We illus a e he encoding wi h he ollowing example.
Example 3.1.13.
Conside he Fische model as depic ed in Figu e 3.1. We show he
encoding o he edge
e
leading om
l2
o
l3
(wi h iden i ie s 2 and 3, espec i ely) in
he i s au oma on. I equi es A1 o be in he espec i e loca ions be o e and a e
he ansi ion, encoded as
kl2k1:=l1
1∧ ¬l1
0
and
kl3k0
1:=l1
1
0∧l1
0
0
. Fu he mo e, i
equi es in ege a iable
id
, encoded as
in 0
, o ha e alue 1 (
kψk:=in 0=
1) and
local clock
c
o
A1
, encoded as
c1
0
, o be o alue la ge han 1024 (
kφk:=c1
0>
1024).
The in ege assignmen
ω
inc emen s he a iable
cn
by one, encoded as
kωk:=
in 0
1= (in 1+
1
)
. All o he a iables keep hei alue du ing he ansi ion s ep. The
en i e encoding looks as ollows.
kek:=l1
1∧ ¬l1
0∧l1
1
0∧l1
0
0
∧(c1
0>1024)∧(in 0=1)∧(in 0
1= (in 1+1))
∧(c1
0
0= (c1
0+δ)) ∧(c2
0
0= (c2
0+δ))
∧(l2
0
0=l2
0)∧(l2
1
0=l2
1)
∧in 0
0=in 0
As explained be o e, ou encoding does no need o compu e any p oduc o
loca ions and is, hus, e y scalable. The same holds ue o he encoding o
synch onized edges, which we desc ibe below. Howe e , we need o compu e all
combina ions o synch onized sende and ecei e edges, which esul s in a bad
scalabili y o models wi h many sende and ecei e edges synch onized ia he
3.1. SMT-ENCODING 51
same channel. As no ed abo e, a di e en kind o encoding wi hou he need o
such a compu a ion migh be easible, bu esul s in an encoding way mo e complex
wi h some so o signaling be ween sende and ecei e ha ensu es exac ly one
edge o each kind.
Thus, we compu e he combina ion o synch onized edges up on end encode
hem simila o he p e ious encoding. The main di e ences a e he usage o wo
sou ce and a ge loca ions, as well as wo cons ain s and assignmen s due o
he sende and ecei e edges belonging o wo dis inc imed au oma a. In he
ollowing, he encoding is o mally de ined.
De ini ion 3.1.14.
Le a ne wo k o imed au oma a
NTA =hA1
,...,
Ani
be gi en
as in De . 2.1.11. Each synch onized edge
e
combined om sende edge
es=
(l1a!, φ1,ψ1,ω1,R2
−−−−−−−−→ l2)∈Ei
and ecei e edge
e = (l3a?, φ2,ψ2,ω2,R2
−−−−−−−−→ l4)∈Ej
o imed
au oma a Aiand Aj(i6=j∈ {1, . . . , n}) is encoded as ollows
kek:=kl1ki∧ kl3kj∧ kl2ki0∧ kl4kj0
∧ kφ1k ∧ kφ2k ∧ kψ1k ∧ kψ2k ∧ kω1;ω2k
^
c∈R1∪R2
kck0=δ^
c∈C (R1∪R2)
kck0=kck+δ
^
h∈{1,...,n}
h/∈{i,j}
mx(Ah)
^
m=0
lh
m
0=lh
m
^
i ∈IV,i /∈ω1;ω2
ki k0=ki k
Using hese encodings o he edges, we can encode he ansi ion ela ion. I is
explained below.
3.1.8 Encoding o T ansi ion Rela ion
The ansi ion ela ion consis s o all unsynch onized edges and he combined
synch onized ones. When he ansi ion ela ion is applied, he cu en s a e in he
conc e e ansi ion sys em is changed acco ding o he aken edge. Thus, an edge
mus be aken, which is encoded as a disjunc ion o he o mulae ep esen ing he
edges. The a iable
δ
modeling he elapsed ime is used wi hin all he encodings o
he edges and, hus, he equi emen ha a nonnega i e amoun o ime has passed
is encoded oge he once o all edges.
De ini ion 3.1.15.
Le a ne wo k o imed au oma a
NTA =hA1
,...,
Ani
be gi en as
in De . 2.1.11. Le
{e1
,
. . .
,
em}
be he se o unsynch onized edges and combined
synch onized edges as in he p e ious de ini ions. The ansi ion ela ion desc ibing
he applica ion o one o hem is encoded as
kT ansk:=(ke1k ∨ · · · ∨ kemk)∧δ≥0.
52 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES
All he abo e de ini ions a e employed o encode he conc e e seman ics o a
ne wo k o imed au oma a as explained. Fo ou e i ica ion app oach, howe e ,
he sa e y p ope y mus also be encoded as SMT- o mula. This encoding is de ined
below.
3.1.9 Encoding o Sa e y P ope y
A sa e y p ope y is de ined as a conjunc ion o nega ions o e o s a e speci ica ions.
Each e o s a e speci ica ion is de ined as a iple o pa ial loca ion ec o , clock
cons ain and in ege cons ain . We ha e desc ibed abo e, how all hese pa s
a e encoded. They a e simply combined ia conjunc ion o encode an e o s a e
speci ica ion.
De ini ion 3.1.16.
Le a ne wo k o imed au oma a
NTA =hA1
,...,
Ani
be gi en as
in De . 2.1.11. Le
e = (¯
l
,
φ
,
ψ)
be an e o s a e speci ica ion as gi en in De ini ion
2.1.13. I is encoded using he abo e de ini ions as
ke k:=^
j∈{1,...,n}
¯
l[j]6=∗
k¯
l[j]kj∧ kφk ∧ kψk,
whe e he encoding o he pa ial loca ion ec o encodes only hose loca ions ha
a e speci ied. In addi ion, cons ain s φand ψa e disca ded, i hey speci y ue.
As s a ed be o e, he encoding o he sa e y p ope y is simply he conjunc ion o
nega ions o he e o s a e speci ica ions. We o mally de ine i in he ollowing.
De ini ion 3.1.17.
Le a ne wo k o imed au oma a
NTA =hA1
,...,
Ani
be gi en as
in De . 2.1.11. Le he sa e y p ope y
ρ=G(¬e 1∧ · · · ∧ ¬e x)
be gi en speci ying
ha no eachable s a e should sa is y one o he e o s a e speci ica ions
e 1
o
e x
.
I is encoded as kρkas ollows.
kρk:=¬ke 1k ∧ · · · ∧ ¬ke xk
We illus a e he encoding wi h he ollowing example.
Example 3.1.18.
Conside again he Fische model as depic ed in Figu e 3.1. I
models he Fische mu ual exclusion algo i hm ha ensu es only a single p ocess
o be in a c i ical sec ion. The c i ical sec ion is modeled as loca ion
l3
and he
numbe o p ocesses in he c i ical sec ion is coun ed ia in ege a iable
cn
. Le
cn >
1 be he e o s a e speci ica ion conside ed he e. I speci ies ha mo e han a
single au oma on is in i s c i ical sec ion a he same ime. The sa e y p ope y o
in e es deno es ha no such e o s a e can occu , o mally
ρ:=G(¬(cn >
1
))
. I
is encoded as kρk=¬(in 1>1).
Finally, all o mulae needed a e explained and de ined. We b ie ly summa ize
hei usage wi hin IC3 below. To his end, we gi e an o e iew o e he que ies
issued o he SMT-sol e .
3.1. SMT-ENCODING 53
3.1.10 Usage o he Encodings in he Que ies
As s a ed be o e, he SMT- o mula encoding he ansi ion ela ion, as well as hose
o he ini ial s a es o he sa e y p ope y ely on he combina ion wi h he unp imed
and p imed in a ian o mulae. In consequence, we c ea e hese o mulae modula ly
in o de o combine hem when needed.
We b ie ly ecall he que ies issued by IC3 (uppe o mula) and show how hey
a e build using ou encoding (lowe o mula).
• (An e o s a e is ini ial.)
kIk ∧ ¬kρk:
kIni k ∧ kIn a k ∧ ¬kρk
• (A p edecesso o an e o s a e is ini ial.)
kIk ∧ kTk ∧ ¬kρk0:
kIni k ∧ kIn a k ∧ kT ansk ∧ kIn a k0∧ ¬kρk0
• (A p edecesso o an e o s a e is a membe o Fk.)
kFkk ∧ kTk ∧ ¬kρk0:
kFkk ∧ kIn a k ∧ kT ansk ∧ kIn a k0∧ ¬kρk0
• (A p edecesso o s a e s ha is dis inc om s is a membe o Fn−1.)
kFn−1k ∧ ¬ksk ∧ kTk ∧ ksk0:
kFn−1k ∧ ¬ksk ∧ kIn a k ∧ kT ansk ∧ kIn a k0∧ ksk0
• (An ini ial s a e is a membe o ¬c.)
kF0k ∧ ¬c:
kF0k ∧ kIn a k ∧ ¬c
• (A p edecesso o a s a e in ¬cis a membe o cand o Fn−1.)
kFn−1k ∧ c∧ kTk ∧ ¬c0:
kFn−1k ∧ c∧ kIn a k ∧ kT ansk ∧ kIn a k0∧ ¬c0
• (A p edecesso o a s a e in ¬cis a membe o Fi.)
kFik ∧ kTk ∧ ¬c0:
kFik ∧ kIn a k ∧ kT ansk ∧ kIn a k0∧ ¬c0
The abo e o mulae encode s a es and ansi ions in he conc e e ansi ion
sys em, as explained in De ini ion 2.1.10. I migh be easible o encode an abs ac ion
o he clock alua ion space di ec ly, e.g., by in oducing a iables o bounds o
clock alua ions. Howe e , he encodings would mos p obably g ow a mo e
complex. In pa icula , he ansi ion ela ion encoding would do so and, hus,
slow down he gene aliza ion s ep. Ou encoding e ains om in oducing his
addi ional complexi y and, ins ead, a o s an auxilia y s ep ou side he scope o
IC3’s gene aliza ion p ocedu e.
This addi ional s ep is i al o ou app oach. Since ou encoding ep esen s
a conc e e ansi ion sys em wi h clocks ha ing alues om
R≥0
, he e migh be
in ini ely many sa is ying in e p e a ions o a sa is iable que y. This in ini y poses

54 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES
a p oblem, especially when conside ing he que ies asking o coun e examples
o induc ion (CTIs). The e migh exis in ini ely many sa is ying in e p e a ions
and, in consequence, in ini ely many CTIs, e.g., wi hin one un o s eng henClauses.
Hence, he algo i hm would ha e o exclude in ini ely many CTIs o e mina ion.
E en when aking in o accoun he gene aliza ion p ocedu e, e mina ion can no be
ensu ed. This is due o he ac , ha he gene aliza ion algo i hm is only capable
o dele ing li e als ( o example
c=
1.771). Tackling his p oblem by al e ing he
gene aliza ion algo i hm o shi alues is ha dly easible.
Thus, we employ an abs ac ion in o de o ensu e e mina ion. Fi s , we need
o ob ain he conc e e s a es ha he sol e has compu ed in o m o a sa is ying
in e p e a ion. This s ep, called s a e ex ac ion, is de ailed below.
3.2 S a e Ex ac ion
Execu ing he IC3 algo i hm using an SMT-sol e wi h he abo e encoding esul s
in CTIs being conc e e s a es. Each sa is ying in e p e a ion is inspec ed o ex ac
alues o he loca ion a iables, clock a iables and in ege a iables. These ep e-
sen he clock alua ion, in ege alua ion and loca ions o a s a e in he conc e e
ansi ion sys em (o wo s a es - p edecesso and successo - in case o an encoded
ansi ion s ep). The clock and in ege alua ions can be ex ac ed di ec ly, howe e ,
he loca ions need o be compu ed om he boolean alues o he loca ion a iables.
The boolean alues ep esen he iden i ie o he loca ion encoded as in ege alue
in bina y o m. The ex ac ion o he conc e e s a e is exempli ied in he ollowing.
Example 3.2.1.
Le he ne wo k o imed au oma a be gi en as depic ed in Figu e
3.1. The que y
kFkk ∧ kIn a k ∧ kT ansk ∧ kIn a k0∧ ¬kρk0
asks he sol e o a
p edecesso s a e (in
Fk
) o an e o s a e. Conside he ollowing pa o a sa is ying
in e p e a ion e u ned by he sol e .
(de ine − un in 0() In 1)
(de ine − un in 1() In 1)
(de ine − un l1
1() Bool ue)
(de ine − un l1
0() Bool alse)
(de ine − un l2
1() Bool ue)
(de ine − un l2
0() Bool alse)
(de ine − un c1
0() Real 1025.0)
(de ine − un c2
0() Real 1.0)
. . .
No e, ha he o ma o he sa is ying in e p e a ion depends on he used sol e .
The p esen ed in e p e a ion ep esen s only alues o he p edecesso s a e. We
ex ac he ollowing s a e: Bo h in ege a iables
in 0
and
in 1
ha e alue 1 and,
hus, he in ege alua ion
i
o he in ege a iables o he model is se acco dingly
(
i(id) =
1,
i(cn ) =
1). The ex ac ion o he clock alua ion
c
is done in exac ly he
3.2. STATE EXTRACTION 55
same way (
c(c1) =
1025.0,
c(c2) =
1.0), whe e
c1
and
c2
deno e clock
c
in au oma a
A1
and
A2
, espec i ely. The ex ac ion o he loca ions is a bi mo e in ol ed.
Taking he alues o he boolean a iables, we build he bina y ep esen a ions
o he iden i ie s. In his example, bo h bina y ep esen a ions a e 10 ep esen ing
loca ion l2 o A1and A2.
As explained abo e, he conc e e clock alua ion poses a po en ial h ead o he
e mina ion o he algo i hm. In he ollowing, we show an example ha ing in ini ely
many such alua ions o CTIs all aking he same edge o an e o s a e.
Example 3.2.2.
We conside he same example as abo e wi h que y
kFkk∧kIn a k ∧
kT ansk ∧ kIn a k0∧ ¬kρk0
asking o a p edecesso s a e (in
Fk
) o an e o s a e.
The sa is ying in e p e a ion ep esen s an edge ansi ion om loca ion
l2
o
l3
in
he i s imed au oma on, while he second one keeps i s loca ion
l2
. The in ege
alua ion changes om
i(id) =
1,
i(cn ) =
1 o
i0(id) =
1,
i0(cn ) =
2. The
espec i e conc e e clock alua ion ound by he sol e is
c(c1) =
1025.0,
c(c2) =
1.0 and does no change (
c= c0
) wi h
δ=
0. I is easy o see, ha he loca ions
and alua ions enable he gi en edge wi h he gi en successo s a e being an e o
s a e, i.e., sa is ying
cn >
1. Clea ly, he e exis in ini ely many o he sa is ying
in e p e a ions o he que y: Keeping all he abo e alues, bu changing
c(c1)
o any a bi a y alue s ic ly la ge han 1024.0. Figu e 3.2 shows he compu ed
conc e e clock alua ion (ma ked as x), as well as he o he alua ions ha could be
used in a sa is ying in e p e a ion (ma ked g ay).
c1
10241023
.
1
2
1025
...
...
0
c2
.
.
.
.
..
.
.
.
..
.
.
.
..
.
.
.
Figu e 3.2: An in ini e numbe o sa is ying in e p e a ions can exis : When changing
he clock alua ion ound by he sol e o Example 3.2.2 (ma ked as x) o any o he
one o hose ma ked g ay, he espec i e in e p e a ion s ill sa is ies he issued que y
In 2012, Kinde mann e al. [KJN12b] p oposed a solu ion o ci cum en in ini ely
many CTIs by using he egion abs ac ion. They ex ac he conc e e s a e, as
shown abo e, and a e wa ds compu e he egion su ounding he ound clock
alua ion. The compu a ion is s aigh - o wa d, in pa icula , due o each conc e e
clock alua ion belonging only o a single, unique egion. This egion is used in lieu
56 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES
o he conc e e clock alua ion o ming an abs ac CTI. The essence o his app oach
is ha e mina ion is ensu ed due o he ac ha he e exis only a ini e numbe o
dis inc egions. Thus, when blocking an abs ac CTI, none o he conc e e clock
alua ions included in he en i e egion can occu again as CTI ( o a speci ic ame)
in he cu en cycle o he
s eng henClauses
p ocedu e. Acco dingly, wi h abs ac
CTIs being blocked, only a ini e numbe o dis inc ames can be c ea ed un il wo
o hem a e ound o be equal (o a coun e example ace is ound). As a esul ,
e mina ion is gua an eed.
Kinde mann examines his app oach ho oughly leading o he conclusion ha i
scales simila o he s a e o he a ool Uppaal, bu is no compe i i e o i due o
la ge un imes in gene al. The main eason o he pe o mance issues is he use
o he egion abs ac ion. Al hough being ini e, he numbe o CTIs may s ill be
eno mously la ge due o exponen ial g ow h o he employed abs ac ion ega ding
ime cons an s and clocks. Thus, he app oach is i ele an in p ac ice.
In gene al, howe e , Kinde mann’s app oach poin s ou a aluable di ec ion. By
applying ini e abs ac ion, IC3 can be u ilized o he e i ica ion o imed au oma a.
Such an abs ac ion should be coa se and e icien ly compu able in o de o be be e
sui ed o p ac ical pu poses.
In ou app oach, de ailed below, we apply he zone abs ac ion. We belie e ha
his abs ac ion is pa icula ly sui able o applica ion in IC3 due o i s p ope ies.
I is coa se han he egion abs ac ion, i is ini e since a zone is he union o
egions and he e exis sophis ica ed algo i hms o compu a ion and manipula ion
o zones. E en hough i is coa se, i is exac enough o desc ibe exac ly all hose
clock alua ions ha each a speci ic zone o a successo s a e ia he same edge.
No e, ha none o he p oblems o s o ing disjunc ions o zones occu ing in o he
app oaches (see he ela ed wo k in Chap e 2) a e p esen in he IC3 app oach.
Howe e , applying he zone abs ac ion is no as s aigh - o wa d as he egion
abs ac ion, since he e is no unique su ounding zone o each clock alua ion. We
explain his issue and ou solu ion in he ollowing.
3.3 Zone Abs ac ion
Ou SMT- o mulae as shown abo e encode he conc e e seman ics o a imed
au oma on. The s a es ex ac ed om sa is ying in e p e a ions a e, hus, conc e e
s a es wi h a single clock alua ion. Unlike in Kinde mann’s app oach, one can no
simply compu e a su ounding zone o such a clock alua ion as he e migh exis
se e al su ounding zones. We exempli y he ambigui y in he ollowing example.
Example 3.3.1.
Le he se o clocks be gi en as
C={c1
,
c2}
. A conc e e clock
alua ion
c
ex ac ed om a sa is ying in e p e a ion o a que y migh con ain
he alues
c(c1) =
1.5,
c(c2) =
0.75. I is depic ed in Figu e 3.3 ma ked as
x
,
oge he wi h se e al su ounding zones. Each such zone is a con ex union o clock
alua ions (de ined as a clock cons ain ) including he ound clock alua ion. Some
o hese zones a e e y ine g ained and some a e ex emely coa se. The di icul y
he e is o chose he igh one.
3.3. ZONE ABSTRACTION 57
c1
3
c2
21
1
2
3
(a) The zone
c1≥1∧c2≤1∧c1−c2≤1
c1
3
c2
21
1
2
3
(b) The zone c1≤2∧c2−c1≤1
c1
3
c2
21
1
2
3
(c) The zone ue
Figu e 3.3: A conc e e clock alua ion, as ex ac ed om a sa is ying in e p e a ion
o an SMT-que y, migh be included in nume ous su ounding zones wi h di e en
size
We sea ch o a zone ha includes he conc e e alua ion ound by he sol e ,
and is as la ge as possible, while pe mi ing only ele an beha io . The las wo
p ope ies a e opposed, bu easonable. A zone ha is oo small may esul in imp ac-
icali y o he app oach, while a zone ha is oo la ge would b eak he IC3 algo i hm.
Fo illus a ion conside compu ing a zone ha equals he egion su ounding he
conc e e clock alua ion. Clea ly, his choice esul s in imp ac icali y due o being
oo ine g ained. I depic s exac ly he app oach p oposed by Kinde mann e al.
[KJN12b]. On he o he hand, a zone
ue
allowing all alua ions would be oo coa se
and disallow he selec i e blocking o speci ic clock alua ions and, in consequence,
b eak he IC3 algo i hm.
We deno e beha io as ele an , i is analog o he one ound ia he SMT-que y,
meaning he same edge is aken wi h he same e o s a e o CTI as successo . Thus,
he zones we a e in e es ed in con ain exac ly hose clock alua ions ha enable he
same edge and each he same (abs ac ) successo s a e as he clock alua ion ound
by he que y.
Due o he abs ac ion o he ound conc e e clock alua ion in o a zone, he IC3
algo i hm no longe deals wi h conc e e s a es as CTIs, bu wi h abs ac s a es. We
deno e hese s a es as abs ac CTIs, as opposed o he p e iously used conc e e CTIs.
Abs ac CTIs a e abs ac s a es as de ined below.
De ini ion 3.3.2
(Abs ac S a e)
.
Le he e be gi en a ne wo k o imed au oma a
NTA =hA1
,...,
Ani
as in De . 2.1.11 wi h conc e e seman ics
TS = (S
,
s0
,
→)
.
The se o abs ac s a es is de ined as
Sa=L×Φ(C)×Ψ(IV)
. An abs ac s a e
sa= (l
,
φ
,
ψ)∈Sa
deno es he se o conc e e s a es
{(l
,
c
,
i)∈S| c|=φ∧ i|=ψ}
.
By aking in o accoun he de ini ion o sa e y p ope ies and abs ac CTIs, i is
easy o o malize he abo e in ui ion o he la ges zone wi h ele an beha io .
64 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES
in ege in a ian exis s o he p edecesso loca ion, he abo e cons ain is e u ned
as depic ed.
Simila ly, he compu a ion o clock cons ain s includes clock in a ian s, gua ds
and ese s. I en i ely elies on manipula ions o di e ence bound ma ices ep e-
sen ing he in ol ed zones.
Lis ing 3.4: Algo i hm: Compu ing he weakes p econdi ion o in ege cons ain s
93 wpClocks ( l , e , l ’ , φ’){
94 / / i n e s e c i o n wi h c l o c k i n a i a n o l ’
95 φ:=and(φ0,In c(l ’ )) ;
96 / / backwa ds compu a ion using edge e
97 φ:=backwa ds(l,l0,e,φ);
98 / / i n e s e c i o n wi h c l o c k i n a i a n o l
99 φ:=and(φ,In c(l)) ;
100 e u n φ;
101 }
Be o e using he backwa ds compu a ion algo i hm as explained in Subsec ion
3.3.1, he algo i hm limi s he allowed clock alua ions acco ding o he clock
in a ian s o loca ion
l0
. To his end, he in e sec ion o he DBMs ep esen ing bo h
zones is build. Subsequen ly, backwa ds compu a ion is employed as de ined in
De ini ion 3.3.4 based on edge
e
. The esul is he se o clock alua ions ha enables
he clock gua d o edge
e
, whose applica ion leads o a alua ion, which espec s
he clock in a ian o
l0
and is included in he successo ’s zone. Finally, his se is
in e sec ed wi h he clock in a ian s o loca ion
l
in o de o include only alua ions
espec ing he p edecesso ’s in a ian s.
Fo illus a ion, we again ex end he abo e example.
Example 3.4.3.
Conside he same si ua ion as in he p e ious example. The ound
e o speci ica ion includes no speci ied clock cons ain s and, in consequence,
he successo zone includes all alua ions. The ex ac ed successo loca ions a e
(l3
,
l2)
and he p edecesso loca ions a e
(l2
,
l2)
wi h he clock cons ain
c1>
1024
es ic ing he applica ion o he aken edge. Applying he p ocedu e
wpClocks
esul s in he ollowing compu a ion. The in e sec ion wi h he successo ’s clock
in a ian does no al e he se o alua ions, as no such in a ian exis s. Then,
he pas is compu ed, which s ill includes all clock alua ions. The applica ion o
ee
and
ese
is also wi hou any e ec , since no clocks a e ese . A e wa ds, he
zone is es ic ed o only include clock alua ions espec ing he p edecesso ’s clock
in a ian and he clock cons ain o he edge (
c1>
1024). Thus, a e he applica ion
o p ocedu e
wpClocks
, he esul ing se o clock alua ions can be speci ied by
cons ain c1>1024.
In summa y, bo h p ocedu es compu ing he se s o p edecesso alua ions a e
designed o include he maximal se s o alua ions ha enable edge
e
while eaching

3.4. ALGORITHM 65
a successo alua ion as speci ied by
φ0
and
ψ0
. Thus, hey a e ex emely impo an ,
bo h ela ed o e iciency and also e mina ion o ou app oach. They a e likewise
used in he
blockCTIs
p ocedu e whene e he con ained que y is sa is iable and a
p edecesso o a CTI needs o be compu ed. In con as o he abo e case using he
e o s a e speci ica ions, no sea ch o a successo s a e is necessa y he e, since i is
known in o m o an abs ac CTI ha al eady includes a zone and in ege cons ain .
These in o ma ions a e, hus, exploi ed o compu e he p edecesso ’s cons ain and
zone. Lis ing 3.5 shows he changed pseudocode.
Lis ing 3.5: Algo i hm: Excluding s a es om he ames in IC3 o imed au oma a
102 blockCTIs ( Se Q) {
103 while(Q6=∅) {
104 / / l e abs ac CTI sa=( l ’ , φ0,ψ0)
105 ge (sa,n ) ∈Q wi h smalles n;
106 i (kFn−1k ∧ ¬ksak ∧ kTk ∧ ksak0unsa is iable)
107 Q : = Q {(sa,n ) } ;
108 gene alizeAndBlock(sa,n) ;
109 else i (n−1==0)
110 / / ound coun e example
111 e u n alse ;
112 else
113 / / e x a c om s a i s y i n g i n e p e a i o n
114 conc e e p edecesso s a e =( l , i, c) ;
115 / / e x a c om s a i s y i n g i n e p e a i o n
116 aken edge e ;
117 in ege cons ain ψ= wpIn ege s ( l , e , l ’ , ψ0);
118 clock cons ain φ= wpClocks ( l , e , l ’ , φ0) ;
119 combine in o abs ac CTI a=( l , φ,ψ) ;
120 Q : = Q ∪{ ( a,n−1 ) } ;
121 }
122 e u n ue ;
123 }
As can be seen, he same mechanisms a e employed in
blockCTIs
in o de o
compu e he p edecesso s a e. Wi h he successo s a e being an abs ac CTI, i s
zone and in ege cons ain s mus ha e been p e iously compu ed and we can
simply euse hem. This is he only di e ence o he abo e case loca ed in he
p ocedu e
s eng henClauses
, in which we p e iously had o make an e o o ind
an abs ac successo s a e.
The compu a ion and usage o ou abs ac s a es se es as means able o ensu e
e mina ion o he algo i hm. Howe e , he e exis models o which e en his
concep can no gua an ee i . We will see easons o his in he ollowing subsec ion,
whe e we analyze and p o e e mina ion unde ce ain es ic ions o he models.
66 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES
3.4.1 Te mina ion
In Chap e 2, we illus a ed he e mina ion gua an ee o he o iginal IC3 algo i hm.
Gi en ha he model is ini e, he e exis only ini ely many s a es. Since he ames
a e se s o s a es and a e equi ed o be dis inc , he e can only be a ini e numbe
o ames. The es o he a gumen a ion is abou each p ocedu e call e mina ing
e en ually and abou p og ess, meaning a leas one o he ames is e ined a e
he blocking phase.
In he case o ou modi ied IC3 algo i hm o imed au oma a using Zones, a
simila easoning can be applied, bu encoun e s a couple o p oblems. The mos
ob ious challenge conce ning he in ini e s a e ansi ion sys em o a imed au oma a
is sol ed using he Zone abs ac ion. Each abs ac CTI includes a zone ins ead
o a single, conc e e clock alua ion. When using backwa ds compu a ion, only
ini ely many such zones can occu o a gi en imed au oma on as hey a e unions
o egions [Bou09]. Thus, he CTIs in ou algo i hm can only include one o hese
ini ely many zones. In addi ion, hey can only con ain one o ini ely many loca ions.
In combina ion wi h a ini e numbe o se s o in ege alua ions encoded in he
in ege cons ain s, ou CTIs a e o ini e quan i y. The gene aliza ion p ocedu e
aking place a e CTI compu a ion can no des oy ini eness, since i can only dele e
some o he li e als. The esul would be a se o loca ions wi h an enla ged zone
and enla ged se o in ege cons ain s. Hence, he same a gumen a ion holds ue
as o he o iginal algo i hm, s a ing ha he e can only be ini ely many di e en
ames and, hus, he algo i hm will e mina e e en ually.
Theo em 3.4.1.
Le a ne wo k o imed au oma a
NTA =hA1
,...,
Ani
be gi en as in De .
2.1.11. I he se o backwa ds eachable alua ions o he in ege a iables
IV
is ini e, hen
he p esen ed algo i hm IC3wi h Zones e mina es.
Howe e , he p esump ion ha he e exis s only a ini e numbe o se s o in ege
alua ions in a CTI may be inco ec . This di icul y comes om in ege assignmen s
i :=i +n
o some
i ∈ IV
and
n∈Z {
0
}
. Whene e a cycle is p esen in he
imed au oma on ha is able o epea edly inc ease o dec ease he alua ion o an
in ege a iable, he e migh exis an unbounded numbe o CTIs. I migh occu
ha hese a e all uled ou by gene aliza ion and he algo i hm e mina es, bu i
can no be gua an eed. Thus, he p esence o such cycles des oys he gua an ee o
e mina ion o ou modi ied IC3 algo i hm. Con a y, he absence o such cons uc s
inducing in ini ely many se s o in ege alua ions gua an ees e mina ion. The
ollowing heo em o malizes he abo e illus a ion.
Theo em 3.4.2.
In gene al, he e i ica ion o sa e y p ope ies o ne wo ks o imed
au oma a as p esen ed in his hesis is undecidable.
This heo em has been p o en o a closely ela ed o malism in 2004 [Bou+04],
which elies on upda es on he clocks o a imed au oma on. I in ol es a i ial e-
duc ion o he hal ing p oblem o de e minis ic 2-coun e machines. Ou o malism
allows a simila educ ion, which does no ely on upda es on clocks, bu ins ead
3.4. ALGORITHM 67
elies on ou in ege a iables being unbounded and assignmen s being able o in-
c emen and dec emen hese alues. We explain he de ails below. The eachabili y
p oblem o de e minis ic 2-coun e machines, which was shown o be undecidable
in 1967 [Min67], can i ially be educed o a sa e y p ope y e i ica ion o ne wo ks
o imed au oma a using ou o malism. A 2-coun e machine
(Q
,
qo
,
4)
consis s o
a ini e se o s a es
Q
wi h ini ial s a e
q0∈Q
, whe e
4 ⊆ Q×Op0×Q
and
Op0=
{inc(c1)
,
inc(c2)
,
es AndJump(c1)
,
es AndJump(c2)
,
condDec(c1)
,
condDec(c2)}
o
wo coun e s
c1
,
c2
ha can be inc emen ed, es ed o ze o o dec emen ed in
dependence o he cu en alue. These ope a ions can be desc ibed as
•inc(ci): Inc emen coun e ci,
• es AndJump(ci): Requi e he alue o coun e ci o be ze o,
•condDec(ci)
: Requi e he alue o coun e
ci
o be s ic ly la ge han ze o and
dec emen i .
No e, ha he la e wo a e some imes combined in o a single ins uc ion wi h wo
dis inc a ge s a es in dependence whe he he coun e can be dec emen ed o no .
The eachabili y p oblem asks whe he an accep ing s a e
q ∈Q
is eachable in a
ini e numbe o s eps s a ing om a gi en ini ial s a e wi h p ede e mined coun e
alues. The educ ion o a imed au oma on is s aigh - o wa d.
Gi en any 2-coun e machine
M= (Q
,
qo
,
4)
, we build a imed au oma on
A= (L
,
l0
,
C
,
IV
,
Σ
,
In c
,
In i
,
E)
and sa e y p ope y
ρ
ha is no in a ian i and
only i
q
is eachable in
M
. The wo coun e s a e mapped o wo in ege a iables
wi h espec i e ini ial alues, i.e.,
IV ={c1
,
c2}
. The e does no exis a clock and
he loca ions ep esen he s a es o he 2-coun e machine, meaning
C=∅
and
L=Q
wi h
l0=q0
. No synch oniza ion akes place and no in a ian s a e gi en
on he loca ions, i.e.,
Σ=∅
,
∀l∈L:In c(l) = ue
and
∀l∈L:In i(l) = ue
.
Fu he mo e, he ins uc ions ha modi y he coun e alues a e mapped o upda es
on he in ege a iables on he edges be ween he loca ions. Fo mally, o e e y
(q1,op,q2)∈ 4, he e exis s an edge e∈E. I op equals
•inc(ci):e= (q1e, ue, ue,ci:=ci+1, ∅
−−−−−−−−−−−−−→ q2),
• es AndJump(ci):e= (q1e, ue,ci=0, ue,∅
−−−−−−−−−−→ q2),
•condDec(ci):e= (q1e, ue,ci>0, ci:=ci−1, ∅
−−−−−−−−−−−−−−−→ q2).
The sa e y p ope y speci ies he loca ion ep esen ing he accep ing s a e
q
o be
an e o s a e, o mally
ρ:=G¬((q )
,
ue
,
ue)
. Checking he eachabili y o he
accep ing s a e in he 2-coun e machine is, hus, educed o checking he iola ion
o he sa e y p ope y. T i ially, any pa h o con igu a ions in he 2-coun e machine
exis s as well in he imed au oma on and, hence, he eachabili y p oblem could be
sol ed i he sa e y p ope y could be checked o iola ion. As a consequence, ou
p oblem o checking sa e y p ope ies o imed au oma a as de ined in Chap e 2
68 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES
is undecidable in gene al. No e, ha he undecidabili y is due o he unbounded
usage o in ege a iables and assignmen s.
3.5 E alua ion
The p esen ed app oach e i ies sa e y p ope ies o ne wo ks o imed au oma a.
One o i s design goals is e iciency ega ding memo y consump ion and un ime.
The IC3 algo i hm unde lying ou app oach is one o he key componen s o achie e
his goal. In addi ion, he abs ac ion o conc e e clock alua ions in o zones is
equally impo an , as i e icien ly handles he in ini y o he clock alua ion space.
In o de o e alua e whe he he design goal is me in p ac ice, we implemen ed
he p esen ed echnique using Ja a. Se e al s anda d models a e employed as
benchma ks in o de o compa e ou me hod wi h he s a e o he a ool Uppaal
and he p e ious app oach by Kinde mann [KJN12b]. These expe imen s p o ide
a basis o es ima e he scalabili y o he p esen ed app oach. The esul s a e e y
p omising, in pa icula ega ding he scalabili y, bu also poin ou some d awbacks.
In he ollowing, we p esen he models employed in ou expe imen s ollowed by
some de ails abou ou implemen a ion. A e wa ds, he expe imen s a e p esen ed
and discussed.
3.5.1 Benchma k Models
We employed se e al s anda d models om li e a u e, as well as a smalle one
ha we de eloped ou sel es conside ing he con ex o Indus y 4.0. In o al, he
ollowing benchma ks a e subsequen ly p esen ed and a e wa ds employed in
nume ous expe imen s.
• Models ob ained om Uppaal websi e [UPP]
–Fische Mu ual Exclusion algo i hm
–Ca ie Sense Mul iple Access wi h Collision De ec ion p o ocol
–FDDI oken ing p o ocol
• FDDI oken ing p o ocol wi h coun ing a iable
• Models ob ained om B u omesso e al. [B u+12]
–Fische Mu ual Exclusion algo i hm
–Lampo Mu ual Exclusion algo i hm
–Sha i -Lynch Mu ual Exclusion algo i hm
• A sh unk model o he Lampo Mu ual Exclusion algo i hm
• Model o he Sha i -Lynch Mu ual Exclusion algo i hm om PAT [PAT]
3.5. EVALUATION 69
Fische Mu ual Exclusion Algo i hm (Uppaal)
One o he mos impo an models
o es ima ing he scalabili y o ou echnique is he ne wo k o imed au oma a,
which we ha e shown p e iously in he examples. I models he Fische Mu ual
Exclusion algo i hm [Lam87] ha ensu es mu ually exclusi e access o a c i ical sec ion
o se e al p ocesses. Gi en i s dependency on ime, i is a pe ec i o be modeled
as a ne wo k o imed au oma a. The e exis se e al models o he Fische algo i hm,
mos o which only di e in small de ails. The model we used in he examples and
ou expe imen s is aken om Uppaal, ound a hei websi e [UPP]. We deno e
i as
Fische _U_x
, whe e
x
is he numbe o imed au oma a. Mu ual exclusion is
handled by each p ocess w i ing i s unique iden i ie o a sha ed a iable when
eques ing access o he c i ical sec ion. A e wai ing a ce ain amoun o ime, he
p ocess is allowed o p oceed only i he sha ed a iable s ill ma ches i s iden i ie .
To his end, each p ocess is modeled as a imed au oma on, each ha ing i s own
unique iden i ie .
Figu e 3.1 shows he model o wo p ocesses. The i s p ocess has iden i ie 1,
while he second one has iden i ie 2. In consequence, he edges be ween loca ions
l1
and
l2
, as well as he ones be ween
l2
and
l3
a e di e en . Each p ocess has o w i e
i s own iden i ie o he sha ed a iable and acco dingly check o i s own iden i ie .
All o he pa s o he model a e equal o e e y imed au oma on. The c i ical sec ion
is modeled as loca ion
l3
and he in ege a iable
cn
coun s he numbe o p ocesses
cu en ly in he c i ical sec ion.
The sa e y p ope y o in e es asks whe he a mos one o he p ocesses is in he
c i ical sec ion a e e y poin in ime. Using he in ege a iable
cn
men ioned abo e,
we can exp ess his sa e y p ope y as ρ:=G¬((∗,∗), ue,cn >1), abb e ia ed as
ρ:=G¬(cn >1).
Wi h he Fische algo i hm being independen o he numbe o p ocesses, i
p o ides a pe ec oppo uni y o scalabili y expe imen s. To his end, he numbe o
p ocesses, ha is, imed au oma a in he ne wo k, is inc eased while he pe o mance
is examined.
Fu he mo e, modi ica ions o he used ime cons an s allow inspec ions o
pe o mance changes caused by ime cons an s. These op ions a e also p esen in
he o he models used wi hin ou expe imen s.
Ca ie Sense Mul iple Access wi h Collision De ec ion P o ocol
We adop ed a
model o he Ca ie Sense Mul iple Access wi h Collision De ec ion P o ocol (CSMA/CD)
also ound a he websi e men ioned abo e [UPP]. We deno e i as
CSMA/CD_x
,
whe e
x
is he numbe o imed au oma a modeling s a ions. I models a b oadcas ing
communica ion p o ocol in which se e al s a ions a e ying o send da a o e a bus.
In his scena io, only one s a ion may send da a a a ime as o he wise wo o mo e
ansmissions would be simul aneous and collide, s. . no da a can be ecei ed by a
s a ion lis ening o he bus. In his p o ocol, a s a ion, willing o b oadcas da a, i s
senses whe he he bus is busy. I so, i wai s a andom amoun o ime and hen
s a s o e . O he wise, i s a s sending da a while lis ening o he bus o collisions,
which may occu due o a p opaga ion delay o he signal, deno ing he ime un il i

70 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES
c<26
c<26
c:=0
c:=0
l0
l3
l1
l2
end?
c:=0
begin?
busy!
c≥26
begin?
c<26
c:=0
cd1!
c≤0
c≤0
c:=0
cd2!
l0
l1
l2
c:=0
begin!
c=808
c:=0
end!
c:=0
cd1?
c:=0
busy?
c:=0
cd1?
c<52
c<52
c:=0
cd1?
c≤808
c<52
c:=0
cd1?
c<52
c:=0
begin!
l0
l1
l2
c:=0
begin!
c=808
c:=0
end!
c:=0
cd2?
c:=0
busy?
c:=0
cd2?
c<52
c<52
c:=0
cd2?
c≤808
c<52
c:=0
cd2?
c<52
c:=0
begin!
Figu e 3.4: Ne wo k o h ee imed au oma a modeling he CSMA/CD p o ocol wi h
a bus (le imed au oma on) and wo communica ing s a ions (o he wo au oma a)
can be sensed by e e y s a ion. In case a collision occu s, all s a ions s op sending
and s a o e again. The model again deno es a mu ual exclusion p oblem, whe e
only one sende should be sending a e he p opaga ion delay ime has passed.
Figu e 3.4 shows he model o wo s a ions. This model does no equi e a
sha ed a iable, bu makes hea y use o synch oniza ion channels. In pa icula ,
all s a ions a e in o med o a collision by he bus consecu i ely i ing synch onized
edges (using cd1!, cd2!, . . . ), one o each s a ion.
The s ic sequence o edges i ed a e a collision educes he eachable po ion
o he s a e space. Ou expe imen s show ha he a io o his eachable po ion
compa ed o he en i e s a e space is an in e es ing cha ac e is ic wi h a wide
in luence o he u ili y o ou algo i hm. The sa e y p ope y used in his CSMA/CD
model speci ies ha he second s a ion (au oma on
A3
) is no allowed o ansmi
(modeled as loca ion
l2
), when he i s s a ion (au oma on
A2
) is ansmi ing
since mo e han 52 ime uni s ( he p opaga ion delay). I is o mally desc ibed as
ρ:=G¬((∗,l2,l2),c2≥52), whe e c2deno es clock cin au oma on A2.
l5
l0
l3
l1
l2
c:=0
2?
c≤0
2!
c≤0
1!
c:=0
1?
c≤0
c≤0
l0
l3l1
l2
c1:=0,c2:=0
1?
c1≤20
l4
c1≥20 ˄ c3<120
c3≤120
1!
c1≥20 ˄ c3≥120
1!
c1:=0,c3:=0
1?
c1≤20
c2≤120
1!
1!
c1≥20 ˄ c2<120
c1≥20 ˄ c2≥120
l5
l0
l3l1
l2
c1:=0,c2:=0
2?
c1≤20
l4
c1≥20 ˄ c3<120
c3≤120
2!
c1≥20 ˄ c3≥120
2!
c1:=0,c3:=0
2?
c1≤20
c2≤120
2!
2!
c1≥20 ˄ c2<120
c1≥20 ˄ c2≥120
Figu e 3.5: Ne wo k o h ee imed au oma a modeling he FDDI Token ing p o ocol
wi h a model o he ing (le imed au oma on) and wo communica ing s a ions
3.5. EVALUATION 71
FDDI Token Ring P o ocol
The las benchma k adop ed om he abo e men-
ioned Uppaal websi e [UPP] is he Token Ring FDDI P o ocol. We deno e i as
FDDI_x
, whe e
x
is he numbe o imed au oma a modeling s a ions. I models a
si ua ion in which se e al symme ic s a ions a e o de ed as a ing and a oken is
passed be ween he s a ions along he ing. In his scena io, he e exis wo op ions
o he oken passing, one is as and he o he is slow. The ing s uc u e is modeled
as a imed au oma on ha de e mines he sequence in which he oken is passed
om s a ion o s a ion, each modeled as an addi ional imed au oma on. Due o he
wo di e en passing modes, his model includes many clocks and ime cons an s,
one o which is linea ly dependen on he numbe o s a ions. Thus, he model is
speci ically sui able o examine he e ec o la ge ime cons an s. Fu he mo e, he
eachable po ion o he s a e space is an ex emely small ac ion o he en i e s a e
space due o he ing s uc u e. This cha ac e is ic allows o in e es ing insigh in
he applicabili y o ou echnique.
Figu e 3.5 shows he model o wo s a ions. This model does no equi e a
sha ed a iable, bu makes use o synch oniza ion channels o en o ce he s a ions
only communica ing in o de o he ing.
The sa e y p ope y speci ies ha he oken is no a wo s a ions a he same
ime. Thus, he e mus no exis a eachable s a e in which wo s a ions a e bo h in
one o he ollowing loca ions:
l1
,
l2
,
l4
,
l5
. Conside ing he mu ual exclusion o only
he i s wo s a ions, his sa e y p ope y is o malized as
ρ:=G¬((∗,l1,l1)) ∧ ¬((∗,l1,l2)) ∧ ¬((∗,l1,l4)) ∧ ¬((∗,l1,l5))
∧¬((∗,l2,l1)) ∧ ¬((∗,l2,l2)) ∧ ¬((∗,l2,l4)) ∧ ¬((∗,l2,l5))
∧¬((∗,l4,l1)) ∧ ¬((∗,l4,l2)) ∧ ¬((∗,l4,l4)) ∧ ¬((∗,l4,l5))
∧¬((∗,l5,l1)) ∧ ¬((∗,l5,l2)) ∧ ¬((∗,l5,l4)) ∧ ¬((∗,l5,l5),
whe e he in ege cons ain and zone ue a e each omi ed o eadabili y.
FDDI Token Ring P o ocol wi h Coun ing Va iable
As can be seen, his way
o speci ying mu ual exclusion is leng hy. Thus, we adap ed he FDDI model by
addi ion o an in ege a iable
cn
ha coun s he numbe o au oma a cu en ly
in any o he men ioned loca ions. We deno e i as
FDDIcoun _x
, whe e
x
is he
numbe o imed au oma a modeling s a ions. Figu e 3.6 shows his adap ed model
o wo s a ions. The sa e y p ope y speci ying mu ual exclusion can, hus, be
educed o
ρ:=G¬(cn >
1
)
. This adap a ion allows o an in e es ing s udy o he
e ec o an addi ional in ege a iable (wi h simul aneous educ ion o he numbe
o e o s a e speci ica ions).
Fische Mu ual Exclusion Algo i hm (B u omesso)
Addi ional mu ual exclusion
algo i hms ha e been employed in ou expe imen s. We adop ed a di e en e -
sion o he Fische Mu ual Exclusion algo i hm as p esen ed by B u omesso e al.
[B u+12], deno ed as
Fische _B_x
, whe e
x
is he numbe o imed au oma a. I is
depic ed in Figu e 3.7.
72 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES
l5
l0
l3
l1
l2
c:=0
2?
c≤0
2!
c≤0
1!
c:=0
1?
c≤0
c≤0
l0
l3l1
l2
c1:=0,c2:=0
1?
c1≤20
l4
c1≥20 ˄ c3<120
c3≤120
1!
c1≥20 ˄ c3≥120
1!
c1:=0,c3:=0
1?
c1≤20
c2≤120
1!
1!
c1≥20 ˄ c2<120
cn :=cn +1
cn :=cn +1
cn :=cn -1
cn :=cn -1
cn :=cn -1
cn :=cn -1
cn :=cn +1
cn :=cn +1
cn :=cn -1
cn :=cn -1
cn :=cn -1
cn :=cn -1
c1≥20 ˄ c2≥120
l5
l0
l3l1
l2
c1:=0,c2:=0
2?
c1≤20
l4
c1≥20 ˄ c3<120
c3≤120
2!
c1≥20 ˄ c3≥120
2!
c1:=0,c3:=0
2?
c1≤20
c2≤120
2!
2!
c1≥20 ˄ c2<120
c1≥20 ˄ c2≥120
Figu e 3.6: Adap ed ne wo k o h ee imed au oma a modeling he FDDI Token ing
p o ocol wi h wo s a ions as in Figu e 3.5 ha includes an addi ional in ege a iable
cn
used o coun he numbe o s a ions ha a e in hei espec i e ansmi ing
loca ions
l0
l1
l2
l3
l4
l5
l6
l7
l8
c≤1024
c≤1024
c≤1024
c≤1024
c≤1024
c≤1024
c≥1
id≠0
c:=0
c≥1
id=0
c:=0
c≥1
c:=0
id:=1
c≥1024
c:=0
c≥1
id=1
c:=0
cn :=cn +1
c≥1
c:=0
cn :=cn -1
c≥1
c:=0
c≥1
c:=0
id:=0
c:=0
c:=0
c≥1
id≠1
c:=0
l0
l1
l2
l3
l4
l5
l6
l7
l8
c≤1024
c≤1024
c≤1024
c≤1024
c≤1024
c≤1024
c≥1
id≠0
c:=0
c≥1
id=0
c:=0
c≥1
c:=0
id:=2
c≥1024
c:=0
c≥1
id=2
c:=0
cn :=cn +1
c≥1
c:=0
cn :=cn -1
c≥1
c:=0
c≥1
c:=0
id:=0
c:=0
c:=0
c≥1
id≠2
c:=0
Figu e 3.7: Ne wo k o wo imed au oma a modeling he Fische Mu ual Exclusion
algo i hm o wo p ocesses as p esen ed by B u omesso e al. [B u+12]
3.5. EVALUATION 73
Lampo and Sha i -Lynch Mu ual Exclusion Algo i hm
B u omesso’s publi-
ca ion also includes models o malizing wo o he mu ual exclusion algo i hms,
namely he Lampo and Sha i -Lynch algo i hms. The o me solely elies on
sha ed a iables, while he la e addi ionally depends on iming cons ain s. We
adop ed a model o each o hese wo algo i hms, deno ed as
Lampo _B_x
and
Sha i Lynch_B_x
, whe e
x
is he numbe o imed au oma a. They a e depic ed in
Figu es 3.8 and 3.9.
l0
l1
l2
l3
l4
l5
l6
l7
l8
id:=1
id=1
y:=1
cn :=cn +1
cn :=cn -1
y≠0
id≠1
y=0
y:=0
l0
l1
l2
l3
l4
l5
l6
l7
l8
id:=2
id=2
y:=1
cn :=cn +1
cn :=cn -1
y≠0
id≠2
y=0
y:=0
Figu e 3.8: Ne wo k o wo imed au oma a modeling he Lampo Mu ual Exclusion
algo i hm o wo p ocesses as p esen ed by B u omesso e al. [B u+12]
Sh unk Model o Lampo Mu ual Exclusion Algo i hm
Fu he mo e, we con-
s uc ed a sh unk e sion o he Lampo model since some o he loca ions a e no
necessa y. I is deno ed as
Lampo _S_x
. The compa ison o his sh unk e sion
wi h he o iginal one allows us o d aw conclusions abou he impac o a la ge
numbe o loca ions in a model. The sh unk model is p esen ed in Figu e 3.10.
Sha i -Lynch Mu ual Exclusion Algo i hm (PAT)
Addi ionally, we employ a e -
sion o he Sha i -Lynch algo i hm in ou expe imen s ha includes ewe loca ions.
The model is aken om he PAT websi e [PAT], deno ed as
Sha i Lynch_P_x
. I
is depic ed in Figu e 3.11. We augmen ed all hese models wi h a coun ing a i-
able, s. . he sa e y p ope y speci ying mu ual exclusion can be o malized as
ρ:=G¬(cn >1).
Lemgo Model
The applicabili y o ou echnique in eal wo ld scena ios is checked
wi h an addi ional model. We de eloped i o ep esen a pa o he Lemgo Sma
Fac o y [inI] o he Hochschule Os wes alen-Lippe [Hoc]. I is simila in e ms o
size and s uc u e o hose imed au oma a models ha a e au oma ically lea ned
om exis ing eal wo ld sys ems [Mai14]. I migh , hus, be sui able o es ima e he
eal wo ld p ac icali y o ou app oach.
80 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES
0.1
1
10
100
1000
10000
5 10 15 20 25 30 35 40
Run ime([seconds]
Numbe (o ( imed(au oma a
FDDI
IC3Zone(LCI)
Uppaal
(a) Run ime o e i ica ion
0
100
200
300
400
500
600
700
5 10 15 20 25 30 35 40
UsedCmemo yC[MB]
Numbe Co C imedCau oma a
FDDI
IC3Zone(LCI)
Uppaal
(b) Max. memo y consump ion
Figu e 3.15: Resul s o he expe imen s using he
FDDI
model: Run ime and
memo y consump ion o ou p esen ed app oach IC3 wi h Zones a e compa ed wi h
s a e o he a ool Uppaal o models wi h di e en numbe o imed au oma a
always examines he en i e s a e space encoded ia he used SMT- o mulae, Uppaal
only examines he eachable s a es ia ( o wa d) explo a ion. Thus, i has a huge
ad an age, i he a io o eachable s a es o he en i e numbe o s a es is small, as
is he case in he FDDI model. Due o he ing s uc u e, he o de in which he
au oma a’s edges may be aken is e y s ic , educing he numbe o eachable
s a es. As an example, conside he FDDI model wi h 20 s a ions. Du ing he en i e
e i ica ion o he sa e y p ope y Uppaal explo es only 8061 s a es, while he en i e
s a e space includes 4
∗
6
20
possible loca ion combina ions, no aking in o accoun
he addi ional clock space. I has, hus, an eno mous ad an age o e ou app oach
exac ly o hose models wi h a small numbe o eachable s a e, whe e he en i e
s a e space is la ge.
The wo dis inc ways o explo ing he model’s s a es esul in di e en sui abil-
i ies o he app oaches o di e en models. In summa y, we would ecommend
using Uppaal o smalle models and hose wi h a small se o eachable s a es
(ha d o es ima e up on ). Ne e heless, his cha ac e is ic migh be guessed by
means o he s uc u e o he model, e.g., when he model allows only e y speci ic
sequences o edges being aken. On he o he hand, we ecommend he app oach
p esen ed in his chap e o be used o la ge models. I has shown o scale well
and is compe i i e o Uppaal o some o he benchma k models. We emphasize he
ac ha i was capable o e i ying sa e y p ope ies o models h ee imes la ge
han Uppaal was capable o o he Fische _Umodel.
Nex , we examine he impac o in ege a iables on ou echnique.

3.5. EVALUATION 81
In ege Va iable Expe imen s
Scaling up he numbe o in ege a iables may
ha e a ious e ec s depending on hei usage. I may en i ely change he s a e space,
o may only be o li le e ec . Thus, we can only exempli y possible impac s o
in ege a iables he e. To his end, we will examine he change in oduced by he
addi ion o he in ege a iable cn in he FDDI model.
Ou adap ed
FDDI
model includes an addi ional in ege a iable
cn
ha coun s
he numbe o au oma a in ansmi ing loca ions. Six ou o eigh edges a e ex ended
by an in ege upda e in each o he au oma a modeling a s a ion. The in oduc ion
o his addi ional a iable has an in e es ing e ec . I simpli ies he ound induc i e
s eng hening o e e y numbe o au oma a o include only wo clauses. The
i s one is he sa e y p ope y
¬(in 0>
1
)
wi h
in 0
encoding he in ege a iable
cn
. The second one
¬(¬l1
0∧(in 0>
0
))
speci ies ( ia he leas signi ican bi o
he loca ion iden i ie s) ha no loca ion o he i s au oma on ( he ing s uc u e)
wi h an e en iden i ie (
l0
,
l2
,
. . .
) is eachable when
cn >
0. Since hese a e he
only loca ions wi h ou going edges inc emen ing
cn
, he coun e can no be la ge
han 1. The conjunc ion o hese wo clauses is induc i e. This e i ica ion hea ily
p o i s om he SMT-encoding o loca ions ia boolean a iables, as well as he ing
s uc u e o he model including wo loca ions o each s a ion. I allows a ound CTI
o be gene alized, s. . i easons abou all loca ions o
A1
wi h e en loca ion iden i ie .
Figu e 3.16 shows he impac on he un ime, which is ex emely imp o ed, ac ually
able o ou pe o m Uppaal.
0.1
1
10
100
1000
10000
5 10 15 20 25 30 35 40 45 50
Run ime([seconds]
Numbe (o ( imed(au oma a
FDDIcoun
IC3Zone(LCI)
Uppaal
(a) Run ime o e i ica ion
0
50
100
150
200
250
300
350
400
5 10 15 20 25 30 35 40 45 50
UsedCmemo yC[MB]
Numbe Co C imedCau oma a
FDDIcoun
IC3Zone(LCI)
Uppaal
(b) Max. memo y consump ion
Figu e 3.16: Resul s o he expe imen s using he
FDDIcoun
model: Run ime and
memo y consump ion o ou p esen ed app oach IC3 wi h Zones a e compa ed wi h
s a e o he a ool Uppaal o models wi h di e en numbe o imed au oma a in
he NTA
The posi i e impac o he loca ion encoding in combina ion wi h he gene al-
iza ion p ocedu e becomes appa en by his example. Ye , he p esen ed encoding
in oduces addi ional in e es ing e ec s.
82 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES
Loca ion Iden i ie Expe imen s
Wi h ou SMT-encoding elying on boolean a i-
ables o encode he iden i ie s o loca ions, we we e in e es ed whe he he ac ual
assignmen o iden i ie s o loca ions a ec s he pe o mance o ou app oach. To his
end, we examined he un imes o he e i ica ion o he mu ual exclusion p ope y
o he
Fische _U
models as abo e, whe e each loca ion
li
(
i∈ {
0,1,2,3
}
) has iden i-
ie
i
. Addi ionally, we pe o med expe imen s wi h a model
Fische _U(swi ched)
,
whe e loca ion
l0
and
l2
swi ched iden i ie s, meaning
l0
has iden i ie 2 and
l2
has
iden i ie 0. The esul s a e shown in Figu e 3.17.
0.1
1
10
100
1000
10000
100000
5 10 15 20 25 30 35 40 45 50
Run ime([seconds]
Numbe (o ( imed(au oma a
Fische (di e en (Iden i ie s
IC3Zone(LCI)(o iginal(iden i ie s
IC3Zone(LCI)(swi ched(iden i ie s
(a) Run ime o e i ica ion
0
200
400
600
800
1000
1200
1400
1600
1800
5 10 15 20 25 30 35 40 45 50
Usednmemo yn[MB]
Numbe no n imednau oma a
Fische ndi e en nIden i ie s
IC3ZonelLCIwno iginalniden i ie s
IC3ZonelLCIwnswi chedniden i ie s
(b) Max. memo y consump ion
Figu e 3.17: Resul s o he expe imen s using he
Fische _U
models (Figu e 3.1) wi h
dis inc assignmen o iden i ie s o he loca ions: The e i ica ion has been execu ed
using he assignmen o loca ion iden i ie s as used be o e, whe e
li
(
i∈ {
0,1,2, 3
}
)
is assigned iden i ie
i
, and also wi h swi ched assignmen s o iden i ie s o
l0
and
l2, s. . l0is assigned iden i ie 2 and l2is assigned 0
Clea ly, he assignmen o iden i ie s is o impo ance, as he uns wi h swi ched
iden i ie s exhibi wo se pe o mance. Compa ing and analyzing hese uns did no
esul in a de ini e answe o why he uns di e ha much.
In hese expe imen s, swi ching he iden i ie s educed he numbe o cycles o he
main loop wi h ewe CTIs ound. Thus, he loss o pe o mance mus ha e di e en
easons. We no iced ha he ins ances wi h swi ched iden i ie s show a signi ican ly
la ge numbe o SMT-que ies. This inc ease migh be due o he gene aliza ion
p ocedu e needing mo e a emp s o disca d li e als, o due o ames and CTIs
being di e en esul ing in he p ocedu es blockCTIs and s eng henClauses issuing
mo e que ies.
In gene al, i is no easible o chose he assignmen o iden i ie s up on such
ha he pe o mance is op imized. This d awback o he loca ion encoding ia
boolean a iables is opposed o he wide gene aliza ion capabili ies as p esen ed
be o e. Thus, he encoding can be summa ized as ambi alen .
Below, we will examine he e ec s o he numbe o loca ions in a model.
3.5. EVALUATION 83
Loca ion Expe imen s
Ou encoding in oduces many a iables by elying on
he loca ions being encoded ia boolean a iables. Thus, mo e li e als ha e o
be ied o be disca ded du ing gene aliza ion, leading o di e se e ec s. On he
one hand, he inc eased numbe o a iables in oduces addi ional o e head in he
SMT- o mulae and in he gene aliza ion p ocedu e. Howe e , as seen abo e i can
be ex emely bene icial in easoning abou se e al loca ions in a single au oma on
du ing gene aliza ion. In he ollowing, we examine models wi h addi ional loca ions
o ge a mo e gene al iew on he impac o loca ions. To his end, we compa e
he
Fische _B
model wi h he
Fische _U
model since hey bo h model he same
algo i hm. They use he same numbe o clocks and in ege a iables, which a e
used in he same way, only di e ing in smalle de ails, e.g., he in a ian s. The mos
impo an dis inc ion, howe e , is ha he la ge model includes i e addi ional
loca ion, which is mo e han wice as much as he smalle model.
Figu e 3.18(a) shows he compa ison o bo h models o up o 15 au oma a in
he NTA. No e, ha he sa e y p ope y could be p o ed o
Fische _U
models up
o 50 au oma a as shown abo e. In o de o ela e he pe o mance change o ou
algo i hm o he la ge model
Fische _B
, Figu e 3.18(b) shows he compa ison wi h
Uppaal’s pe o mance.
0.1
1
10
100
1000
10000
100000
2 4 6 8 10 12 14
Run imeB[seconds]
Numbe Bo B imedBau oma a
Fische _UB s.BFische _B
IC3Zone(LCI)B o BFische _U
IC3Zone(LCI)B o BFische _B
(a) Run ime o IC3 wi h Zones o bo h models
0.1
1
10
100
1000
10000
100000
2 4 6 8 10 12 14
Run imeC[seconds]
Numbe Co C imedCau oma a
Fische _B
IC3ZonelLCI)
Uppaal
(b) Run ime o IC3 wi h Zones and Uppaal o
Fische _B
Figu e 3.18: Resul s o he expe imen s compa ing he pe o mance o he e i ica-
ions using he wo
Fische
models: IC3 wi h Zones pe o ms signi ican ly wo se o
he Fische _Bmodel
The expe imen s show ha ou app oach pe o ms signi ican ly wo se in he
p esence o many loca ions. The decline is mo e in ense han he one obse ed o
Uppaal, possibly due o ou loca ion encoding being based on boolean a iables,
which in oduces o e head i he numbe o loca ions is la ge. The de e io a ion
migh , howe e , also be due o an unsui able loca ion iden i ie assignmen as seen
in he p e ious pa ag aph o due o he gene al size o he model.
We ex end his insigh wi h he compa ison o un imes o he e i ica ion
expe imen s using he
Lampo _B
and
Lampo _S
models, which only di e by he
84 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES
numbe o loca ions. The un imes o ou app oach o bo h models a e compa ed
in Figu e 3.19, as well as he un imes o Uppaal o bo h models.
0.1
1
10
100
1000
10000
100000
2 4 6 8 10 12 14 16 18
Run imeB[seconds]
Numbe Bo B imedBau oma a
Lampo _SB s.BLampo _B
IC3Zone(LCI)B o BLampo _S
IC3Zone(LCI)B o BLampo _B
(a) Run ime o IC3 wi h Zones o bo h models
0.1
1
10
100
1000
10000
100000
2 4 6 8 10 12 14 16 18
Run imeB[seconds]
Numbe Bo B imedBau oma a
Lampo _SB s.BLampo _B
UppaalB o BLampo _S
UppaalB o BLampo _B
(b) Run ime o Uppaal o bo h models
Figu e 3.19: Resul s o he expe imen s compa ing he pe o mance o he e i ica-
ions using he wo
Lampo
models: IC3 wi h Zones pe o ms signi ican ly be e o
he sh unk Lampo model
Clea ly, ou p esen ed app oach eac s wo se o he addi ional loca ions in he
la ge model. The inc ease o un ime is wo se han he one o Uppaal. The
conclusion d awn be o e is, hus, suppo ed by his expe imen . Ou algo i hm
handles models wi h many loca ions (in he single au oma a) wo se han Uppaal.
Expe imen s wi h he wo dis inc Sha i Lynch models each he same conclusion
(see Tables A.7 and A.8 in he Appendix).
We checked whe he he bad scalabili y in e ms o loca ions is caused by he
loca ion encoding ia boolean a iables. To his end, we eplaced his encoding
ia se e al boolean a iables wi h an al e na i e encoding o he loca ions ia a
single in ege a iable pe au oma on. The esul ing pe o mance was be e , bu
he inc ease was no as signi ican as expec ed. Howe e , he loss o he abili y
o gene alize he loca ions wi hin a single au oma on (as possible wi h boolean
a iables) led o a signi ican ly wo sened pe o mance wi h he
FDDIcoun
model.
In summa y, he usage o an adap ed encoding is possible and migh e en yield a
be e pe o mance o some models, bu we ecommend he usage o he encoding
p esen ed in his chap e due o he imp o ed gene aliza ion abili y.
In he ollowing, we compa e ou app oach wi h he p e ious a emp o u ilize
IC3 o imed au oma a e i ica ion in o de o poin ou he ad ancemen o
ou app oach. We compa e i wi h Kinde mann’s IC3 app oach using he egion
abs ac ion [KJN12b]. Fo a ai compa ison ega ding he used p og amming
language, SMT-sol e , encoding and heu is ic, we eimplemen ed his app oach.
3.5. EVALUATION 85
Used Cons an IC3Regions(LCI) IC3 wi h Zones(LCI)
Run ime (s) Memo y (MB) Run ime (s) Memo y (MB)
1 1186,2 669,6 480,2 264,4
4 2174,3 740,2 483,2 262,6
16 2179,7 741,3 482,6 263,9
64 2860,0 779,7 481,5 263,1
256 2628,4 742,3 483,0 263,7
1024 2860,5 778,3 481,9 264,6
Table 3.2: Scalabili y expe imen s wi h dis inc ime cons an s in he
Fische _U_15(swi ched)model wi h 15 p ocesses
Expe imen s wi h he used Abs ac ion
The employed egion abs ac ion ende s
Kinde mann’s app oach non-p ac ical due o he eno mous numbe he egions. This
insigni icance o he egion abs ac ion o p ac ical pu poses has been explained in
he p e ious chap e . In pa icula , i s exponen ial g ow h in dependence on he size
o ime cons an s is a c ucial a gumen .
Table 3.2 illus a es his signi ican d awback. The sa e y p ope y is e i ied o
Fische _U(swi ched)
models wi h 15 p ocesses and di e en ime cons an s. This
expe imen pe ec ly shows he lack o he egion-based echnique o cope wi h la ge
cons an s, while ou app oach is una ec ed.
Fo illus a ion o his ad an age, we p esen he un imes o Kinde mann’s
app oach o he
Fische _U(swi ched)
,
CSMA/CD
and
FDDI
model in Figu es 3.20,
3.21 and 3.22. These expe imen s clea ly show he imp o emen accomplished by
using he zone abs ac ion.
0.1
1
10
100
1000
10000
100000
5 10 15 20 25
Run imeZ[seconds]
Numbe Zo Z imedZau oma a
Fische _U
IC3Zone(LCI)
IC3Region(LCI)
(a) Run ime o e i ica ion
0
200
400
600
800
1000
1200
1400
1600
5 10 15 20 25
UsedImemo yI[MB]
Numbe Io I imedIau oma a
Fische _U
IC3ZoneRLCIg
IC3RegionRLCIg
(b) Max. memo y consump ion
Figu e 3.20: Resul s o he expe imen s using he
Fische _U(swi ched)
model: Run-
ime and memo y consump ion o ou p esen ed app oach IC3 wi h Zones a e
compa ed wi h he p e ious app oach using he egion abs ac ion o models wi h
di e en numbe o imed au oma a in he NTA

86 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES
0.1
1
10
100
1000
10000
100000
5 10 15 20 25 30
Run imeI[seconds]
Numbe Io I imedIau oma a
CSMA/CD
IC3Zone(LCI)
IC3Region(LCI)
(a) Run ime o e i ica ion
0
200
400
600
800
1000
1200
1400
1600
1800
5 10 15 20 25 30
Used/memo y/[MB]
Numbe /o / imed/au oma a
CSMA/CD
IC3ZoneRLCIg
IC3RegionRLCIg
(b) Max. memo y consump ion
Figu e 3.21: Resul s o he expe imen s using he
CSMA/CD
model: Run ime and
memo y consump ion o ou p esen ed app oach IC3 wi h Zones a e compa ed wi h
he p e ious app oach using he egion abs ac ion o models wi h di e en numbe
o imed au oma a in he NTA
1
10
100
1000
10000
2 4 6 8 10 12 14 16 18 20
Run ime([seconds]
Numbe (o ( imed(au oma a
FDDI
IC3Zone(LCI)
IC3Region(LCI)
(a) Run ime o e i ica ion
0
100
200
300
400
500
600
700
2 4 6 8 10 12 14 16 18 20
UsedImemo yI[MB]
Numbe Io I imedIau oma a
FDDI
IC3ZonegLCI)
IC3RegiongLCI)
(b) Max. memo y consump ion
Figu e 3.22: Resul s o he expe imen s using he
FDDI
model: Run ime and
memo y consump ion o ou p esen ed app oach IC3 wi h Zones a e compa ed wi h
he p e ious app oach using he egion abs ac ion o models wi h di e en numbe
o imed au oma a in he NTA
3.5. EVALUATION 87
In o de o es he p ac icali y one las ime, we e i ied he men ioned sa e y
p ope y o he
Lemgo
model p esen ed abo e. Table 3.3 shows he un ime and
memo y o ou app oach when e i ying he eal wo ld example om Lemgo. I
is appa en , ha he pe o mance is su icien and he p esen ed app oach is o
p ac ical alue.
IC3 wi h Zones(LCI) IC3 wi h Zones(CLI) Uppaal
Run ime Memo y Run ime Memo y Run ime Memo y
Lemgo model 0,7 79,1 0,7 75,2 0,1 35,1
Table 3.3: Expe imen s using ou
Lemgo
model (Figu e 3.12): The un imes (seconds)
and memo y consump ion (MB) a e depic ed o ou app oach IC3 wi h Zones wi h
wo dis inc heu is ics o a iable o de ing (
LCI
and
CLI
), as well as o he ool
Uppaal
3.5.5 Induc i e S eng hening Expe imen s
In addi ion o he e i ica ion esul s ha a e "The e exis s a coun e example ace,
i.e., he p ope y is no in a ian " o "The p ope y is in a ian ", ou echnique yields
an ex a ou come in he la e case. I compu es an induc i e s eng hening o he
sa e y p ope y, which is a o mula encoding an induc i e se o s a es ha all sa is y
he sa e y p ope y. Due o i s induc i eness, i i ially includes all eachable s a es
(which means i is an o e app oxima ion). I can, hus, be used as an easy means
o alida e a success ul e i ica ion. To his end, he h ee p ope ies o induc i e
s eng henings (De ini ion 2.4.1) ha e o be checked. This check again employs
SMT-sol ing and usually signi ican ly ou pe o ms a comple e e- e i ica ion. As a
esul , he addi ional ou come in o m o an induc i e s eng hening can be o huge
impo ance.
Fo illus a ion, conside he ollowing scena io ha in ol es wo pa ies. On he
one hand, he e exis s a clien ha wan s o e i y a sa e y p ope y o a speci ic
model. Howe e , his esou ces in o m o ime and memo y a e usually es ic ed,
s. . he canno execu e he e i ica ion himsel . On he o he hand, he e exis s a
p o ide , e.g., a compu ing cen e , ha possesses he necessa y esou ces and is,
hus, capable o execu ing he desi ed e i ica ion. The impo an aspec in such
scena ios is he ques ion whe he he p o ide is us wo hy and he clien can us
he esul o he p o ide . A his poin a ce i ica e, he e he induc i e s eng hening,
can be employed. To his end, he p o ide ships he ce i ica e o he clien . Since
he alida ion o he ce i ica e is by a easie han he en i e e i ica ion, he clien
is able o alida e i using his limi ed esou ces. I he shipped o mula is indeed an
induc i e s eng hening o he desi ed sa e y p ope y, he clien can be su e ha
he sa e y p ope y is in a ian . Such app oaches a e called p oo -ca ying and a e
widely employed in se e al domains [Nec02], [DKP09].
We ha e pe o med a alida ion o he induc i e s eng henings ound du ing
ou expe imen s in he p e ious chap e . The bene i o alida ion compa ed o
88 CHAPTER 3. TIMED AUTOMATA VERIFICATION VIA IC3 WITH ZONES
e i ica ion is ob ious when conside ing he un imes in Tables A.11 o A.21 wi h
Tables A.1 o A.10. As can be seen, mos induc i e s eng henings ound in ou
expe imen s can be alida ed wi hin seconds. The speed up in compa ison wi h an
en i e e i ica ion un is signi ican ly be e , he la ge he ins ance. In pa icula ,
he e exis smalle ins ances, whe e almos no speed up was measu able. In con as ,
in some la ge ins ances he equi ed ime o alida ion was as small as oughly
0,02% o he ime equi ed o e i ica ion. Wi h i s small size (max. 2 MB in ou
expe imen s) he induc i e s eng henings compu ed by ou echnique a e pe ec ly
sui able o be used in ce i ying scena ios.
In addi ion, hey a e o alue in o he scena ios, whe e we speed up he e i i-
ca ion o a econ igu ed model o eason abou an en i e amily o models. These
app oaches a e p esen ed in he subsequen chap e s.
3.6 Summa y
In summa y, we ha e p esen ed an app oach o he e i ica ion o sa e y p ope ies
o ne wo ks o imed au oma a. To his end, we ha e de eloped a concep ha
combines he success ul algo i hm IC3 wi h he Zone abs ac ion o employ he
un ime and memo y e iciency o i o he e i ica ion o imed sys ems.
We ha e gi en an SMT-encoding ha is designed wi h IC3’s gene aliza ion p oce-
du e in mind. Using backwa ds compu a ion, we ha e shown how o inco po a e he
Zone abs ac ion in o he algo i hm. The necessa y modi ica ions a e only punc ual
and, hus, allow he usage o mos o he op imiza ions p oposed o IC3 so a and
in he u u e.
We ha e implemen ed he concep in Ja a and e alua ed i s s eng hs and
weaknesses in nume ous expe imen s.
The p esen ed echnique scales well and shows p omising esul s. I is com-
pe i i e o s a e-o - he-a ools in many ins ances. Howe e , i s weakness is he
dependence on he size o he en i e s a e space. In con as , o he ools only depend
on he size o he eachable po ion o he s a e space.
Taking in o accoun he addi ional ou come o a success ul e i ica ion in o m
o an induc i e s eng hening o he sa e y p ope y, we conclude ha he p esen ed
echnique is de ini ely o alue ( o example in p oo -ca ying app oaches) and yields
p omising esul s. This addi ional ou come is undamen al o he wo app oaches
p esen ed in he nex chap e s, in which i is used o speed up he e i ica ion o a
econ igu ed model and o eason abou a amily o models.
4
Inc emen al Induc i e Ve i ica ion
o Pa ame e ized Timed Sys ems
In he p e ious chap e , we ha e p oposed a no el combina ion o wo well-known
echniques ha can be used o e i y sa e y p ope ies o imed au oma a. Aiming
a model-based design p ocesses, his echnique is well sui ed o be employed o
he o mal e i ica ion o sa e y p ope ies o eal- ime sys ems. Wi h an inc easing
numbe o sys ems being ime-based and sa e y c i ical, he e exis s a la ge demand
o such echniques.
In some s uc u ed model-based design p ocesses, an i e a i e p ocedu e igge s
a epea ed econ igu a ion o he model un il a inal design is ound. A simila
scena io is he econ igu a ion a li e ime o a sys em, e.g., due o sel -adap a ion.
In hese scena ios, he e exis s a need o e i y p ope ies o econ igu ed models,
which ha e al eady been e i ied be o e o he o iginal model.
Like o he s a e-o - he-a echniques, he p e iously p esen ed app oach does
no co e hese scena ios. I e i ies a sa e y p ope y o a ixed model. In o de
o cope wi h a econ igu ed model, i would es a he e i ica ion om sc a ch
like in o he app oaches. I is, howe e , likely ha he econ igu ed model is only
sligh ly changed. Thus, i is desi able and p omising o euse he esul s o he
p e ious e i ica ion. We s udy his euse in he ollowing. Chap e s 4 and 5 p opose
a wo k low o a es ic ed subse o models and econ igu a ions, while Chap e 6
explo es he gene al case.
Conside he speci ic se ing, whe e he sys em consis s o an a bi a y, bu ixed
numbe o equal p ocesses. Though his se ing is speci ic, i includes a la ge numbe
o si ua ions, e.g., p ocesses communica ing ia a pee o pee p o ocol o execu ing a
mu ual exclusion algo i hm. Using he echnique om he p e ious chap e enables
us o e i y sa e y p ope ies o each such gi en model wi h a ixed numbe o
p ocesses. We a e, howe e , in e es ed in he e i ica ion o he sa e y p ope y o
e e y such model as he numbe o p ocesses is a bi a y. Fo illus a ion conside a
sys em
[P1|| . . . ||Pn]
wi h a ixed numbe
n
o p ocesses ensu ing mu ual exclusion.
A econ igu a ion ha adds an addi ional p ocess equi es an new e i ica ion o
89
96 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS
•∀c∈Cg:π( c)(c) = c(c).
•∀k∈ {1, . . . , n}:∀c∈Cl
k:π( c)(c) = 






c(ci)i k =j,
c(cj)i k =i,
c(c)else,
whe e
ci
and
cj
e e o he clock
c
in au oma on
Ai
(
c∈Cl
i
) and
Aj
(
c∈Cl
j
),
espec i ely.
•∀i ∈ IV6id :π( i)(i ) = i(i ).
•∀i ∈ IVid :π( i)(i ) = 






i i i(i ) = j,
j i i(i ) = i,
i(i )else.
No e, ha we also use
π(m)
o deno e he iden i ie o he au oma on wi h which
m
has been swapped, o mally π(m) = 






i i m =j,
j i m =i,
m else.
The swap ope a ion swaps he loca ions o he wo au oma a. Fu he mo e, i
in e changes he alues o hei local clocks, as well as alues o iden i ie awa e
in ege a iables ha e e o one o he wo au oma a. The swap ope a ion is
applicable, whene e he wo swapped au oma a ha e he same se o loca ions and
local clocks. Howe e , i s applicabili y does no ensu e symme y as de ined below.
No e, ha a pe mu a ion in ol ing mo e han wo au oma a being swapped can
easily be ealized ia se e al swap ope a ions in sequence. We employ his swap
ope a ion o de ine he no ion o symme y equi ed in ou wo k low.
De ini ion 4.2.2
(Symme y o he S a e Space)
.
Le a ne wo k o imed au oma a
NTA =hA1
,...,
Ani
be gi en wi h conc e e seman ics
TS = (S
,
s0
,
→)
. I is symme ic,
i o any swap
π
and any s a es
s1
,
s2∈S
, i holds ha
s1→s2
wi h ime delay
δ
and aken edge
e
o imed au oma on
Ai
i and only i
π(s1)→π(s2)
wi h ime
delay
δ
and aken edge
e
o imed au oma on
Aπ(i)
. Fu he mo e, i mus hold ha
s=s0i and only i π(s) = s0.
Ou de ini ion o symme y ensu es he ini ial s a e o be symme ic, as well as
pa hs o be symme ic. This implies o a s a e
s
ha is eachable ia a pa h om an
ini ial s a e, ha all i s swapped s a es
π(s)
a e eachable ia he espec i e swapped
pa hs. No e, ha he no ion o symme y cha ac e izes
π
o be an au omo phism on
he ansi ion sys em ha is he conc e e seman ics TS (c. . [Hen+04]).
As men ioned abo e, he applicabili y o he swap ope a ion is no su icien o
ensu e his no ion. I can, howe e , be ensu ed ia he speci ic es ic ions on in ege
a iables as abo e. To his end, we o malize ou models as empla es ha a e bound
o hese es ic ions. We ha e p o en in he Appendix B.1 ha all ne wo ks o imed
au oma a c ea ed ia hese empla es mee ou no ion o symme y.

4.3. SPECIFICATION VIA TEMPLATES 97
4.3 Speci ica ion ia Templa es
Symme ic ne wo ks o imed au oma a allowed in ou inc emen al app oach a e
de ined as ins an ia ions o a empla e. A empla e is he abs ac speci ica ion o a
pa ame e ized ne wo k o imed au oma a using he abo e ede ini ions o in ege
a iables. In o de o ac ually c ea e he ne wo k, i is ins an ia ed se e al imes
wi h he dis inc iden i ie s o he au oma a. The esul ing imed au oma a in he
ne wo k a e, hus, dis inc in dependence o hei iden i ie s. In summa y, empla es
a e an in ui i e way o o malizing symme ic models o ou app oach. We de ine
his concep below. I is closely ela ed o he empla es as de ined in Uppaal, bu
imposes he abo e es ic ions on he au oma a.
De ini ion 4.3.1
(Timed Au oma on Templa e)
.
Le he se
Cg
o global clocks be
gi en, as well as he global se o in ege a iables
IV =IV6id ∪ IVid
as he union
o disjoin se s o iden i ie unawa e (
IV6id
) and awa e (
IVid
) in ege a iables, s. .
IV6id ∩ IVid =∅
. A symme ic imed au oma on empla e
A(pid)
de ined o e globally
sha ed
Cg
and
IV
is a uple
A(pid) = (L
,
l0
,
C
,
IV
,
∅
,
In c
,
In i(pid)
,
E(pid))
such
ha
•pid ∈N≥1is a unique pa ame e , called iden i ie ,
•Lis a ini e se o loca ions,
•l0∈Lis he ini ial loca ion,
•C=Cl∪Cg
is he union o he ini e and disjoin se s o local and global clocks
wi h ini ial alua ion c
0,
•IV is he ini e se o sha ed in ege a iables wi h ini ial alua ion i
0,
•∅is he se o synch oniza ion channels (no synch oniza ion is allowed),
•In c:L→Φ(C)is a o al unc ion o clock in a ian s, s. . c
0|=In c(l0),
•In i(pid):L→Ψ(IV,pid)is a o al unc ion o in ege in a ian s,
s. . i
0|=In i(pid)(l0), and
•E(pid)⊆L× {e} × Φ(C)×Ψ(IV
,
pid)×Ω(IV
,
pid)×
2
C×L
is he se o
edges.
Ins an ia ing a empla e
A(pid)
wi h unique iden i ie
pid =j∈N≥1
esul s in
imed au oma on
Aj
. The ollowing example illus a es he p ocess o ins an ia ion.
Example Figu e 4.3 shows he empla e ep esen ing he Fische _Umodel shown
in he p e ious chap e (Figu e 3.1) modeling he Fische mu ual exclusion algo i hm.
I can be used o c ea e he symme ic model wi h any numbe o au oma a. The e
exis s only one in ege a iable (
id
) ha is awa e o iden i ie s and he cons ain s
and assignmen s in ol ing i a e pa ame e ized wi h
pid
. The empla e can be
ins an ia ed, e.g., wi h he wo iden i ie s 1 and 2 esul ing in he au oma a depic ed
98 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS
in Figu e 3.1. When ins an ia ing he empla e wi h a unique iden i ie , e.g.,
pid =
2,
a imed au oma on
A2
is c ea ed in which he pa ame e
pid
is eplaced by he ac ual
iden i ie 2. Fo ins ance, he au oma on con ains he cons ain
id =
2 ins ead o he
pa ame e ized one id =pid.
cn :=cn +1
id:=0;
cn :=cn -1
id=0 c≤1024
c:=0
id=0
c≤1024
id:=pid
c:=0
c>1024
id=pid
c:=0
l0
l3
l1
l2
Figu e 4.3: Example o a imed au oma on empla e ha ep esen s he Fische
mu ual exclusion algo i hm (Fische _U)
We employ empla es as in ui i e means o speci y a pa ame e ized imed sys em
modeled as symme ic ne wo k o imed au oma a. In o de o c ea e a model o a
ixed numbe
n∈N≥1
o au oma a, he empla e is ins an ia ed
n
imed wi h he
espec i e iden i ie s 1 o
n
. We o malize his c ea ion o a symme ic ne wo k o
imed au oma a wi h ixed numbe o au oma a below.
De ini ion 4.3.2
(Symme ic Ne wo k o Timed Au oma a)
.
Gi en
n∈N≥1
and
he imed au oma on empla e
A(pid)
as de ined in De ini ion 4.3.1. The symme ic
ne wo k o imed au oma a wi h
n
imed au oma a is de ined as
NTAn=hA1
,
. . .
,
Ani
,
whe e Aiis he ins an ia ion o A(pid)wi h pid =i(i∈ {1, . . . , n}).
This de ini ion o ne wo ks o imed au oma a ia empla es ensu es he models
o be symme ic. Sec ion B.1 in he Appendix p o es ou no ion o symme y o
hold o he models.
In addi ion o symme ic models, ou echnique elies on he sa e y p ope y o
be symme ic, oo. I is de ined as ollows.
De ini ion 4.3.3
(Symme y o he Sa e y P ope y)
.
Le a ne wo k o imed au oma a
NTA =hA1
,...,
Ani
be gi en wi h conc e e seman ics
TS = (S
,
s0
,
→)
. Gi en any
swap
π
and s a e
s∈S
, a sa e y p ope y
ρ
is symme ic i i holds ha
s|=ρ
i and
only i π(s)|=ρ.
We ensu e his symme y ia ede ini ion o he sa e y p ope y. The adap ed
de ini ion includes all pe mu a ions o imed au oma a in he ne wo k and, hus, is
inhe en ly symme ic.
4.3. SPECIFICATION VIA TEMPLATES 99
Recall he de ini ion o e o s a e speci ica ions (De ini ion 2.1.13). An e o
s a e speci ica ion
e
easons abou he loca ions, in ege and clock alua ions o
s a es in a ne wo k
NTAm
o
m
imed au oma a. In o de o employ he e o s a e
speci ica ion also o la ge models o size
n≥m
(as in a pa ame e ized sys em),
we c ea e a scaled e o s a e speci ica ion
e n
. To his end, he pa ial loca ion
ec o simply needs o be illed wi h he unspeci ied loca ion elemen (
∗
) o all
addi ional au oma a. We ob ain a symme ic e o s a e speci ica ion by conside ing all
pe mu a ions o he n imed au oma a.
De ini ion 4.3.4
(Symme ic E o S a e Speci ica ion)
.
Gi en an e o s a e speci ica-
ion
e = ( ¯
lm
,
φ
,
ψ)
o
NTAm
as in De ini ion 2.1.13, whe e
ψ=ψ0∧ψ1(
1
)∧ · · · ∧
ψm(m)
con ains pa ame e ized cons ain s o he
m
au oma a. The scaled e o s a e
speci ica ion o
NTAn
(
n≥m
) is de ined as
e n= (¯
l
,
φ
,
ψ)
wi h
∀i∈ {
1,
. . .
,
m}:
¯
l[i] = ¯
lm[i]and ∀i∈ {m+1, . . . , n}:¯
l[i] = ∗.
The symme ic e o s a e speci ica ion o
NTAn
is de ined as
e n
sym =∃π:e n
π
o pe mu a ion π(c . De . 4.2.1) wi h e n
π= (π(¯
l),π(φ),π(ψ)) being de ined as
•∀i∈ {1, . . . , n}:π(¯
l)[i] = ¯
l[π(i)],
•π(φ) = 












π(φ1)∧π(φ2)i φ=φ1∧φ2,
(π(x)−π(y)) ./ ni φ= (x−y)./ n,
π(x)./ ni φ=x./ n,
ue i φ= ue,
whe e
π(x)
e e s o clock
x
i sel i
x∈Cg
o o he wise e e s o he espec i e
clock in Cl
π(i)i x∈Cl
i,
•π(ψ) = ψ0∧ψ1(π(1)) ∧ · · · ∧ ψm(π(m)).
Wi h he exis en ial quan i ica ion, which is eplaced by enume a ion and dis-
junc ion in he SMT-encoding, any combina ion o imed au oma a is possible and,
hus, he e o s a e is symme ic. Fo illus a ion, conside he ollowing example.
Example 4.3.5.
Le he model
Fische _U_
3 be gi en (
n=
3). Conside an e o
s a e speci ica ion
e = ((∗
,
l1)
,
c1≤
0,
cn ≤
1
∧id =
1
)
e e ing o
m=
2 imed
au oma a, namely
A1
and
A2
, and
c1
deno ing clock
c
in
A1
. I speci ies ha
any s a e is an e o s a e ha includes loca ion
l1
o au oma on
A2
, a alue o
c
o
A1
less o equal o 0, and
cn ≤
1 and
id =
1. As can be seen, he imed
au oma on
A3
is no e e ed. The scaled e sion simply s a es ha he loca ion
o
A3
is unde ined, o mally
e 3= ((∗
,
l1
,
∗)
,
c1≤
0,
cn ≤
1
∧id =
1
)
. When
conside ing he swap
π1=swap1,2
he esul ing pe mu ed e o s a e speci ica ion is
e 3
π1= ((l1
,
∗
,
∗)
,
c2≤
0,
cn ≤
1
∧id =
2
)
, whe e
c2
deno es clock
c
in
A2
. Ano he
swap migh be
π2=swap1,3
esul ing in he speci ica ion
e 3
π2= ((∗
,
l1
,
∗)
,
c3≤
0,
cn ≤
1
∧id =
3
)
wi h
c3
deno ing clock
c
in
A3
. In o de o achie e symme y, all
pe mu a ions ha e o be conside ed.
100 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS
Wi h enume a ion, he symme ic e o s a e speci ica ion is as ollows.
e 3
sym =((∗,l1,∗),c1≤0, cn ≤1∧id =1)
∨((∗,∗,l1),c1≤0, cn ≤1∧id =1)
∨((l1,∗,∗),c2≤0, cn ≤1∧id =2)
∨((∗,∗,l1),c2≤0, cn ≤1∧id =2)
∨((∗,l1,∗),c3≤0, cn ≤1∧id =3)
∨((l1,∗,∗),c3≤0, cn ≤1∧id =3)
I any o hem is sa is ied by a s a e
s
, hen
s
is an e o s a e. T i ially, any swap
π(s)
is also an e o s a e, since all pe mu a ions o he e o s a e speci ica ion a e
conside ed.
The abo e symme ic e o s a e speci ica ions allow o he de ini ion o sym-
me ic sa e y p ope ies.
De ini ion 4.3.6
(Symme ic Sa e y P ope y)
.
Le
NTAn
be a gi en ne wo k o
n
imed au oma a. The symme ic sa e y p ope y is de ined as
ρn=¬(e
1
n
sym)∧
¬(e 2n
sym)∧. . . o symme ic e o s a e speci ica ions e 1n
sym,e 2n
sym,. . . .
Gi en he abo e de ini ions, we de ine he ac ual e i ica ion ques ions we a e
in e es ed in when conside ing pa ame e ized imed sys ems.
Ve i ica ion Ques ion:
Gi en he imed au oma on empla e
A(pid)
and
a symme ic sa e y p ope y
ρ
, does he sa e y p ope y
ρn
hold o all
ne wo ks o imed au oma a
NTAn
consis ing o
n∈N≥1
ins an ia ions
o he empla e?
Since he e o s a es in he sa e y p ope y a e de ined o models wi h mo e han o
exac ly
m
imed au oma a, we say
ρn
holds o
NTAn
wi h
n<m
, bu need o e i y
he p ope y o all
n≥m
. In he ollowing, we sho ly elabo a e on he decidabili y
o his e i ica ion ques ion.
4.4 Decidabili y
In gene al, he abo e e i ica ion ques ion is undecidable. T i ially, he a gumen-
a ion o he p e ious chap e (Subsec ion 3.4.1) can be applied o ou symme ic
models as well. One eason o undecidabili y is he exis ence o upda es on he iden-
i ie unawa e in ege a iables as has been shown ia educ ion in he men ioned
subsec ion. An addi ional issue in he abo e e i ica ion ques ion is he ixed, bu
a bi a y la ge numbe o imed au oma a. This allows o a educ ion ha exploi s
he numbe o au oma a as shown by Abdulla e al. [ADM04] o imed ne wo ks.
Thei educ ion can be adap ed o i ou o malism by ep esen ing he con olle
ia an in ege a iable and using a global clock in combina ion wi h addi ional
in ege a iables o synch oniza ion o edges.
4.5. BASIC APPROACH 101
Thus, he e i ica ion ques ion o pa ame e ized imed sys ems is in gene al
undecidable. Howe e , Abdulla has shown ha he e exis some decidable ins ances,
e.g., when a p ocess includes a mos one clock like in he Fische models [AJ03].
Ou expe imen s a e in line wi h hese insigh s. Hence, an app oach answe ing he
gi en e i ica ion ques ion is easonable o some models. We show ou inc emen al
echnique o his p oblem in he ollowing.
4.5 Basic App oach
We p opose o inc emen ally e i y he symme ic models wi h inc easing numbe
n
o imed au oma a. To his end, we ha ness he symme y and composi ion aspec
esul ing in a Te mina ion Theo em ha ensu es he sa e y p ope y o hold o all
n∈Nupon success ul applica ion.
Valid
o ]NTAn+1?
Check]Sa e y]P ope y
o ]NTAn]
CEX
n:=n+1 [no]
[yes]
Sa e y]P ope y]holds] o ]all]n
Induc i e]s eng hening
n=max(1,m,
Ex apola e
Figu e 4.4: Basic wo k low
The wo k low can be seen in Figu e 4.4. I comp ises a loop ha is inde ini ely
i e a ed un il he Te mina ion Theo em is applicable, i.e., ou ex apola ion p oduces
a alid induc i e s eng hening o
NTAn+1
. Howe e , since he e i ica ion ques ion
is undecidable in gene al, he e exis ins ances ha un inde ini ely wi h ou heo em
ne e being applicable. The app oach is en i ely based on SMT-sol ing and wo ks
as ollows. Ou wo k low s a s wi h he smalles model. Taking in o accoun ha
he sa e y p ope y is speci ied o e
m
imed au oma a (c . De ini ion 4.3.4), we s a

102 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS
wi h a ne wo k o imed au oma a
NTAn
, whe e
n=max(
1,
m)
. The symme ic
sa e y p ope y
ρn
is e i ied o
NTAn
using ou IC3-based echnique IC3 wi h
Zones p esen ed in he p e ious chap e p o iding an induc i e s eng hening o he
sa e y p ope y in case o success. O he wise, a coun e example ace is ound and
he sa e y p ope y does no hold o all
n∈N≥1
. The induc i e s eng hening is
p o ided as an SMT- o mula
kFk
in conjunc i e no mal o m. I is a conjunc ion
o clauses, which consis o loca ion, clock and in ege li e als easoning abou he
n
imed au oma a in he model
NTAn
. In o de o use i o he nex la ge model
NTAn+1
, we execu e a subsequen ex apola ion s ep. De ini ion 4.5.1 speci ies his
ex apola ion p ocedu e wi h which we yield an SMT- o mula
kFkexp(n+1)
easoning
abou all imed au oma a in NTAn+1.
De ini ion 4.5.1
(Ex apola ion o an Induc i e S eng hening)
.
Gi en he SMT-
o mula
kFk
ep esen ing he induc i e s eng hening
F
o sa e y p ope y
ρn
o
he ne wo k o imed au oma a
NTAn
.
kFkexp(x)
is he SMT- o mula ep esen ing
he Ex apola ion o
F
o a ne wo k
NTAx
o
x≥n
imed au oma a.
kFkexp(x)
is
de ined as he SMT- o mula ep esen ing he conjunc ion o
π(F)
o all possible
pe mu a ions
π
o he
x
imed au oma a. To his end,
kFk
is pe mu ed acco ding
o he ope a ion
swap
, i.e., loca ion li e als a e swapped, as well as local clocks and
alues o iden i ie awa e in ege a iables di e en om he neu al elemen 0.
The implemen a ion o he ex apola ion p ocedu e pe mu es clauses sepa a ely.
To his end, only clauses ha a e no iden ical up o pe mu a ion a e conside ed. This
allows an e icien handling o clauses and esul s in a low un ime. The ollowing
example illus a es he abo e ex apola ion p ocedu e.
Example 4.5.2.
Conside he imed au oma on empla e depic ed in Figu e 4.3. The
ins an ia ion o
n=
2 esul s in he symme ic ne wo k o imed au oma a depic ed
in Figu e 3.1. The e i ica ion o he symme ic sa e y p ope y
ρ:=¬(cn >
1
)
compu es he induc i e s eng hening as depic ed in Table 4.1 in he second
column. The e exis i e clauses ha a e no iden ical up o pe mu a ion. The i s
column o Table 4.2 depic s ep esen a i es o hese clauses. The applica ion o
he ex apola ion p ocedu e compu es all pe mu ed clauses o hese ep esen a i es
o all pe mu a ions o he
n+
1
=
3 imed au oma a. The iden i ie awa e in ege
a iable
id
is ep esen ed in he encoding as
in 0
and has o be conside ed in he
pe mu a ions whene e he compa ed alue in he li e al is a speci ic iden i ie .
The iden i ie unawa e in ege a iable
cn
is ep esen ed in he encoding as
in 1
and mus no be conside ed in he pe mu a ions a all. In addi ion, all loca ion
and local clock a iables ha e o be conside ed o he pe mu a ions. The esul ing
clauses a e depic ed in he second column o he men ioned able. As can be
seen, he ex apola ed o mula equals he induc i e s eng hening compu ed in
he p e ious chap e o
Fische _U_
3. I shows ha i is possible o in e a alid
induc i e s eng hening o he sa e y p ope y o
n+
1 au oma a om an induc i e
s eng hening o he sa e y p ope y o
n
au oma a. Ou wo k low elies on his
po en ial.
4.5. BASIC APPROACH 103
ep esen a i e clause om kFk kFkexp(3)
(in 1≤1) (in 1≤1)
∧((in 06=0)∨(in 1≤0)) ∧((in 06=0)∨(in 1≤0))
∧(¬l1
0∨l1
1∨(in 1≤0)) ∧(¬l1
0∨l1
1∨(in 1≤0))
∧(¬l2
0∨l2
1∨(in 1≤0))
∧(¬l3
0∨l3
1∨(in 1≤0))
∧(l1
0∨(in 06=1)∨(in 1≤0)) ∧(l1
0∨(in 06=1)∨(in 1≤0))
∧(l2
0∨(in 06=2)∨(in 1≤0))
∧(l3
0∨(in 06=3)∨(in 1≤0))
∧((c1
0≤1024.0)∨(in 06=1)∨(c2
0>1024.0)) ∧((c1
0≤1024.0)∨(in 06=1)∨(c2
0>1024.0))
∧((c1
0≤1024.0)∨(in 06=1)∨(c3
0>1024.0))
∧((c2
0≤1024.0)∨(in 06=2)∨(c1
0>1024.0))
∧((c2
0≤1024.0)∨(in 06=2)∨(c3
0>1024.0))
∧((c3
0≤1024.0)∨(in 06=3)∨(c2
0>1024.0))
∧((c3
0≤1024.0)∨(in 06=3)∨(c1
0>1024.0))
Table 4.2: Each o he clauses ( ha a e no iden ical up o pe mu a ion) in he com-
pu ed induc i e s eng hening o
n
au oma a (le ) is pe mu ed o all pe mu a ions
o he n+1 au oma a in o de o c ea e he ex apola ed o mula ( igh )
The esul ing ex apola ed o mula
kFkexp(n+1)
is deno ed as candida e induc i e
s eng hening o
NTAn+1
. I is hen checked o alidi y, i.e., whe he all h ee
cha ac e is ics o induc i e s eng henings hold ue o he ex apola ed o mula
kFkexp(n+1)
and model
NTAn+1
. I in alid,
n
is inc emen ed and he nex i e a ion
o he loop is s a ed. O he wise, he candida e ep esen s a alid induc i e s eng h-
ening o
ρn+1
o
NTAn+1
, in which case ou Te mina ion Theo em (Theo em 4.5.1)
applies. I s a es ha he sa e y p ope y holds
∀n∈N≥1
, i he candida e is a alid
induc i e s eng hening.
Theo em 4.5.1
(Te mina ion Theo em)
.
Gi en he SMT- o mula
kFk
ep esen ing an
induc i e s eng hening F o
ρn
o
NTAn
. I
kFkexp(n+1)
is an induc i e s eng hening o
ρn+1 o NTAn+1, hen kFkexp(n+2)is an induc i e s eng hening o ρn+2 o NTAn+2.
The p oo o co ec ness is gi en in he subsequen chap e o a mo e gene al
o malism.
The inc emen al design o he wo k low yields he bene i o s a ing wi h
small ne wo ks o imed au oma a, which a e e icien ly e i iable. Thus, a as
o e all pe o mance o ou app oach is likely in case he Te mina ion Theo em can
be applied ea ly. Addi ionally, ou heo em is mos sui able o an inc emen al
wo k low, being able o eason abou all
n∈N≥1
by aking in o accoun he esul s
o a speci ic ins ance.
We illus a e he wo k low in he ollowing.
Example 4.5.3.
As an example conside he
Fische _U
empla e as gi en in Figu e
4.3 wi h he symme ic sa e y p ope y ρ:=¬(cn >1)speci ying alues o x=0
imed au oma a. Ou wo k low s a s wi h he e i ica ion o he sa e y p ope y
o he symme ic ne wo k o
n=
1 imed au oma a
NTAn
. A e success ul
e i ica ion, he ound induc i e s eng hening
kFk= (in 1≤
1
)∧(l1
0∨(in 1≤
0
)) ∧(l1
1∨(in 1≤
0
))
is e u ned as can be seen in Table 4.1. The ex apola ion
p ocedu e p oduces a candida e o mula wi h i e clauses, namely
kFkexp(n+1)=
104 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS
(in 1≤
1
)∧(l1
0∨(in 1≤
0
)) ∧(l2
0∨(in 1≤
0
)) ∧(l1
1∨(in 1≤
0
)) ∧(l2
1∨(in 1≤
0
))
.
The candida e is no induc i e o
NTAn+1
, as Consecu ion ails. Thus, he nex cycle
s a s wi h he e i ica ion o he sa e y p ope y
ρn
o
NTAn
wi h
n=
2. A e
success ul e i ica ion he esul ing induc i e s eng hening is again ex apola ed
in o a candida e, which is checked o alidi y (which means whe he Theo em 4.5.1
is applicable). This cycle is i e a ed inde ini ely un il he heo em can be applied, a
coun e example ace is ound du ing a un o IC3 wi h Zones o he sys ems uns
ou o memo y o ime.
4.6 Op imiza ions
Technically, he p esen ed wo k low can be ealized using any e i ica ion echnique
esul ing in an induc i e s eng hening as de ined abo e. Howe e , we designed
some op imiza ions ailo ed speci ically o ou algo i hm IC3 wi h Zones shown in
Chap e 3. We p esen hese op imiza ions in he ollowing, namely a
Feedback
-loop
and he
Gene aliza ion
o he ound induc i e s eng hening. These enhancemen s
ha e dis inc aims wi hin he wo k low. The la e is designed o inc ease he
applicabili y o Theo em 4.5.1, while he o me is cons uc ed o speed up he
e i ica ion o models in he IC3 algo i hm i sel . We s a wi h a de ailed desc ip ion
o his speed-up op imiza ion.
4.6.1 Feedback Loop
Du ing he basic loop o ou wo k low, we p opose a candida e induc i e s eng hen-
ing
kFkexp(n+1)
o he nex la ge model
NTAn+1
. In case he Te mina ion Theo em
can no be applied, i.e., he candida e is no a alid induc i e s eng hening, i is
disca ded so a . I migh , howe e , be o subs an ial alue. E en hough i is no a
alid induc i e s eng hening i migh be simila o one, as some o i s clauses migh
occu wi hin a alid induc i e s eng hening. These clauses should be ex ac ed
and used o accele a e he e i ica ion p ocess. To his end, he p oposed candida e
is injec ed in o he e i ica ion un o IC3 wi h Zones o
NTAn+1
. We call his a
Feedback
-loop, since he clauses o he candida e a e ed back in o he cycle ins ead
o simply being disca ded. In o de o decide, which o he clauses a e ele an , i.e.,
can be eused wi hou b eaking he p ope ies o he ames in he IC3 algo i hm, we
use wo dis inc me hods. On he one hand, we employ he inc emen al me hod o
Chockle e al. [Cho+11] o injec an induc i e subse o he clauses in he candida e
o mula in o each ame o IC3. On he o he hand, we employ ou own me hod
o injec clauses ha a e induc i e ela i e o he se o ini ial s a es ( ame
F0
) in o
he ame F1. We deno e he o me one as Chockle -Feedback and he la e one as
F ame1-Feedback. Bo h me hods a e shown below.
Chockle -Feedback
The ollowing me hod is aken om Chockle e al. [Cho+11],
whe e i is used o inc emen al e i ica ion o ha dwa e models. I sea ches o he
la ges subse o he clauses in he candida e o mula
kFkexp(n+1)
ha is induc i e.
4.6. OPTIMIZATIONS 105
This se o clauses can, hus, be conjoined o all ames in IC3 wi h Zones. As a
esul , he sea ch space o CTIs in he ames is p uned hea ily up on . Fo mally,
i sea ches he la ges subse
C⊆clauses(kFkexp(n+1))
o clauses in he candida e
ha is induc i e, i.e.,
•Ini ia ion: kIn+1k ∧ ¬kCkis unsa is iable,
•Consecu ion: kCk ∧ kTn+1k ∧ ¬kCk0is unsa is iable,
wi h he o mulae
kIn+1k
and
kTn+1k
deno ing he encoding o he se o ini ial
s a es and he ansi ion ela ion o
NTAn+1
wi h in a ian s as shown, e.g., in
Subsec ion 3.1.10.
The conjunc ion o each o he ames wi h he se
C
o clauses clea ly p ese es
he ou p ope ies o he ames, as
C
is induc i e. I is ex emely powe ul
in p uning he conside ed s a es in he ames. Howe e , we obse ed ha he
induc i e se o clauses
C
is a he small o some models, since many o he clauses
hinde induc i eness. Despi e being o alue o he IC3 algo i hm, hese clauses
a e disca ded. Fo his eason, we cons uc ed a weake Feedback me hod de ailed
below.
F ame
1
-Feedback
Ins ead o sea ching an induc i e subse o clauses ha a e
conjoined o e e y ame, ou
F ame
1-Feedback sea ches a subse o clauses ha
is induc i e ela i e o he se o ini ial s a es, bu can only be conjoined o ame
F1
. Fo mally, gi en he p oposed candida e o mula
kFkexp(n+1)
, we compu e he
la ges subse C⊆clauses(kFkexp(n+1))o clauses ha a e ini ialized and induc i e
ela i e o F0=In+1:
•Ini ia ion: kIn+1k ∧ ¬kCkis unsa is iable,
•Consecu ion ela i e o In+1:kIn+1k ∧ kTn+1k ∧ ¬kCk0is unsa is iable,
wi h he o mulae
kIn+1k
and
kTn+1k
deno ing he encoding o he se o ini ial
s a es and he ansi ion ela ion o
NTAn+1
wi h in a ian s as shown, e.g., in
Subsec ion 3.1.10.
The esul is injec ed in o IC3 wi h Zones as clauses o ame
F1
(c . Sec ion 2.4),
which may p e en he cos ly edisco e y o some o hem. Al hough he conjunc ion
wi h
F1
does no p une he la ge ames
F2
,
. . .
he me hod is o impo ance. Clea ly,
he numbe o clauses in
C
is no smalle in he
F ame
1-Feedback han in he
Chockle
-Feedback, as an induc i e se o clauses is also induc i e ela i e o
F0
.
Fu he mo e, he clauses o he la e me hod can be p opaga ed o la ge ames
du ing he un o IC3 wi h Zones. Thus, he es ic ion o he
F ame
1-Feedback o
conjoin clauses only wi h F1is no a se ious cu back.
Bo h hese eedback me hods can be used sepa a ely o in combina ion. Fu -
he mo e, hei implemen a ion is simple as he clauses only ha e o be checked
and inse ed a he s a o IC3 wi h Zones and he es o he algo i hm p oceeds
en i ely as be o e. Ou implemen a ion is based on he one desc ibed by Chockle e
al. [Cho+11] using auxilia y a iables o inding he injec ed subse s.
112 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS
esul ing induc i e s eng hening migh be di e en , which in u n a ec s he
subsequen cycles o ou app oach. Thus, he
Feedback
-op imiza ion has a signi ican
impac on ou app oach.
In he ollowing, we e alua e whe he he combina ion o bo h op imiza ions
u he imp o es he pe o mance. As s a ed be o e, his combina ion allows o wo
op ions. On he one hand, he ex apola ed gene alized se o clauses can be used
in he
Feedback
-loop. On he o he hand, he ex apola ed non-gene alized se o
clauses can be used.
Table 4.7 shows he pe o mance using he wo op ions.
Fische _U
Fische _U
(swi ched)
Fische _B
Lampo _B
Lampo _S
Sha i Lynch_B
Sha i Lynch_P
Feedback using non-gene alized se o clauses (all clauses)
Chockle - Run ime (s) 1,3 2,0 55,1 OOM 1,3 OOT OOM
Chockle - Ve i ied
∀n∈N∀n∈N∀n∈N1-7 ∀n∈N1-3 1-6models NTAn
o which n?
F ame1 - Run ime (s) 1,2 1,1 34,9 9,0 1,7 199,7 OOT
F ame1 - Ve i ied
∀n∈N∀n∈N∀n∈N∀n∈N∀n∈N∀n∈N1-4models NTAn
o which n?
Bo h - Run ime (s) 1,3 1,2 36,0 55,7 1,6 958,1 OOT
Bo h - Ve i ied
∀n∈N∀n∈N∀n∈N∀n∈N∀n∈N∀n∈N1-4models NTAn
o which n?
Feedback using gene alized se o clauses
Chockle - Run ime (s) 1,3 2,0 50,5 OOM 1,4 OOM 880,3
Chockle - Ve i ied
∀n∈N∀n∈N∀n∈N1-8 ∀n∈N1-3 ∀n∈Nmodels NTAn
o which n?
F ame1 - Run ime (s) 1,5 1,1 35,4 OOM 1,5 6622,6 OOT
F ame1 - Ve i ied
∀n∈N∀n∈N∀n∈N1-8 ∀n∈N∀n∈N1-4models NTAn
o which n?
Bo h - Run ime (s) 1,3 1,1 35,7,1 OOM 1,6 6981,5 OOT
Bo h - Ve i ied
∀n∈N∀n∈N∀n∈N1-8 ∀n∈N∀n∈N1-4models NTAn
o which n?
Table 4.7: Run ime needed o he e i ica ion o a symme ic sa e y p ope y o
he pa ame e ized imed sys ems using he wo k low wi h bo h op imiza ions. The
sa e y p ope y was e i ied o he en i e pa ame e ized sys em (ma ked as
∀n∈N
in he second ow) o o only a ew ins ances wi h ixed
n
, whe e we gi e he sizes
o he models ha we e success ully e i ied
Clea ly, he expe imen s show ha he combina ion o op imiza ions does no
imp o e he o e all pe o mance. The basic wo k low op imized only by he
F ame
1-
Feedback loop s ill shows he bes esul s.
In summa y o he abo e expe imen s, we conclude ha ou wo k low is o alue,
e en i he e i ica ion un is incomple e. I e i ies smalle models wi h ixed
n∈N
be o e unning ou o ime o memo y and is, hus, no en i ely useless in such a

4.7. EVALUATION 113
Fische _U
Fische _U
(swi ched)
Fische _B
Lampo _B
Lampo _S
Sha i Lynch_B
Sha i Lynch_P
Run ime (s) 1,6 1,2 87,8 8,5 1,7 28,1 2778,5
Ve i ied
∀n∈N∀n∈N∀n∈N∀n∈N∀n∈N∀n∈N∀n∈Nmodels NTAn
o which n?
Uppaal - Run ime (s) 0,7 0,7 17,8 5,3 0,4 0,3 1218,5
Uppaal - Ve i ied
8 8 5 6 6 4 13models NTAn
o which n?
IC3 - Run ime (s) 0,9 0,8 6,7 5,3 1,1 17,3 149,5
IC3 - Ve i ied
2 2 2 2 2 2 3models NTAn
o which n?
Table 4.8: Compa ison o ou wo k low ( i s ows) wi h e i ica ions o ins ances
wi h ixed n ha could be e i ied in he same ime
case. Fu he mo e, ou p oposed
Feedback
-op imiza ion accele a es he uns o ou
IC3 wi h Zones algo i hm, which ende s la ge models e i iable ha could no be
e i ied wi hou he injec ed clauses. The o e all pe o mance o he wo k low using
he op imiza ions is e y p omising and he echnique, in gene al, has he bene i
o e i ying pa ame e ized imed sys ems o all
n∈N
. In o de o illus a e his
bene i , we show a compa ison wi h e i ica ions o models wi h ixed
n∈N
below.
4.7.2 Compa ison wi h ixed Models
We demons a e his bene i by compa ison wi h he ool Uppaal and a single
e i ica ion un o ou algo i hm IC3 wi h Zones o he p e ious chap e . As hese
ools can only e i y models wi h a ixed
n∈N
, we show he la ges model wi h
ixed
n
ha hese ools we e able o e i y in he same ime ha he abo e p esen ed
echnique equi es o he e i ica ion o he en i e pa ame e ized sys em o all
n∈N. Table 4.8 shows he un imes and sizes o he e i ied models.
The p esen ed inc emen al wo k low (using he op imiza ion F ame1-Feedback)
clea ly imp o es he e i ica ion o single models wi h ixed size. Due o i s abili y o
ex apola e induc i e s eng henings o la ge models, i is able o eason abou all
n∈N
by only e i ying small models. The euse o p e ious compu a ion esul s by
injec ing clauses o he candida e in he nex e i ica ion un addi ionally inc eases
he e iciency. Thus, ools capable o only e i ying models wi h ixed
n∈N
a e no
able o compe e wi h he p esen ed app oach.
In he ollowing, we illus a e he impo ance o induc i e s eng henings o
alida ion and euse. I known, an induc i e s eng hening can easily be alida ed
as shown in Subsec ion 3.5.5. Ou app oach esul s in an induc i e s eng hening
ha can be ex apola ed o any
n∈N
. We show he alida ion ime o Uppaal’s
Fische model (
Fische _U
). No e, ha Uppaal was only able o e i y models up
o
n=
13 and ou app oach o he p e ious chap e has e i ied models up o
114 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS
Fische _Un=10 n=20 n=30 n=40 n=50 n=100
Time (s) 0,8 1,5 3,7 6,8 12,7 135,3
Table 4.9: Valida ion imes o he induc i e s eng henings compu ed and ex apo-
la ed by he p esen ed app oach
n=
50. Table 4.9 shows he ime needed o alida e he ex apola ed induc i e
s eng henings o models wi h ixed n.
Clea ly, he app oach p esen ed in his chap e pe o ms well. Due o he
p esen ed Te mina ion Theo em, such a alida ion is no necessa y. Ou inc emen al
wo k low p o ides o a e i ica ion o all n∈Nupon success.
4.8 Rela ed Wo k
The ela ed wo k o IC3 and e i ica ion o sa e y p ope ies o imed au oma a has
been p esen ed in Chap e 2. The ollowing ela ed wo k is, hus, only conce ned
wi h he e i ica ion o sa e y p ope ies o pa ame e ized ( imed) sys ems and
symme y.
Pa ame e ized Sys ems
The e exis nume ous publica ions conce ning he un-
imed case. I has been shown ha his e i ica ion ques ion is, in gene al, unde-
cidable [AK86]. Ye , se e al wo ks deal wi h his e i ica ion ques ion, esul ing
in semi-algo i hms o wo king wi h es ic ed amilies o models. The wo ks o
pa ame e ized sys ems migh be ca ego ized as ollows.
Ne wo k In a ian s:
Many o hese app oaches equi e human in e ac ion, e.g.,
he p oposi ion o an in a ian o closu e. Wolpe e al. [WL90] equi e he
manual speci ica ion o a ne wo k in a ian . The in a ian s a e used o check
whe he he p ope y holds ue o he en i e se o models. The manual
speci ica ion, howe e , is a d awback. A simila inding has been made by
Ku shan and McMillan [KM89], whe e he in a ian is deno ed as p ocess
in a ian . I is used o e i ica ion o he en i e se o models, bu needs o
be speci ied manually. Se e al app oaches y o o e come he p oblem o
manual p oposi ion o an in a ian . They syn hesize in a ian s au oma ically,
e.g., based on on ne wo k g amma s and abs ac ion (Cla ke e al. [CGJ95]) o
based on a ixpoin compu a ion using heu is ics (Lesens e al. [LHR97]).
Regula Model Checking:
O he app oaches a e based on eachabili y analysis
wi h s a es ep esen ed as wo ds and ini e s a e ansduce s in be ween. These
echniques a e deno ed as egula model checking and di e by he employed
models, ansduce s and widening ope a o s. Bouajjani e al. we e amongs
he i s o publish abou his echnique [Bou+00]. Ano he ep esen a i e
is Kes en e al. [Kes+97] using symbolic model checking. Abdulla e al.
ex ended he echniques in a ious di ec ions. They examined he e ec o
ha ing global condi ions [Abd+99], and in oduced inc emen al upda es o he
4.8. RELATED WORK 115
ansduce s [Abd+02b]. Fu he wo k conce ns o he imp o emen s [Abd+03]
and speci ic s uc u es [Abd+02a], [BT02].
Symme y Reduc ion:
In addi ion o he abo e echniques some esea che s educe
he e i ica ion in pa ame e ized sys ems o he one in a quo ien s uc u e,
which only includes ep esen a i es o symme ic s a es. Two impo an wo ks
in his ield a e Eme son e al. [ES96] and Cla ke e al. [Cla+96]. La e , Eme son
e al. [ES97] and Gyu is e al. [GS97] in oduced ai ness and on- he ly model
checking o he app oach. The usage o symme y in quo ien s uc u es was
imp o ed by an explici modeling o symme ic a iables, deno ed scala se s,
by Ip and Dill [ID96]. This explici modeling is close o he one employed in
ou wo k, whe e we explici ly de ine in ege a iables
IVid
ha a e a ec ed
by symme y. Howe e , he echnique closes o ou s is he ollowing.
In isible In a ian s:
Pnueli e al. [PRZ01], [A o+01] in oduced an app oach ha
au oma ically compu es s eng henings o p ope ies ha may be used o
p o e he p ope y o all models. To his end, hey employ a p ojec -abs ac -
p ocedu e, whe e he se o eachable s a es is compu ed, which is p ojec ed
o a smalle model (some e e ences o a iables a e dele ed). A e wa ds,
he esul is abs ac ed o again include all p ocesses o he model (simila
o ou ex apola ion p ocedu e). The ou come is checked o induc i eness.
Addi ionally, he au ho s in oduce a Small Model Theo em, which s a es ha an
induc i e s eng hening holds o all models, i i holds in he models up o a
speci ic size depending on he s uc u e o he models. This heo em de ines a
cu o up o which he models ha e o be conside ed only. I is close in spi i
o ou Te mina ion Theo em, which also de ines so o a cu o (dynamically
checked e e y i e a ion). Ou heo em, howe e , is sui able o he inc emen al
wo k low wi h changing candida e o mulae e e y i e a ion.
Apa om he abo e me hod, he e exis o he wo ks ha u ilize a cu o o
e i ica ion. They equi e speci ic amilies o models (e.g., ings [EN95]) o
compu e a cu o [EK00] up o which he model needs o be e i ied in o de
o gua an ee he p ope y o hold o all models.
Pa ame e ized Timed Sys ems
In addi ion o he abo e ela ed wo k aiming o
un imed models, he e exis a ious, bu ewe , publica ions aiming o pa ame e -
ized imed sys ems. One o he i s o ac ually use his e minology was Maha a
[Mah05]. Apa om wo k wi h Abdulla [Abd+04] in which hey use imed pe i
ne s o he modeling o pa ame e ized imed sys ems, hey also eason abou de-
cidabili y o pa ame e ized imed sys ems in gene al. Abdulla e al. showed ha
eachabili y analysis o imed ne wo ks wi h only a single clock pe p ocess is
decidable [AJ03]. Howe e , when inc easing he numbe o clocks he eachabili y
ques ion becomes undecidable [ADM04].
Va ious o he wo ks exis ha conside pa ame e ized imed sys ems. B u -
omesso e al. [B u+12] and Ca ioni e al. [CGR10] employ SMT-encodings in a
decidable agmen in he heo y o a ay o e i ica ion. As e anoaei e al. [As +15]
116 CHAPTER 4. INCREMENTAL INDUCTIVE VERIFICATION OF PTS
combine locally compu ed in a ian s in o de o yield in a ian s o all models. I
builds upon he Small Model Theo em o Pnueli ans e ed o he domain o hyb id
au oma a by Johnson e al. [JM12]. Fo hei own app oach, Johnson e al. em-
ploy Pnueli’s P ojec -Abs ac -P ocedu e in a ixpoin compu a ion ha sea ches
an induc i e s eng hening o a coun e example o a ixed numbe o p ocesses.
Wi h i s usage o he small model heo em, his wo k is closes o ou app oach. As
explained abo e, ou Te mina ion Theo em is simila in ha is compu es a cu o up
o which size he models ha e o be conside ed. The main di e ence, howe e , is
he inc emen al na u e o ou heo em, as i s applicabili y o he cu en candida e
o mula is checked e e y cycle.
4.9 Summa y
The echnique p esen ed in his chap e is capable o e i ying sa e y p ope ies o
pa ame e ized imed sys ems gi en as ne wo ks o imed au oma a. To his end, we
employ an inc emen al wo k low ha e i ies he sa e y p ope y o models o a
ixed size, s a ing wi h he smalles one possible. Using he induc i e s eng hening
compu ed du ing his e i ica ion, we y o eason abou he en i e pa ame e ized
sys em. I his s ep ails, he nex cycle o he wo k low is s a ed wi h he nex la ge
model. O he wise, he easoning in o m o ou Te mina ion Theo em could be
applied and we success ully e i ied he sa e y p ope y o he en i e pa ame e ized
imed sys em, i.e., o all i s models wi h any numbe o imed au oma a.
The abili y o eason abou an en i e pa ame e ized sys em is o high alue, as
many mu ual exclusion algo i hms and pee o pee p o ocols can be modeled as
such a sys em. The bene i is ha p ope ies o hese algo i hms o p o ocols can
be checked o any numbe o p ocesses execu ing hem. I is a i al aspec when
dealing wi h adap i e sys ems, as is he case in he con ex o Indus y 4.0. Using
ou echnique allows he e i ica ion o he en i e pa ame e ized imed sys em. As
an example o he applica ion con ex , conside i s usage du ing he design phase,
which allows he sa e econ igu a ion o he sys em du ing li e ime wi hou he need
o u he e i ica ion. The addi ion o emo al o one o he p ocesses ha execu e
he mu ual exclusion algo i hm o p o ocol has al eady been p o en o be sa e. This
a p io i e i ica ion o he en i e sys em is a i al aspec when dealing wi h adap i e
and scalable sys ems.
In he ollowing chap e , we will elax some o he es ic ions imposed on he
models allowed in he p esen ed app oach. Ou echnique will, hus, be applicable
o an e en la ge se o sys ems, which will g ea ly imp o e i s p ac icali y.
5
Ve i ica ion o Ex ended
Pa ame e ized Timed Sys ems
Wi h mos o oday’s sys ems being sa e y c i ical, model-based design p ocesses o e
a s uc u ed p ocedu e o ensu e a ce ain quali y. They allow he o mal modeling
and e i ica ion o p ope ies du ing he design phase o a sys em. Howe e , du ing
his phase, he models migh be epea edly econ igu ed un il a inal design is ound.
In addi ion, such econ igu a ions may also occu a li e ime o he sys em, e.g.,
due o sel -adap a ion. Since he sys em’s beha io migh change unexpec ed, hese
econ igu a ions aise he need o edo e i ica ions ha ha e al eady been done.
In such a se ing, a e un o he e i ica ion om sc a ch is no e icien . We ha e,
hus, p oposed o euse he esul om he p e ious e i ica ion un. In he p e ious
chap e , we ha e success ully in oduced an inc emen al echnique ha ollows
his pa adigm o pa ame e ized imed sys ems modeled ia a imed au oma on
empla e. I can be applied o a ious mu ual exclusion algo i hms o pee o pee
p o ocols. I s bene i is he e i ica ion o he sa e y p ope y o sys ems wi h an
a bi a y, bu ixed numbe o p ocesses execu ing such an algo i hm. Conside ing
a unning sys em o such p ocesses, he sys em is sa e (w. . . he e i ied sa e y
p ope y) i espec i e o he numbe o p ocesses. In pa icula , i implies ha a
econ igu a ion o he sys em by adding o emo ing a p ocess is sa e and does no
equi e a new e i ica ion un. This app oach enables an a p io i e i ica ion o he
en i e sys em and, he eby, a oids online e i ica ions du ing li e ime.
In his chap e , we will elax some es ic ions imposed on he models o
which ou echnique can be employed o e i y sa e y p ope ies. We b oaden
he pa ame e ized imed sys ems ha we e conside ed in he p e ious chap e
(
∀n∈N:[P1|| . . . ||Pn]
). Up o now hey consis ed o a pa ame e ized numbe
n
o ins an ia ions o a p ocess
P
, which in oduced a symme ic s a e space. The
ex ended pa ame e ized imed sys ems (
∀n∈N:[S|| . . . ||R||P1|| . . . ||Pn]
) now
addi ionally include a ini e numbe o ex a p ocesses
S
o
R
. We also pe mi a
es ic ed so o synch oniza ion. As an example, his ex ension allows o model
117

118 CHAPTER 5. EXTENDED PARAMETERIZED TIMED SYSTEMS
an addi ional communica ion medium, e.g., a bus. This elaxa ion p o ides o a
b oade applicabili y o he echnique.
Up o now, he models we e c ea ed as ne wo ks o imed au oma a, whe e he
au oma a a e ins ances o a imed au oma on empla e. The size o he model was
gi en as pa ame e deno ing he numbe o au oma a.
In he ex ended o malism, an addi ional, ixed numbe o ex a imed au oma a
accompany he pa ame e ized numbe o au oma a ins an ia ed om he empla e.
These ex a au oma a allow o he modeling o componen s associa ed wi h he
pa ame e ized sys em, e.g., a communica ion medium o a se e in combina ion
wi h he pa ame e ized numbe o imed au oma a modeling clien s. Fu he mo e,
we allow a limi ed so o synch oniza ion be ween he imed au oma a ia channels
wi h he es ic ion ha a mos one o he symme ic au oma a mus be in ol ed in
he synch oniza ion.
In he ollowing, we p o ide he upda ed de ini ions used o he models. A -
e wa ds, we ede ine he conside ed
swap
ope a ions ha a e used o de ine he
in ended no ion o symme y. We b ie ly ecall he wo k low and gi e he p oo o
ou Te mina ion Theo em, be o e concluding his chap e wi h a sho expe imen
using one such ex ended model speci ying a ga e and con olle o a ain c ossing
wi h an a bi a y numbe o ains. No e, ha he p e ious chap e is a special case
o he o malism in oduced below. When conside ing models wi hou ex a imed
au oma a and wi hou synch oniza ion, we ecei e he o malism and no ion o
symme y as be o e.
We s a wi h he ede ini ion o he employed models.
5.1 Ex ension o he Modeling App oach
The models conside ed in his chap e a e ex ensions o hose om he p e ious
chap e . They addi ionally allow ex a imed au oma a in he ne wo k ha a e
no ins an ia ed om he empla e, as well as synch oniza ion wi h he ex a au-
oma a. The symme ic au oma a ins an ia ed om he empla e can no synch onize
wi h each o he , as his would in alida e ou Te mina ion Theo em employed o
he easoning abou he en i e pa ame e ized imed sys em. We i s upda e he
de ini ion o empla es in o de o e lec he added abili y o synch onize edges.
No e, ha he employed synch oniza ion channel is equal in each ins an ia ion, i.e.,
he synch oniza ion channel does no depend on he au oma on’s iden i ie . In
addi ion, synch oniza ion is only allowed wi h he ex a au oma a, no among he
ins an ia ions o he empla e. The de ini ion o empla es using synch oniza ion is
gi en below.
De ini ion 5.1.1
(Timed Au oma on Templa e using Synch oniza ion)
.
Le he se
Cg
o global clocks be gi en, as well as he global se o in ege a iables
IV =
IV6id ∪ IVid
as he union o disjoin se s o iden i ie unawa e (
IV6id
) and awa e (
IVid
)
in ege a iables, s. .
IV6id ∩ IVid =∅
. In addi ion, le
Σ
be he global se o channels.
Asymme ic imed au oma on empla e
A(pid)
using synch oniza ion de ined o e glob-
5.1. EXTENSION OF THE MODELING APPROACH 119
ally sha ed
Cg
,
Σ
and
IV
is a uple
A(pid) = (L
,
l0
,
C
,
IV
,
Σ
,
In c
,
In i(pid)
,
E(pid))
such ha
•pid ∈N≥1is a unique pa ame e , called iden i ie ,
•Lis a ini e se o loca ions,
•l0∈Lis he ini ial loca ion,
•C=Cl∪Cg
is he union o he ini e and disjoin se s o local and global clocks
wi h ini ial alua ion c
0,
•IV is he ini e se o sha ed in ege a iables wi h ini ial alua ion i
0,
•Σis he ini e se o sha ed synch oniza ion channels,
•In c:L→Φ(C)is a o al unc ion o clock in a ian s, s. . c
0|=In c(l0),
•In i(pid):L→Ψ(IV,pid)is a o al unc ion o in ege in a ian s,
s. . i
0|=In i(pid)(l0), and
•E(pid)⊆L×Σsync ×Φ(C)×Ψ(IV
,
pid)×Ω(IV
,
pid)×
2
C×L
is he se o
edges.
I mus hold ha
∀e1∈E
wi h synch oniza ion label
a?∈Σsync
, he e does no exis
an edge e2∈Ewi h synch oniza ion label a! and ice e sa.
As be o e, ins an ia ing a empla e
A(pid)
wi h unique iden i ie
pid =j∈N≥1
esul s in imed au oma on
Aj
. Unlike be o e, he ne wo ks o imed au oma a
conside ed in his chap e do no only include ins an ia ions o a empla e, bu
addi ionally con ain a ini e numbe o ex a imed au oma a. These supplemen a y
au oma a ha e o obey he es ic ions o iden i ie awa e in ege a iables
IVid
as de ined in he p e ious chap e . E ec i ely his means ha e en in he ex a
au oma a he a iables ha a e awa e o he au oma a’s iden i ie can only be applied
in es ic ed cons ain s and assignmen s (using each au oma on’s own iden i ie ).
O he wise, he symme y o he s a e space, on which ou app oach is based, could
be des oyed. We o malize ou ex ended o malism wi h ex a au oma a below.
De ini ion 5.1.2
(Ex ended Symme ic Ne wo k o Timed Au oma a)
.
Gi en
x∈N≥0
ex a imed au oma a
A1
o
Ax
wi h unique iden i ie s 1 o
x
ha a e de ined as
in De ini ion 2.1.8, bu wi h he es ic ions on in ege a iables
IVid
as abo e,
whe e in each au oma on
Ai
(
i∈ {
1,
. . .
,
x}
) only ins an ia ed cons ain s
Ψ(IV
,
i)
and assignmen s
Ω(IV
,
i)
a e allowed. Gi en pa ame e
n∈N≥1
and he imed
au oma on empla e
A(pid)
using synch oniza ion as de ined in De ini ion 5.1.1.
The Ex ended Symme ic Ne wo k o Timed Au oma a wi h
x+n
imed au oma a is
de ined as
NTAn=hA1
,
. . .
,
Ax
,
Ax+1. . .
,
Ax+ni
, whe e
Ai
(
i∈ {x+
1,
. . .
,
x+n}
)
is he ins an ia ion o A(pid)wi h pid =i.
No e, ha he de ini ion o symme ic ne wo ks o imed au oma a in he p e ious
chap e is a special case o he abo e ede ini ion, in which no synch oniza ion is
used and x=0 ex a au oma a a e gi en.
120 CHAPTER 5. EXTENDED PARAMETERIZED TIMED SYSTEMS
In he ollowing, we illus a e he concep o ex a au oma a in he ne wo k wi h
an example i s p oposed in 1994 [AD94] (he e sligh ly changed).
Figu e 5.1: Illus a ion o he T ain-Con olle -Ga e model
Example 5.1.3.
Conside a ain c ossing ha con ains a ga e ac ua ed by a con olle
as depic ed in Figu e 5.1. Whene e one o a ixed, bu a bi a y numbe o ains is
c ossing a senso , he con olle ecei es he signal app oaching. I equi es 1 ime
uni o send he lowe ing signal o he ga e. The ga e needs a mos 1 addi ional
ime uni , un il he ga e is lowe ed. The ain eaches he c ossing a e a leas 3
ime uni s and exi s i a e a mos 5 ime uni s. When exi ing, a senso ells he
con olle ha he ain has exi ed, which needs up o 1 ime uni o signal he ga e
ha i should aise. This inishing mo e equi es 1 o 2 ime uni s.
Figu e 5.2 shows he wo imed au oma a ep esen ing he ga e (Figu e 5.2(a))
and he con olle (Figu e 5.2(b)), as well as he empla e ha is ins an ia ed o
ep esen he ains (Figu e 5.2(c)). Clea ly, no iden i ie awa e in ege a iable is
needed in his scena io. I does, howe e , make use o he added synch oniza ion
capabili ies in oduced in his chap e . As can be seen, all ains use he same
synch oniza ion wi h he ex a au oma a.
l0
l2
l1
l3
lowe ?
c:=0
c≤1
aise?
c:=0
c≤2
c≥1
(a) Ga e
l0
l2
l1
l3
app oach?
c:=0
c≤1
c=1
lowe !
exi ?
c:=0
c≤1
aise!
(b) Con olle
l0l1
l2
app oach!
c:=0
c≤5
c≥3
c≤5
exi !
cn :=cn +1
cn :=cn -1
(c) T ain Templa e
Figu e 5.2: T ain Templa e and ex a imed au oma a modeling he Con olle and Ga e
The in oduc ion o ex a au oma a in he models does no comply wi h ou
p e ious no ion o symme y, as hese ex a au oma a can no be swapped wi h
any o he one. Thus, we ede ine he in ended no ion such ha i only co e s he
ins an ia ions o he empla e. To his end, he swap ope a ion needs o be adap ed.
5.2. SYMMETRY 121
5.2 Symme y
The ex a au oma a in oduced abo e a e no ins an ia ed om he empla e like
all he o he au oma a. They a e, hus, no symme ic, i.e., hey can no be used
in e changeably and mus no be aken in o accoun in he swap ope a ion. The
necessa y adap a ion o he swap ope a ion is gi en below. I es ic s he swap o
be only applicable o symme ic imed au oma a, i.e., hose ha a e ins an ia ed
om he same empla e. As explained, he in ui ion behind his es ic ion is ha
he symme ic au oma a can be used in e changeably, while all o he s can’ .
De ini ion 5.2.1
(Swap)
.
Le an ex ended ne wo k o imed au oma a
NTAn=
hA1
,...,
Ax+ni
be gi en as de ined in De ini ion 5.1.2 wi h conc e e seman ics
TS =
(S
,
s0
,
→)
. Le
A1
o
Ax
be he ex a imed au oma a and
Ax+1
o
Ax+n
he symme ic
imed au oma a ins an ia ed om empla e
A(pid)
as de ined in De ini ion 5.1.1.
Aswap
π=swapi,j
swaps wo imed au oma a
Ai
and
Aj
(
i
,
j∈ {x+
1,
. . .
,
x+n}
)
ins an ia ed om
A(pid)
. I changes he s a e
s= ((l1
,...,
lx+n)
,
c
,
i)∈S
in o he
s a e π(s) = ((π(l1), ..., π(lx+n)),π( c),π( i)) ∈Swi h
•∀k∈ {1, . . . , x+n}:π(lk) = 






lii k =j,
lji k =i,
lkelse.
•∀c∈Cg:π( c)(c) = c(c).
•∀k∈ {1, . . . , x+n}:∀c∈Cl
k:π( c)(c) = 






c(ci)i k =j,
c(cj)i k =i,
c(c)else,
whe e
ci
and
cj
e e clock
c
in au oma on
Ai
(
c∈Cl
i
) and
Aj
(
c∈Cl
j
),
espec i ely.
•∀i ∈ IV6id :π( i)(i ) = i(i ).
•∀i ∈ IVid :π( i)(i ) = 






i i i(i ) = j,
j i i(i ) = i,
i(i )else.
No e, ha we also use
π(m)
o deno e he iden i ie o he au oma on wi h which
m
has been swapped, o mally π(m) = 






i i m =j,
j i m =i,
m else.
The e ec o he swap ope a ion is he same as in he p e ious chap e . I swaps
he loca ions o he wo au oma a, he alues o hei local clocks, as well as alues
o iden i ie awa e in ege a iables ha e e o one o he wo au oma a. The
only di e ence is he es ic ion o be applied only o symme ic imed au oma a.
Again, a pe mu a ion in ol ing mo e han wo au oma a being swapped can easily
128 CHAPTER 5. EXTENDED PARAMETERIZED TIMED SYSTEMS
s a es. Clea ly, Consecu ion o
kFkexp(n+1)
o
NTAn+1
does no hold,
which is a con adic ion.
In summa y, we ha e eached a con adic ion in bo h cases.
We demons a e he p ac icali y o he ex ended app oach in he ollowing.
5.3 Expe imen s
Conside ing he abo e example o he ain c ossing, we ha e conduc ed expe imen s
wi h wo dis inc sa e y p ope ies. The i s p ope y
ρlowe ed
has been p esen ed
abo e (Example 5.2.6) and speci ies ha he ga e has o be closed en i ely, when a
ain is c ossing. The second one (
ρoccupied
) deno es ha he c ossing is no occupied
o no eason, i.e., he ga e is only lowe ing, i a leas one ain is app oaching o in
he c ossing. I is speci ied ia he e o s a e speci ica ion
e = ((l1
,
∗
,
∗)
,
ue
,
cn <
1
)
using an iden i ie unawa e a iable
cn
ha coun s he ains ha a e no a
away ( ha a e no in loca ion l0).
Ou wo k low success ully e i ies hese sa e y p ope ies. The espec i e un-
imes wi h and wi hou op imiza ions a e shown in Tables 5.1 and 5.2.
Run ime (s) Ve i ied models NTAn o which n?
No Op imiza ion OOM 1-8
Gene aliza ion 8,5 ∀n∈N
Chockle -Feedback 7,4 ∀n∈N
Gene aliza ion and Chockle -Feedback 3,6 ∀n∈N
using non-gene alized se o clauses
Gene aliza ion and Chockle -Feedback 3,6 ∀n∈N
using gene alized se o clauses
F ame1-Feedback 3,0 ∀n∈N
Gene aliza ion and F ame1-Feedback 2,6 ∀n∈N
using non-gene alized se o clauses
Gene aliza ion and F ame1-Feedback 2,5 ∀n∈N
using gene alized se o clauses
Bo h-Feedback 4,8 ∀n∈N
Gene aliza ion and Bo h-Feedback 3,3 ∀n∈N
using non-gene alized se o clauses
Gene aliza ion and Bo h-Feedback 3,5 ∀n∈N
using gene alized se o clauses
Table 5.1: Ve i ica ion expe imen s o he sa e y p ope y
ρlowe ed
and he T ain-
Con olle -Ga e model
As can be seen, bo h sa e y p ope ies ha e been success ully e i ied wi hin
easonable ime. Again, he op imiza ion o using he F ame1-Feedback has shown
o be a good op ion.

5.4. SUMMARY 129
Run ime (s) Ve i ied models NTAn o which n?
No Op imiza ion OOM 1-7
Gene aliza ion 13,0 ∀n∈N
Chockle -Feedback OOM 1-9
Gene aliza ion and Chockle -Feedback OOM 1-9
using non-gene alized se o clauses
Gene aliza ion and Chockle -Feedback 6,2 ∀n∈N
using gene alized se o clauses
F ame1-Feedback 25,7 ∀n∈N
Gene aliza ion and F ame1-Feedback 4,6 ∀n∈N
using non-gene alized se o clauses
Gene aliza ion and F ame1-Feedback OOM 1-7
using gene alized se o clauses
Bo h-Feedback 11,4 ∀n∈N
Gene aliza ion and Bo h-Feedback 8,7 ∀n∈N
using non-gene alized se o clauses
Gene aliza ion and Bo h-Feedback OOM 1-7
using gene alized se o clauses
Table 5.2: Ve i ica ion expe imen s o he sa e y p ope y
ρoccupied
and he T ain-
Con olle -Ga e model
5.4 Summa y
In summa y, he p esen ed ex ensions o he allowed modeling o malism in ou
pa ame e ized se ing a e aluable in ha hey signi ican ly inc ease he modeling
capabili ies wi hou a d awback. They allow he modeling o se e -clien si ua ions,
as well as o he e ec s like a communica ion medium.
The necessa y adap a ions we e small and we we e able o use he o e all wo k-
low, as well as he Te mina ion Theo em wi hou modi ica ions. The expe imen s
we e success ul and p omising and emphasize he p ac icali y o he app oach.
Using his ex ended o malism, ou inc emen al wo k low enables he e i ica ion
o sa e y p ope ies o a b oad numbe o pa ame e ized imed sys ems ha a e
composed o a ini e numbe o auxilia y p ocesses accompanying a ixed, bu
a bi a y la ge numbe o ins an ia ions o he same p ocess. This ex ension adds
signi ican alue o ou echnique. Ye , i ’s applica ion a ea emains he a p io i
e i ica ion o p ope ies o an a bi a y, bu ixed numbe o equal p ocesses. This
con ex is in line wi h he pa adigm o Indus y 4.0, which acili a es he adap a ion
o sys ems du ing li e ime. The bene i s o ou p oposed echnique o his scena io
a e ob ious. I a oids an online e i ica ion by execu ing an a p io i e i ica ion,
which emo es he necessi y o e i y e e y single econ igu ed model, in which he
numbe o p ocesses has been changed.
O he econ igu a ions, howe e , can no be handled using his echnique. We
will examine he e ec s o gene al econ igu a ions in he ollowing chap e and
gi e a bes -guess app oach, as he e ec s o econ igu a ions can no be es ima ed
easily in gene al.
6
Induc i e Ve i ica ion o
Recon igu ed Models
Timed o malisms a e o signi ican impo ance o he modeling o oday’s sys ems.
As explained, mos o hese sys ems a e sa e y c i ical and, hus, model-based design
p ocesses a e employed o ensu e a ce ain quali y. To his end, o mal models a e
c ea ed and p ope ies a e e i ied o hese models. Du ing such design p ocedu es,
howe e , he models migh epea edly be econ igu ed, esul ing in a need o edo
he e i ica ion. These econ igu a ions migh also occu la e on, e.g., i he model
ep esen s an adap i e and sel -op imizing sys em as in Indus y 4.0.
As e e y such econ igu a ion changes he s a e space o he model, he desi ed
sa e y p ope ies need o be e i ied again. Doing his om sc a ch is e y ine icien ,
in pa icula , when conside ing ha he o iginal, simila model has been examined
be o e.
In he p e ious wo chap e s, we ha e p oposed a echnique ha e i ies sa e y
p ope ies o pa ame e ized imed sys ems. Wi hin such es ic ed models, ou
echnique p e en s he cos ly e i ica ion om sc a ch when dealing wi h econ-
igu a ions ha change he numbe o p ocesses. I does so using an inc emen al
wo k low speci ically designed o pa ame e ized sys ems. One o he op imiza ions
p esen ed o his echnique, namely he
Feedback
-loop, is sui able o be used in a
gene al se ing.
I injec s an induc i e s eng hening compu ed o he o iginal model in o he
e i ica ion un o he econ igu ed model. By doing so, some o he clauses in he
induc i e s eng hening a e injec ed in o all ames o he IC3 un, o a leas in o
he ame
F1
(see Subsec ion 4.6.1). Ou expe imen s ha e shown ha his euse o
clauses success ully p e en s he cos ly edisco e y o some o hem and, by doing
so, speeds up he en i e e i ica ion un.
So a , we ha e employed his accele a ion echnique only o symme ic e-
con igu a ions in he se ing o pa ame e ized imed sys ems. In he ollowing,
we will y o u ilize i s bene i s o econ igu ed models in gene al and examine
131
132 CHAPTER 6. INDUCTIVE VERIFICATION OF RECONFIGURED MODELS
he e ec i eness in se e al expe imen s. We s a wi h a classi ica ion o possible
econ igu a ions.
Taking in o accoun he gene ali y o models exp essible wi h ou o malism
o ne wo ks o imed au oma a (Chap e 2), se e al ypes o econ igu a ion a e
possible as de ailed in he ollowing. We cha ac e ize econ igu a ions o a model
wi hin he ollowing h ee ca ego ies:
• Addi ion o new pa s o he model,
• Dele ion o pa s o he model,
• Replacemen /Modi ica ion o pa s o he model.
We illus a e hese ca ego ies below.
Addi ion
Analog o he addi ion o a symme ic imed au oma on as in he p e i-
ous chap e , o he pa s can be added o a model. When conside ing a ne wo k o
imed au oma a modeling he in e ac ion o se e al componen s in he eal wo ld,
he addi ion o an ex a imed au oma on may ep esen he addi ion o a new
componen in e ac ing wi h he o he s. Fu he mo e, smalle addi ions a e possible.
An ex a loca ion migh model a new disc e e s a e o a sys em, an edge models
addi ional in e ac ion. No e, ha he addi ion o a pa o he model does no always
esul in addi ional beha io , e.g., a cons ain added o an edge es ic s he exis ing
beha io .
Dele ion
In con as , dele ed po ions o he model migh speci y he emo al o a
pa o he sys em, a s a e o in e ac ion. These would be pe o med ia he emo al
o an en i e imed au oma on in he model, o o a loca ion o edge, espec i ely.
E en smalle changes o he cons ain s o upda es o edges can be conside ed,
whe e i should be no ed ha he emo al o a cons ain migh allow addi ional
beha io o he model.
As illus a ed, he op ions o modi y eal-wo ld sys ems and, in consequence,
hei models a e di e se. The hi d ca ego y con ains econ igu a ions ha a e e y
speci ic as hey eplace de ailed pa s o he model.
Replacemen
In addi ion o he abo e men ioned econ igu a ions, he e exis hose
ha al e pa s o he model wi hou addi ion o dele ion. These econ igu a ions
essen ially ely on clock o in ege cons ain s being al e ed, o assignmen s and
ese s being changed. They co espond, o ins ance, o he adap a ion o iming
pa ame e s in he modeled sys ems.
The abo e a ie y o econ igu a ions makes he euse o p e ious e i ica ion
esul s ex emely challenging. In his chap e , we p opose a gene al p ocedu e
o employ hese esul s anyhow. I is hea ily based on he
Feedback
- echniques
p esen ed in he p e ious chap e , which allow he euse o se e al clauses o an
133
induc i e s eng hening compu ed o he o iginal model in o de o speed up he
e i ica ion un o he econ igu ed model.
Ou algo i hm p esen ed in Chap e 3 success ully combines he IC3 algo i hm
wi h he Zone abs ac ion o he e i ica ion o sa e y p ope ies o ne wo ks o
imed au oma a. In case he sa e y p ope y is in a ian , i yields an induc i e
s eng hening o he sa e y p ope y as addi ional ou come. Via an e icien alidi y
check, he induc i e s eng hening can easily be checked o gua an ee he sa e y
p ope y’s in a iance o he o iginal model. In combina ion wi h a econ igu ed
model, howe e , a simple check o alidi y o he induc i e s eng hening will
mos o en ail hough he sa e y p ope y is indeed in a ian . The eason is ha
he o mula is no induc i e o he econ igu ed model. The ailed induc i eness
o igina es om a changed s a e space. Depending on he pe o med econ igu a ion,
he change o he s a e space may be d as ic.
In he p e ious wo chap e s, his change was an icipa ed based on he s uc u e
o he models, i.e., he symme y, ia an ex apola ion p ocedu e. This p ocedu e
adap s he induc i e s eng hening as an icipa ed, s. . i is close o a alid induc i e
s eng hening o he econ igu ed model. Howe e , due o he la ge a ie y o
econ igu a ions, he change o s a e space can no be an icipa ed in gene al.
In o de o gi e an in ui ion why he euse o a o mula migh be o bene i e en
wi hou an adap a ion, conside he ollowing example.
Example 6.0.1.
Le he
Fische _U_
2 model be gi en as depic ed in Figu e 3.1. The
induc i e s eng hening o he sa e y p ope y
ρ:=¬(cn >
1
)
compu ed by ou
algo i hm IC3 wi h Zones is lis ed in he i s column o Table 6.1
Fische _U_2 Fische _U_2(2048)
(in 1≤1) (in 1≤1)
∧((in 06=0)∨(in 1≤0)) ∧((in 06=0)∨(in 1≤0))
∧(¬l1
0∨l1
1∨(in 1≤0)) ∧(¬l1
0∨l1
1∨(in 1≤0))
∧(¬l2
0∨l2
1∨(in 1≤0)) ∧(¬l2
0∨l2
1∨(in 1≤0))
∧(l1
0∨(in 06=1)∨(in 1≤0)) ∧(l1
0∨(in 06=1)∨(in 1≤0))
∧(l2
0∨(in 06=2)∨(in 1≤0)) ∧(l2
0∨(in 06=2)∨(in 1≤0))
∧((c1
0≤1024.0)∨(in 06=1)∨(c2
0>1024.0)) ∧((c1
0≤2048.0)∨(in 06=1)∨(c2
0>2048.0))
∧((c2
0≤1024.0)∨(in 06=2)∨(c1
0>1024.0)) ∧((c2
0≤2048.0)∨(in 06=2)∨(c1
0>2048.0))
Table 6.1: Induc i e s eng henings compu ed o he models
Fische _U_
2 and he
econ igu ed model Fische _U_2(2048)as depic ed in Figu e 6.1
When changing he iming pa ame e s o he Fische algo i hm, a econ igu ed
model migh look as depic ed in Figu e 6.1. I equals he o iginal model, excep ha
he wai ing imes ha he algo i hm adhe es o a e now doubled. The co esponding
induc i e s eng hening o he econ igu ed model compu ed wi hou he euse o
he o iginal induc i e s eng hening is lis ed in he second column o Table 6.1.
Clea ly, he wo induc i e s eng henings a e simila . In ac , hey bo h consis s
o eigh clauses and di e only a li e als e e ing he ime cons an s. In pa icula ,
he i s six clauses a e exac ly he same. Thus, he injec ion o he o me induc i e
s eng hening in o he un o ou algo i hm IC3 wi h Zones (Chap e 3) o e i y he

134 CHAPTER 6. INDUCTIVE VERIFICATION OF RECONFIGURED MODELS
cn :=cn +1
id:=0;
cn :=cn -1
id=0 c≤2048
c:=0
id=0
c≤2048
id:=1
c:=0
c>2048
id=1
c:=0
l0
l3
l1
l2
cn :=cn +1
id:=0;
cn :=cn -1
id=0 c≤2048
c:=0
id=0
c≤2048
id:=2
c:=0
c>2048
id=2
c:=0
l0
l3
l1
l2
Figu e 6.1: Recon igu ed Fische model
Fische _U_
2
(
2048
)
wi h al e ed ime con-
s an s, whe e all cons an s 1024 a e eplaced by 2048
econ igu ed model, should p e en he cos ly edisco e y o hese six clauses and,
hus, speed up he e i ica ion un.
Howe e , he injec ion o a p e iously compu ed induc i e s eng hening migh
no always be bene icial, as obse able in he un imes depic ed in Table 6.2. Fo
he model
Fische _U_
15
(
2048
)
wi h 15 p ocesses, i compa es a e i ica ion om
sc a ch as desc ibed in Chap e 3 o he one ha u ilizes he induc i e s eng hening
p e iously compu ed o he o iginal model Fische _U_15. We show he esul s o
all h ee dis inc
Feedback
- echniques p esen ed in he p e ious chap e (
Chockle
-
Feedback [Cho+11],
F ame
1-Feedback,
Bo h
-Feedback). All o hem a e clea ly
in e io o a e i ica ion om sc a ch. The eason is ha he change in he model is
a he d as ic (all ime cons an s a e changed) esul ing in a signi ican change o
he s a e space conce ning he ime domain. In addi ion, he a ion o clauses ha
we e o alue, i.e., ac ually occu in he new induc i e s eng hening compu ed o
he econ igu ed model, is a he small (compa ed o he 6 ou o 8 clauses eused
o Fische _U_2(2048)).
Howe e , he o e all idea o eusing old e i ica ion esul s migh be o alue in
he gene al se ing e en so. In e es ingly, in he symme ic se ing o he p e ious
chap e s he euse could be op imized. The employed ex apola ion p ocedu e
Run ime (s) Memo y (MB)
Ve i ica ion econ igu ed model 140,6 267,8
( om sc a ch)
Ve i ica ion econ igu ed model 176,8 287,5
wi h Chockle -Feedback
Ve i ica ion econ igu ed model 245,9 245,1
wi h F ame1-Feedback
Ve i ica ion econ igu ed model 359,5 261,5
wi h Bo h-Feedback
Table 6.2: Compa ison o he un imes o e i ica ion om sc a ch o using he
dis inc Feedback- echniques wi h model Fische _U_15(2048)
6.1. ADAPTATION OF THE FORMULA 135
adap s he o iginal induc i e s eng hening in o de o e lec he econ igu a ion,
ha is he addi ion o a symme ic imed au oma on. In gene al, his modi ica ion
is no manda o y. In he symme ic se ing, howe e , he esul s p o ed o be o
signi ican alue in o m o he p esen ed wo k low. Hence, we will examine he
easibili y o an adap a ion p ocedu e o he gene al case in he ollowing.
6.1 Adap a ion o he Fo mula
Op imally, an adap a ion o he induc i e s eng hening o mula acco ding o he
applied econ igu a ion would esul in a alid induc i e s eng hening o a e-
con igu ed model. To illus a e such an op imal app oach, conside he ollowing
example.
Example 6.1.1.
Conside again he o iginal
Fische _U_
2 model and he econ igu ed
Fische _U_
2
(
2048
)
model as explained in he p e ious example. They a e depic ed
in Figu es 3.1 and 6.1, whe e he econ igu a ion eplaces all ime cons an s 1024 in
he o iginal model by he cons an 2048. An op imal adap a ion o he o mula would
change all ime cons an s acco ding o he econ igu a ion, i.e., eplace all cons an s
1024 in he o mula by 2048. The esul ing o mula is a alid induc i e s eng hening
o he econ igu ed model. In ac , i equals he induc i e s eng hening o he
econ igu ed model lis ed be o e in he second column o Table 6.1.
We also pe o med he adap a ion wi h he
Fische _U_
15 example abo e, in
which he euse o he induc i e s eng hening was unsuccess ul. When compa ing
he un imes o he e i ica ions, i is ob ious ha he adap ed o mula imp o es
on he non-adap ed one. The esul s a e shown in Table 6.3, which displays he
un imes o IC3 wi h Zones wi h injec ion o he adap ed induc i e s eng hening
using he dis inc
Feedback
- echniques. Fu he mo e, i includes he un ime o
a simple alida ion o he adap ed induc i e s eng hening as a e e ence ime.
The compa ison wi h Table 6.2 shows a signi ican imp o emen o e he euse o
he o iginal (non-adap ed) induc i e s eng hening and o e he e i ica ion om
sc a ch.
This example ep esen s an op imal se ing, whe e a alid induc i e s eng h-
ening o he econ igu ed model could be p oduced by adap ing he induc i e
s eng hening o he o iginal model. I is, howe e , no ep esen a i e, as many
challenges hinde such pe ec adap ion in he usual case. This is due o he ac
ha he impac o a econ igu a ion can ha dly be es ima ed, in pa icula i he
econ igu a ion is mo e complex. In he ollowing, we p opose adap a ions o he
o mula o he h ee dis inc ca ego ies o econ igu a ions shown abo e.
Adap a ion o Addi ion-Recon igu a ions
The impossibili y o an adap a ion can
bes be obse ed when conside ing econ igu a ions ha include he addi ion o
pa s o he model. In gene al, an addi ional imed au oma on, as well as addi ional
edges o loca ions in exis ing au oma a in oduce addi ional beha io in in e ac ion
wi h he o iginal pa s o he model. This means he s a e space may change in
136 CHAPTER 6. INDUCTIVE VERIFICATION OF RECONFIGURED MODELS
Run ime (s) Memo y (MB)
Valida ion o adap ed induc i e s eng hening 1,1 48,4
Ve i ica ion econ igu ed model
36,6 100,0wi h Chockle -Feedback
(adap ed induc i e s eng hening)
Ve i ica ion econ igu ed model
25,8 82,8wi h F ame1-Feedback
(adap ed induc i e s eng hening)
Ve i ica ion econ igu ed model
36,7 102,2wi h Bo h-Feedback
(adap ed induc i e s eng hening)
Table 6.3: Compa ison o he un imes o alida ion and e i ica ion injec -
ing he adap ed o mula using he dis inc
Feedback
- echniques wi h model
Fische _U_15(2048)
a ious ways, which can no be es ima ed wi hou knowledge abou any s uc u al
cha ac e is ics like symme y. Thus, a pe ec adap a ion o he o iginal induc i e
s eng hening is no easible in gene al. Fo econ igu a ions ha include he addi ion
o pa s, we a e unable o adap he o mula, as we can no es ima e he changed
s a e space. In consequence, he o mula emains unchanged wi h he hope ha he
s a e space has no changed, o a leas is simila o he o iginal one.
Adap a ion o Dele ion-Recon igu a ions
The same a gumen a ion holds ue
when conside ing econ igu a ions including he dele ion o pa s o he model.
As abo e, he e ec on he s a e space can ha dly be es ima ed. Fo illus a ion
pu pose, conside he dele ion o a single cons ain . I s emo al weakens he
es ic ions on an edge o loca ion and migh allow o addi ional beha io ha
migh inc ease he eachable po ion o he s a e space, s. . a s a e iola ing he
sa e y p ope y is now eachable. Adap ing he induc i e s eng hening o he sa e y
p ope y acco ding o hese changes in he s a e space is no easible. Howe e , when
conside ing he emo al o o he pa s o a model, e.g., an en i e imed au oma on,
he o mula can, and in ac mus , be adap ed o e lec his change. I would
o he wise include a iables ha do no exis in he encoding o he model. Thus, we
adap he o mula as ollows.
The e migh exis li e als in some o he clauses o he o mula ha e e o
dele ed pa s emo ed du ing he econ igu a ion. We p opose wo dis inc op ions
how hese li e als can be handled.
De ini ion 6.1.2
(Adap a ion o Dele ed Pa s)
.
Le an induc i e s eng hening
F
o
a sa e y p ope y be compu ed o an o iginal model
NTA
. We adap he o mula
kFk
conce ning pa s o he model dele ed in a econ igu a ion as ollows. Fo each
clause
c
in
kFk
ha includes a leas one li e al e e ing a nonexis en pa (clock,
loca ion o in ege a iable) in he econ igu ed model, we ei he
6.1. ADAPTATION OF THE FORMULA 137
• Dele e he en i e clause, o
• Dele e all disjunc s ha e e nonexis en pa s in he econ igu ed model.
This app oach is illus a ed in he ollowing example.
Example 6.1.3.
Conside a model and a econ igu a ion in which a local clock
c0
in imed au oma on wi h iden i ie 1 is dele ed. As a esul , he espec i e clock
a iable
c1
0
mus no be used and has o be emo ed om he induc i e s eng hening
o mula. Howe e , simply dele ing he clock a iable is no an op ion, as i would
esul in an in alid o mula ha includes de o med cons ain s. Conside ing he
clause
l1
0∨(c1
0≥
1
)
illus a es his issue. Dele ing he clock a iable
c1
0
encoding
clock
c0
in imed au oma on wi h iden i ie 1 esul s in he in alid o mula
l1
0∨(≥
1
)
.
The abo e p esen ed p ocedu es o dele ing he en i e clause o only he a ec ed
li e als yield dis inc esul s. Ei he he clause is disca ded in i s en i e y o he
disjunc (c1
0≥1)is emo ed esul ing in clause l1
0.
Adap a ion o Replacemen -Recon igu a ions
Las ly, econ igu a ions ha al e
he model by speci ic eplacemen s o pa s o e he bes chance o adap he induc-
i e s eng hening acco dingly. This is due o he s uc u e o hese econ igu a ions,
whe e he model is modi ied wi hou addi ion o dele ion. Thus, hese econ igu-
a ions include he modi ica ion o cons ain s, assignmen s and se s o clocks o
be ese . The la e wo modi ica ions ( ese clocks and assignmen s) a e o a ious
e ec and, hus, emain wi hou adap a ion o he induc i e s eng hening o mula,
much like he addi ion o dele ion o pa s. Changes on cons ain s, howe e , can be
handled pa ly as we will see in he ollowing. Basically, he changes in cons ain s
ha can be handled a e hose ha eplace cons an s. As explained in Chap e 3,
he cons ain s a e inco po a ed in he p edecesso compu a ion wi hin he weakes
p econdi ion compu a ion. To his end, hey may be combined wi h o he cons ain s
( o example in he All-Pai s-Sho es -Pa hs algo i hm o he backwa ds compu a-
ion o he p edecesso zone) o be combined wi h clock ese s o assignmen s ( o
in ege a iables). As a esul , he cons ain s may occu modi ied o unmodi ied in
he induc i e s eng hening, o don’ occu a all. Hence, he chances o a easonable
adap a ion o he o mula can be e y di e se.
Bes Case: Whene e he econ igu ed cons ain can be uniquely ela ed o pa s
o he o mula, an adap a ion is easy, e.g., whene e all cons ain s in he model
a e unique and occu unmodi ied in he o mula. Fo illus a ion, again conside
Example 6.1.1. All cons ain s in he model a e changed and he adap a ion o he
o mula can, hus, be easily pe o med by eplacing all cons an s in he o mula.
Since all cons ain s a e changed, i does no ma e whe he he li e al
(c1
0≥
1024
)
e e s he in a ian cons ain o loca ion
l1
o he gua d cons ain o he edge
be ween loca ions l1and l2.
P oblema ic Mapping: The lack o said knowledge, howe e , esul s in he ques ion
which pa s o he o mula should be eplaced. Since no eliable in o ma ion is gi en