GMD Research Series GMD ­ Forschungszentrum Informationstechnik GmbH Ulrich Nitsche Verification of Co-Operating Systems and Behaviour Abstraction N° 7/1998 © GMD 1998 GMD ­ Forschungszentrum Informationstechnik GmbH Schloß Birlinghoven D-53754 Sankt Augustin Telefon +49 -2241 -14 -0 Telefax +49 -2241 -14 -2618 http://www.gmd.de In der Reihe GMD Research Series werden Forschungs- und Entwicklungsergebnisse aus der GMD zum wissenschaftlichen, nicht- kommerziellen Gebrauch veröffentlicht. Jegliche Inhaltsänderung des Dokuments sowie die entgeltliche Weitergabe sind verboten. The purpose of the GMD Research Series is the dissemination of scientific work for scientific use. The commercial distribution of this document is prohibited, as is any modification of its content. Anschrift des Verfassers/Address of the author: Ulrich Nitsche Department of Electronics and Computer Science University of Southampton Highfield, Southampton SO17 1BJ, Großbritannien Die vorliegende Veröffentlichung entstand im/ The present publication was prepared within: Institut für Telekooperationstechnik (TKT) Institute for Telecooperation Technology http://www.tkt.gmd.de DF1 Die Deutsche Bibliothek - CIP-Einheitsaufnahme: Nitsche, Ulrich: Verification of Co-Operating Systems and Behaviour Abstraction / Ulrich Nitsche. GMD ­ Forschungszentrum Informationstechnik GmbH. - Sankt Augustin : GMD ­ Forschungszentrum Informationstechnik, 1998 (GMD Research Series ; 1998, No. 7) Zugl.: Frankfurt (Main), Univ., Diss., 1998 ISBN 3-88457-331-4 ISSN 1435-2699 ISBN 3-88457-331-4 Abstract Chec king the design or sp eci cation of a co op erating i e concurren t and reactiv e system for correctness is an imp ortan t task in the dev elopmen t of complex w e call them industrial sized systems Applying the w ell established approac h of automatic veri c ation of sp eci cations using mo del che cking tec hniques one is con fron ted with sev ere complexit y problems when v erifying large systems The source of these complexit y problems is the excessiv e size of the state space that represen ts the b eha viour of a sp eci cation as w ell as the necessit y of exhaustiv ely searc hing the state space when mo del c hec king The ob vious aim when dealing with complex systems is to reduce the state space as m uc h as p ossible without loss of imp ortan t information concerning the actual v eri cation task W e sho w in this thesis whic h information ab out the b eha viour of a sp eci cation can b e obtained from prop erties of a simpli ed v ersion of the b eha viour The step from the original b eha viour w e call it the c oncr ete b eha viour of a sp eci cation to its simpli ed v ersion is called abstr action The b eha viour of a sp eci cation is represen ted b y the minim al state space corresp onding to the sp eci cation whic h in fact means that w e do not consider additional state information but only the b eha viour itself i e in nite sequences of actions F or this reason w e call our ab straction tec hnique b ehaviour abstr action In formal terms w e de ne an abstraction b y an alphab etic language homomorphism Alphab etic language homomorphisms o er t w o abstraction concepts action r enaming and action hiding It is esp ecially the fact that w e deal with abstractions that comprise action hiding that mak es our approac h quite p o w erful with regard to the aim of obtaining a small nite state represen tation of the abstract b eha viour The application area of the concepts w e dev elop in this thesis is the area of c o op er ating systems These are lo osely coupled reactiv e concurren t systems F or this t yp e of system it is often not su cien t to c hec k a prop ert y without making an y fairness assumptions On the other hand dealing with fairness is not an easy task in the sense that one has to mak e the righ t c hoice whic h fairness assumption to tak e W e ha v e to note that this statemen t is heuristically based In principle there is a c hance that abstraction do es not decrease or ev en increases the state space Nev ertheless in practice these cases are quite un usual iii iv in to accoun t T o b e freed from explicitly lo oking at fairness issues w e de ne in this thesis a relativized v ersion of liv eness r elative liveness A relativ e liv eness prop ert y is a liv eness prop ert y with resp ect to the univ erse of a sp eci cation s b eha viour Relativ e liv eness is also kno wn as machine closur e The use of relativ e liv eness prop erties in v eri cation of co op erating systems using b eha viour abstraction pro v es to b e somewhat delicate Arbitrary alphab etic lan guage homomorphisms are not an adequate basis for abstraction when one w an ts to c hec k relativ e liv eness prop erties W e sho w that the de nition of a homomorphism that is simple on a b eha viour is exactly the righ t c hoice to establish an abstraction tec hnique that preserv es relativ e liv eness prop erties Based on this result w e sho w additionally for another class of prop erties eventuality pr op erties that they to o are preserv ed under simple homomorphic abstractions Finally w e apply the results of this thesis to three di eren t examples that are c hosen to illustrate di eren t asp ects of the established results One of the examples has a concrete practically relev an t bac kground it sho ws ho w the established approac h can b e used to detect servic e inter actions in in telligen t net w orks Erw eiterte deutsc hsprac hige Zusammenfassu ng Bei der En t wic klung k omplexer Systeme ist es auf Grund des un ub ersc haubaren Zusammenspiels v ersc hiedener Komp onen ten mittlerw ei le not w endig gew orden im mer feinere Metho den zur systematisc hen Suc he nac h m oglic hen F ehlern im Sy stem einzusetzen Als sehr n utzlic h hat sic h das Aufsp uren v on k onzeptionellen F ehlern b ereits im En t wurf bzw der formalen Sp ezi k ation eines Systems v or dessen eigen tlic her Realisierung gezeigt da sic h hierdurc h k ostspielige Nac h b esserungsar b eiten an b ereits realisierten o der gar v ermarkteten Systemen v ermeiden lassen k onnen Der Begri System l a t sic h in diesem Kon text sehr w eit fassen wir b eziehen uns allerdings aussc hlie lic h auf tec hnisc he Systeme die in ihrer En t wurfs phase durc h geeignete mathematisc he Mo delle b esc hreibbar sind V on b esonderer Bedeutung ist die rec hnergest utzte Korrektheits ub erpr ufung v on Systemsp ezi k ationen Betrac h ten wir Systeme einer realen im industriellen Bereic h angesiedelten Gr o enordn ung sto en wir sc hnell auf k omplexit atsb edingte Probleme b ei der An w endung ublic her automatisc her V eri kationsmetho den Der Zustands raum d h der endlic he Automat der das V erhalten eines sp ezi zierten Systems b esc hreibt ist einfac h zu gro als da g angige V eri k ationsv erfahren die eine erheb lic he algorithmisc he Laufzeitk omplexi t at b esitzen e zien t einsetzbar w aren Das o ensic h tlic he Ziel im Blic k auf die auftretenden Komplexit atsproblem e ist eine aus reic hend stark e Reduktion des Zustandsraums ohne durc h diese Reduktion wic h tige Informationen b ez uglic h der V eri k ationsfragestellung zu v erlieren Genaugenom men geh t es um die F rage nac h der Information die wir un ter Kenn tnis einer v erein fac hten Repr asen tation des V erhaltens einer Sp ezi k ation ub er deren eigen tlic hes k onkretes V erhalten erhalten k onnen In der v orliegenden Dissertation wird genau diese Problemstellung b etrac h tet und f ur v ersc hiedene Eigensc haftsklassen gel ost W as wissen wir ub er das V erhalten eines Systems w enn wir Eigensc haften einer v ereinfac h ten V arian te des V erhaltens k en nen und wissen wie das v ereinfac h te V erhalten aus dem urspr unglic hen b erec hnet wurde Den Sc hritt v om urspr unglic hen V erhalten das wir auc h konkr etes V erhal ten nennen zu einem v ereinfac h ten V erhalten nennen wir A bstr aktion das Ergebnis v vi der Abstraktion das abstr akte V erhalten Das V erhalten einer Sp ezi k ation stellen wir durc h seinen minim alen Zustandsraum dar d h durc h einen minim ie rten de terministisc hen endlic hen Automaten mit aussc hlie lic h akzeptierenden Zust anden Dies b edeutet da wir ub er das V erhalten n ur die absolut not w endige Zustandsin formation b esitzen und so eine exakte Ub ereinstimm ung des V erhaltens mit seiner Darstellung b esteh t Aus diesem Grund ist die Abstraktion eines V erhaltens direkt auf die durc h das V erhalten b esc hrieb ene F olge v on Aktionen b ezogen und nic h t auf Zustandsinformation des das V erhalten b esc hreib enden Automaten wir sprec hen daher v on V erhaltensabstr aktion F ormal de nieren wir V erhaltensabstraktionen durc h alphab etisc he Sprac hhomo morphismen Da alphab etisc he Sprac hhomomorphismen das Um b enennen und L o sc hen v on Buc hstab en festlegen und wir Buc hstab en in einem W ort als Aktionen in einem Ablauf eines Systems in terpretieren erm oglic h t die V erw endung alphab e tisc her Sprac hhomomorphismen als Abstraktionsk onzept das Umb enennen und das V erb er gen v on Aktionen Insb esondere die T atsac he da das b etrac h tete Abstrak tionsk onzept das V erb ergen v on Aktionen erlaubt erm oglic h t im allgemeinen b eson ders stark e Reduktionen des Zustandsraums Bei dieser Au erung m ussen wir aller dings et w as v orsic h tig sein Da innerhalb des Prozesses v on der Homomorphismus Ber e chnung bis zur Berec hn ung des Minimalautomaten zum homomorphen Bild der Sc hritt en thalten ist den p oten tiell nic h tdetermi nistisc hen Automaten zur Bild sprac he deterministisc h zu mac hen k ann das abstrakte V erhalten im Prinzip durc h einen gr o eren Zustandsraum dargestellt sein als das k onkrete V erhalten einer Sp ezi k ation Daher sind unsere obigen Bemerkungen heuristisc h motiviert Beim bishe rigen praktisc hen Einsatz der dargestellten Abstraktionsmetho de w ar der abstrakte Zustandsraum imm er w esen tlic h kleiner als der k onkrete w as hei en soll da je nac h Gr o e des k onkreten Zustandsraums der abstrakte Zustandsraum um einige Zehnerp otenzen w eniger Zust ande en thielt Diese Beobac h tung en tspric h t auc h den Erfahrungen mit anderen Abstraktionsans atzen die in der Literatur dargestellt w er den da ublic herw eise Abstraktionen en tsprec hend der zugrundeliegenden Sp ezi k a tion im Hin blic k auf eine Zustandsreduktion de niert w erden Das t ypisc he An w endungsfeld der in dieser Dissertation en t wic k elten Metho den ist der Bereic h der ko op erier enden Systeme Dies sind lose gek opp elte reaktiv e neb enl au ge Systeme also Systeme die aus mindestens zw ei nic h ttermi nie renden auf au ere Signale reagierenden Komp onen ten b estehen die n ur sc h w ac h sync hro nisiert sind Eine w esen tlic he Sc h wierigk eit b ei der V eri k ation solc her Systeme ist da der Nac h w eis v on Eigensc haften ohne F airnessannahmen im allgemeinen zu stark ist um k o op erierende Systeme zu v eri zieren Zu stark hei t hierb ei da k orrekte Systeme als nic h t k orrekt erk ann t w erden k onnen F airness ub erlegungen w erfen wiederum das Problem auf den f ur die gegeb ene F ragestellung ad aquaten F airnessb egri nden zu m ussen Um zu v ermei den explizit F airnessb esc hr ankun gen de nieren zu m ussen ub er die dann faire W orte in einem System v erhalten vii c harakterisiert w erden de nieren wir in der v orliegenden Dissertation eine V erallge meinerung v on un ter F airnessb esc hr ankungen erf ullten Eigensc haften Wir b etrac h ten eine relativierte F orm v on Leb endigk eitseigensc haften die wir r elative L eb endig keitseigenschaften nennen Diese Leb endigk eitseigensc haften hei en relativ da sie relativ zum V erhalten einer Sp ezi k ation de niert sind Alle partiellen Berec hn un gen einer Sp ezi k ation sind zu v ollst andigen Berec hn ungen fortsetzbar so da die b etre ende Eigensc haft erf ullt wird Relativ e Leb endigk eitseigensc haften sind auc h un ter dem Begri der Maschinenab geschlossenhe it b ek ann t Generell k ann durc h Abstraktionen die V erletzung v on Eigensc haften b ei der Be trac htung fairer abstrakter Berec hn ungen eines endlic hen Zustandssystems v erb or gen bleib en Daher ist es nic h t v erwunderlic h da auc h die V eri k ation relativ er Le b endigk eitseigensc haften anhand v on Abstraktionen des System v erhalte ns Sc h wie rigk eiten b ereitet Im allgemeinen k ann man nic h t v on relativ en Leb endigk eitseigen sc haften des abstrakten V erhaltens auf en tsprec hende relativ e Leb endigk eitseigen sc haften des k onkreten V erhaltens sc hlie en Daher stellen alphab etisc he Sprac hho momorphisme n b ezogen auf relativ e Leb endigk eitseigensc haften einen zu generellen Mec hanism us zur De nition v on V erhaltensabstraktionen dar Einen f ur die An forderungen der Ub erpr ufung relativ er Leb endigk eitseigensc haften an Abstraktio nen des System v erhaltens ad aquaten Abstraktionsmec hanism us erhalten wir durc h Besc hr ankung der zul assigen Homomorphismen auf die Klasse der Homomorphis men die schlicht auf dem k onkreten V erhalten des Systems sind Die Sc hlic h theit v on Homomorphismen liefert uns wie wir zeigen w erden eine hinreic hende als auc h not w endige Bedingung um an V erhaltensabstraktionen relativ e Leb endigk eitseigen sc haften des k onkreten System v erhaltens zu v eri zieren Aufbauend auf den Ergeb nissen ub er relativ e Leb endigk eitseigensc haften und sc hlic h te Abstraktionen zeigen wir da sc hlic h te Homomorphismen auc h ein ad aquates Abstraktionsk onzept f ur Ir gendwann Eigenschaften Eventuality Pr op erties darstellen dies sind Eigen sc haften deren Erf ullung in einem System v erhalten imme r irgendw ann m oglich ist Als Besc hreibungssprac hen f ur Eigensc haften und das V erhalten v on Systemen v er w enden wir temp or ale L o gik resp ektiv e end liche b eschriftete T r ansitionssysteme nite state Lab elled T ransition Systems L TS F ormeln der temp oralen Logik er m oglic hen es Aussagen ub er den c hronologisc hen Ablauf v on Aktionsfolgen zu for m ulieren Sie c harakterisieren formal eine Un terklasse der regul aren Sprac hen die sogenannten sternfreien Sprac hen L TS sind endlic he Automaten mit aus sc hlie lic h akzeptierenden Zust anden Sie b esc hreib en genau die Klasse der regu l aren Sprac hen die durc h den Eilenb er g Limes pr a xab geschlossener r e gul ar er Spr achen darstellbar sind Die Ergebnisse die in der v orliegenden Dissertation pr asen tiert w erden sind generell v on der F orm Der Eilen b erg Limes einer pr a xab gesc hlossenen regul aren Sprac he erf ullt in der en tsprec henden W eise eine temp o rale Logikformel genau dann w enn der Eilen b erg Limes des homomorphen Bildes der Sprac he eine en tsprec hende temp orale Logikformel in der selb en W eise erf ullt viii Im Anhang an diese Dissertation b etrac h ten wir auc h eine v ollst andige Charak terisierung sc hlic h ter Abstraktionen in der Eigensc haften allgemein durc h regul are Sprac hen repr asen tiert w erden Um den praktisc hen Einsatz der in der v orliegenden Dissertation en t wic k elten Ergeb nisse zu dokumen tieren w enden wir die Resultate auf drei v ersc hiedene Beispiele an anhand derer v ersc hiedene Asp ekte des V eri k ationsansatzes mittels V erhal tensabstraktion illustriert w erden Das Sp ektrum reic h t hier v on den p oten tiellen Reduktionsm oglic hk ei ten des Ansatzes ub er mehrstu ge Abstraktionen bis hin zu einer praktisc hen Anforderungen en tnommenen F ragestellung zur Aufdec kung unerw unsc h ter W ec hselwirkungen v on Diensten in Intel ligent en Netzen Das die m oglic he Zustandsraumreduktion illustrierende Beispiel en th alt ein v ereinfac h tes V erbindungsauf und abbauprotok oll Mehrstu ge Abstraktionen w erden am Bei spiel der Un tersuc h ung des Basic Cal l State Mo dels des Grundmo dells des T ele fondienstes b esc hrieb en Im Beispiel mit dem st arksten Praxisb ezug wird die unerw unsc h te W ec hselwirkung der T elefondienste Cal l F orwar ding Unc onditional und Sele ctive Cal l R eje ction auf Sp ezi k ationseb ene aufgedec kt Neb en den b ereits genann ten inhaltlic hen Punkten en th alt die v orliegende Disserta tion nat urlic h auc h eine Einordn ung der erzielten Ergebnisse in existierende Arb eiten so wie eine die en t wic k elte n Ans atze b ew ertende Sc hlu b emerkung Ac kno wledgemen ts It is di cult to thank all the p eople who in some w a y ha v e con tributed to this thesis and I am quite a w are of the fact that trying to do so is an in tractable task Nev ertheless I w an t to name at least the most imp ortan t p ersons I ask ev eryb o dy whom I ma y ha v e omitted to please accept m y ap ologies I w ould lik e to start with Dr Peter Ochsenschl ager who sup ervised m y thesis from the start He w as alw a ys there to answ er ev en silly questions and to guide the dev elopmen t of this thesis in neither to o strong nor to o w eak a w a y He aroused m y in terest in formal metho ds and v eri cation And not least he rst de ned simple homomorphisms that are widely used throughout the thesis I thank Peter for his guidance friendship and patience and for sharing his exp erience with me Another imp ortan t role with resp ect to m y thesis w as pla y ed b y Pr of Dr Eckart R aub old During his p erio d as the head of the Institute for T eleco op eration T ec hnol ogy of GMD the German National Researc h Cen tre for Information T ec hnology the thesis w as initiated He is m y sup ervisor at the Univ ersit y of F rankfurt and prev en ted this thesis from b eing to o theory prone The metho ds dev elop ed in this thesis w ere applied to service in teraction detection in a join t pro ject of GMD and Deutsc he T elek om where Pr of R aub old is no w the head of the researc h and dev el opmen t division I thank him for encouraging me to write this thesis and for his sup ervision During the w ork on this thesis I had the pleasure to visit the researc h group of Pr of Dr Pierr e Wolp er at the Institute Mon te ore of the Univ ersit y of Li ege Belgium He is the third p erson who had a strong in uence on the shap e of the thesis He made me giv e a top ological c haracterization of relativ e liv eness that help ed m uc h to motiv ate wh y one should lo ok at relativ e liv eness prop erties I thank Pierr e for his hospitalit y and encouragemen t for the man y time consuming discussions and last but not least for b eing willing to b ecome a mem b er of the b oard of examiners of m y thesis My sta y at Li ege w as supp orted b y a D AAD fello wship under gran t HSP I I A UFE that I gratefully ac kno wledge ix x According to the regulation at the Univ ersit y of F rankfurt for a thesis written in English I needed an additional review of the thesis I am v ery grateful to Pr of Dr Wolfgang Thomas for agreeing to tak e on this job In addition I thank Pr of Thomas for his suggestions of ho w to impro v e the thesis There are a lot of colleagues at GMD s Institute for T eleco op eration T ec hnology who had a great impact on this thesis to o I cannot name them all In particular I w an t to thank J ur gen R epp for his friendship and the man y discussions w e had Additional thanks for in teresting discussions go to F r ank Nie ner Wolfgang Orth R oland R ieke and Helmut Wiland I thank our studen ts F arhad F atahi V anani R alph Demant and R afael Galvez Estr ada for their CFU and SCR sp eci cation that I used as a basis for the sp eci cation in Section I kindly ask ev ery one at GMD who feels that he or she should ha v e b een explicitly men tioned to o to b e patien t with me A t the Univ ersit y of Li ege I thank Bernar d Boigelot Philipp e L ejoly and Dr Pasc al Grib omont for their hospitalit y and for the time they sp en t on discussions and in tro ducing me to Mon te ore s facilities The con tact with Dr Bernhar d Heinemann w as also v ery v aluable for me I thank him for his p ermanen t in terest in m y w ork and his supp ort and am grateful to him for sta ying in touc h with me Also Dr Glenn Bruns and Dr John Derrick ha v e touc hed signi can tly the pro cess of establishing this thesis I w an t to thank them b oth Pr of Dr A mir Pnueli ma y not ha v e ev en realized that he ga v e me an imp ortan t hin t with resp ect to relativ e liv eness prop erties at the REA CT meeting at T amp ere I am v ery thankful for his hin t Jane R ippin and Bernar d Parslow help ed to impro v e the presen tation signi can tly They indep enden tly read draft v ersions of this thesis v ery carefully and corrected man y mistak es I thank them v ery m uc h for the e ort they sp en t in correcting the man uscript An y mistak es that remain are m y o wn I w ould lik e to sa y thank y ou to m y family and friends who had to share the ups and do wns with me during the w ork on this thesis It is m y deep wish to thank m y paren ts Hilde gar d and Erich Nitsche for their p er manen t moral as w ell as nancial supp ort during m y whole life I thank them for their lo v e Last but absolutely not least I thank Heidrun Ultes for her lo v e encouragemen t and supp ort as w ell as for her patien t w a y of dealing with m y alw a ys not the b est of mo o ds when nishing this thesis If an y one had to su er from the fact that I wrote a thesis then it w as her I am deeply thankful to her Gewidmet meinen Eltern Hilde gar d und Erich Nitsche so wie Heidrun und Juliana Ultes Con ten ts In tro duction General F ramew ork Beha viour Prop erties Abstraction Related W ork Organization of the Thesis Pre Publications Preliminaries Notation and Basic De nitions Automata Theoretic Bac kground Prop erties Abstraction Comm uting Limit and Homomorphism Preserv ation Brief Summary of the Chapter PL TL and Abstraction A Syn tactical Restriction of the F orm ulae xiii xiv CONTENTS Purely T emp oral F orm ulae and Abstraction PL TL F orm ulae and Abstraction Nonerasing Homomorphisms A Nonhomomorphic Mapping Brief Summary of the Chapter Relativ e Liv eness A Motiv ating Example Relativ e Safet y and Liv eness Alternativ e Characterizations Relativ e Liv eness and F airness Relativ e Liv eness and Abstraction Impro ving the Results Ev en tualit y Prop erties Brief Summary of the Chapter Examples State Space Reduction Example The Proto col The Analysis of the Proto col The Phase Separation Prop ert y Establishing a Connection is Alw a ys P ossible A Remark on Complexit y Reduction Detection of Logical Service In teractions A Brief In tro duction to Service In teractions in In telligen t Net w orks Sp eci cation of CFU and SCR CONTENTS xv Completing the Sp eci cation In teraction of CFU and SCR V eri cation of a BCSM Sp eci cation Brief Summary of the Chapter Conclusions Summary F urther Study A A Characterization of Simplicit y A Preliminaries A Characterizing Simple Homomorphisms A Brief Summary of App endix A B Ev en tualit y Prop erties and CTL B In terpretation of Languages B De ning CTL with resp ect to T lim L B Relation to Ev en tualit y Prop erties B Brief Summary of App endix B xvi CONTENTS Chapter In tro duction General F ramew ork V eri c ation is the systematic searc h for errors in a system s sp eci cation w e c hec k whether the sp eci ed system meets sp eci c correctness requiremen ts If v eri cation is successful w e kno w that the sp eci ed system is error free with resp ect to the c hec k ed requiremen ts The systems w e are considering are c o op er ating systems Co op erating systems are closed systems no outside in teractions consisting of at least t w o di eren t comp onen ts Usually the comp onen ts in teract with one another quite rarely lo ose c oupling All comp onen ts are r e active i e they sho w an ongoing b eha viour in time and react to ev en ts in v ok ed b y their en vironmen t A comp onen t s en vironmen t is all other comp onen ts of the system Unless comp onen ts in teract they act concurren tly i e the b eha viour of one comp onen t is then indep enden t of the b eha viour of all other comp onen ts Therefore co op erating systems are r e active c oncurr ent systems Man y di eren t examples of co op erating systems of practical in terest exist e g computer net w orks telephone systems systems of async hronous electronic circuits and distributed systems in general A c omputation of a comp onen t of a co op erating system is a sequence of actions Here an action is an atomic ev en t of a comp onen t The de nition of actions often dep ends on our view of the system and the prop erties w e w an t to c hec k There can b e questions w e w an t to ask ab out a system where a complex sequence of ev en ts is in terpreted as a single action that cannot b e assumed to b e atomic in other cases Chec king the correctness of some distributed application in most cases for instance do es not require a detailed consideration of the in v olv ed comm unic ation medium idealized comm unication is assumed i e message transfer is view ed as a single action In con trast for a comm uni cation proto col that deals with corrupted CHAPTER INTR ODUCTION messages considering the in ternal b eha viour of a comm unic ation c hannel is of high imp ortance Th us in the second case message transfer cannot b e considered to b e atomic Beha viour The b ehaviour of a co op erating system is the set of all p ossible c omputations of the system A computation is an in nite sequence of lo c al actions compatible with in teractions b et w een comp onen ts Here lo cal means that the action is asso ciated with one comp onen t A computation is considered in nite b ecause the system s comp onen ts are reactiv e and hence sho w an ongoing b eha viour in time A computa tion is a c hronological sequence of actions This means if in a computation action a of comp onen t A app ears b efore action b of comp onen t B then comp onen t A has p erformed action a b efore B has p erformed b If a and b can b e executed concur ren tly then the b eha viour of the system con tains a computation where a is b efore b as w ell as a corresp onding computation where b is b efore a This represen tation of concurrency is called interle aving of concurren t actions Hence w e consider inter le aving semantics W e assume the n um b er of di eren t actions a co op erating system ma y p erform to b e nite Consequen tly a computation is an w ord o v er a nite alphab et The alphab et s letters are the actions of the system Then the b eha viour of a co op erating system is a set of w ords i e it is an language Tho o v er the alphab et of actions W e consider nite state co op erating systems i e co op erating systems that consist of nitely man y comp onen ts and eac h comp onen t has nitely man y in ternal states A global state of a co op erating system is determined b y one state p er comp onen t F ormally suc h a nite state system is an automaton with only accepting states i e w e use the term nite state system as a synon ym for the notion of nite state lab elled transition system The nite w ord languages accepted b y nite state systems are the pre x closed regular languages Pre x closed means that all pre xes of w ords in the language are also w ords in language The languages accepted b y nite state systems are the limits Eilen b erg limits of pre x closed regular languages Eil This corresp onds to our in tuition computations of a co op erating system are in nitely con tin ued partial computations of the system Considering only pre x closed languages corresp onds to the observ ation that for all partial i e nite computations of a system all their pre xes are also partial computations of the system PR OPER TIES Prop erties As already men tioned w e w an t to c hec k whether a co op erating system satis es par ticular pr op erties W e reduce this question to the question whether the b eha viour of the system satis es the prop erties since with resp ect to satisfaction of prop erties w e regard systems to b e fully c haracterized b y their b eha viour The prop erties w e are dealing with are line ar prop erties The term linear refers to the satisfaction condition for this t yp e of prop ert y A system or more exactly a systems s b e ha viour satis es a prop ert y linearly if and only if all its computations satisfy the prop ert y Consequen tly a set of computations can b e partitioned in to the set of computations that satisfy the prop ert y and the set of computations that do not Therefore w e can iden tify a prop ert y with the set of computations that satisfy it T o form ulate prop erties explicitly w e use the language of prop ositional linear time temp oral logic Eme In practice when considering v eri cation t w o di eren t t yp es of questions are fre quen tly ask ed Do es nothing bad happ en and Will something go o d ev en tually happ en Referring to these questions prop erties can b e classi ed in to safety and liveness prop erties AS Lam Roughly sp eaking safet y prop erties guaran tee the absence of bad situations meaning that if a computation do es not satisfy the prop ert y then there is a nite pre x of the computation suc h that all computations sharing this pre x do not satisfy the prop ert y there is a p oin t in the computa tion where the bad situation can b e detected Liv eness guaran tees progress of the system b y guaran teeing that something go o d ev en tually happ ens A prop ert y is called a liv eness prop ert y if all partial computations can b e extended to a complete computation that satis es the prop ert y T o b e able to v erify liv eness prop erties of a system it is almost alw a ys necessary to include a fairness h yp othesis in the system description F ra In tro ducing a fairness h yp othesis mak es it p ossible to ignore b eha viours that corresp ond to ex treme execution scenarios and that in an y case w ould not o ccur in an y reasonable implem en tation Ev en though this in tuition is clear making fairness precise is some what more complicated should one b e we akly or str ongly fair tr ansition or pr o c ess fair or is not justic e or ev en c omp assion what fairness should really b e MP Of course there is a rational w a y of c ho osing whic h fairness notion is adequate for a giv en problem b y considering the nature of the mo del b eing used and making rea sonable assumptions ab out ho w it migh t b e implem en ted but it remains that this c hoice is crucial and delicate F urthermore in tro ducing a fairness h yp othesis often mak es the v eri cation pro cess somewhat more problematic This is esp ecially true in the con text of abstraction see the next section Indeed since after mo ving to the abstract lev el one deals with a reduced set of actions it can b ecome imp ossible to express correctly the fairness h yp othesis under whic h the system is correct This mak es one wish for a more general and abstract notion of truth under fairness that CHAPTER INTR ODUCTION w ould con tribute to simplifyi ng v eri cation esp ecially in the con text of abstraction In tuitiv ely the notion to b e formalized is that of a prop ert y b eing true pro vided one is giv en some con trol o v er the c hoices made during in nite executions In other w ords one w an ts to c haracterize the prop erties that can b e made true b y some fair implem en tati on of the system W e consider in this thesis a c haracterization of suc h prop erties Our c haracteriza tion is straigh tforw ardly the notion of a liv eness prop ert y considered r elative to the b ehaviours of the system That is w e de ne r elative liveness pr op erties as prop erties that are liv eness prop erties if one restricts the univ erse of b eha viours to those of the system Their de nition is a relativized v ersion of the de nition of liv eness ev ery partial computation of the system can b e extended to a computation of the system that satis es the prop ert y Relativ e liv eness prop erties also satisfy an adapted v er sion of the top ological c haracterization of liv eness prop erties they are dense sets within the system s b eha viour Not surprisingly w e also sho w the notion of safet y prop erties can b e similarly transp osed in to the notion of r elative safety pr op erties T op ologically these prop erties are the closed sets within the univ erse of b eha viours of the system F or a prop ert y to b e a relativ e liv eness prop ert y of a system corresp onds in the desired abstract sense to the prop ert y b eing satis ed under fairness In crude terms the system almost satis es its relativ e liv eness prop erties it just needs the help of some fairness remem b er that ev ery pre x of a b eha viour of the system can b e extended to a an in nite b eha viour that satis es the prop ert y The fact that a prop ert y is a relativ e safet y prop ert y means that b eha viours of the system that do not satisfy the prop ert y can b e detected after a nite pre x F urthermore w e sho w that for regular systems and prop erties c hec king relativ e liv eness and relativ e safet y are decidable problems This and the fact that in a reasonable sense relativ e liv eness prop erties can b e satis ed b y some fair impleme n tation are rst indications of the usefulness of this concept for v eri cation In addition w e consider another t yp e of prop ert y that at rst glance app ears to b e a sp ecial case of a relativ e liv eness prop ert y It will turn out that there is a sligh t di erence F or some v eri cation tasks it can b e of in terest to c hec k a condition indep enden t of the so far partial computation the system can meet some require men ts ev en tually F or a comm uni cation proto col for example the requiremen t can b e r e aching the initial state W e call this t yp e of prop ert y an eventuality pr op erty A prop ert y is an ev en tualit y prop ert y of a system s b eha viour if and only if for eac h partial computation a computation exists con tin uing this partial computation and satifying ev en tually the prop ert y Ev en tualit y prop erties can b e c haracterized In this thesis w e in v estigate only relativ e liv eness prop erties in the con text of abstraction since these are natural prop erties one usually is in terested to c hec k for co op erating systems The notion of relativ e safet y prop erties is included in this thesis for completeness reasons and is in v estigated exhaustiv ely in Hen with resp ect to real time systems ABSTRA CTION b y the AG E F fragmen t Nit c Nit b of CTL CES They are also consid ered in Kur KV ev en tualit y prop erties are called always p ossibly pr op erties in KV In most cases satisfaction of an ev en tualit y prop ert y can b e reduced to the satisfaction of a corresp onding relativ e liv eness prop ert y Abstraction The size n um b er of states of a nite state represen tation of a co op erating system s b eha viour can gro w exp onen tially in the size of the sp eci cation of the system This observ ation is kno wn as state sp ac e explosion State space explosion is indeed a problem if w e realize that the time complexit y of kno wn v eri cation algorithms is linear in the n um b er of states of a system at b est Eme LP W ol Hence state space explosion is a limiting factor for the use of formal v eri cation in practice A promising approac h to deal with state space explosion is abstr action v ery often w e need not tak e in to accoun t in ternal actions of comp onen ts that are unimp ortan t with resp ect to the prop erties to b e v eri ed There exists a v ariet y of abstraction tec hniques Bru CGL GL Kur Nit a Nit c Nit d Oc h b Oc h a Sif that use di eren t concepts to simplify the state space W e de ne in this thesis abstractions directly on the b eha viour of a co op erating system not lo oking at the state structure of p ossible nite state represen tations Hence w e call the considered t yp e of abstraction b ehaviour abstr action What kind of state space simpli cation do es b eha viour abstraction o er There are essen tially t w o di eren t asp ects that are of practical in terest Actions ma y exist on the one hand that are completely unimp ortan t with resp ect to the prop erties to b e c hec k ed On the other hand there ma y b e actions that are not completely unimp ortan t but whic h need not b e distinguished from other actions W e can hide the former actions completely in all computations of the system without c hanging in principle the basic prop erties of a computation The latter actions can b e iden ti ed with other actions b y giving the iden ti ed actions a common name without ha ving an e ect on the v eri cation purp ose These t w o abstraction concepts are kno wn as action hiding and action r enaming resp ectiv ely What w e need to de ne b eha viour abstractions formally is the easy to apply concept of alphab etic language homomorphisms Har HU that is w ell established in for mal language theory W e only ha v e to mo dify this concept in an ob vious w a y to apply not only to nite w ord languages but to languages Nit a Unfortunately there is a remaining crucial problem alphab etic language homomorphisms are a to o general to ol for c hec king relativ e liv eness prop erties on abstractions Beha viours ex ist that do not satisfy a relativ e liv eness prop ert y but their abstractions ma y T o prev en t an abstraction from hiding the violation of a relativ e liv eness prop ert y w e CHAPTER INTR ODUCTION use the notion of simplicity of a homomorphism on a b eha viour Oc h Oc h b to de ne the righ t abstraction tec hnique W e sho w in this thesis that homomor phisms that are simple on a b eha viour cannot hide the violation of relativ e liv eness prop erties as w ell as the violation of ev en tualit y prop erties that are expressed b y a linear time prop ositional temp oral logic form ula In the more general case of regular prop erties w e sho w that simplicit y of a homomorphism on a b eha viour is not only a su cien t but a necessary condition to b e able to c hec k relativ e liv eness prop erties on an abstract b eha viour NO a NO a NO b see App endix A The practicalit y of abstraction approac hes is ev en increased if one can nd a partial state space construction metho d that allo ws the construction of the abstract state space without an exhaustiv e construction of the concrete one F or the abstraction tec hnique presen ted in this thesis a comp ositional analysis approac h that excellen tly ts to the abstraction tec hnique is presen ted in Oc h a Related W ork The abstraction approac h presen ted in this thesis is based on concepts dev elop ed b y P eter Oc hsensc hl ager F or the v eri cation of relativ e liv eness prop erties on ab stractions the k ey de nition is the one of a simple homomorphism Oc h Oc h b The w ealth of the abstraction tec hniques that w e will dev elop can b e increased b y a tec hnique for the e cien t construction of the minimal nite state system repre sen ting the abstract b eha viour Ho w to construct e cien tly the abstract state space using a comp ositional analysis metho d is presen ted in Oc h a Oc h Com bining the results of the presen t thesis with the ones in Oc h a Oc h w e can c hec k prop erties of a state space that w e do not ha v e to construct exhaustiv ely at all A v ariet y of abstraction approac hes can b e found in literature with resp ect to dif feren t description languages for systems and prop erties and di eren t mathematical to ols for de ning abstractions Most of the approac hes in literature co v er the v eri cation of prop ositional linear time temp oral logic PL TL form ulae using abstraction and th us are comparable to Chapter Abstraction approac hes for the v eri cation of relativ e liv eness prop erties and ev en tualit y prop erties resp ectiv ely are so far not established In addition most existing abstraction approac hes lac k a concept for action hiding b ecause action hiding demands prop erties of the abstraction to b e mo di ed to hold for the concrete b eha viour what the ma jorit y of abstraction approac hes a v oids Glenn Bruns Bru de nes abstraction mappings on CCS sp eci cations Mil that preserv e form ulae of the mo dal calculus Koz Sti Glenn Bruns results co v er more prop erties than the ones considered in Chapter b ecause the mo dal calculus is more expressiv e than PL TL Bruns uses a notion of action hiding based RELA TED W ORK on CCS concept of in ternal actions that is w eak er than the one de ned via alphab etic language homomorphisms So the abstractions he considers in general do not decrease the size of the state space as m uc h as the approac h presen ted in this thesis Joseph Sifakis Sif lo oks at structure preserving relations on the states of nite state systems These are homomorphsims on states He sho ws the preserv ation of prop erties describ ed b y a linear time as w ell as a branc hing time logic Sifakis homomorphisms are related to bisim ulations Mil if b oth the relation and its in v erse are homomorphisms then the relation is a bisim ulation The metho d of Sif relates states to states not c hanging actions of the system Compared to action renaming and hiding pro vided b y alphab etic language homomorphisms one cannot exp ect corresp ondingly signi can t reductions of the state space The w ork in Sif is con tin ued b y Susanne Graf and Claire Loiseaux also applying it to practical v eri cation tasks without c hanging the principal abstraction mec hanism GL Gra The abstraction approac h that is most closely related to the one presen ted in Chap ter is the one of Rob ert Kurshan Kur He considers automata with b o olean algebra transition lab els to determine the letters that can b e read when a transition is tak en As abstractions Rob ert Kurshan considers b o olean algebra homomorphisms applied to the transition lab els These b o olean algebra homomorphisms result in formal language terms exactly in non erasing alphab etic language homomorphisms A concept of action hiding mapping to the empt y w ord is not included Hence the results in Kur are strongly related to Section of this thesis In addition Kurshan applies his approac h to real time systems Clark e Grum b erg and Long CGL presen t another closely related abstraction approac h They again consider only action renaming to b e precise they iden tify lab elled states with one another since they lo ok at transition systems without tran sition lab els Their approac h is lo cated in the area of hardw are v eri cation There one is usually in terested in collapsing the n um b er of di eren t v alues that ma y b e assigned to the system s v ariables By iden tifying di eren t v alues they are able to decrease the n um b er of di eren t system states imm ensely without the need of an action hiding mec hanism Clark e Grum b erg and Long describ e prop erties in CTL CES Therefore their approac h is related in some w a y to ev en tualit y prop erties Nev ertheless the approac h in CGL is not v ery suitable for the v eri cation of co op erating systems where explicit hiding of actions is almost alw a ys essen tial The Clark e Grum b erg and Long approac h is extended in DGG and Dam When talking ab out state space explosion a v oidance b esides abstractions there exists another line of researc h that has to b e men tioned One can consider compu tations to b e equiv alen t if they are equal except for p erm utations of neigh b oured indep endent actions The equiv alence classes with resp ect to this equiv alence rela CHAPTER INTR ODUCTION tion are called tr ac es The b eha viour of a system is then represen ted b y its set of traces This w a y of dealing with state space explosion is called p artial or der metho ds or tr ac e semantics Go d GW GW GW Maz V al b V al a W G P artial order metho ds also o er the p ossibilit y to reduce the state space signi can tly Nev ertheless since the order of indep enden t actions is partly ignored they are so far not applicable in general for the v eri cation of liv eness prop erties The de nition of a r elative liveness pr op erty that w e presen t in this thesis is nearly equiv alen t to the de nition of machine closur e AL AL AH Mac hine closure is a condition of a subset of a b eha viour with resp ect to the b eha viour In this con text the subset of the b eha viour B is called a progress prop ert y AL or B liv eness condition AH resp ectiv ely Using the notion of mac hine closure T om Henzinger to o de nes relativ e liv eness and safet y in Hen He assumes that the prop erties are subsets of the considered b eha viour and then relaxes the de ni tion to general prop erties obtaining an equiv alen t de nition to the one presen ted in this thesis He giv es alternativ e but equiv alen t top ological c haracterizations of rela tiv e liv eness and safet y Henzinger in v estigates esp ecially relativ e safet y prop erties b ecause he is in terested in real time systems where timing constrain ts mak e liv e ness prop erties collapse to safet y prop erties An exhaustiv e in v estigation of relativ e liv eness prop erties as presen ted in this thesis is not co v ered in Hen In KV Orna Kupferman and Moshe V ardi presen t a mo dule che cking approac h for temp oral v eri cation There they establish a tec hnique for the comp onen t wise v eri cation with resp ect to di eren t en vironmen ts Kupferman and V ardi consider b esides other prop ert y classes a fragmen t of CTL that they call always p ossi bly prop erties Alw a ys p ossibly prop erties are exactly the ev en tualit y prop erties presen ted b y the AG E F fr agment of CTL as established in App endix B The ab straction and v eri cation approac h for ev en tualit y prop erties as it is presen ted in this thesis th us app ears to b e a suitable abstraction metho d for mo dule c hec king alw a ys p ossibly prop erties Organization of the Thesis In Chapter w e in tro duce the notions of b eha viour prop ert y and abstraction that w e use throughout this thesis The basic de nitions are all tak en from formal language theory esp ecially theory of languages and from concepts in temp oral logics The de nitions are mo di ed up to the exten t needed to t in to the con text During the w ork for this thesis the concept of relativ e liv eness and corresp ondingly its dual relativ e safet y ha v e b een dev elop ed indep enden tly of Hen establishing an ob vious relativization of unconditional safet y and liv eness AS to obtain a v eri cation mec hanism for co op erating systems based on relativ e liv eness OR GANIZA TION OF THE THESIS of co op erating systems Additionally w e consider three di eren t t yp es of prop ert y preserv ation under abstraction Chapter con tains abstraction results for the prop ositional linear time temp oral logic PL TL W e de ne a syn tactical transformation on PL TL form ulae that estab lishes a w eak preserv ation result for PL TL prop erties under alphab etic language homomorphism abstractions Assuming that the abstracting homomorphism is non erasing w e sho w a strong preserv ation result for PL TL By extending erasing al phab etic language homomorphisms to non homomorphic mappings w e can pro v e that the resulting abstraction tec hnique preserv es PL TL prop erties su cien tly The terms we ak su cient and str ong preserv ation of prop erties are de ned in Chapter W e de ne relativ e liv eness prop erties in Chapter and in addition the dual concept of relativ e safet y prop erties W e giv e a top ological as w ell as a set inclusion de nition of these prop erties The set inclusion de nition rev eals an algorithm for deciding relativ e liv eness and safet y for regular prop erties on regular b eha viour W e re late relativ e liv eness to mac hine closure whic h is a nearly equiv alen t concept and sho w ho w to construct a nite state system to a b eha viour that satis es a relativ e liv eness prop ert y suc h that all strongly fair F ra computations of the nite state system satisfy the prop ert y linearly W e presen t an example in the in tro duction of Chapter that motiv ates the de nition of relativ e liv eness In addition the example rev eals that b eha viour abstraction is a delicate task when dealing with relativ e liv e ness prop erties F or handling the problems that arise with regard to relativ e liv eness prop erties and abstraction w e de ne the notion of simplicit y of homomorphisms on b eha viours and sho w that simple homomorphisms are the righ t to ol for the de ni tion of abstractions that su cien tly preserv e relativ e liv eness prop erties In addition to relativ e liv eness prop erties w e de ne ev en tualit y prop erties a prop ert y class closely related to relativ e liv eness prop erties and pro v e corresp onding results for ev en tualit y prop erties as w e pro v e for relativ e liv eness prop erties Considering an example w e can c haracterize the sligh t di erence b et w een relativ e liv eness and ev en tualit y prop erties T o illustrate the usefulness of the presen ted results w e apply them to three di eren t examples in Chapter First w e use an example from Oc h a to sho w that the established preserv ation results allo w the v eri cation of sp eci cations that ha v e state spaces of arbitrary size The second and third examples are tak en from the area of service in teraction detection in in telligen t net w orks These examples are in tro duced b y giving a short in tro duction to the service in teraction problem The decision to consider these examples is motiv ated b y their practical relev ance as w ell as the fact that they are t ypical examples of co op erating systems It is esp ecially the second example where w e sho w the in teraction of the services Cal l F orwar ding Unc onditional and Sele ctive Cal l R eje ction that has a high practical relev ance W e presen t in this example all steps from the sp eci cation of the services to the detection of their in teraction CHAPTER INTR ODUCTION In Chapter w e presen t a summary of the results in this thesis and giv e an outlo ok on topics for further study In addition to the main c hapters this thesis con tains t w o app endices App endix A con tains the precise c haracterization of simple homomorphisms with resp ect to preserv ation of relativ e liv eness prop erties In App endix B w e presen t explicitly the relation b et w een ev en tualit y prop erties and the AG E F fragmen t of CTL W e ha v e app ended to eac h c hapter a brief informal summary of the c hapter s results Pre Publications The main results presen ted in this thesis ha v e already app eared in a series of tec hni cal rep orts DFV GE DFV GE Nit b NO a NO b NOR w orkshop con tributions Nit d NO a and review ed pap ers CDGE CDFV Nit a Nit c Nit Nit b Nit a NO b Results published in these pap ers are pre sen ted in a uni ed and extended framew ork in this thesis Bet w een handing in of this thesis in Decem b er and its defence in Marc h additional pap ers related to the thesis w ere published or accepted for publication NNO NORR Nit NW NNO Nit The pap er NW w on the b est student p ap er awar d of the th Ann ual A CM Symp osium on Principles of Distributed Computing San ta Barbara CA Nit is an abridged v ersion of Nit a NO a and NO b are revised v ersions of NO a Chapter Preliminaries In this c hapter w e giv e the terms b ehaviour pr op erty abstr action and pr op erty pr eservation a formally precise meaning W e start with the de nition of a system s b eha viour using a nite automaton description The k ey notion is B uc hi acceptance of w ords W e represen t a system s b eha viour b y a regular language suc h that eac h w ord represen ts a computation of the system Realizing that eac h pre x of a partial computation of a system is itself a partial computation of the system w e ha v e to deal with regular languages that are Eilen b erg limi ts Eil of pre x closed regular languages P artial computations are nitely long w ords and a partial b eha viour of a system is a pre x closed regular language The automaton mo del for the represen tation of b eha viours is the nite state lab elled transition system that w e brie y call nite state system W e de ne prop erties linearly i e their satisfaction is de ned with resp ect to eac h computation of a system separately W e classify prop erties in the usual w a y in to safet y and liv eness prop erties and in tersections of a safet y and a liv eness prop ert y AS T o describ e linear prop erties w e use the prop ositional linear time temp oral logic PL TL Eme W e use alphab etic language homomorphisms extended to in nite w ords to de ne the abstraction of a b eha viour Alphab etic language homomorphisms are a formal implem en tation of action renaming and action hiding they allo w the renaming of transition lab els as w ell as the complete remo v al of transitions in a nite state system If w e determinize and minim ize the resulting nite state system then w e obtain the nite state system that w e use to represen t the abstract b eha viour The notion of prop ert y preserv ation describ es the relation of prop erties of the ab straction to prop erties of the original b eha viour W e will distinguish three di eren t Deterministic and nondeterministic nite state systems no acceptance condition represen t the same class of languages CHAPTER PRELIMINARIES t yp es of prop ert y preserv ation W e b egin this c hapter with a brief description of the notation that w e use and the basic de nitions Notation and Basic De nitions By I N w e designate the set f g of natural n um b ers I N denotes the set f g of non negativ e in tegers Additionally w e de ne m n I N m n fi I N j m i ng Let b e a set of nite cardinalit y i e an alphab et represen ting the p ossible actions of a system A computation of the system is an in nite sequence of actions There fore w e represen t computations b y in nite w ords o v er so called w ords o v er W e designate the set of all w ords o v er b y Hence the b eha viour of a system i e the set of all computations a system can p erform is a subset of Subsets of are called languages o v er W e represen t systems b y their b eha viour whic h w e de ne using nite automata without acceptance conditions A partial computation is a nitely long sequence of actions in Therefore it is a nitary w ord o v er The set of all w ords i e partial computations o v er is denoted b y also con taining the empt y w ord denoted b y A partial b eha viour is a subset of i e it is a language o v er T o de ne sets that con tain b oth nite and in nite computations w e write for Let w w w w w n I N b e a partial computation and let x n x x x b e a computation o v er F or i j I N i j w e set w w w i i j x x x Let L b e a partial b eha viour and let L b e a b e i i j ha viour o v er F or i j I N w e write w x and x to denote the i j i j i sub w ords w w w x x x and the su x x x x resp ectiv ely i i i i j i i i max j n The length of a w ord w is the n um b er n of letters it con tains suc h that m ultiple o ccurences of a letter are m ultiply coun ted W e write jw j to denote the length of w F or an w ord x w e set jxj F or a language L and a w ord w the leftquotien t of L b y w is c ont w L fv j w v Lg F or an language L and a w ord w the leftquotien t of L b y w is c ont w L fx j w x L g W e use the notation c ont w L instead of w L whic h is used in formal language theory Ber Har The c ont w L notation b etter re ects that the leftquotien t is the set of p ossible con tin uations of w ords in a language or an language resp ectiv ely In addition the c ont w L notation a v oids to confuse leftquotien ts and in v erse homom orphism s in further de nitions A UTOMA T A THEORETIC BA CK GR OUND Automata Theoretic Bac kground Let b e an alphab et represen ting the p ossible actions of a system W e represen t the system b y the sequences of actions that it p erforms Hence w e represen t it b y its b eha viour T o describ e b eha viours w e use nite state systems i e nite automata with only accepting states De nition A nite automaton A Q q F c onsists of a nite set Q of states an input alphab et a tr ansition r elation Q Q an initial state q Q and a set F of nal states Har HU Tho Final states ar e also c al le d ac c epting states T o b e able to represen t b eha viours i e languages in terms of automata w e de ne a run of an automaton on an w ord o v er its input alphab et De nition L et A Q q F b e a nite automaton and let x b e an wor d in x x x x A run of A on x is a se quenc e q q q Q of states such that q is the initial state of A i e q q and i I N q x q i i i F or a run r Q of A on x r denotes the set of al l states that r ep e at in nitely often in r In tuitiv ely a run of A on x is a sequence of states A runs through when reading x A run is successful if and only if A visits at least one accepting state in nitely often F ormally this is captured b y B uc hi acceptance B uc The set of all B uc hi accepted w ords is the b eha viour that is describ ed b y A De nition L et A Q q F b e a nite automaton and let x b e an wor d in L et r b e a run of A on x We c al l r suc c essful if and only if r F We say that A B uchi ac c epts x if and only if ther e exists an ac c epting run of A on x B uc Tho The b ehaviour i e the language r epr esente d by A is L A fx j A B uchi ac c epts xg De nition L anguages that ar e B uchi ac c eptable by some nite automaton ar e c al le d r e gular languages Tho W e ha v e considered so far computations that are complete i e in nite Regarding time w e ha v e considered the sequences of actions that a system w ould p erform in an in nite amoun t of time What is also of in terest are the sequences of actions that a system p erforms in a nite amoun t of time W e call them partial computations CHAPTER PRELIMINARIES Since partial computations are nite they are simply w ords o v er The set of all w ords o v er or in our con text the set of partial computations o v er is denoted b y Subsets of are called languages o v er or partial b eha viours o v er W e consider only regular partial b eha viours i e partial b eha viours represen ted b y nite automata W e use a de nition of acceptance of partial b eha viours that is corresp onding to B uc hi acceptance based on the notion of a partial run De nition L et A Q q F b e a nite automaton and let w b e a wor d over w w w w w n I N A p artial run of A on w is a nite n se quenc e q q q q Q of states such that q is the initial state of A i e n q q and i n q w q i i i An automaton accepts a w ord if and only if it can reac h an accepting state when reading the w ord In terms of a partial run this is co v ered b y the follo wing de nition De nition L et A Q q F b e a nite automaton and let w b e a wor d over L et p p p p p n jw j b e a p artial run of A on w We c al l n p ac c epting if and only if p F We say that A ac c epts w if and only if ther e n exists an ac c epting p artial run of A on w The p artial b ehaviour i e the set of p artial c omputations r epr esente d by A is de ne d as L A fw j A ac c epts w g If for all states q in Q and all letters a in the successor state of q with resp ect to a is uniquely determined then A is called deterministic De nition L et A Q q F b e a nite automaton If q Q a jfp Q j q a p gj the tr ansition r elation is uniquely determine d for al l q and a then A is c al le d a deterministic automaton Otherwise A is c al le d nondeterministic In the in nite case i e for languages the kno wn equiv alence of the language classes accepted b y deterministic and nondeterministic automata do es not hold Note Ther e exist languages i e system b ehaviours that c an only b e r ep r esente d by nondeterministic nite automata but not by deterministic ones A n example of a r e gular language that demands a nondeterministic B uchi automaton to ac c ept it is the language that c ontains al l wor ds over fa bg which c ontain only nitely many o c curr enc es of letter a Tho A UTOMA T A THEORETIC BA CK GR OUND F or nitary languages the w ell kno wn equiv alence of nondeterminism and determin ism holds Har HU In v arious con texts w e will need the notion of nite pre xes of w ords w ords De nition L et w b e a p artial c omputation let x b e a c omputation let L b e a p artial b ehaviour and let L b e a b ehaviour over The set of pr e xes of w is pr e w fw j i jw j g If v is a pr e x of w i e v pr e w i such that v and v w then v is c al le d a pr op er pr e x of w The set of nite pr e xes of x is pr e x fx j i I N g The sets of pr e xes of L and L i S S r esp e ctively ar e pr e L pr e w and pr e L pr e x w L x L In tuitiv ely computations of a system are in nitely con tin ued partial computations W e can formalize this observ ation using the notion of the Eilen b erg limi t De nition L et L b e a p artial b ehaviour over The Eilenb er g limit l im L of L is de ne d as l im L fx j w pr e x w Lg R e ad as ther e exist in nitely many di er ent W e ma y sa y brie y limit instead of Eilen b erg limit Regarding the remarks so far a b eha viour of a system is the limit of a regular language Hence a b eha viour is a deterministic B uc hi language Note A n language L c an b e ac c epte d by a deterministic B uchi automaton if and only if ther e exists a r e gular set L such that l im L L L is the r e gular language that is nite wor d ac c epte d by the B uchi automaton ac c epting l im L Tho Lo oking at a b eha viour it w ould generally mak e no sense to allo w partial computa tions to ha v e pre xes that are not partial computations of the system Therefore w e consider only pre x closed partial b eha viours De nition L et L b e a p artial b ehaviour over L is c al le d pr e x close d if and only if pr e L L Pre x closed regular languages are accepted b y nite automata with only accepting states W e call these automata nite state systems CHAPTER PRELIMINARIES De nition L et A Q q F b e a nite automaton If F Q A has no ac c eptanc e c ondition then we c al l A a nite state system Note The class of pr e x close d r e gular languages is exactly the class of p ar tial b ehaviours that ar e ac c eptable by nite state systems W e consider in this thesis only partial b eha viours that are pre x closed regular lan guages and b eha viours that are Eilen b erg limi ts of pre x closed regular languages Prop erties In this section w e de ne prop erties of a system s b eha viour T o b e precise w e de ne line ar prop erties Here linear refers to the w a y these prop erties are satis ed a b eha viour satis es a prop ert y if and only if all its computations do So satisfaction of prop erties is established with resp ect to computations and is then extended linearly to b eha viours meaning that satisfaction is preserv ed under set union In tuitiv ely a prop ert y partitions the set in to the set Y of the computations that satisfy the prop ert y and the set N of computations that do not T o de ne a prop ert y formally w e simply iden tify the prop ert y with the set Y of computations that satisfy it De nition L et b e an alphab et A pr op erty P over is a subset of henc e it is an language over We say that a b ehaviour L satis es P written L j P if and only if L P W e can c haracterize prop erties in regard to their in tuitiv e meaning AS Lam There are prop erties that demand the absence of bad situations i e the absence of ob vious errors This t yp e of prop erties is referred to as safety prop erties What can w e sa y ab out safet y prop erties The ob vious error is an error that if it o ccurred could not b e xed If suc h an error o ccurs in a computation meaning that the computation do es not satisfy the safet y prop ert y there m ust b e a p oin t in the sequence of actions where indep enden t of the further actions the prop ert y cannot b e satis ed In more formal terms there m ust b e a pre x of the w ord A nite state system is often called a nite state lab elled transition system F or pre x closed languages L the Eilen b erg limit l im L corresp onds to the set A L whic h con tains all w ords suc h that al l their nite pre xes are in L W e consider in this thesis the Eilen b erg limit rather than the A op erator for reasons of generalit y some results on l im L presen ted in this thesis also hold for non pre x closed regular languages L PR OPER TIES whereat indep enden t of the follo wing su x the safet y prop ert y cannot b e satis ed W e giv e a de nition equiv alen t to the one in AS where w e use the notion of pre x sets This de nition is more suitable for b eing compared to the de nitions of relativ e safet y and relativ e liv eness in Chapter than the notation used in AS De nition A pr op erty P is c al le d a safety pr op erty if and only if for al l x x j P implies that ther e exists a pr e x w pr e w such that for al l y we have w y j P Other prop erties of in terest are the ones that demand that an in tended condition will ev en tually o ccur something go o d will ev en tually happ en These prop erties are called liveness prop erties F or a liv eness prop ert y the p ossible satisfaction of the prop ert y m ust b e indep enden t of the partial computation up to this p oin t Hence for all partial computations there m ust exist a computation suc h that if the partial computation and the computation are concatenated the resulting computation will satisfy the prop ert y W e presen t the de nition of liv eness of AS De nition A pr op erty P is c al le d a liveness pr op erty if and only if for al l w ther e exists an wor d x such that w x j P A liv eness prop ert y is a pr o gr ess prop ert y since it demands progress in direction to meet sp eci c requiremen ts An in teresting result ab out liv eness and safet y is that all prop erties can b e represen ted as the in tersection of a liv eness and a safet y prop ert y Note L et P b e a pr op erty over Then P is the interse ction of a liveness pr op erty P and a safety pr op erty P AS l s The pro of of this note in AS is based on a c haracterization of liv eness prop erties as dense sets and the safet y prop erties as closed sets in the Can tor top ology o v er Eil see Section T o describ e prop erties w e use a logical description language pr op ositional line ar time temp or al lo gic PL TL Eme Pn u The smallest PL TL form ulae are atomic prop ositions PL TL form ulae are de ned with resp ect to a set AP of atomic prop ositions The atomic prop ositions are com bined b y b o olean connectiv es and temp or al op erators W e start with the de nition of PL TL s syn tax De nition First of al l al l atomic pr op ositions and the pr op osition tr ue ar e PL TL formulae If and ar e PL TL formulae then so ar e CHAPTER PRELIMINARIES X and U Only formulae that ar e c onstructable as pr esente d ar e PL TL formulae It is usual to in tro duce additional op erators as abbreviations of particular op erator com binations De nition As additional op er ators we de ne F tr ue U G F B U T o impro v e presen tation pairs of paren theses in PL TL form ulae can b e omitted with resp ect to the op erators priorities De nition The temp or al op er ators U B F G and X ar e of highest priority fol lowe d by fol lowe d by fol lowe d by fol lowe d by fol lowe d by A mbiguities ar e hand le d fr om right to left e g G U is e quivalent to G U PL TL form ulae are in terpreted o v er in nite sequences of truth v alues for the atomic AP prop ositions i e o v er functions of the t yp e I N or equiv alen tly o v er w ords AP de ned on the alphab et W e will also in terpret PL TL form ulae o v er w ords de ned on an arbitrary alphab et with the help of a lab elling function that assigns truth v alues for atomic prop ositions to letters in the alphab et PR OPER TIES De nition L et b e an alphab et and let AP b e a set of atomic pr op ositions AP A lab el ling function of letters with truth values for atomic pr op ositions takes a letter in to the set of atomic pr op ositions that we de ne to b e satis e d for the letter As w e in terpret letters as actions of a system lab els actions with their atomic prop erties The seman tics i e the meaning of a PL TL form ula is then de ned with AP resp ect to an w ord x and a lab elling function in tro ducing a satisfaction relation j F or a PL TL form ula read x j as x satis es with resp ect to the lab elling of letters with truth v alues for s atomic prop ositions PL TL s seman tics is de ned in the follo wing manner De nition L et b e an alphab et let AP b e the set of atomic pr op ositions of a AP PL TL formula let b e a lab el ling function and let x b e a c omputation in L et and b e PL TL formulae Then x j if and only if one of the fol lowing c onditions is satis e d If tr ue then x j If is an atomic pr op osition then x j if and only if x If then x j if and only if it is not the c ase that x j If then x j if and only if x j and x j If X then x j if and only if x j If U then x j if and only if ther e exists an i I N such that x j and for al l j i x j i j All other op erators abbreviate particular op erator com binations Although their meaning can b e deriv ed from the upp er seman tics de nition w e de ne the seman tics of the temp oral op erators explicitly The meaning of the deriv ed b o olean connectiv es is w ell kno wn De nition F or the additional temp or al op er ators the satisfaction r elation is de ne d in the fol lowing way If F then x j if and only if ther e exists an i I N such that x j i CHAPTER PRELIMINARIES If G then x j if and only if for al l i I N x j i If B then x j if and only if ther e exists no i I N such that x j or ther e exists an i I N and ther e exists a j i such that i x j x j and for al l k i x j i j k A PL TL form ula describ es a linear prop ert y since its satisfaction is de ned with resp ect to single computations De nition L et b e an alphab et let AP b e the set of atomic pr op ositions AP of a PL TL formula let b e a lab el ling function and let L b e an language Then L satis es L j if and only if for al l x L x j A PL TL form ula describ es a prop ert y in the ob vious w a y De nition L et b e an alphab et let AP b e the set of atomic pr op ositions of AP a PL TL formula and let b e a lab el ling function Then the pr op erty describ e d by with r esp e ct to is the set fx j x j g The satisfaction relation for PL TL form ulae is exactly compatible with the general de nition of satisfaction of linear prop erties Note L et b e an alphab et let AP b e the set of atomic pr op ositions of a AP PL TL formula let b e a lab el ling function and let L b e an language Then L j if and only if L In Chapter when de ning a syn tactical transformation for PL TL form ulae w e ha v e to distinguish PL TL form ulae where the scop es of the temp oral op erators co v er all atomic prop ositions De nition We c al l a PL TL formula pur ely temp or al if and only if al l atomic pr op ositions ar e in the sc op e of a temp or al op er ator De nition means that purely temp oral PL TL form ulae cannot b e separated in to di eren t subform ulae suc h that the PL TL form ula is a b o olean com bination of the subform ulae and at least one subform ula is a single atomic prop osition Note The pr oblem of whether a nite automaton is an automaton that B uchi ac c epts for a PL TL formula and a lab el ling function is PSP A CE c omplete GPVW VW WVS Wol ABSTRA CTION Abstraction V eri cation of temp oral prop erties describ ed b y PL TL form ulae is a rather complex task Mo del c hec king i e c hec king whether a system s b eha viour satis es a form ula is a PSP A CE complete problem Eme Ev en though algorithms exist for c hec king satisfaction of a PL TL form ula in an regular b eha viour that are exp onen tial in the size of the form ula and linear in the size of the B uc hi automaton represen ting the b eha viour LP the automaton s size is usually a limiting factor for v eri cation tasks of practical relev ance T o measure the size of a PL TL form ula w e coun t the n um b er of op erators in the form ula As the size of an automaton w e consider its n um b er of states Instead of automaton size w e also sa y size of the state space of a system The main reason for automata sizes b eing a limiting factor for practical v eri cation tasks is ob viously the tremendous size of state spaces that corresp ond to industrial sized sp eci cations Co op erating systems consist of sev eral comp onen ts that are lo osely coupled Hence the size of the state space of the complete system is nearly the pro duct of the state space sizes of its comp onen ts and eac h comp onen t itself can b e a rather complex system T o deal with systems whose b eha viour represen tations are to o large to c hec k prop erties e cien tly w e can re ect up on the fact that the considered b eha viours quite often con tain information that is of no imp ortance at all with regard to the prop er ties to b e c hec k ed If w e tak e only actions in to accoun t that are essen tial with resp ect to the prop erties of in terest not taking in to accoun t all other actions w e sa y that w e are lo oking at an abstraction of a system s b eha viour Not taking actions in to accoun t means hiding them in a particular b eha viour There is also the case where it is only imp ortan t that one action from a bunc h of actions has to app ear in a com putation Here w e can iden tify actions with one another b y giving them a common name Remem b ering that w e represen t actions b y letters action renaming and hid ing is exactly co v ered b y alphab etic language homomorphisms Eil Har HU Since alphab etic language homomorphisms are initially de ned for nite w ords w e extend them additionally to partial mappings on w ords leading to what w e call an abstraction homomorphism De nition L et and b e two alphab ets We c al l a mapping h an abstr action homomorphism if and only if the fol lowing c onditions hold If we c onstr ain h to a mapping on letters in then we obtain a total function h f g If v w and x then h v w h v h w and h v x h v h x CHAPTER PRELIMINARIES If we c onstr ain h to a mapping on wor ds over then we obtain a p artial function h i e we de ne h to b e unde ne d for wor ds which it would map to nitely long wor ds note that Instead of abstraction homomorphism w e also ma y sa y abstracting homomorphism De nition sa ys that h is the extension of a function that tak es letters to letters or the empt y w ord This extension is done letterwise F or nite w ords as already men tioned suc h a mapping is called an alphab etic language homomorphism T o b e able to distinguish precisely b et w een w ords and w ords w e de ne h in suc h a w a y that h x is only de ned for an w ord x if h x itself is an w ord if there is an n I N suc h that for all i n h x then h x is unde ned otherwise it is i de ned The application of abstraction homomorphisms to languages and languages is done in the usual w a y De nition L et h b e an abstr action homomorphism and let M Then h M fh x j x M g Note Using De nition we c an determine the set of wor ds x over such that h x is de ne d by h h Since w e are considering b eha viours that are Eilen b erg limi ts of pre x closed regular languages w e ha v e to de ne the abstract b eha viour to a concrete one in these terms De nition L et h b e an abstr action homomorphism and let L b e a pr e x close d r e gular language We de ne the abstr action of the c oncr ete b ehaviour l im L with r esp e ct to h to b e l im h L W e sho w that this de nition is reasonable for pre x closed regular L since in this case l im h L b ecomes equal to h l im L Comm uting Limit and Homomorphism W e will need later on in some pro ofs a condition that implies for a language L and an abstraction homomorphism h that l im h L is a subset of h l im L this implies l im h L h l im L This subset condition do es not COMMUTING LIMIT AND HOMOMORPHISM hold for the general case W e pro v e it for pre x closed regular languages T o do so w e use K onig s Lemma in a suitable presen tation HR Lemma Lemma K onig s Lemma L et R E E b e a r elation E is an arbitr ary S set and let for al l n I N E b e a nite nonempty subset of E such that E n n n I N is in nite and to e ach e E ther e exists an f E such that f e R Then n n ther e exists an in nite se quenc e e in E such that e E and e e R n n n n n n I N for al l n I N Let L b e a pre x closed regular language Let h b e an abstrac tion homomorphism If x is an w ord in l im h L then there exists a sequence n n n n w of w ords w h L suc h that w pr e x and jw j n for all n I N n I N The last condition holds b ecause L is pre x closed implies that h L is pre x closed n to o w is the sequence of all pre xes of x and th us generates x as its limit n I N n n T o eac h of the w w e construct a set U of minimal in v erse images of w U is the n n n n set of all w ords u in h w L suc h that there is no shorter w ord v in h w L with c ont u L c ont v L Remem b er that c ont u L is the leftquotien t of L b y u see Section De nition We de ne for al l n I N n n U fu h w L j v h w L juj jv j c ont u L c ont v L g n n n Because all w are in h L there m ust b e a u L suc h that h u w Consequen tly w e ha v e Observ ation U is not empty for al l n I N n Let u U F or all v U suc h that c ont u L c ont v L w e ha v e jv j juj b y n n de nition of U Because there are only nitely man y sets c ont w L w their n n um b er corresp onds to the n um b er of states of the minim al automaton accepting L w e obtain Both conditions pre x closedness and regularit y are necessary for enabling us to comm ute limit and homom orphism Let L b e the not pre x closed regular language a b and let h b e an ab straction homom orphism determined b y h a a and h b Then l im L and th us h l im L is the empt y set but h L a and th us l im h L a Hence l im h L h l im L n n Also for the pre x closed non regular con text free language L pr e fa b jn I N g w e ha v e l im L h l im L and l im h L a n The notation w should not b e confused with the nth p o w er of w CHAPTER PRELIMINARIES Observ ation U is a nite set for al l n I N n Because U U if n m and all U are nonempt y sets w e observ e n m n S Observ ation U is an in nite set n n I N By w e designate the prop er pre x relation i e for all u v u v if and only if u v and u pr e v W e sho w Lemma F or al l n I N and al l v U ther e exists a wor d u U such n n that u v n Pro of Let v b e in U and let u b e in pr e v suc h that h u w Hence u v n n Because L is pre x closed u is in L and th us u h w L The rest of v after u w e designate v i e v uv W e supp ose that u is not in U and sho w a n con tradiction n If u U then there m ust b e a w ord u h w L suc h that ju j juj and n n n c ont u L c ont u L Because u is in h w L w e ha v e h u v w Be cause c ont u L c ont u L w e obtain u v L and c ont v L c ont u v L n So u v is in h w L c ont u v L c ont v L and ju v j jv j Therefore v U whic h con tradicts the c hoice of v n W e ha v e sho wn for the construction of U that all preconditions hold to n n I N apply K onig s Lemma Th us w e can pro v e the tec hnical lemma that w e will need in further pro ofs Lemma If L is a pr e x close d r e gular language and h is an abstr action homomorphism then l im h L h l im L Pro of If l im h L then h l im L Therefore w e can assume l im h L l im h L h l im L Let x l im h L Then there exists an in nite sequence n n n w of w ords in h L suc h that jw j n and w pr e x for all n I N n I N W e construct an in nite sequence U of subsets of L as de ned ab o v e With n n I N resp ect to the ab o v e observ ations and the previous lemma w e ha v e seen that all PRESER V A TION S U are nonempt y nite sets U is an in nite set and for all v U there n n n n I N exists a u U suc h that u v n n According to K onig s Lemma there exists an in nite sequence u of w ords in n I N n n n n L suc h that u U and u u for all n I N The sequence u uniquely n n I N n n generates a w ord y l im L and b ecause h u w for all n I N w e obtain h y x So for all x l im h L there exists a y l im L suc h that x h y Th us l im h L h l im L h l im L l im h L Let x b e in l im L suc h that h x is de ned Because L is pre x closed all u pr e x are in L So for all u pr e x h u is in pr e h x Because h x is de ned there are in nitely man y di eren t h u in pr e h x for u pr e x L Th us h x is in l im h L and w e obtain h l im L l im h L Preserv ation It is our aim to c hec k prop erties on the abstraction of a system s b eha viour and to dra w conclusions ab out prop erties of the system s b eha viour itself W e refer to the b eha viour of the system as the original b eha viour or as the concrete b eha viour to distinguish it from its abstraction What w e ask is What can w e sa y ab out the preserv ation of prop erties under abstraction Here preserv ation essen tially de scrib es that violation of requiremen ts b y the concrete b eha viour is not hidden b y the abstraction W e classify preserv ation results in to three groups strong preserv ation su cien t preserv ation and w eak preserv ation W e de ne these classes with resp ect to necessary transformations of PL TL form ulae W e sa y that an abstraction strongly preserv es PL TL prop erties if and only if the same form ula is satis ed for the original b eha viour as for the abstraction What ma y v ary is the lab elling function that is used to ev aluate the form ula for the abstract and the concrete b eha viour resp ectiv ely Abstraction tec hniques that strongly preserv e prop erties are usually rather limited i e they do not allo w to decrease su cien tly the n um b er of states to represen t the abstract b eha viour compared to the n um b er of states necessary to represen t the concrete b eha viour F or example in Section the abstraction tec hnique that strongly preserv es PL TL prop erties do es not p ermit hiding of actions A more promising preserv ation result is su cien t preserv ation If w e obtain informa tion ab out all computations of the original b eha viour from a PL TL prop ert y of the abstraction but the form ula represen ting the prop ert y of the concrete b eha viour ma y b e syn tactically mo di ed then w e sa y that the prop ert y is su cien tly pre CHAPTER PRELIMINARIES serv ed F or PL TL prop erties w e will establish a su cien t preserv ation result only for a non homomorphic abstraction tec hnique Section F or relativ e liv eness prop erties represen ted b y PL TL form ulae Chapter w e will establish a su cien t preserv ation result for homomorphic abstractions presuming that the abstraction homomorphism is simple on the b eha viour simplici t y of homomorphisms is de ned in Section Abstractions de ned b y homomorphisms ha v e the adv an tage of b e ing easily implem en ted and of p ermitting action renaming and action hiding They usually allo w an imme nse collapse of the state space that represen ts a concrete b e ha viour resulting in a reasonably small nite state system represen ting the abstract b eha viour F or PL TL prop erties with usual linear satisfaction and for homomorphic abstrac tions w e will only b e able to sho w that if a computation is not completely hidden b y the abstraction then it satis es a prop ert y corresp onding to the one of the ab straction W e call this not v ery satisfactory t yp e of preserv ation w eak preserv ation In formal terms instead of l im L w e can only pro v e l im L h h to satisfy prop erties corresp onding to prop erties of l im h L Brief Summary of the Chapter W e ha v e de ned the b eha viour of a system to b e the Eilen b erg limit l im L of a pre x closed regular language L The language s alphab et con tains the actions of the system Eac h w ord in a b eha viour is a computation of the system A prop ert y is the set of computations that in tuitiv ely satisfy the prop ert y Hence it is a subset of the set of all computations o v er action alphab et i e a subset of T o describ e prop erties w e use the language of prop ositional linear time temp oral logic PL TL An abstraction establishes a reduced b eha viour of a system that tak es only actions in to accoun t whic h are imp ortan t with resp ect to a prop ert y one w an ts to c hec k W e call the reduced b eha viour abstract b eha viour A nite state represen tation of an abstract b eha viour is usually m uc h smaller than a nite state represen tation of the original b eha viour F or this reason abstraction is in general necessary to deal with large so called industrial sized systems in order to handle the complexit y Prop ert y preserv ation c haracterizes the usefulness of abstraction with resp ect to v eri cation It qualitativ ely measures the amoun t of information ab out a b eha viour whic h can b e obtained automatically from kno wing its abstraction Chapter PL TL and Abstraction W e de ne in this c hapter abstraction tec hniques that in v arious w a ys preserv e linear prop erties describ ed b y PL TL form ulae W e pro v e that abstraction homo morphisms w eakly preserv e PL TL prop erties T o do so w e de ne a mapping R on PL TL form ulae that syn tactically rewrites them in suc h a w a y that the con crete b eha viour of a system satis es R if its abstract b eha viour satis es for a PL TL form ula Nit a W eak preserv ation of prop erties is not a v ery satisfac tory result Informally R con tains only information ab out visible computations under the abstraction of the concrete b eha viour Nev ertheless to de ne R w e de ne a mapping R that w e use throughout this thesis W e sho w for all abstract computations x all concrete computations x suc h that x is an abstraction of x and all PL TL form ulae that x satis es R if and only if x satis es W e pro v e for non erasing abstraction homomorphisms no letter is tak en to the empt y w ord that they strongly preserv e PL TL form ulae This is not a surprising result if w e consider that the ab o v e men tioned syn tactical transformation R handles essen tially sub w ords of a concrete computation that are mapp ed on If no letter is tak en to i e no action is hidden then R b ecomes the iden tit y function and con sequen tly w e ha v e a strong preserv ation result Non erasing abstraction tec hniques are quite frequen tly used CGL GL Kur Sif They ha v e the adv an tage of establishing strong preserv ation results and the dra wbac k that they do not pro vide an action hiding mec hanism whic h is v ery useful for collapsing large state spaces De ning based on homomorphic abstraction a non homomorphic abstraction tec h nique that disallo ws complete hiding of computations but includes action hiding w e get a su cien t preserv ation result for PL TL form ulae with resp ect to this abstraction tec hnique Before starting to establish the preserv ation results for PL TL form ulae with resp ect to di eren t abstraction tec hniques w e rst de ne a presen tation of PL TL form ulae CHAPTER PL TL AND ABSTRA CTION that mak es the de nition of syn tactical transformations on the form ulae easier w e use a represen tation that iden ti es abstract actions and atomic prop ositions of the PL TL form ulae with one another This mere syn tactical restriction do es not limit the expressiv eness of PL TL In addition the restricted represen tation is practically v ery useful A Syn tactical Restriction of the F orm ulae It is our aim to obtain from PL TL prop erties of an abstract b eha viour of a co op erating system as m uc h information ab out its original b eha viour as p ossible T o do so w e de ne a syn tactical transformation on PL TL form ulae The syn tactical transformation is de ned as a function that tak es PL TL form ulae to PL TL form ulae W e do not de ne this function for arbitrary PL TL form ulae but for a syn tactically restricted sub class of PL TL This restriction do es not limit the expressiv eness of the form ulae and it will also not limit the usual w a y of form ulating PL TL prop erties First w e disallo w b o olean or temp oral op erators in the scop e of the negation op erator De nition We say that a PL TL formula is in ne gation normalform if and only if exclusively a single atomic pr op osition or the pr op osition tr ue is in the sc op e of e ach ne gation i e al l ne gations ar e plac e d dir e ctly in fr ont of an atomic pr op osi tion or tr ue It is easy to construct a PL TL form ula in negation normalform to an arbitrary PL TL form ula b y using dual op erators and F and G and U and B are dual op erators X is dual to itself W e c hec k prop erties of b eha viours of co op erating systems i e languages The PL TL form ulae ha v e to describ e the structure of computations i e of the w ords that satisfy the prop ert y Accordingly w e consider PL TL form ulae ha ving actions as their atomic prop ositions De nition L et b e an alphab et of actions We de ne that a PL TL formula is in normalform if and only if is in ne gation normalform and al l atomic pr op ositions of ar e in i e AP We evaluate PL TL formulae in normalform using a lab el ling function that identi es the atomic pr op ositions with the letters in We de ne the lab el ling function such that a a fag PUREL Y TEMPORAL F ORMULAE AND ABSTRA CTION Note F or al l PL TL formulae over a set AP of atomic pr op ositions and al l AP lab el ling functions ther e exists a PL TL formula in normalform such that for al l x x j if and only if x j This means that restricting to PL TL form ulae in normalform do es not limit ex pressiv eness compared to unrestricted PL TL form ulae W e will c hec k PL TL form ulae on an abstract b eha viour to obtain corresp onding prop erties of the original b eha viour If h is the abstracting homomor phism then the form ulae that w e c hec k on the abstraction will b e in normalform T o obtain prop erties of the original b eha viour from its abstraction w e ha v e to de ne a suitable represen tation for the deriv ed PL TL form ulae W e use the same atomic prop ositions as in normalform extended b y the additional atomic prop osition De nition L et h b e an abstr acting homomorphism We say that a PL TL formula is in h r epr esentation if and only if al l atomic pr op ositions in ar e in f g F ormulae in h r epr esentation wil l b e evaluate d with r esp e ct to h T o evaluate a PL TL formula in h r epr esentation we de ne the h lab el ling function f g F or al l c we de ne c fh c g h h Purely T emp oral F orm ulae and Abstraction Let and b e t w o alphab ets let h b e an abstracting homomorphism and let L b e an language represen ting some abstract b eha viour W e de ne a mapping T that tak es a purely temp oral PL TL form ulae in normalform to a PL TL form ulae in h represen tation suc h that for all purely temp oral in normalform h L j T if and only if L j Remem b er that a purely h temp oral PL TL form ula is a PL TL form ula suc h that all atomic prop ositions are in the scop e of a temp oral op erator see De nition The main purp ose of T is to cop e with actions that h tak es to If h w ere nonerasing h to ok no actions to then T w ould b e the iden tit y function First w e in v estigate the case where a PL TL form ula do es not con tain temp oral op erators i e w e are dealing with a b o olean form ula In this case w e ha v e to b e sligh tly cautious b ecause w e ha v e to a v oid that a concrete action that is hidden b y the abstraction satis es some atomic prop osition a with resp ect to Otherwise w e could construct h PL TL form ulae in normalform that are con tradictions with resp ect to but satis able with resp ect to h CHAPTER PL TL AND ABSTRA CTION De nition We de ne N to b e a mapping on PL TL formulae that r eplac es al l subformulae a of a PL TL formula by a wher e a is an atomic pr op osition Lemma L et h b e an abstr acting homomorphism L et x b e an abstr act c omputation and let x h x L et b e a b o ole an formula in normalform Then x j if and only if x j U N h Pro of Let i I N suc h that h x x and for all j i h x W e ha v e i j for all atomic prop ositions a that x j a if and only if x j a and i h th us x j a if and only if x j a Because h x w e ha v e h i i x j a if and only if x j a According to the seman tics h i of b o olean connectiv es w e obtain x j if and only if x j N h i F or all j i h x whic h means that x j N and x j Th us j h h j j x j if and only if x j U N h Considering N instead of is quite imp ortan t Otherwise the if part in V Lemma w ould not hold Let us lo ok at the form ula a F or all x a V w e ob viously ha v e x j a But for x h x suc h that h x a V V w e ha v e x j a Only b y considering N a do w e obtain the h a a V desired result x j N a h a Corollary L et h b e an abstr acting homomorphism L et L b e an language L et b e a b o ole an formula in normalform Then L j if and only if h L j U N h Pro of Corollary is a consequence of Lemma considering that satisfac tion of a PL TL form ula b y an language stands for satisfaction of the form ula b y all w ords in the language No w w e de ne the mapping T that tak es a PL TL form ula in normalform to a PL TL form ula in h represen tation The purp ose of T is a syn tactical transformation that is compatible with in tersp ersed sub w ords that h tak es to De nition L et b e a PL TL formula in normalform for some alphab et PUREL Y TEMPORAL F ORMULAE AND ABSTRA CTION L et b b e a binary b o ole an op er ator i e b f g We de ne tr ue if tr ue tr ue if tr ue a if a a if a and a T b T if b T T U T if U T B T if B F T if F G T if G U X U T if X W e sho w for this transformation that an abstract computation satis es a purely temp oral PL TL prop ert y if and only if corresp onding concrete computations satisfy the transformed prop ert y Lemma L et h b e an abstr acting homomorphism L et x b e an abstr act c omputation and let x h x L et b e a pur ely temp or al PL TL formula in normalform Then x j if and only if x j T h Remark L emma is not surprising b e c ause T takes c ar e of subwor ds of wor ds in h x that h takes to not changing the gener al structur e of Pro of The pro of is b y induction on the structure of If con tains exactly one temp oral op erator that quan ti es o v er all atomic prop ositions in the induction s basis then all prop er subform ulae of are b o olean form ulae and hence T N By Lemma for all prop er subform ulae of and all x h x w e ha v e x j if and only if x j U N Therefore if h x x j h if and only if x j N W e use this equiv alence to pro v e the induction s basis h CHAPTER PL TL AND ABSTRA CTION Because all atomic prop ositions of are in the scop e of the only temp oral op erator w e need not pro v e the induction s basis for b o olean connectiv es U x j U if and only if there exists an i I N suc h that x j and for all j i x j This is equiv alen t to the existence of i j a k I N suc h that x j N and for all l k suc h that h x x j k h l l h N Th us x j U if and only if x j N U N h B x j B if and only if there exists no i I N suc h that x j or there exists an i I N and a j i suc h that x j i i x j and for all k i x j This is equiv alen t to There k j exists no l I N suc h that x j N or there exists an l I N and an m l h l suc h that x j N x j N and for all n l x j N l h m h n h Therefore x j B if and only if x j N B N h F x j F if and only if there exists an i I N suc h that x j i This is equiv alen t to the existence of a j I N suc h that x j N Hence h j x j F if and only if x j F N h G x j G if and only if x j for all i I N This is equiv alen t i to F or all j I N suc h that h x x j N note that there are in nitely j j h man y di eren t j I N suc h that h x Consequen tly x j G if and j only if x j G N h X x j X if and only if x j Equiv alen tly there exists a j I N and a k j suc h that x j N h x and for all l j h k j suc h that l k h x So x j X if and only if x j U l h X U N This last step nishes the pro of of the induction s basis As the induction s h y p othesis supp ose that for all prop er subform ulae of that satisfy the lemm a s preconditions x j if and only if x j T for all x and all h x h x The prop er subform ulae of need not necessarily satisfy the preconditions of the lemma b ecause they can con tain atomic prop ositions that are not in the scop e of a temp oral op erator of the subform ula Hence in general a subform ula of is the b o olean com bination of b o olean form ulae and purely temp oral form ulae b By induction w e ha v e x j if and only if x j T According to t t h t Lemma x j if and only if x j U N Th us x j if b h b b and only if x j U T b ecause T N Hence if h x then h b b b x j if and only if x j T Therefore for all subform ulae of w e b h b ha v e if h x then x j if and only if x j W e use this condition h as an extension of the induction s h yp othesis PUREL Y TEMPORAL F ORMULAE AND ABSTRA CTION b Because of the lemma s preconditions and m ust b e purely temp o ral subform ulae of for a binary b o olean connectiv e b Then b y induction and b y the seman tics of b o olean connectiv es x j b if and only if x j h T b T U x j U if and only if there exists an i I N suc h that x j and for all j i x j By induction this is equiv alen t to i j the existence of a k I N suc h that x j T and for all l k x j h h k l T or h x Therefore x j U if and only if x j l h T U T B x j B if and only if there exists no i I N suc h that x j or there exists an i I N and a j i suc h that x j i i x j and for all k i x j By induction this is equiv alen t k j to There exists no l I N suc h that x j T or there exists an l I N h l and an m l suc h that x j T x j T and for all n l l h m h x j T Therefore x j B if and only if x j T B T h h n F x j F if and only if there exists an i I N suc h that x j i By induction this is equiv alen t to the existence of a j I N suc h that x j h j T Hence x j F if and only if x j F T h G x j G if and only if x j for all i I N By induction this i is equiv alen t to F or all j I N suc h that h x w e ha v e x j T note j j h that there are in nitely man y di eren t j I N suc h that h x Consequen tly j x j G if and only if x j G T h X x j X if and only if x j Equiv alen tly b y induc tion there exists a j I N and a k j suc h that x j T h x h k j and for all l j suc h that l k h x So x j X if and only if l x j U X U T h Corollary L et h b e an abstr acting homomorphism L et L b e an language L et b e a pur ely temp or al PL TL formula in normalform Then L j if and only if h L j T h Pro of Corollary is a consequence of Lemma considering that satis faction of a PL TL form ula b y an language corresp onds to its satisfaction b y all w ords in the language CHAPTER PL TL AND ABSTRA CTION PL TL F orm ulae and Abstraction No w w e generalize Lemma for arbitrary PL TL form ulae in normalform Based on the mapping T w e de ne a mapping R that tak es PL TL form ulae in normalform to PL TL form ulae in h represen tation De nition L et b e a PL TL formula in normalform If is a b o ole an formula we de ne R U T and if is a pur ely temp or al PL TL formula we de ne R T Otherwise is the b o ole an c ombination of maximal pur ely temp or al subformulae and maximal b o ole an subformulae We obtain R by substituting al l by t b t T and al l by U T t b b W e obtain a result for PL TL form ulae in normalform that corresp onds to Lemma Corollary L et h b e an abstr acting homomorphism L et x b e an abstr act c omputation and let x h x L et b e a PL TL formula in normalform Then x j if and only if x j R h Pro of Corollary is a consequence of Lemma and Lemma consid ering the seman tics of b o olean connectiv es and taking in to accoun t T N b b for all b o olean form ulae in normalform b Corollary L et h b e an abstr acting homomorphism L et L b e an language L et b e a PL TL formula in normalform Then L j if and only if h L j R h Pro of Corollary is a consequence of Corollary considering that satis faction of a PL TL form ula b y an language corresp onds to its satisfaction b y all w ords in the language W e use the notation R to indicate that R is the basis for a mapping R w e de ne later W e call R and R the r etr anslation functions for PL TL PL TL F ORMULAE AND ABSTRA CTION According to Corollary R con tains as m uc h information ab out h L as can b e deriv ed from kno wing whether L j or L j No w w e in v estigate the relation b et w een prop erties of l im h L and l im L F or this purp ose w e extend R to cop e with w ords x in l im L suc h that h x is unde ned No information ab out these w ords is con tained in l im h L and th us they are not considered in the de nition of R De nition L et h b e an abstr acting homomorphism L et b e a PL TL formula in normalform L et f inite b e a non atomic pr op osition that is h satis e d for an wor d x if and only if h x is unde ne d We de ne R to b e f inite R h Considering f inite do es not lead us out of the scop e of PL TL b ecause w e can h express f inite b y F G b ehind some p oin t h tak es ev erything to h Corollary L et h b e an abstr acting homomorphism L et L L et b e a PL TL formula in normalform Then l im L j R if l im h L j h Pro of According to Corollary w e kno w that l im h L j if and only if h l im h L j R But l im L ma y con tain w ords x suc h that h x h is unde ned These w ords are not in h l im h L W e partition l im L in to t w o sets de f and unde f that con tain all w ords x in l im L suc h that h h h x is de ned and all w ords x in l im L suc h that h x is unde ned resp ec tiv ely W e ha v e h de f h l im L and h unde f Therefore de f is a h h h subset of h l im h L According to Corollary l im h L j implies de f j R All w ords x in unde f satisfy f inite Th us l im L j R h h h h h if l im h L j Corollary is the main result w e establish for PL TL form ulae with resp ect to homomorphic abstraction Because of the f inite part that is added to R PL TL h form ulae are only we akly preserv ed b y homomorphic abstractions This is not a v ery satisfactory result In the next t w o sections w e establish b etter results based on Corollary Ho w far a w a y the w eak preserv ation result of Corollary is from su cien t preserv ation of prop erties is c haracterized b y the follo wing t w o corollaries Corollary h R for al l PL TL formulae in h normalform CHAPTER PL TL AND ABSTRA CTION Pro of By de nition w e ha v e j According to Corollary w e obtain h j R and th us h R h h Corollary R n f inite h for b eing a PL TL h h h formula in normalform Pro of By de nition w e ha v e R n f inite j R W e no h h h h tice R n f inite h h R n f inite There h h h h h h fore b y Corollary h R n f inite j Hence w e obtain h h h R n f inite h h h h By Corollary w e ha v e h R Because h h f inite w e obtain h R n f inite h h h h h The t w o corollaries once again rev eal that the computations that are hidden b y the abstraction i e the computations in f inite are the delicate ones with h h resp ect to v eri cation using abstractions Nonerasing Homomorphisms In this section w e sho w that for nonerasing homomorphisms and limits of pre x closed regular languages PL TL form ulae are str ongly pr eserve d b y in v erse homomor phic abstractions R b ecomes the iden tit y function and all if conditions b ecome if and only if conditions This is not a surprising result since the only aim of R is to handle sub w ords of w ords in l im L that are tak en to It is imp ortan t to notice that the results of this section migh t app ear b etter than they are b ecause when dealing with abstraction in practice one is usually in terested in hiding most of the actions But action hiding is only p ossible when using erasing homomorphisms Corollary L et h b e an abstr acting homomorphism such that for al l a h a L et b e a PL TL formula in normalform and let L Then L j if and only if h L j h Pro of Because h a for all a the atomic prop osition cannot b e satis ed b y a letter a By Corollary w e ha v e L j if and only if h L j h R So what w e do is to replace all o ccurences of the atomic prop osition in R A NONHOMOMORPHIC MAPPING b y f al se tr ue and sho w that the resulting form ula that w e designate R is equiv alen t to The b o olean subform ulae of are replaced b y U T in R So no w they b b ha v e to b e replaced b y f al se U T whic h is considering the next paragraph b equiv alen t to replacing them b y b The purely temp oral subform ulae of are replaced b y T in R In T t t t the atomic prop osition only o ccurs as an op erand of b o olean negated as an op erand of b o olean and at the left hand side of the un til op erator U Therefore if w e replace b y f al se in T the resulting form ula is equiv alen t to t t Because the b o olean connectiv es that com bine the subform ulae are not c hanged in R compared to w e obtain R is equiv alen t to Corollary L et h b e an abstr acting homomorphism such that for al l a h a L et b e a PL TL formula in normalform and let L b e a pr e x close d r e gular language Then l im h L j if and only if l im L j h Pro of Because f inite w e ha v e according to Corollary and h h Corollary h R By Corollary R is equiv alen t h to with resp ect to Hence h So if l im L h h h then h l im L By Lemma w e obtain l im h L Therefore l im L j implies l im h L j h By Corollary w e ha v e l im h L j implies l im L j R R is h de ned as R f inite By Corollary R is equiv alen t to Because h for all a h a f inite can nev er b e satis ed b y an w ord in l im L R h is equiv alen t to Therefore l im h L j implies l im L j h A Nonhomomorphic Mapping In this section w e de ne a t yp e of mapping on subsets of that is an extension of abstracting homomorphisms W e sho w that these mappings preserv e PL TL form ulae su cien tly ev en if the underlying homomorphism is erasing This means w e will not regard the f inite part in the construction of R considering R is su cien t h CHAPTER PL TL AND ABSTRA CTION The mapping that w e de ne is unfortunately not as easy to handle as abstraction homomorphisms Let h b e an alphab etic homomorphism the nitary part of an abstraction f g homomorphism Let L Based on h w e de ne a mapping H that preserv es information ab out w ords w L that ha v e an in nite con tin uation in l im L that is completely tak en to b y h h De nition L et f such that h f L fw L j x c ont w l im L h pr e x f gg f g L et H such that h H L h L h f L f g T o op erate on languages w e de ne a mapping on w ords corresp onding to H De nition L et x We de ne H f g If h x is de ne d then H x h x Otherwise H x max h pr e x W e should notice that H L is a regular language or a regular language if L is a regular language or a regular language resp ectiv ely Lemma L et h b e an abstr acting homomorphism let L b e a pr e x close d r e gular language and let H b e the mapping c orr esp onding to h as de ne d ab ove Then H l im L l im H L h Pro of Let L L f L f g Let h f g f g b e an abstracting homomorphism suc h that h a h a for all a and h h An automaton accepting f L can b e constructed in the follo wing w a y Mark all states in an automaton accepting L from whic h a lo op con taining an accepting state is reac hable suc h that all transition lab els of the lo op as w ell as all transition lab els on the path to the lo op are tak en to b y h Mak e the mark ed states the only accepting states of the automaton Then the automaton h accepts f L A NONHOMOMORPHIC MAPPING Then h L H L and h l im L H l im L Because L is a pre x closed reg ular language L is a pre x closed regular language According to Lemma h l im L l im h L and therefore H l im L l im H L W e ha v e de ned H in suc h a w a y that if is a letter in an w ord in l im H L then all subsequen t letters are also W e extend the de nition of PL TL form ulae in normalform to t to w ords in l im H L De nition L et b e an alphab et We say that a PL TL formula is in extende d normalform if and only if it is in ne gation normalform f g is its set of atomic pr op ositions and it c ontains the atomic pr op osition only in the form G We evaluate PL TL formulae in extende d normalform using the extende d f g lab el ling function f g We de ne a fag for al l a and f g The extended normalform of PL TL form ulae corresp onds to our de nition of l im H L app ears only in in nite su xes and represen ts in nite su xes of an original computation that h tak es to Lemma L et h b e an abstr acting homomorphism L et L b e a pr e x close d r e gular language L et b e a PL TL formula in extende d normalform Then l im H L j if and only if l im L j R h Pro of Let x l im L If h x is de ned then H x h x l im H L By Corollary w e ha v e x j R if and only if H x j h If h x is unde ned then H x w where w max h pr e x Let w b e the smallest w ord in pr e x suc h that h w w Let h f g f g suc h that h a h a for all a and h Then h w H x Let b e except that the atomic prop osition is substituted b y the atomic prop osition Then is in f g normalform By de nition of extended normalform w e ha v e z j if and only if z j for all z f g f g If w e regard Corollary and h w H x then w j R if and h only if H x j By de nition of w and R w j R if and f g h only if x j R W e obtain x j R if and only if H x j h h W e ha v e for all x l im L x j R if and only if H x j Therefore h l im L j R if and only if H l im L j According to Lemma h CHAPTER PL TL AND ABSTRA CTION H l im L j if and only if l im H L j and w e nally obtain l im L j R if and only if l im H L j h If L is not a pre x closed regular language then w e only ha v e l im L j R h if l im H L j Hence the essen tially imp ortan t condition for the v alidit y of Lemma is l im L H H l im L W e use Lemma to establish a metho d for the v eri cation of PL TL prop erties under homomorphic abstractions suc h that prop erties are su cien tly preserv ed Corollary L et L b e a pr e x close d r e gular language let h b e an abstr action homomorphism and let b e a PL TL formula in extende d normalform L et Then l im h L f g j implies l im L j R h Pro of Let W e notice that if l im L f g satis es a PL TL prop ert y then l im L do es to o If w e extend h in suc h a w a y that it hides then the corresp onding H L f g as de ned in De nition is equal to h L f g W e ha v e simply extended eac h partial computation in L b y arbitrarily man y actions that are hidden under the abstraction Regarding Lemma if l im h L f g j for some PL TL form ula in extended normalform then l im L f g and th us l im L satis es R with re sp ect to h This corollary is v ery useful in practice W e presen t its application in the example c hapter Chapter where w e use the follo wing terminology De nition We c al l l im L f g the extension of l im L Brief Summary of the Chapter W e pro v ed some preserv ation results for PL TL form ulae with resp ect to abstraction F or this purp ose w e de ned a syn tactical transformation R on PL TL form ulae and extended it to a syn tactical transformation R R tak es care of sub w ords that an The con v erse of this result do es not hold F or instance l im a b a a satis es F a If h is the iden tit y function on a and b then l im h a b a a b a do es not satisfy R F a F a b ecause b is in l im h a b a BRIEF SUMMAR Y OF THE CHAPTER abstraction homomorphism ma y map on the empt y w ord The mapping R in addition handles w ords that are hidden b y the abstraction Corollary sa ys that homomorphic abstractions in general preserv e PL TL form ulae only w eakly Prohibiting the abstraction homomorphism to hide actions establishes a strong preserv ation result for PL TL Corollary Giving up the demand that the abstraction mapping has to b e a language homomorphism al lo ws PL TL form ulae to b e su cien tly preserv ed ev en when action hiding is allo w ed Lemma Regarding the results of this c hapter PL TL prop erties with linear satisfaction re lation form a prop ert y class that do es not pro vide a to o satisfactory basis for v eri cation using b eha viour abstraction The results for homomorphic abstraction are not go o d as long as action hiding is allo w ed Without action hiding the decreasing p o w er i e reduction of the state space of abstraction tec hniques su ers If w e try to balance b et w een action hiding and su cien t preserv ation w e ha v e to in tro duce a dumm y action that disallo ws the abstraction mapping from hiding to o m uc h The resulting mapping is not a language homomorphism an ymore and is th us not as easy to handle as language homomorphisms Nev ertheless it rev eals the most applicable abstraction tec hnique for the v eri cation of PL TL form ulae on abstractions The most useful result is Corollary extending eac h partial b eha viour of a ho momorphic abstraction b y arbitrary dumm y actions establishes a su cien t preser v ation result The only dra wbac k is that w e ha v e only an implication and not an if and only if condition in Corollary CHAPTER PL TL AND ABSTRA CTION Chapter Relativ e Liv eness W e de ne r elative liveness pr op erties of a co op erating system in this c hapter Rel ativ e liv eness prop erties are liv eness prop erties with resp ect to a b eha viour If is the b eha viour then a relativ e liv eness prop ert y with resp ect to b ecomes an unconditional liv eness prop ert y as de ned in AS In addition to relativ e liv eness prop erties w e de ne as their dual prop erties r elative safety pr op erties T o sho w decidabilit y of regular relativ e liv eness and relativ e safet y prop erties and to c haracterize the t w o prop ert y classes precisely w e giv e alternativ e set inclusion de nitions and c haracterize them top ologically Satisfaction of relativ e liv eness prop erties is related to satisfaction of linear prop erties b y all reasonable computations of a system Here reasonable is related to fairness W e will pro v e relativ e liv eness prop erties to establish linear satisfaction under strong fairness F ra if p ossibly state information is added F or relativ e liv eness prop erties w e sho w ho w to v erify them on abstractions of a system s b eha viour In this con text w e ha v e to b e cautious with resp ect to the question what t yp e of homomorphic abstraction preserv es relativ e liv eness prop erties su cien tly W e pro v e homomorphisms that are simple on the b eha viour Oc h Oc h b to b e a suitable basis for the v eri cation of relativ e liv eness prop erties on abstractions W e de ne relativ e liv eness as a satisfaction relation for prop erties Relativ e liv e ness is also called mac hine closure AL AL AH or appro ximate satisfaction NO a NO a NO b In the con text of real time systems relativ e liv eness and safet y prop erties are studied in Hen F or co op erating systems systems consisting of at least t w o in teracting comp onen ts linear prop erties without fairness constrain ts can b e to o strict for v eri cation pur CHAPTER RELA TIVE LIVENESS p oses correct systems can b e considered incorrect The author prop oses that rela tiv e liv eness prop erties are suitable for the v eri cation of co op erating systems T o motiv ate this prop osition w e start with a small example A Motiv ating Example Figure sho ws a small but t ypical example of a co op erating system It is sp eci ed b y a P etri net P et Rei The system is a serv er that after ha ving receiv ed a r eq uest can send a r esul t or a r ej ection to its clien t dep ending on the a v ailabilit y of a resource f r ee or l ock If the resource is free when needed y es the serv er will send a r esul t Un til the result is sen t the resource is seized b y the serv er If the resource is lo c k ed when needed no the serv er will resp ond r ej ect result yes request lock free reject no Figure An example system The b eha viour of the system is represen ted b y the nite state system in Figure the reac habilit y graph of the P etri net In all subsequen t gures of this c hapter the initial state of a nite state system is shaded grey The nite state system in Fig ure do es not satisfy the prop ert y represen ted b y the PL TL form ula G F r esul t a result is in nitely often pro duced W e notice that G F r esul t is a t ypical liv eness prop ert y F or example l ock r eq uest no r ej ect is a computation of the example system that do es not satisfy G F r esul t Nev ertheless one w ould regard the example system in tuitiv ely as b eing correct in regard to G F r esul t since all reasonable computations of the system satisfy the prop ert y Here the term reasonable is related to fairness F ra Belo w reasonable can b e read as fair without determining a concrete fairness concept W e w eak en the de nition of linear satisfaction of a prop ert y a prop ert y is a relativ e liv eness prop ert y of a system s b eha viour if all partial i e nite computations can b e extended to a complete in nite one suc h that the whole computation satis es the prop ert y According to this informal de nition G F r esul t is a relativ e liv eness prop ert y of Figure A MOTIV A TING EXAMPLE no reject request lock lock lock free free free reject request result yes Figure The example system s b eha viour Figure sho ws a nite state system describing the b eha viour of a system that is similar to Figure but con tains an error In con trast to Figure in Figure if the resource is lo c k ed there is no p ossibilit y to free it again A request th us nev er receiv es a result W e in tro duce another di erence compared to Figure if the resource is a v ailable then additionally there is a p ossibilit y to reject a request The second di erence is in tro duced to rev eal di culties that can arise in the con text of b eha viour abstraction reject no request lock lock request result, yes reject Figure An example system with an error In Figure not all reasonable computations satisfy G F r esul t if the resource is lo c k ed there is no p ossibilit y an ymore to send a result ev en tually Hence G F r esul t can nev er b e satis ed for a partial computation that con tains the action l ock So there exist reasonable computations of the nite state system in Figure that do not satisfy G F r esul t And indeed G F r esul t is not a relativ e liv eness prop ert y of the nite state system in Figure The considered examples should ha v e giv en a a v our what ma y mak e the v eri cation of co op erating systems di cult In general w e ha v e no con trol of the system in suc h a w a y that w e can guaran tee that one comp onen t of the system is in a particular state when needed b y another com p onen t to pro duce a result A t ypical example is a telephone system no one can CHAPTER RELA TIVE LIVENESS guaran tee that whenev er I w an t to call someone he or she will b e there Nev erthe less the telephone system will not necessarily b e incorrect if I nev er reac h him or her Ignoring suc h extreme scenarios is exactly the purp ose of considering relativ e liv eness prop erties only reasonable parts of a b eha viour are tak en in to accoun t If w e only ask for the p ossible resp onses to a request w e do not tak e in to consid eration the actions y es no l ock and f r ee in our example system Not considering particular actions is exactly b eha viour abstraction F or Figure a suitable ab straction homomorphism tak es y es no l ock and f r ee to the empt y w ord hiding of actions and lea v es r eq uest r esul t and r ej ect unc hanged Application of this homomorphism to the nite state system of Figure giv es us the minim al nite state system in Figure that represen ts the resulting abstract b eha viour of the system in Figure result request reject Figure The abstract b eha viour of the example system G F r esul t is a relativ e liv eness prop ert y of the abstract b eha viour Figure as w ell as of the original b eha viour Figure So in this case the relativ e liv eness prop ert y is pr eserve d b y the abstraction the prop ert y of the original b eha viour corresp onds to the prop ert y of the abstraction with resp ect to the abstracting ho momorphism If w e apply the same homomorphism to the nite state system in Figure w e also obtain Figure represen ting the abstract b eha viour Here the relativ e liv e ness prop ert y G F r esul t is not preserv ed b y the abstraction b ecause the b eha viour represen ted b y Figure do es not satisfy G F r esul t Hence w e nd that relativ e liv eness prop erties are delicate to handle with resp ect to their preserv ation b y ab stractions W e presen t a condition in this c hapter that ensures that an abstraction su cien tly preserv es relativ e liv eness prop erties the simplicity of the abstracting homomorphism Oc h Oc h b on the b eha viour RELA TIVE SAFETY AND LIVENESS Relativ e Safet y and Liv eness In this section w e de ne relativ e liv eness prop erties of an language As their dual prop erties w e de ne relativ e safet y prop erties Let L b e an language represen ting the b eha viour of a system and let P b e a prop ert y De nition We c al l the pr op erty P a r elative liveness pr op erty of L written L j P if and only if w pr e L x c ont w L w x P RL AP F or a PL TL formula and a lab el ling function we write L j RL if is a r elative liveness pr op erty of L Thus L j if and only if w RL pr e L x c ont w L w x j De nition We c al l the pr op erty P a r elative safety pr op erty of L if and only if x L x P w pr e x z c ont w L w z P Note If L then the de nitions of r elative liveness and r elative safety ar e e quivalent to the de nitions of liveness and safety in AS se e De nition and De nition Alternativ e Characterizations T o pro v e relativ e liv eness and safet y to b e decidable for regular languages w e giv e alternativ e set inclusion c haracterizations of relativ e liv eness and safet y Lemma P is a r elative liveness pr op erty of L if and only if pr e L pr e L P Pro of By de nition L j P if and only if for all w pr e L there exists RL x c ont w L suc h that w x P Hence w e ha v e w pr e L P for all w pr e L This is equiv alen t to pr e L pr e L P On the other hand pr e L P pr e L and th us pr e L pr e L P If pr e L pr e L P then w pr e L P for all w pr e L Therefore for all w pr e L there exists an x c ont w L suc h that w x P and hence P is a relativ e liv eness prop ert y of L CHAPTER RELA TIVE LIVENESS Lemma P is a r elative safety pr op erty of L if and only if L l im pr e L P P Pro of By de nition P is a relativ e safet y prop ert y of L if and only if x L x P w pr e x z c ont w L w z P By taking the coun terp ositiv e of the implication this is equiv alen t to x L w pr e x z c ont w L w z P x P The part w pr e x z c ont w L w z P is equiv alen t to the condition pr e x pr e L P Th us P is a relativ e safet y prop ert y of L if and only if x L pr e x pr e L P x P All w ords x in L suc h that pr e x pr e L P can b e represen ted b y the set L l im pr e L P Th us P is a relativ e safet y prop ert y of L if and only if L l im pr e L P P Corollary It is de cidable whether P is a r elative liveness pr op erty or a r el ative safety pr op erty of a r e gular language L if P is a r e gular language or a pr op erty describ e d by some PL TL formula Pro of The c haracterizations giv en b y Lemma and Lemma are decidable problems for regular sets and regular languages resp ectiv ely Eil Har HU Tho AP F or all PL TL form ulae and lab elling functions is a regular language c hec king whether a B uc hi automaton and a PL TL form ula describ e the same prop ert y is a PSP A CE complete problem VW WVS W ol Similar to safet y and liv eness prop erties in AS a linear prop ert y of L can b e partitioned in to a relativ e safet y and a relativ e liv eness part Corollary L P if and only if P is a r elative safety pr op erty of L and P is a r elative liveness pr op erty of L Pro of If P is a prop ert y satis ed in L L P then ob viously P is a relativ e safet y and a relativ e liv eness prop ert y of L AL TERNA TIVE CHARA CTERIZA TIONS If P is a relativ e safet y prop ert y of L then L l im pr e L P P Lemma If additionally P is a relativ e liv eness prop ert y of L then b y Lemma pr e L pr e L P Therefore w e can replace pr e L P b y pr e L in the safet y condition and obtain L l im pr e L P Because L l im pr e L L w e nally obtain L P T o c haracterize relativ e liv eness and relativ e safet y more precisely w e sho w ho w to em b ed them in to the Can tor top ology i e the top ological space o v er compatible with the follo wing metric Eil F or top ological notions see Kel De nition L et common x y designate the longest c ommon pr e x of two wor ds x and y in We de ne the metric d x y by x y x y d x y jcommon x y j x d x x Lemma P is a r elative liveness pr op erty of L if and only if L P is a dense set in L Pro of Let L j P and let x L Then pr e L pr e L P Th us pr e x RL pr e L P and w e ha v e w pr e x y L P w pr e y W e get for all x L and all is related to that there is a y L P suc h that jw j d x y So L P is a dense set in L Let L P b e a dense set in L Then for all x L and all there exists y L P suc h that d x y Let x b e in L let w b e in pr e x and let Because L P is a dense set in L there exists y L P suc h that jw j w pr e y Th us pr e L pr e L P Because pr e L P pr e L w e ha v e pr e L pr e L P By Lemma P is a relativ e liv eness prop ert y of L Lemma P is a r elative safety pr op erty of L if and only if L P is a close d set in L Pro of P is a relativ e safet y prop ert y of L if and only if x L x P w pr e x z c ont w L w z P If P is the complemen t of P with resp ect to L i e P L n P whic h is equiv alen t to P L n L P then P is a relativ e safet y prop ert y of L if and CHAPTER RELA TIVE LIVENESS only if x L x P w pr e x z c ont w L w z P If w e de ne this condition top ologically then P is a relativ e safet y prop ert y of L if and only if x P y L d x y y P Th us P is a relativ e safet y prop ert y of L if and only if P is an op en set in L Because P L n L P is the complemen t of L P with resp ect to L w e nally obtain that P is a relativ e safet y prop ert y of L if and only if L P is a closed set in L T o round things o w e also presen t the v ery close relation b et w een relativ e liv eness and mac hine closure De nition L et L The p air L is c al le d machine close d AL AL AH if and only if pr e L pr e Note A c c or ding to L emma P is a r elative liveness pr op erty of L if and only if L L P is machine close d Relativ e Liv eness and F airness As men tioned in the in tro duction of this c hapter from an in tuitiv e p oin t of view rel ativ e liv eness and satisfaction of prop erties under fairness F ra MP are closely related But relativ e liv eness can di er from usual fairness concepts F or example not all strongly fair w ords in the minim al automaton represen tation of fa bg satisfy F a X a e g a b do es not but F a X a is a relativ e liv eness prop ert y of fa bg What w e can sho w is that w e can alw a ys nd a nite state implem en tati on of a regular b eha viour suc h that all strongly fair computations of the implem en tati on satisfy the prop ert y De nition L et A Q q F b e a nite automaton A run r Q of A is str ongly fair on x if and only if for al l q r if q a q then i I N r q x a r q A tr ansition that is in nitely often i i i p ossible is in nitely often taken A c omputation x is a str ongly fair c omputation of A if and only if ther e exists an ac c epting str ongly fair run of A on x Lemma L et L b e a pr e x close d r e gular language and let P b e an r e gular pr op erty such that l im L j P Then ther e exists a nite state system A RL ac c epting l im L such that al l str ongly fair c omputations of A satisfy P RELA TIVE LIVENESS AND ABSTRA CTION Pro of If P is a relativ e liv eness prop ert y of l im L then b y Lemma pr e l im L pr e l im L P Because L is a pre x closed regular language l im L l im pr e l im L W e construct a reduced B uc hi automaton accepting l im L P Eil Tho Here reduced means that there are no states from whic h no w ord can b e accepted and all states are reac hable from the initial state Let A b e the nite state system obtained from this B uc hi automaton b y making all states accepting states A accepts l im L Additionally b y de nition of a strongly fair run all strongly fair computations of A meet in nitely often a state that w as a former accepting state in the B uc hi automaton for l im L P Therefore all strongly fair computations are in l im L P and th us satisfy P Unfortunately A can b e m uc h larger than the minim al nite state system accepting l im L and th us is an incon v enien t represen tation of l im L Therefore relativ e liv eness ma y b e regarded as a t yp e of fairness condition that allo ws a more compact represen tation of a system s b eha viour Relativ e Liv eness and Abstraction Let L b e a pre x closed regular language let h b e an abstracting homomorphism and let b e a PL TL form ula in normalform W e sho w in this section a preserv ation theorem for relativ e liv eness prop erties if h satis es a condition that w e call simplicity on L see De nition then l im h L j RL if and only if l im L j R h RL Our goal is to pro v e relativ e liv eness prop erties of the b eha viour l im L of a system b y considering only the abstract b eha viour l im h L More sp eci cally w e are in terested in the preserv ation of relativ e liv eness prop erties under the abstraction homomorphism Essen tial information ab out the relativ e liv eness prop erties of l im L is con tained in the sets c ont w L for w L A t the abstract lev el w e ob viously ha v e ac cess to c ont h w h L but w e really need h c ont w L in order to b e able to establish relativ e liv eness prop erties that will also hold at the concrete system lev el Th us w e ha v e to in v estigate the relation b et w een the sets h c ont w L and c ont h w h L and nd conditions under whic h c ont h w h L can b e used instead of h c ont w L In general h c ont w L is a prop er subset of c ont h w h L In order to ob In general the size of this nite state system is giv en b y the pro duct of the sizes of the b eha viour nite state system and the prop ert y automaton CHAPTER RELA TIVE LIVENESS tain su cien t information ab out h c ont w L from c ont h w h L one w ould b e tempted to require equalit y of the t w o sets Ho w ev er this is stronger than needed Indeed since w e are dealing with relativ e liv eness prop erties it is su cien t that c ont h w h L ev en tually coincides with h c ont w L This condition is the one called simplicity of an abstraction homomorphism in Oc h Oc h b Its pre cise de nition is as follo ws De nition A n abstr acting homomorphism h is c al le d simple in a wor d w L on a language L if and only if ther e exists a u c ont h w h L such that c ont u c ont h w h L c ont u h c ont w L h is c al le d simple on L if and only if it is simple in al l wor ds w L on L Theorem will sho w that this de nition indeed meets all the requiremen ts w e ha v e informally describ ed ab o v e More details ab out simple homomorphisms can b e found in Oc h Oc h b where a n um b er of su cien t conditions for simplicit y of a homomorphism are listed since deciding simplicit y in general is a complex task Theorem L et L b e a pr e x close d r e gular language let h b e an abstr acting homomorphism such that h is simple on L and h L do es not c ontain maximal wor ds and let b e a PL TL formula in normalform Then l im h L j implies l im L j R h RL RL Pro of Because h is simple on L there exists for all u L a v c ont h u h L suc h that c ont v h c ont u L c ont v c ont h u h L c ont h u v h L Let u L and let v c ont h u h L suc h that Condition is satis ed W e as sume that l im h L j and will deriv e that l im L j R By de nition h RL RL l im h L j if and only if RL r pr e l im h L s c ont r l im h L r s j If w e replace in particular r b y h u v whic h is in pr e l im h L b ecause h L do es not con tain maximal w ords then w e obtain that there exists an w ord y c ont h u v l im h L l im c ont h u v h L suc h that h u v y j w L is a maxim al w ord in L if and only if c ont w L f g RELA TIVE LIVENESS AND ABSTRA CTION According to Condition y l im c ont h u v h L is equiv alen t to y l im c ont v h c ont u L c ont v l im h c ont u L Th us w e kno w that v y is in l im h c ont u L whic h is b y Lemma equiv alen t to v y h l im c ont u L So there exists an x l im c ont u L suc h that h x v y W e set z v y and summarize for all u L there exists an x l im c ont u L and a z c ont h u l im h L suc h that h x z b y Condition and h u z j b y Condition According to Corollary w e obtain ux j R W e ha v e for all u L there exists an x c ont u l im L h suc h that ux j R Th us l im L j R h h RL As p oin ted out b y means of the example in the in tro duction of this c hapter Theo rem do es not hold if w e do not restrict the abstracting homomorphism to b e simple Theorem L et L b e a pr e x close d r e gular language L et h b e an abstr acting homomorphism such that h L do es not c ontain maximal wor ds L et b e a PL TL formula in normalform Then l im L j R implies l im h L j h RL RL Pro of W e assume l im L j R and sho w l im h L j Let w h RL RL pr e l im h L let w pr e l im L h w and let x c ont w l im L suc h that w x j R h If h w x is de ned then b y Corollary h w x j Therefore there exists an x h x c ont w l im h L suc h that w x j If h w x is unde ned then there is a pre x v of w x suc h that h c ont v pr e w x f g In fact there are in nitely man y of these pre xes v Then b y de nition of R and w e ha v e for all y that v y j R h h If there exists a y suc h that h y c ont h v l im h L then let x b e the only w ord in c ont w fh v y g x is in c ont w l im h L According to Corollary w x j If there exists no y suc h that h y c ont h v l im h L then h L con tains maximal w ords whic h con tradicts the theorem s preconditions CHAPTER RELA TIVE LIVENESS So for all w pr e l im h L there exists an x c ont w l im h L suc h that w x j Th us l im h L j RL Corollary L et L b e a pr e x close d r e gular language let h b e an abstr acting homomorphism such that h is simple on L and h L do es not c ontain maximal wor ds and let b e a PL TL formula in normalform Then l im h L j if and only if l im L j R h RL RL Pro of This corollary is a summary of Theorem and Theorem Impro ving the Results If a language L con tains maximal w ords i e w ords that ha v e no con tin uation in L then l im L con tains no information ab out them if w is a maximal w ord in L then w pr e l im L T o a v oid this loss of information w e extend maximal w ords b y dumm y l etters F ormally w e de ne the satisfaction of relativ e liv eness prop erties on L itself instead on l im L De nition L et L L et We de ne the set of maximal wor ds of L to b e max L fw L j c ont w L f gg We de ne the extension of L to b e xtd L L max L f g If L is a regular language then the construction of an automaton accepting xtd L is easy for all accepting states in a reduced automaton accepting L that ha v e no outgoing transition add a self lo op lab elled with to that state Then the resulting automaton accepts xtd L AP De nition L et L let b e a PL TL formula and let b e a lab el ling function is a r elative liveness pr op erty of L with r esp e ct to written L j if and only if l im xtd L j RL RL AP De nition L et b e a lab el ling function for an alphab et and a set of atomic pr op ositions AP AP f g We de ne the extension of to b e the function f g such that a a for al l a and f g IMPR O VING THE RESUL TS AP f g We de ne the extension of to b e the function f g such that a a for al l a and f g Recall that for an alphab et the extended lab elling function is already de ned in De nition Corollary L et h b e an abstr acting homomorphism that is simple on the pr e x close d r e gular language L L et b e a PL TL formula in extende d normalform se e De nition Then L j R if and only if h L j h RL RL Pro of Let the extension of L with resp ect to empt y abstract su xes b e the language xtd L L fw L j h c ont w L f gg f g h Let h f g f g b e the abstracting homomorphism de ned b y h a h a for all a and h Because h is simple on L h is simple on xtd L and h xtd L xtd h L The latter equalit y holds b ecause the sim h h plicit y of h on L implies for all w L c ont h w h L f g if h c ont w L f g Oc h Because h xtd L xtd h L h xtd L do es not con tain maximal h h w ords Let b e the PL TL form ula that w e obtain b y replacing the atomic prop osition in b y a new atomic prop osition W e ha v e l im h xtd L j if and only if l im h xtd L j h h RL RL l im xtd L j R if and only if l im xtd L j R and h h h RL RL l im xtd L j R if and only if l im xtd L j R h h h h RL RL Additionally b y Corollary w e ha v e l im h xtd L j if and only if h RL l im xtd L j R According to the ab o v e established equiv alences w e h h RL nally obtain L j R if and only if h L j h RL RL By this result w e can sho w that simplicit y of a homomorphism on a b eha viour is not only a su cien t but also a necessary condition of an abstraction to preserv e su cien tly all relativ e liv eness prop erties of the b eha viour NO a NO a NO b W e pro v e this relation in App endix A CHAPTER RELA TIVE LIVENESS Ev en tualit y Prop erties There exists another class of prop erties that w e call eventuality pr op erties that is pratically imp ortan t Their de nition is closely related to the de nition of relativ e liv eness prop erties On the logical lev el ev en tualit y prop erties are de ned b y a fragmen t of the ful l c omputation tr e e lo gic CTL CE CES Tho that w e call the AG E F fragmen t of CTL Nit c Nit b The name of this sub class of CTL comes from the fact that all AG E F form ulae ha v e the structure AG E F for some PL TL form ula Instead of de ning the seman tics of ev en tualit y prop erties on the basis of CTL s seman tics w e giv e their de nition as concisely as p ossible Then w e sho w that for ev en tualit y prop erties w e can establish exactly the same preserv ation results as for relativ e liv eness prop erties The exact relation b et w een ev en tualit y prop erties and the AG E F fragmen t of CTL is presen ted in App endix B In practice one is often in terested to pro v e a condition lik e whatev er has happ ened b efore the system should b e able ev en tually to meet some requiremen ts W e formalize this t yp e of condition b y the notion of ev en tualit y prop erties AP De nition L et b e a PL TL formula and let b e a lab el ling function We say that is an eventuality pr op erty of a system s b ehaviour L with r esp e ct to written L j if and only if E V w pr e L x c ont w L x j F F or the relation of ev en tualit y prop erties to relativ e liv eness prop erties w e can mak e the follo wing observ ations F is a relativ e liv eness prop ert y of L if is an ev en tualit y prop ert y of L and is an ev en tualit y prop ert y of L if G F is a relativ e liv eness prop ert y of L L j G F L j L j F RL E V RL One ma y conjecture that for the rst implication an if and only if condition ma y hold L j L j G F Indeed the author to o assumed this for some E V RL time But there is a sligh t di erence b et w een b eing an ev en tualit y prop ert y and G F b eing a relativ e liv eness prop ert y of L This di erence is rev ealed b y considering as an example the PL TL form ula a X G a Let L b e fa bg The Ev en tualit y prop erties are also considered as a practically relev an t prop ert y class in KV where they are called always p ossibly pr op erties EVENTUALITY PR OPER TIES prop ert y a X G a is an ev en tualit y prop ert y of fa bg but G F a X G a is not a relativ e liv eness prop ert y of this language Therefore L j G F L j L j F RL E V RL If quan ti es only o v er a nite pre x of an w ord satisfying i e if x j x then there exists w pr e x suc h that w j then the if and only if condition is established F or ev en tualit y prop erties w e can establish a result corresp onding to Theorem for relativ e liv eness prop erties Theorem L et L b e a pr e x close d r e gular language let h b e an abstr acting homomorphism such that h is simple on L and h L do es not c ontain maximal wor ds and let b e a PL TL formula in normalform Then l im h L j implies l im L j R h E V E V The pro of of this theorem is more or less iden tical to that of Theorem Pro of Because h is simple on L there exists for all u L a v c ont h u h L suc h that c ont v h c ont u L c ont v c ont h u h L c ont h u v h L Let u L and let v c ont h u h L suc h that Condition is satis ed W e assume that l im h L j and will deriv e that l im L j R By h E V E V de nition l im h L j if and only if E V r pr e l im h L s c ont r l im h L s j F If w e replace in particular r b y h u v whic h is in pr e l im h L b ecause h L do es not con tain maximal w ords then w e obtain that there exists an w ord y c ont h u v l im h L l im c ont h u v h L suc h that a X G a is a satis able PL TL form ula but G F a X G a is a con tradiction CHAPTER RELA TIVE LIVENESS y j F and therefore v y j F By Condition y l im c ont h u v h L is equiv alen t to y l im c ont v h c ont u L c ont v l im h c ont u L Th us w e kno w that v y is in l im h c ont u L whic h is according to Lemma equiv alen t to v y h l im c ont u L So there exists an x l im c ont u L suc h that h x v y W e set z v y and summarize for all u L there exists an x l im c ont u L and a z c ont h u l im h L suc h that h x z b y Condition and z j F b y Condition According to Corollary w e obtain x j h R F whic h implies x j F R W e ha v e for all u L there ex h ists an x c ont u l im L suc h that x j F R Th us w e nally obtain h l im L j R h E V Theorem L et L b e a pr e x close d r e gular language let h b e an abstr acting homomorphism such that h L do es not c ontain maximal wor ds and let b e a PL TL formula in normalform Then l im L j R implies l im h L j h E V E V The pro of of Theorem is nearly iden tical to the pro of of Theorem Pro of W e assume l im L j R and sho w l im h L j Let w h E V E V pr e l im h L let w pr e l im L h w and let x c ont w l im L suc h that x j F R Let z b e the su x of x suc h that z j R and u the h h pre x of x leading to this su x i e x uz If h z is de ned then b y Corollary h z j Therefore there exists an x h x c ont w l im h L suc h that x j F If h z is unde ned then there is a pre x v of z suc h that h c ont v pr e z f g Then b y de nition of R and w e ha v e for all y that v y j R h h If there exists a y suc h that h y c ont h w uv l im h L then let z b e the only w ord in c ont w h u fh v y g z is in c ont w h u l im h L BRIEF SUMMAR Y OF THE CHAPTER According to Corollary z j Therefore there exists an x h u z c ont w l im h L suc h that x j F If there exists no y suc h that h y c ont h w uv l im h L then h L con tains maximal w ords whic h con tradicts the theorem s preconditions So for all w pr e l im h L there exists an x c ont w l im h L suc h that x j F Th us l im h L j E V Corollary L et L b e a pr e x close d r e gular language let h b e an abstr acting homomorphism such that h is simple on L and h L do es not c ontain maximal wor ds and let b e a PL TL formula in normalform Then l im h L j if and only if l im L j R h E V E V Pro of The corollary is a summary of Theorem and Theorem Again as for relativ e liv eness prop erties this result can b e extended to h L con taining maximal w ords if w e add arbitrarily man y dumm y actions to maximal partial computations W e omit rep eating this ob vious construction here In fact the construction is not v ery helpful for ev en tualit y prop erties If h L con tains maximal w ords and w e extend them b y f g then eac h ev en tualit y prop ert y of xtd h L m ust b e the disjunction of the PL TL form ula of main in terest and another PL TL form ula lik e G This latter part is necessary b ecause for all w max h L c ont w xtd h L f g and l im f g ev en tually satis es nothing else but G for example So ev en when making the construction an ev en tualit y prop ert y satis ed for the extension of a b eha viour do es not rev eal information ab out maximal partial computations in the b eha viour Brief Summary of the Chapter W e ha v e de ned relativ e liv eness prop erties of a b eha viour They establish a satisfac tion relation for prop erties di ering from linear satisfaction The satisfaction relation is strongly related to satisfaction of prop erties under fairness W e pro v ed explicitly if an regular prop ert y is a relativ e liv eness prop ert y of a deterministic regular b eha viour then there exists a nite state impleme n tation of the b eha viour suc h that all strongly fair computations satisfy the prop ert y linearly see Lemma Relativ e liv eness prop erties are liv eness prop erties relativ e to a system s b eha viour In addition w e ha v e de ned their dual relativ e safet y prop erties F or b oth prop ert y CHAPTER RELA TIVE LIVENESS classes w e ga v e set inclusion and top ological c haracterizations establishing decidabil it y results Section F or relativ e liv eness prop erties w e sho w ed that they are su cien tly preserv ed b y abstraction homomorphisms that are simple on the b eha viour Corollary and Corollary W e de ned another class of prop erties that are closely related to relativ e liv eness prop erties ev en tualit y prop erties If a prop ert y is an ev en tualit y prop ert y of a system s b eha viour then it is alw a ys p ossible to satisfy the prop ert y ev en tually Ev en tualit y prop erties can b e c haracterized in the A G E F fragmen t of CTL see App endix B W e pro v ed preserv ation results for ev en tualit y prop erties that are similar to the ones for relativ e liv eness prop erties Chapter Examples In this c hapter w e apply the v eri cation metho ds that w e ha v e dev elop ed in the pre vious c hapters to three di eren t examples of co op erating systems F or v erifying the example systems esp ecially for computing abstractions the Pro duct Net Mac hine Oc h as w ell as the SH V eri cation T o ol NOR w as used The rst example that w e consider demonstrates the p ossible amoun t of state space reduction that w e can ac hiev e b y the application of homomorphic abstractions In the second example w e deal with the detection of undesired in teractions in in telligen t net w orks IN CPR P SCORE This second example is presen ted in full detail including all sp eci cations of the system s comp onen ts W e rev eal a service in teraction b et w een t w o in v estigated services c al l forwar ding unc onditional and sele ctive c al l r eje ction In the third example w e c hec k a sp eci cation of the b asic c al l state mo del BCSM c ap ability set CS for conformance with its de nition in the standards Q xx esp ecially Q Statemen ts ab out the satisfaction of temp oral logic form ulae are in this c hapter alw a ys made with resp ect to the appropriate lab elling functions State Space Reduction Example In this section w e lo ok at an example of a co op erating system in Oc h a that b y in v olving sev eral iden tical transp ort media can gro w arbitrarily large The system is a framew ork for an idealized comm unic ation proto col for the establishmen t and release of a connection for data transmission In Oc h a prop erties of the proto col are v eri ed b y constructing formal language theoretic pro ofs System abstractions are de ned there b y simple homomorphisms Th us w e can apply en tirely the meth o ds w e ha v e dev elop ed in this thesis W e c hec k the same prop erties as in Oc h a CHAPTER EXAMPLES using the preserv ation results that w e ha v e established in previous c hapters instead of constructing pro ofs as done in Oc h a The Proto col The purp ose of the comm unic ation proto col that w e in v estigate is the establishmen t and release of a data connection data phase in a con trolled manner The system the proto col is designed for is presen ted sc hematically in Figure AT TB A T B TA BT Figure The comp onen ts of the system The system consists of three distributed comp onen ts a sender A a receiv er B and a transp ort system T W e consider an asymmetric comm unication i e the comm unic ating partners pla y xed roles e g only A ma y initiate the establishmen t of a connection There are t w o links b et w een A and T and b et w een B and T resp ectiv ely a FIF O queue for A to send messages to T and a FIF O queue for T to send messages to A The same holds for the connections b et w een B and T Consequen tly A sends a message to T stands for A adds a message to the queue AT W e describ e the proto col brie y in an informal manner If A w an ts to establish a connection to comm unicate with B via T then A sends c onne ct r e quest to T T can reject this request b y sending disc onne ct or accept it b y transmitting c onne ct r e quest to B B can also reject the request b y sending disc onne ct to T or B accepts the request b y sending c onne ct c on rmation In b oth cases T transfers B s resp onse to A A t an y time A B or T can indep enden tly decide to release the connection b y sending disc onne ct If B resp onds c onne ct c on rmation to A s c onne ct r e quest then B en ters a lo c al data phase If A receiv es c onne ct c on rmation then A en ters a lo cal data phase If A and B are lo cally in a data phase then the system is in a glob al data phase What w e w an t to c hec k is that the system releases a global data phase b y A and B releasing their lo cal data phases In other w ords the system can only en ter a new global data phase if in b et w een A and B are sim ultaneously not in lo cal data phases Hence the proto col shall guaran tee that global data phases are terminated FIF O First In First Out ST A TE SP A CE REDUCTION EXAMPLE in a correct manner suc h that all en tities in v olv ed in the comm unic ation are in a consisten t state and suc h that future c onne ct r e quests are alw a ys treated in a similar w a y In Oc h a the proto col is sp eci ed using high lev el P etri Nets P et Rei called Pro duct Nets BOP W e do not presen t the proto col s sp eci cation in this thesis but use the description of its abstract b eha viour to pro v e some prop erties of its concrete b eha viour The adv an tage of our approac h is the use of temp oral logic mo del c hec king and an automated retranslation metho d for c hec king prop erties of the concrete b eha viour instead of designing pro ofs on formal languages as done in Oc h a The Analysis of the Proto col A complete reac habilit y analysis of the proto col using the Pro duct Net Mac hine PNM Oc h leads to a reac habilit y graph ha ving states and transitions Oc h a The reac habilit y graph Hac Nit P et is a nite state represen tation of the sp eci cation s b eha viour The actions of the system are represen ted b y the net s transitions or more precisely b y the transition s names together with v alue bindings of v ariables The reac habilit y graph is strongly connected whic h implies that all abstraction ho momorphisms that w e de ne on the b eha viour represen ted b y the graph are simple on the b eha viour Oc h Oc h b Therefore w e can apply our tec hniques for prop ert y retranslation completely BD AD BC AC BD BC AD BD AC Figure The abstract b eha viour of the system The particular abstraction used in Oc h a leads to a nite state represen tation of the system s abstract b eha viour that is depicted in Figure CHAPTER EXAMPLES The abstract actions in Figure ha v e to b e in terpreted as follo ws AC and B C indicate that A and B resp ectiv ely en ter a lo cal data phase AC onnect B C onnect AD and B D denote the release of a data phase AD isconnect B D isconnect F or the abstract b eha viour in Figure w e sho w some prop erties in the follo wing sections The Phase Separation Prop ert y In Oc h a it is sho wn that a phase separation prop ert y holds for the proto col i e b et w een t w o global data phases b oth A and B are at the same time not in a lo cal data phase In Oc h a the phase separation prop ert y is describ ed b y conditions on formal languages fy nfAD g j x x AC y L g f B D g fy nfB D g j x x B C y L g f AC AC AD g Herein fAC AD B C B D g is the abstract action alphab et and L is the ab stract partial b eha viour of the proto col L is the pre x closed regular language accepted b y the nite state system in Figure Roughly sp eaking condition indicates that after A has en tered a lo cal data phase A releases the data phase immedi ately or B releases its lo cal data phase rst and then A releases its data phase B D The meaning of condition is that after en tering a lo cal data phase B releases it immedi ately or B releases its data phase after A has en tered AC or has en tered and released AC AD its lo cal data phase T ogether conditions and guaran tee a global phase separation prop ert y No new global data phase can b e en tered b efore the old one is released completely b y A and B W e describ e conditions and using PL TL form ulae instead of formal lan guage descriptions W e omit paren theses to impro v e readabilit y G AC X AD B D X AD G B C X B D AC X B D AD X B D F orm ula and form ula describ e prop erties that hold for the abstraction sho wn in Figure In Oc h a a formal language pro of is used to sho w that the phase separation prop ert y also holds for the visible part of the original b eha viour of the proto col W e need not construct a formal pro of but ha v e to just apply the retranslation function R for PL TL to obtain corresp onding prop erties for the concrete b eha viour ST A TE SP A CE REDUCTION EXAMPLE By applying the retranslation function R De nition to form ula and form ula omitting as man y paren theses as p ossible w e obtain f inite h G AC U X U AD B D U X U AD f inite h G B C U X U B D AC U X U B D AD U X U B D According to Corollary form ula and form ula hold for the original b eha viour of the sp eci cation Because if an atomic prop osition a di eren t from is satis ed then is not satis ed and vice v ersa w e can simplify form ulae lik e a U X and a U X to a X and a X Also a can b e simpli ed to a and G G F to G for all PL TL form ulae Applying these simpli cations to form ula and form ula w e obtain f inite G AC X U AD B D X U AD h f inite G B C X U B D AC X U B D AD X U B D h These form ulae that are satis ed for the original b eha viour of the considered sp eci cation are quite similar to and The main di erence b eside the f inite h part is that eac h Next op erator X is follo w ed b y U instead of directly for some PL TL form ula Since is just an abbreviation for uninmp ortan t actions with resp ect to the phase separation prop ert y w e nd that the phase separation prop ert y holds as w ell for the in nitely visible computations of the concrete system as it do es for the abstraction Establishing a Connection is Alw a ys P ossible In Oc h a it is also sho wn that indep enden t of the partial b eha viour so far a connection can alw a ys b e ev en tually established This condition is again form ulated using a formal language de nition x L y x y B C AC L W e pro v e the ful lmen t of this requiremen t in the concrete b eha viour of the system under consideration b y an application of Corollary instead of constructing an CHAPTER EXAMPLES expicit pro of as done in Oc h a W e are no w dealing with an ev en tualit y prop ert y W e rewrite condition in a PL TL form ula that is an ev en tualit y prop ert y of the abstract b eha viour Figure B C X AC Retranslation of form ula with resp ect to R leads to B C U X U AC Because the abstraction homomorphism to compute L is simple on the concrete b e ha viour Oc h a and L do es not con tain maximal w ords form ula represen ts an ev en tualit y prop ert y of the concrete b eha viour b y Corollary Applying equiv alen t simpli cation steps as in Section w e obtain as a nal result that B C X U AC is an ev en tualit y prop ert y of the concrete b eha viour Because the abstracting homomorphism do es not hide the release of a connection b y B this condition guaran tees that indep enden t of the past partial b eha viour a connection can alw a ys b e ev en tually established for the concrete b eha viour of the in v estigated sp eci cation This is exactly the requiremen t w e w an ted to c hec k A Remark on Complexit y Reduction In the previous sections w e ha v e nev er calculated the concrete b eha viour of the system under consideration This means that b y applying the metho ds w e ha v e de v elop ed in this thesis in com bination with partial state space construction metho ds lik e the comp ositional approac h in Oc h a w e can pro v e prop erties of the concrete b eha viour of a sp eci cation without ha ving to compute a nite state description of this original b eha viour at all In Oc h a it is sho wn that the abstract b eha viour of a v ery large system in v olv ing n transp ort media where n is an arbitrary natural n um b er as depicted in Figure can b e computed without an exhaustiv e state space construction for the original b eha viour The abstract b eha viour of this system is still the one presen ted in Figure Ob viously di eren t but similar and simple homomorphisms ha v e b een used in the construction of the abstract b eha viour represen tation Th us form ula and for m ula represen t linear prop erties of the system depicted in Figure and form ula represen ts an ev en tualit y prop ert y of this system Therefore the DETECTION OF LOGICAL SER VICE INTERA CTIONS AT1 TT 1 2 TnB A T1 T2 ... Tn B T A 1 TT 2 1 BTn Figure The n fold extended system phase sep ar ation pr op erty as w ell as the p ossible c onne ction establishment pr op erty is satis ed there Because the system in Figure can gro w arbitrarily large w e ha v e sho wn that the phase separation prop ert y holds for systems of arbitrary size that are of the t yp e presen ted in Figure T o summarize the retranslation metho d presen ted in this thesis can allo w the v eri cation of prop erties of v ery large and ev en arbitrarily large system sp eci cations where no direct v eri cation metho d not using an y kind of mo del abstraction is tractable Using the prop ert y preserv ation results of the previous c hapters frees us from constructing explicit pro ofs for eac h particular sp eci cation and allo ws us to apply a systematic uniform and e ectiv ely computable metho d to v erify prop erties of a system s concrete b eha viour from prop erties of its abstraction Detection of Logical Service In teractions In the previous section w e dealt with an example that rev ealed the complexit y re duction that abstraction can in tro duce in to the v eri cation pro cess making at rst glance in tractable v eri cation tasks tractable On the other hand the previous sec tion s example is of no direct practical relev ance So in the curren t section w e consider an example that is practically relev an t w e deal with service in teraction detection on the logical lev el This is searc hing for undesired in terferences of ser vices in a telephone system of to da y These telephone systems are called in telligen t net w orks IN The term lo gic al level emphasizes that w e do not consider the basic call pro cess of the net w ork but sp ecify the functionalit y of the services directly as suming an idealized call pro cess As a side remark the area of telephon y is an area where one t ypically deals with co op erating systems W e select the services c al l forwar ding unc onditional CFU and sele ctive c al l r eje c tion SCR to c hec k for in teraction b et w een them indeed nding an in teraction b et w een the t w o services The sp eci cation of the logical functionalit y of CFU and SCR is su cien tly small that w e can presen t it completely in this thesis W e start with a brief in tro duction to the general problem of service in teractions in in telli gen t net w orks After an informal description of the services CFU and SCR w e CHAPTER EXAMPLES presen t their formal Pro duct Net sp eci cation whic h is a mo di ed v ersion of the one in CDGE Finally w e c hec k for in teractions b et w een the sp eci ed services sho wing that SCR can in terfere CFU in an undesired w a y A Brief In tro duction to Service In teractions in In tel ligen t Net w orks The in telligen t net w ork IN is a concept for the fast and economical pro vision of new telecomm uni cation services that go b ey ond the limits of con v en tional telephon y One of the ma jor obstacles to rapid service creation in an IN is the problem of service in teraction The service in teraction SI problem o ccurs if one telecomm unic ation service c hanges or sub v erts the op eration of another The range of problems caused b y suc h in teractions ma y v ary from an undesired service b eha viour sligh tly anno ying to the users to large nancial losses or serious net w ork breakdo wns In general there are sev eral w a ys to tac kle the service in teraction problem a v oidance detection and resolution Av oidance aims at dev eloping service platforms and service creation en viron men ts that lead to less in teraction prone service implem en tations It is ho w ev er unrealistic to assume that new arc hitectures will b e able to completely solv e i e a v oid the SI problem Detection approac hes aim at iden tifying p oten tial service in teractions during service creation Based on the service sp eci cations an analysis will b e made that lo oks for con icts inconsistencies etc b et w een the com bined sp eci ca tions Resolution aims at pro viding a solution to in teractions that are either already kno wn from detection or just detected at run time Suc h a solution ma y v ary from a complete re sp eci cation and re design of a service service prioritisa tion run time mec hanisms that will handle the in teraction at run time when it o ccurs to the decision to do nothing W e will tak e up the second p oin t service in teraction detection on the sp eci cation lev el Man y of the service in teraction detection approac hes P are based on the same idea but di er in the selected formal tec hniques they apply One often found idea is a v eri cation based approac h see e g SCORE CPR giv en a sp eci cation of a service in some sp eci cation language and a formal sp eci cation of its requiremen ts it can b e v alidated whether the service meets its requiremen ts No w considering p ossible com binations of services an in teraction can b e detected if one of the services no longer satis es all its requiremen ts DETECTION OF LOGICAL SER VICE INTERA CTIONS W e will c hec k the services c al l forwar ding unc onditional CFU and sele ctive c al l r eje ction SCR for undesired in teractions b et w een one another CFU renders for w arding incoming telephone calls to another telephone terminal p ossible If activ e CFU forw ards al l incoming calls to a sp eci ed terminal SCR allo ws the rejection of telephone calls of selected callers arriving at a telephone terminal If activ e SCR stops calls from sp eci c users ev en b eing signalled Lo oking at the informal description of CFU and SCR it is quite ob vious that they in teract if subscrib er B forw ards calls to the terminal of subscrib er C subscrib er C rejects calls from A and A calls B what will happ en Receiving A s call at C s terminal w ould violate SCR not receiving A s call at C s terminal w ould vi olate CFU assuming that B do es not reject calls from A W e will detect exactly this in teraction in the formal sp eci cation of CFU and SCR applying the metho ds dev elop ed in this thesis In general a sp eci cation of sev eral services including a mo del of the basic call pro cess has a v ery large state space So the n um b er of di eren t services that ma y b e com bined to b e c hec k ed for service in teraction is rather limited The v eri cation and abstraction approac h presen ted in this thesis is a helpful to ol to allo w the searc h for service in teractions for man y more com bined services than without b eha viour abstraction Although not essen tial for the in v estigation of CFU and SCR the state spaces are not v ery large for the com bination of these services the example sho ws that abstraction decreases the state space size of the CFU SCR sp eci cation and that service in teraction can b e detected b y considering the services abstract b eha viours Sp eci cation of CFU and SCR W e presen t the sp eci cation of CFU and SCR in su cien t detail to b e able to follo w eac h step in the analysis and v eri cation of the services W e sp ecify the services using Pro duct Nets BOP OP whic h are high lev el P etri Nets P et Rei with individual tok ens W e do not giv e the de nition of Pro duct Nets here but describ e eac h comp onen t of the sp eci cation exhaustiv ely in an informal w a y that ev ery one should b e able to follo w all imp ortan t v eri cation steps ev en without understanding the formal sp eci cation in detail The sp eci cation is sub divided in to v arious subnets Iden tically named places in di eren t subnets are iden ti ed with one another resulting in the complete sp eci cation According to the w a y in whic h w e com bine subnets to a complete sp eci cation one usually sa ys that the sp eci cation is syn thesized from subnets b y glueing identic al ly name d plac es Since w e searc h for lo gic al in teractions of the services w e describ e b oth services on a high abstraction lev el assuming a v ery simpli ed basic call pro cess the activ ation CHAPTER EXAMPLES of a service simply dep ends on its parameters The parameter that in v ok es CFU is a telephone n um b er to whic h an incoming call has to b e forw arded SCR s parameter is a list of telephone n um b ers that iden tify incoming calls to b e rejected The simpli ed dialling pro cess is depicted in Figure Subscrib ers i e partic ipan ts in the telephone service are iden ti ed b y natural n um b ers W e iden tify subscrib ers with their iden ti ers and simply sa y subscrib er instead of iden ti er of the subscrib er T o b e ev en more precise when w e sa y subscrib er w e actually ha v e the subscrib er s telephone line in mind The place subscrib ers con tains as its initial marking the particular com bination of subscrib ers that is to b e analysed The places lo c al establishment and busy are initially mark ed empt y local_establishment + A_calls_B subscribers busy Figure Dialling T o the v ariables A and B that o ccur in Figure the calling and called subscrib er are assigned when transition A c al ls B res Then the calling subscrib er assigned to v ariable A is stored in place busy and the pair c al ler c al le e is put in to place lo c al establishment A can call B only if A is not already engaged con tained in place busy This is pro vided b y the inhibitor arc from busy to A c al ls B E g if subscrib er calls subscrib er A c al ls B res for A and B then the tok en is put in place lo c al establishment Before ring A c al ls B it is c hec k ed whether tok en is not already in place busy If A c al ls B res for A and B then tok en is put in to place busy A pair c al ler c al le e in place lo c al establishment is in terpreted as a call request e g subscrib er calls subscrib er There are t w o p ossibilities of handling a call request dep ending on whether CFU e g for subscrib er is activ ated The CFU service is depicted in Figure The activ ation or deactiv ation of the service is determined b y the initial marking of place CFU If place CFU con tains for exam ple tok en then CFU is activ e for subscrib er forw arding his her calls to subscrib er If there is no tok en n in CFU n I N then CFU is not activ e for subscrib er CFU con tains at most one tok en i n for eac h i I N DETECTION OF LOGICAL SER VICE INTERA CTIONS CFU do_not_forward forward global_establishment local_establishment Figure The CFU service Dep ending on the activ ation of CFU one of the transitions do not forwar d or forwar d res remo ving tok en c al ler c al le e from place lo c al establishment and putting a corresp onding tok en c al ler new c al le e req in to glob al establishment If the tran sition do not forwar d res new c al le e is the old c al le e of place lo c al establishment If forwar d res new c al le e is determined b y the marking of place CFU req indicates that curren tly the request to establish a connection is pro cessed If for example place lo c al establishment con tains tok en subscrib er calls subscrib er and place CFU con tains tok en subscrib er forw ards his her incoming calls to subscrib er then tok en in place lo c al establishment is remo v ed b y ring transition forwar d and the tok en req is put in to place glob al establishment the call from subscrib er is forw arded to subscrib er req describ es the connection s curren t state If a connection to a sp eci c line is requested it has to b e c hec k ed whether this line is free or engaged This is sho wn in Figure If the called line is not busy no iden ti er tok en in place busy transition fr e e is enabled and will re Otherwise transition engage d res If the caller receiv es an idle tone this is represen ted b y the free part of the tok en c al ler c al le e free there is the p ossibilit y of hanging up b efore the callee answ ers This premature hanging up is sp eci ed in Figure Premature hanging up is mo delled b y transition onho ok by A Firing it remo v es the curren t call from place glob al establishment and c al ler and c al le e are remo v ed from place busy No w w e come to the establishmen t of a connection Since a connection can b e established only if SCR do es not reject its establishmen t Figure presen ts the mo delling of the SCR service CHAPTER EXAMPLES global_establishment free engaged busy Figure Connect Engaged + onhook_by_A global_establishment busy Figure Premature Hanging Up T o mo del the SCR service place SCR con tains subscrib er pairs subscrib er subscrib er describing that subscrib er rejects calls from subscrib er T ran sition o ho ok by B is only enabled if place glob al establishment con tains a tok en c al ler c al le e free suc h that no tok en c al le e c al ler is in place SCR meaning that the actual call is not rejected b y the SCR service If not rejected b y SCR b y ring onho ok by B a connection b et w een c al ler and c al le e will b e established b y putting c al ler c al le e in to place establishe d c onne ction Hanging up if the callee is busy or from an established connection is presen ted in Figure If a caller gets a busy signal e g tok en busy in place glob al establishment the caller in the example subscrib er can hang up This is mo delled b y transition onho ok when busy Firing transition onho ok when busy remo v es the caller from place busy F rom an established connection c al ler c al le e in place c onne ction establishe d c al ler or c al le e ma y hang up This is mo delled b y transition onho ok when c al ling The tok en c al ler c al le e will b e remo v ed from place c onne ction establishe d if on ho ok when c al ling res and c al ler and c al le e will b e remo v ed from place busy Completing the Sp eci cation As already men tioned the complete sp eci cation is the com bination of all subnets presen ted so far b y iden tifying iden tically named places What in addition is missing are the domains of the places since w e are dealing with individual tok ens DETECTION OF LOGICAL SER VICE INTERA CTIONS SCR offhook_by_B established_connection global_establishment Figure SCR global_establishment onhook_when_busy busy + onhook_when_calling established_connection Figure Hanging Up F or Pro duct Nets the places domains are called ob ject structures They are de ned in the net s pream ble F or the CFU SCR sp eci cation the tok ens do not ha v e a v ery complex structure Therefore the sp eci cation s pream ble is not particularly complicated defset STATE f req busy free g defob SUBSCRIBER S NAT defob SUBSCRIBER PAIRS pro NAT NAT defob CALLS pro NAT NAT STATE NAT is the prede ned set of non negativ e in tegers STATE is a nite set that w e de ne b y en umerating its elemen ts The de nition of domains starts with the k eyw ord CHAPTER EXAMPLES defob The k eyw ord pro designates the Cartesian pro duct of sets The assignmen t of domains to places of the sp eci cation is listed in T able Place Domain subscrib ers SUBSCRIBER S busy SUBSCRIBER S lo c al establishment SUBSCRIBER PAIRS CFU SUBSCRIBER PAIRS SCR SUBSCRIBER PAIRS c onne ction establishe d SUBSCRIBER PAIRS glob al establishment CALLS T able The places domains The initial marking of a Pro duct Net describ es the initial state of the sp eci cation F or the CFU SCR sp eci cation place subscrib ers is initially mark ed with iden ti ers of subscrib ers Places CFU and SCR ma y optionally b e initally mark ed indicating for whom CFU and SCR are activ ated resp ectiv ely All other places are not initially mark ed In teraction of CFU and SCR W e presen t no w the analysis and v eri cation of the CFU SCR sp eci cation In CDGE a similar sp eci cation is in v estigated There additional information is added to the sp eci cation for v eri cation purp oses if in CDGE for a particular abstraction the minim al nite state system is empt y then an in teraction b et w een CFU and SCR m ust ha v e o ccurred In this thesis w e ha v e a v oided adding additional information to the sp eci cation This enforces the need to c hec k a small temp oral logic form ula on the abstract b eha viour instead of only c hec king for empt yness The b ene t of this thesis approac h is that it is generally applicable to service in terac tion in v estigations It is curren tly applied to real life service in teraction problems in detailed sp eci cations including the basic call pro cess of the telephone service DFV GE DFV GE T o b e able to searc h for service in teractions w e rst ha v e to compute a represen tation of the sp eci cation s b eha viour with resp ect to an initial marking initial state The initial marking determines the n um b er of subscrib ers as w ell as the ac tiv e services The computation of the represen tation of the b eha viour is called com plete reac habilit y analysis the resulting nite state system is the reac habilit y graph Hac Nit P et T able sho ws the size of the CFU SCR sp eci cation s DETECTION OF LOGICAL SER VICE INTERA CTIONS reac habilit y graph with resp ect to di eren t initial markings The reac habilit y graphs ha v e b een computed using the Pro duct Net Mac hine PNM Oc h V eri cation later on is done using the SH V eri cation T o ol NOR add on the PNM Initial Marking Reac habilit y Graph Plac e tokens in the place n um b er of states subscrib ers subscrib ers subscrib ers subscrib ers CFU subscrib ers SCR subscrib ers CFU SCR T able Di eren t reac habilit y analysis results The rst three ro ws of T able are only included to giv e an impression of the gro wth of nite state systems represen ting the b eha viour of concurren t sp eci cations the more subscrib ers there are the more calls can b e initiated concurren tly leading to a more complex b eha viour With resp ect to service in teraction the last three ro ws of T able are imp ortan t W e sho w that com bining CFU and SCR last ro w do es not limit the functionalit y of SCR th ro w but that of CFU th ro w Hence w e detect a service in teraction b y sho wing SCR ma y disturb CFU All reac habilit y graphs brie y presen ted in T able are strongly connected There fore all homomorphisms applied to the language accepted b y the reac habilit y graph are simple on this language Oc h Consequen tly w e can fully apply the metho ds presen ted in the previous c hapters T o searc h for service in teractions w e c hec k eac h service sep erately for its basic prop erties Afterw ards w e c hec k whether the service still satis es these basic prop erties when com bined with other services W e start with the in v estigation of SCR i e w e v erify prop erties of the b eha viour computed with resp ect to the initial marking giv en in the th ro w of T able W e c hec k the prop ert y if subscrib er calls subscrib er subscrib er will not notice this call b y considering an abstraction of the b eha viour of the activ ated SCR service T o do so w e ha v e to de ne a suitable homomorphism The actions of the concrete b eha viour are red transitions of the sp eci cation plus the in terpretation v alue binding of the transitions v ariables With resp ect to CHAPTER EXAMPLES the prop ert y w e w an t to c hec k it is imp ortan t to k eep visible the acceptance of a call from subscrib er under the abstraction Therefore w e map the ring of transition o ho ok by B with v ariable A ha ving v alue to the abstract action o ho ok Another imp ortan t action of the concrete b eha viour is hanging up b y subscrib er or b y his or her partner in an existing call Th us w e tak e the ring of transitions onho ok by A onho ok when c al ling and onho ok when busy for A to the abstract action onho ok Finally it is imp ortan t to k eep visible subscrib er calling subscrib er Th us ring of transition A c al ls B with A and B is tak en to abstract action c al ling All other actions of the concrete b eha viour are ignored b y taking them to the empt y w ord What w e describ ed ab o v e in an informal manner is an abstracting homomorphism on the b eha viour of the SCR service sp eci cation De ning this homomorphism using the features of the homomorphism editor of the SH V eri cation T o ol NOR w e can compute the nite state system of Figure represen ting the abstract b eha viour of SCR onhook calling onhook offhook onhook Figure SCR The extension see De nition of the b eha viour represen ted in Figure satis es the PL TL form ula G cal l ing X onhook G According to Corollary w e obtain that the concrete b eha viour of the SCR The homom orphism editor is a user in terface of the SH V eri cation T o ol NOR that helps to de ne abstractions on the concrete b eha viour of a sp eci cation The set of concrete actions can b e partitioned in to di eren t sets with resp ect to user de nable predicates on the action alphab et as w ell as b y en umeration of actions On eac h of those sets di eren t homom orphic mappings can b e de ned resulting in a single homomo rphism on the concrete b eha viour Su cien t conditions that guaran tee simplicit y of the homom orphism can b e c hec k ed automatically During the w ork on this thesis it turned out that the homomorphi sm editor is a v ery helpful or ev en necessary to ol for de ning abstractions e cien tly Th us in addition to nding suitable abstraction tec hniques it is a complex task to dev elop practically applicable mec hanisms for the de nition of concrete abstractions DETECTION OF LOGICAL SER VICE INTERA CTIONS sp eci cation satis es G cal l ing U X U onhook G G F Simplifying this form ula as in Section w e obtain G cal l ing X U onhook G This form ula is satis ed b y the concrete b eha viour of the CFU SCR sp eci cation with resp ect to the h lab eling function where h is the abstraction homomorphism w e applied to obtain Figure In terpreting the ab o v e form ula informally w e nd that whenev er calls a call is either not accepted b efore it is terminated or it is nev er accepted In other w ords can nev er call whic h is the desired prop ert y for the SCR service for the considered constellation of parameters Computing a corresp onding abstraction for the com bination of SCR and CFU leads to an abstract b eha viour presen ted in Figure onhook calling onhook Figure SCR CFU The extension of this b eha viour also satis es G cal l ing X onhook G Consequen tly b y the same argumen t as for the SCR sp eci cation when analysed separately the concrete b eha viour of the CFU SCR com bination still satis es the requiremen ts for the SCR service Therefore with resp ect to these requiremen ts w e do not detect an in teraction of CFU and SCR with resp ect to the SCR service T o v erify the CFU service w e use a di eren t abstracting homomorphism whic h is a mo di cation of the one used for the SCR service w e no w hide the A c al ls B transition completely but k eep visible the ring of the forwar d transition for v ariable A ha ving v alue W e call the corresp onding abstract action forwar d Applying this homomorphism to the b eha viour computed with resp ect to the initial marking depicted in the th ro w of T able results in an abstract b eha viour presen ted in Figure CHAPTER EXAMPLES onhook forward onhook offhook offhook onhook Figure CFU The PL TL form ula G F forwar d X o ho ok is a relativ e liv eness prop ert y of the b eha viour of Figure By Theorem and after applying some simpli cation steps w e obtain that G F forwar d X U o ho ok in terpreted in regard to the corresp onding h lab eling function is a relativ e liv eness prop ert y of the concrete b eha viour Its informal in terpretation is it is alw a ys p ossi ble that in nitely often a forw arded call leads to an established connection This is a prop ert y that the CFU service ob viously should satisfy Applying the corresp onding homomorphism to the b eha viour of the com bined sp eci cation of CFU and SCR last ro w of T able w e obtain Figure represen ting the abstract b eha viour onhook forward onhook Figure CFU SCR The prop ert y G F forwar d X o ho ok is not a relativ e liv eness prop ert y of Figure Hence b y Theorem G F forwar d U o ho ok VERIFICA TION OF A BCSM SPECIFICA TION in terpreted in resp ect to the corresp onding h lab eling function is not a relativ e liv eness prop ert y of the concrete b eha viour Therefore b y com bining CFU and SCR an imp ortan t prop ert y of CFU is violated Hence w e ha v e detected an in teraction of CFU and SCR with resp ect to CFU if SCR is activ e some forw arded calls ma y not b e signalled V eri cation of a BCSM Sp eci cation In the previous section w e ha v e c hec k ed CFU and SCR for in teractions on the logical lev el The sp eci cation of services including their in terpla y on the logical lev el is not su cien t for an exhaustiv e searc h for in teractions What is missing is the em b edding of the services in a mo del of the basic call pro cess of an in telligen t net w ork IN This call pro cess named the b asic c al l state mo del BCSM is curren tly b eing standardized This standardization pro cess is structured in eigh t steps Eac h step leads to a more detailed BCSM These di eren tly detailed standardization steps are called c ap ability sets CS The curren tly standardized capabilit y set is CS see Q xx and esp ecially Q In this section w e v erify a Pro duct Net sp eci cation of the BCSM throughout this section w e assume CS when brie y talking of BCSM W e do not presen t the sp eci cation itself but relate nite state systems that w e computed as abstractions of the BCSM sp eci cation s b eha viour to automata descriptions in the standard ization pap er Q The complete sp eci cation can b e found in DFV GE Before starting with v eri cation w e giv e a brief in tro duction to the BCSM The BCSM handles the basic call pro cess of an IN This call pro cess is in ternally structured distinguishing caller and callee The part of the BCSM related to a caller is named originating BCSM abbreviated O BCSM The callee orien ted part is named terminating BCSM or T BCSM Services in the IN are add on features of the BCSM The in terface b et w een BCSM and services is the servic e lo gic The general structure of an IN including caller and callee is depicted in Figure Dashes represen t comm uni cation c hannels The BCSM is some kind of a nite state system The states are called p oints in c al l PIC Added to PIC are dete ction p oints DP from where the service logic ma y b e in v ok ed The nite state system that represen ts the BCSM is describ ed graphically as w ell as textually in the standard Q A Pro duct Net sp eci cation of the originating as w ell as the terminating BCSM w as established in the SER VINT pro ject NO b DFV GE DFV GE There am biguities in the standard and con tradictions b et w een the textual and graphical description of the BCSM are resolv ed CHAPTER EXAMPLES Caller O-BCSM Service Logic Callee T-BCSM Figure The basic structure of an IN Tw o abstractions of the BCSM sp eci cation s b eha viour lea ving visible only the ac tions related to the O BCSM and T BCSM resp ectiv ely lead to exactly the resolv ed nite state systems of the standard Q represen ting O BCSM and T BCSM If w e abstract with resp ect to the b eha viour of the subscrib ers in the IN w e obtain nite state systems represen ting reasonable subscrib er b eha viour Since all abstrac tions men tioned are obtained b y applying an abstracting homomorphism that is sim ple on the concrete b eha viour relativ e liv eness prop erties of the abstract b eha viour represen t corresp onding relativ e liv eness prop erties of the concrete b eha viour This observ ation in principle is su cien t to v erify the correctness of the sp eci cation in comparison to Q the comp onen ts of the BCSM b eha v e in their concrete en vironmen t in the same w a y as they w ould b eha v e in an idealized en vironmen t In the subsequen t paragraphs w e lo ok at t w o di eren t abstract b eha viours more closely c hec king explicitly some of their prop erties These t w o b eha viours are the one of the caller and the one of the T BCSM T o v erify the caller s b eha viour w e apply an abstracting homomorphism that k eeps visible all actions related to the caller and ignores all other actions The actions that are related to the caller are o ho ok the caller tak es the handset dial ling the caller dials a n um b er and onho ok the caller hangs up Applying the abstracting homomorphism informally de ned ab o v e to the BCSM sp eci cation s b eha viour w e obtain the nite state system in Figure describing the caller s abstract b e ha viour A prop ert y that a caller should satisfy is after lifting the handset the caller ma y hang up imme diately or he or she ma y dial or remain on the line forev er In temp oral logic G o ho ok X onho ok dial ling G This form ula is satis ed b y the extension of the b eha viour represen ted in Fig ure Hence according to Corollary the concrete b eha viour satis es G o ho ok U X U onho ok dial ling G VERIFICA TION OF A BCSM SPECIFICA TION offhook onhook onhook dialling Figure The caller s abstract b eha viour Simpli cation of this form ula leads to G o ho ok U onho ok dial ling G Th us w e ha v e sho wn that in the BCSM sp eci cation a caller b eha v es in suc h a w a y that after lifting the handset he or she dials a n um b er hangs up immediatel y or remains on the line No other action of the caller is p ossible after the o ho ok action since represen ts actions that are not p erformed b y the caller Therefore the caller meets a requiremen t that w e w ould ha v e exp ected for a caller b eha ving reasonably Chec king a prop ert y of the caller s b eha viour once again illustrates ho w abstraction can extract a part of the concrete b eha viour of a sp eci cation that represen ts one of its sp eci c asp ects No w w e turn to the v eri cation of the T BCSM After applying a homomorphism that is the iden tit y function on actions relev an t to the T BCSM and that tak es all other actions to the empt y w ord w e obtain the nite state system in Figure that represen ts the abstract b eha viour of the whole BCSM sp eci cation that is related to the T part The abstracting homomorphism is simple on the concrete b eha viour It extracts the T BCSM s b eha viour when the T BCSM is em b edded in the en vironmen t that is the O BCSM W e obtain exactly the b eha viour as presen ted in the standard Q Consequen tly all prop erties that the standard demands the T BCSM to satisfy are indeed satis ed for the T BCSM in the BCSM sp eci ca tion Nev ertheless w e c hec k explicitly a prop ert y of the T BCSM b y rstly applying another abstraction step Figure con tains some actions that are in terruptions to the straigh tforw ard call ing pro cess These actions are not authorize d c al le d p arty busy no answer and exc eption Whenev er one of these actions o ccurs an exception handling is nec essary The exception handling is p erformed b y PIC Occurrence of the action r eturn PIC to start indicates that a successful exception handling has tak en place CHAPTER EXAMPLES return_PIC11_to_start not_authorized authorized return_DP17_to_start DP13_not_armed DP12_not_armed called_party_busy DP14_not_armed exception called_party_alert no_answer called_party_answer answer disconnect DP15_not_armed DP16_not_armed mid_call Figure T BCSM T o c hec k the prop ert y whenev er an in terruption of the calling pro cess o ccurs an ex ception handling tak es place w e can de ne a suitable abstraction on the b eha viour presen ted in Figure that k eeps visible the in terruption and the exception han dling and c hec k a suitable temp oral logic form ula on the abstract b eha viour A suitable abstraction on T BCSM s b eha viour is de ned b y the homomorphism that maps not authorize d c al le d p arty busy no answer and exc eption on the abstract action interruption that maps action r eturn PIC to start on the abstract action exc eption hand ling and that tak es all other actions to the empt y w ord The resulting abstract b eha viour is depicted in Figure Ob viously G interruption X exc eption hand ling represen ts a relativ e liv eness prop ert y of the b eha viour presen ted in Figure Let h b e the abstracting ho BRIEF SUMMAR Y OF THE CHAPTER exception_handling interruption Figure An abstraction of the T BCSM momorphism on the concrete b eha viour that generates the abstract b eha viour in Figure and let h b e the abstracting homomorphism on this abstract b eha viour that generates the more abstract b eha viour presen ted in Figure Let des ignate the comp osition of mappings Because h is simple on the concrete b eha viour and h is simple on the b eha viour presen ted in Figure b oth b eha viours ha v e a strongly connected nite state represen tation h h is simple on the BCSM sp ec i cation s b eha viour Oc h W e obtain according to Corollary that with resp ect to the h h lab elling function h h G interruption U X U exc eption hand ling is a relativ e liv eness prop ert y of the BCSM sp eci cation s b eha viour Simpli cation of this form ula leads to G interruption U exc eption hand ling If w e in terpret this result w e nd that the reasonable computations of the BCSM sp eci cation in this con text the reasonable computations are once again the fair ones satisfy the c orr e ct exc eption hand ling pr op erty This last v eri cation example illustrates ho w step wise abstraction can b e p erformed Regarding the results of this thesis the step wise abstraction can b e regarded as an in v erse step wise re nemen t Brief Summary of the Chapter W e ha v e applied the v eri cation results with resp ect to b eha viour abstraction that w e ha v e dev elop ed in this thesis to di eren t examples F or all t yp es of established preserv ation results regarding the three t yp es of prop erties line ar prop erties r elative liveness prop erties and eventuality prop erties w e ha v e illustrated the use of the preserv ation results on at least one of the examples The rst example illustrates the p ossible decrease of the state space when applying an abstraction homomorphism to a b eha viour This example is not orien ted to CHAPTER EXAMPLES realistic applications The second and third examples are application orien ted Both are tak en from the area of telephon y an area that con tains a lot of examples of co op erating systems Of particular in terest is the second example There a complete sp eci cation and v eri cation pro cess is illustrated The topic of concern is the detection of service in teractions in in telligen t net w orks W e pro v ed that the services c al l forwar ding unc onditional and sele ctive c al l r eje ction ma y in teract in an undesired w a y This result and the w a y w e ac hiev ed it con tribute in part to third part y funded v eri cation pro jects SER VINT NO b DFV GE and SER VINT DFV GE that deal with the detection of service in teractions in in telligen t net w orks The SER VINT and SER VINT pro jects are join t pro jects of GMD and Deutsc he T elek om Chapter Conclusions Summary W e ha v e de ned abstractions of a co op erating system s b eha viour and dev elop ed concepts for the v eri cation of di eren t t yp es of prop erties using this kind of b e ha viour abstraction This led to dev eloping an original approac h for the v eri cation of co op erating systems using b eha viour abstraction Abstractions ha v e b een de ned via alphab etic language homomorphisms and their extension to languages that w e ha v e called abstraction abstracting homomorphisms W e ha v e consid ered the b eha viour of a system to b e the Eilen b erg limit of a pre x closed regular language The delicate p oin t when dealing with v eri cation and abstraction is that abstraction alw a ys means loss of information and w e ha v e to b e cautious that no information is lost that is imp ortan t with resp ect to the prop ert y to b e v eri ed F or di eren t kinds of prop erties w e ha v e therefore in v estigated b y what t yp e of abstraction they are su cien tly preserv ed First w e ha v e sho wn that prop erties expressible in prop ositional linear time temp oral logic PL TL are only w eakly preserv ed b y abstraction homomorphisms w e do not obtain information ab out the whole concrete b eha viour Only for abstraction ho momorphisms that do not allo w hiding of actions ha v e w e got a strong preserv ation result Because w e are usually in terested in ha ving a concept for action hiding in abstrac tions w e ha v e de ned based on abstraction homomorphisms a non homomorphic abstraction tec hnique that allo ws a preserv ation of su cien tly man y information ab out the concrete b eha viour on the abstract lev el CHAPTER CONCLUSIONS F or co op erating systems i e systems con taining sev eral comp onen ts suc h that no comp onen t has direct con trol o v er other comp onen ts linear satisfaction the usual satisfaction relation for PL TL can b e to o strict in the sense that extreme executions migh t fail to satisfy a PL TL prop ert y linearly F or this purp ose w e ha v e de ned relativ e liv eness prop erties W e ha v e not in terpreted relativ e liv eness as a prop ert y classi cation but as a satisfaction relation for prop erties F or relativ e liv eness prop erties and a sligh t mo di cation of a sub class ev en tualit y prop erties w e ha v e pro v ed that abstraction homomorphisms that are simple on the concrete b eha viour form an abstraction class that preserv es these prop erties su cien tly W e ha v e applied the dev elop ed concepts for v eri cation using b eha viour abstractions to some examples including practically relev an t examples The detection of service in teractions in in telligen t net w orks can b e men tioned in this con text The results es tablished in this thesis con tributed to the join t pro jects SER VINT and SER VINT of GMD and Deutsc he T elek om aiming at the dev elopmen t of a formal metho d to detect service in teractions on the sp eci cation lev el NO b DFV GE DFV GE The fo cus of this thesis has b een to establish a theoretical framew ork for v eri cation using abstraction leading to a practically applicable v eri cation tec hnique On the theoretical lev el this thesis included parts from formal language theory and temp oral logics Practical w ork considerations w ere the underlying motiv e for establishing a theory for v eri cation using b eha viour abstraction The dev elop ed concepts are indeed application orien ted in the sense that the established results are algorithmic and mean while implem en te d as part of the SH V eri cation T o ol NOR NORR The to ol itself is used in the SER VINT and SER VINT pro jects F urther Study The approac h presen ted in Chapter includes a syn tactical transformation of PL TL form ulae PL TL as an language description language cannot represen t all regular languages In fact PL TL represen table languages are equiv alen t to the star free regular languages Tho T o ha v e an approac h as presen ted in Chapter for the whole language class of regular languages it w ould b e in teresting to extend the results to an extension of PL TL that is equiv alen t to all regular languages W ol An imp ortan t criterion for the usefulness of abstraction tec hniques is the p ossibilit y of a v oiding an exhaustiv e construction of the state space represen ting a system s concrete b eha viour to construct a represen tation of its abstract one Suc h a partial state space construction metho d for the comp ositional analysis of sp eci cations is presen ted in Oc h a Oc h Impro v em en ts of partial state space construction tec hniques for the computation of an abstract b eha viour represen tations are alw a ys FUR THER STUD Y w elcome A promising approac h ma y b e to include partial order metho ds e g Go d W G When using partial order metho ds to reduce the state space preserv ation of liv eness prop erties is delicate Nev ertheless using partial orders only with resp ect to transi tions that are lab elled with actions hidden b y the abstraction the abstraction of the concrete b eha viour w ould b e equiv alen t to the abstraction of a corresp onding trace automaton an automaton represen tation of traces Go d Go d Com bining this idea with the comp ositional analysis of Oc h a Oc h should b e ev en more e cien t than partial orders or comp ositional analysis on their o wn There exist approac hes that represen t b eha viours b y lab elled Mark o v c hains V ar VW In this con text a system satis es a prop ert y if and only if the set of computations that do not satisfy the prop ert y has measure with resp ect to the probabilit y w eigh ts of the system s transitions This w a y of v erifying systems is called pr ob abilistic v eri cation Because relativ e liv eness prop erties are related to almost satisfying a prop ert y linearly there are some hin ts that the satisfaction relation of relativ e liv eness prop erties ma y b e more or less related to probabilistic v eri cation Lo oking at this problem in detail calls for the searc h of a suitable relation b et w een Can tor top ology Kel and the top ology related to measurable spaces Coh A question of more theoretical in terest is whether considering Eilen b erg limi ts of pre x closed regular languages as b eha viours can b e relaxed to Eilen b erg limits of ric her language classes Note that comm uting Eilen b erg limit and homomorphism pla ys an imp ortan t role in the main pro ofs of this thesis F or the languages discussed in F o otnote on P age comm uti ng limit and homomorphism is prohibited b y blo c king the in nite con tin uabilit y of w ords b y a xed n um b er of particular letters in the fo otnote the letter b at the end of eac h w ord in the language By application of the homomorphism whic h ignores these letters the blo c king is remo v ed and an in nite con tin uations exist Ho w ev er in this case the homomorphism is highly not simple on the b eha viour Simplici t y of the homomorphism is the other imp ortan t condition in the pro ofs Hence it w ould b e in teresting to c hec k whether for simple homomorphisms the language class for whic h homomorphism and Eilen b erg limit comm ute can b e enlarged to non pre x closed or non regular languages If one could iden tify suc h languages the results of this thesis without an y c hanges also w ould hold for them CHAPTER CONCLUSIONS App endix A A Characterization of Simplicit y A Preliminaries Let L b e a pre x closed regular language Let max L b e the set of maximal w ords in L If max L consists of a single w ord w e iden tify max L with this w ord Let L L max L f g W e designate f g b y If L L then L is maximal with resp ect to Consequen tly L is maximal with resp ect to Let h b e an abstracting homomorphism Let h b e h except that additionally h W e de ne h and h Let x and y If l im h pr e x fy g then h x h x y If l im h pr e x then h x max h pr e x and h x max h pr e x W e can establish a result correp onding to Lemma Its pro of is similar to that of Lemma Note A l im h L h l im L NO a NO a A Characterizing Simple Homomorphisms W e giv e a c haracterization of homomorphisms that are simple on a b eha viour W e sho w that an abstraction preserv es relativ e liv eness prop erties su cien tly if and only if the abstraction homomorphism is simple on the concrete b eha viour W e rst pro v e a theorem similar to Theorem APPENDIX A A CHARA CTERIZA TION OF SIMPLICITY Theorem A If h is simple on L then for al l P l im h L j P implies RL l im L j h P RL Pro of Let P suc h that l im h L j P Then b y Lemma it su ces to RL sho w that L pr e l im L h P b ecause pr e l im L L So let x L Case x L Then x uv with u L v f g and c ont u L f g Regarding simplicit y of h on L this implies c ont h u h L f g whic h means h u l im h L According to the assumptions of the theorem and h x pr e h u w e ha v e h x pr e l im h L P So there exists a y l im h L P suc h that h x pr e y This implies y h x h x Because x l im L w e ha v e x pr e l im L h P Case x L Because h is simple on L there exists a w ord u c ont h x h L suc h that c ont u h c ont x L c ont h x u h L Then b y the assumptions of the the orem there exists a y suc h that h x uy l im h L P So uy l im u c ont h x u h L l im h c ont x L No w according to Note A l im h c ont x L h l im c ont x L So there exists a z l im c ont x L suc h that h z uy Th us xz l im L and h xz h x uy P and w e ha v e x pr e l im L h P Theorem A If for al l P l im h L j P implies l im L j h P RL RL then h is simple on L Pro of Assume h is not simple on L Then there exists an x L suc h that for all u c ont h x h L there exists a v c ont h x u h L suc h that uv h c ont x L Because h c ont x L h c ont x L w e also ha v e uv h c ont x L If u c ont h x h L and u c ont h x h L then u u u suc h that u c ont h x h L u f g and c ont h x u h L f g Since h is not simple on L in x this implies u h c ont x L and therefore u u u h c ont x L Th us for all u c ont h x h L there is a v c ont h x u h L suc h that uv h c ont x L F or x L suc h that h is not simple on L in x w e de ne the prop ert y P as P l im h L n h x l im c ont x L F or P according to Lemma it su ces to sho w that pr e l im h L P pr e l im h L and pr e l im L h P pr e l im L F or pro ving the rst equation w e sho w l im h L l im pr e P b ecause h L is pre x closed and l im h L P P If w l im h L and h x pr e w then A BRIEF SUMMAR Y OF APPENDIX A w P No w let w h x y l im h L Then for all u pr e y there exists a v c ont h x u h L suc h that uv h c ont x L whic h implies h x uv h x c ont x L So h x uv pr e P and h x u pr e P Hence w l im pr e P completing the pro of of the rst equation No w w e pro v e pr e l im L h P pr e l im L Considering the set x w e ha v e l im L h P x x l im c ont x L h P Assume that there exists a y in x l im c ont x L h P Then y x l im c ont x L and h y P Th us h y l im h L and h y h y and therefore l im h pr e y So there exists a w c ont x L suc h that h y h xw l im h L Hence c ont h xw h L f g whic h implies the simplicit y of h on L in x This is a con tradiction to the assumption that h is not simple on L in x Th us there exists no y in x l im c ont x L h P Corollary A l im h L j P implies l im L j h P for al l P if RL RL and only if h is simple on L Pro of Corollary A is a direct consequence of Theorem A and Theorem A Corollary A l im h L j P implies l im L j h P for al l r e gular P RL RL if and only if h is simple on L Pro of The case of regular prop erties is a sp ecial case of Theorem A Prop ert y P in the pro of of Theorem A is regular for an regular L regarding that regular languages are preserv ed under b o olean op erations Tho A Brief Summary of App endix A Corollary A establishes a complete c haracterization of simplicit y the simplici t y of a homomorphism on a b eha viour is not only a su cien t but also a necessary condition for abstractions to preserv e su cien tly regular relativ e liv eness prop erties APPENDIX A A CHARA CTERIZA TION OF SIMPLICITY App endix B Ev en tualit y Prop erties and CTL In this app endix w e sho w ho w w e ha v e to in terpret languages suc h that b y the def inition of CTL CE CES Eme and restricting to form ulae A G E F where is a PL TL form ula w e obtain exactly the seman tics de nition of ev en tualit y prop erties B In terpretation of Languages Let L b e a pre x closed regular language W e represen t l im L b y a nitely branc hing tree T of in nite depth if l im L is not empt y W e de ne T lim L lim L in suc h a w a y that all nitely long sequences of lab els of no des along a nitely long path in T starting at T s ro ot are in L All in nitely long paths of lab els lim L lim L of no des along in nitely long paths starting at T s ro ot are in l im L lim L De nition B F or al l w L let succ w c ont w L i e succ w is the set of al l letters in that c an fol low w in L We de ne T r e cursively lim L The r o ot of T denote d by r oot T is lab el le d with lim L lim L If is a no de in T such that the p ath fr om the r o ot is lab el le d with w lim L then has jsucc w j many child no des and e ach child no de is lab el le d with an element of succ w r esp e ctively The set of al l child no des of a no de is designate d chil dr en T do es not c ontain any other no des than the ones describ e d lim L F or a no de in T l abel designates the lab el of nodes T designates lim L lim L the set of al l no des in T lim L APPENDIX B EVENTUALITY PR OPER TIES AND CTL T o b e precise T is in fact a forest of jsucc j man y trees Eac h of these trees lim L represen ts all w ords in l im L that start with the same letter T o obtain a unique represen tation of l im L w e ha v e link ed these trees to a particular no de T s lim L ro ot whic h has to b e lab elled with the empt y w ord for not c hanging the fact that path lab els corresp ond to w ords in the language B De ning CTL with resp ect to T l im L W e giv e CTL syn tax de nition and afterw ards presen t the de nition of its seman tics with resp ect to T whic h is the ob vious adaption of CTL seman tics CE lim L CES Eme to the structure of T lim L De nition B We de ne the syntax of CTL with r esp e ct to a set AP of atomic pr op ositions Eme A l l atomic pr op ositions ar e state formulae If and ar e state formulae then so ar e and If is a p ath formula then A and E ar e state formulae Each state formula is also a p ath formula If and ar e p ath formulae then so ar e and If and ar e p ath formulae then so ar e U and X No other formulae ar e CTL formulae De ning the seman tics of CTL with resp ect to T w e ha v e to tak e care ab out lim L T s ro ot b ecause it is the only no de with l abel W e de ne the lim L satisfaction relation j b et w een no des of T and CTL form ulae suc h that lim L T satis es a CTL form ula if and only if its ro ot do es initial satisfaction The lim L AP satisfaction relation is de ned with resp ect to a lab elling function that tak es no de lab els to the set of atomic prop ositions that determines to b e satis ed for the no de lab el De nition B L et and b e CTL formulae and let b e a no de in T lim L L et for al l no des of T path designate the set of al l in nite p aths in T lim L lim L that start at B DEFINING CTL WITH RESPECT TO T LI M L If AP and l abel then j if and only if chil dr en l abel If AP and l abel then j if and only if l abel j if and only if it is not the c ase that j j if and only if j and j S If l abel then j E if and only if path j childr en If l abel then j E if and only if path j S If l abel then j A if and only if path j childr en If l abel then j A if and only if path j L et s s s b e an in nite p ath in T starting at a no de s such that lim L l abel s i e s is not the r o ot of T lim L If AP then j if and only if l abel s j if and only if it is not the c ase that j j if and only if j and j j X if and only if j j U if and only if ther e exist an i I N such that j and for i al l j i j j j E if and only if path s j j A if and only if path s j W e use this satisfaction relation on no des of T to de ne the satisfaction relation lim L on T itself as satisfaction in T s ro ot in tial satisfaction lim L lim L AP De nition B L et b e a CTL formula and let b e a lab el ling function of no de lab els with atomic pr op ositions Then T j with r esp e ct to lim L if and only if r oot T j with r esp e ct to lim L In De nition B w e ha v e adapted usual CTL seman tics to t to T lim L APPENDIX B EVENTUALITY PR OPER TIES AND CTL B Relation to Ev en tualit y Prop erties Observ ation B If is a PL TL formula then T satis es A G E F lim L if and only if nodes T x path x j F lim L Considering that nodes T x path is b y de nition of T lim L lim L equiv alen t to w pr e l im L x c ont w l im L w e obtain the follo wing observ ation Observ ation B If is a PL TL formula then T satis es A G E F lim L if and only if w pr e l im L x c ont w l im L x j F Relating these t w o observ ations to one another leads to the follo wing lemm a Lemma B L et b e a PL TL formula is an eventuality pr op erty of l im L if and only if T j A G E F lim L Pro of Lemma B is a direct consequence of Observ ation B and Observ a tion B B Brief Summary of App endix B W e ha v e sho wn that ev en tualit y prop erties are c haracterized exactly b y the A G E F fragmen t of CTL Lemma B i e they are c haracterized b y form ulae of the t yp e A G E F suc h that is a PL TL form ula Bibliograph y AH Ra jeev Alur and Thomas A Henzinger Lo cal liv eness for comp o sitional mo deling of fair reactiv e systems In Pierre W olp er editor Computer A ide d V eri c ation CA V v olume of L e ctur e Notes in Computer Scine c e pages Springer AL Mart n Abadi and Leslie Lamp ort The existence of re nemen t map pings SR C Rep ort DEC System Researc h Cen ter July AL Mart n Abadi and Leslie Lamp ort Comp osing sp eci cations SR C Rep ort DEC System Researc h Cen ter Octob er AS Bo w en Alp ern and F red B Sc hneider De ning liv eness Information Pr o c essing L etters Octob er Ber Jean Berstel T r ansductions and Context F r e e L anguages Studi en b uc her Informatik T eubner V erlag Stuttgart rst edition Bes Eik e Best editor CONCUR v olume of L e ctur e Notes in Com puter Scienc e Springer V erlag BOP Heinz J urgen Burkhardt P eter Oc hsensc hl ager and Rainer Prinoth Pro duct nets a formal description tec hnique for co op erating sys tems GMD Studien Gesellsc haft f ur Mathematik und Daten v er arb eitung GMD Darmstadt Septem b er Bru Glenn Bruns A practical tec hnique for pro cess abstraction In Best Bes pages B uc J R B uc hi On a decision metho d in restricted second order arith metic In E Nagel et al editors Pr o c e e dings of the International Congr ess on L o gic Metho dolo gy and Philosophy of Scienc e pages Stanford Univ ersit y Press CDFV Carla Cap ellmann Ralph Deman t F arhad F atahi V anani Raphael Galv ez Estrada Ulric h Nitsc he and P eter Oc hsensc hl ager V eri cation b y b eha vior abstraction A case study of service in teraction BIBLIOGRAPHY detection in in telligen t telephone net w orks In Pr o c e e dings of the th International Confer enc e on Computer A ide d V eri c ation CA V v olume of L e ctur e Notes in Computer Scienc e pages New Brunswic k NJ Springer V erlag CDGE Carla Cap ellmann Ralph Deman t Raphael Galv ez Estrada Ulric h Nitsc he and P eter Oc hsensc hl ager Case study Service in terac tion detection b y formal v eri cation under b eha viour abstraction In Tiziana Margaria editor Pr o c e e dings of the st International Work shop on A dvanc e d Intel ligent Networks AIN pages P as sau German y Marc h CE Edm und M Clark e and E Allen Emerson Design and syn thesis of sync hronization sk eletons using branc hing time temp oral logic In Dexter Kozen editor L o gic of Pr o gr ams v olume of L e ctur e Notes in Computer Scienc e pages Springer V erlag CES Edm und M Clark e E Allen Emerson and A Prasad Sistla Au tomatic v eri cation of nite state concurren t systems using temp oral logic sp eci cations A CM T r ansactions on Pr o gr amming L anguages and Systems CGL Edm und M Clark e Orna Grum b erg and Da vid E Long Mo del c hec king and abstraction In Pr o c e e dings of the th A CM Symp osium on Principles of Pr o gr amming L anguages Albuquerque Coh Donald L Cohn Me asur e The ory Birkh auser Boston CPR Pierre Com b es Simon Pic kin and B eatrice Renard A user view of services and net w ork F ormal sp eci cation and in teraction detection In Pr o c e e dings of IEEE IN Workshop Heidelb erg Dam Dennis Dams A bstr act Interpr etation and Partition R e nement for Mo del Che cking PhD thesis T ec hnisc he Univ ersiteit Eindho v en Eindho v en The Netherlands DFV GE Ralph Deman t F arhad F atahi V anani Rafael Galv ez Estrada Ul ric h Nitsc he and P eter Oc hsensc hl ager Absc hlu b eric h t des GMD T elek om Pro jekts F ormale Sp ezi k ations und V eri k ationsmetho den zur Behandlung der Service In teraction Problematik SER VINT Absc hlu b eric h t GMD Dezem b er DFV GE Ralph Deman t F arhad F atahi V anani Rafael Galv ez Estrada Ul ric h Nitsc he and P eter Oc hsensc hl ager Zwisc hen b eric h t des GMD T elek om Pro jekts F ormale Sp ezi k ations und V eri k ation smetho den zur Behandlung der Service In teraction Problematik SER VINT Zwisc hen b eric h t GMD July BIBLIOGRAPHY DGG Dennis Dams Rob Gerth and Orna Grum b erg Abstract in terpre tation of reactiv e systems Abstractions preserving CTL CTL and CTL In Ernst R udiger Olderog editor Working Confer enc e on Pr o gr amming Conc epts Metho ds and Calculi IFIP T ransactions Amsterdam North Holland DOR J org Desel Andreas Ob erw eis and W olfgang Reisig editors Work shop A lgorithmen und Werkzeuge f ur Petrinetze Hum b oldt Univ er sit at Berlin Eil S Eilen b erg A utomata L anguages and Machines v olume A Aca demic Press New Y ork Eme E Allen Emerson T emp oral and mo dal logic In v an Leeu w en vL pages F ra Nissim F rancez F airness Springer V erlag New Y ork rst edition GL Susanne Graf and Claire Loiseaux Prop ert y preserving abstractions under parallel comp osition In T APSOFT v olume of L e ctur e Notes in Computer Scienc e pages Springer V erlag Go d P atrice Go defroid Using partial orders to impro v e automatic v eri ca tion metho ds In Edm und M Clark e and Rob ert P Kurshan editors Computer A ide d V eri c ation CA V v olume of L e ctur e Notes in Computer Scienc e pages New Brunswic k Springer V erlag Go d P atrice Go defroid Partial Or der Metho ds for the V eri c ation of Con curr ent Systems A n Appr o ach to the State Explosion Pr oblem PhD thesis Univ ersit e de Li ege Li ege Belgium GPVW Rob Gerth Doron P eled Moshe Y V ardi and Pierre W olp er Sim ple on the y automatic v eri cation of linear temp oral logic In Pi otr Dem binski and Marek Srednia w a editors Pr oto c ol Sp e ci c ation T esting and V eri c ation XV pages Chapman Hall Gra Susanne Graf V eri cation of a distributed cac he memory b y using abstractions In Da vid L Dill editor Computer A ide d V eri c ation CA V v olume of L e ctur e Notes in Computer Scienc e pages Stanford Springer V erlag GW P atrice Go defroid and Pierre W olp er A partial approac h to mo del c hec king In th A nnual IEEE Symp osium on L o gic in Computer Scienc e pages IEEE Computer So ciet y Press BIBLIOGRAPHY GW P atrice Go defroid and Pierre W olp er Using partial orders for the e cien t v eri cation of deadlo c k freedom and safet y prop erties In K G Larsen and A Sk ou editors CA V Computer A ide d V eri c ation v olume of L e ctur e Notes in Computer Scienc e pages Springer V erlag GW P atrice Go defroid and Pierre W olp er Using partial orders for the e cien t v eri cation of deadlo c k freedom and safet y prop erties F ormal Metho ds in System Design April Hac Mic hel Hac k Decidabilit y questions for p etri nets T ec hnical Rep ort MIT Har Mic hael A Harrison Intr o duction to F ormal L anguage The ory Addison W esley Reading Mass rst edition Hen Thomas A Henzinger So oner is safer than later Information Pr o c essing L etters HR H J Ho ogeb o om and G Rozen b erg In nitary languages Basic the ory and applications to concurren t systems In J W de Bakk er W P de Ro ev er and G Rozen b erg editors Curr ent T r ends in Con curr ency v olume of L e ctur e Notes in Computer Scienc e pages Springer V erlag HU John E Hop croft and Je rey D Ullman Intr o duction to A utomata The ory L anguages and Computation Addison W esley Reading Mass rst edition Kel J L Kelley Gener al T op olo gy V an Nostrand Princeton Koz Dexter Kozen Results on the prop ositional m u calculus The or etic al Computer Scienc e Kur Rob ert P Kurshan Computer A ide d V eri c ation of Co or dinating Pr o c esses Princeton Univ ersit y Press Princeton New Jersey rst edition KV Orna Kupferman and Moshe Y V ardi Mo dule c hec king In Ra jeev Alur and Thomas A Henzinger editors CA V v olume of L e ctur e Notes in Computer Scienc e pages New Brunswic k N J Springer V erlag Lam Leslie Lamp ort Pro ving the correctness of m ultipro cess programs IEEE T r ansactions on Softwar e Engine ering SE BIBLIOGRAPHY LP Orna Lic h tenstein and Amir Pn ueli Chec king that nite state concur ren t programs satisfy their linear sp eci cation In th A nnual A CM Symp osium on Principles of Pr o gr amming L anguages pages A CM Press Jan uary Maz An toni Mazurkiewicz T race theory In Petri Nets Applic ation and R elationships to Other Mo dels of Concurr ency A dvanc es in Petri Nets Part II Pr o c e e dings of an A dvanc e d Course v olume of L e ctur e Notes in Computer Scienc e pages Springer Mil Robin Milner Communic ation and Concurr ency Pren tice Hall In ternational Hertfordshire rst edition MP Zohar Manna and Amir Pn ueli The T emp or al L o gic of R e active and Concurr ent Systems Sp e ci c ation Springer V erlag New Y ork rst edition Nit Ulric h Nitsc he Erreic h bark eitsanalyse v on Pro duktnetzen Arb eitspa piere der GMD Gesellsc haft f ur Mathematik und Daten v erar b eitung GMD Darmstadt April Nit a Ulric h Nitsc he Prop ositional linear temp oral logic and language ho momorphism s In Anil Nero de and Y uri V Matiy asevic h editors Pr o c e e dings of the r d International Symp osium on L o gic al F ounda tions of Computer Scienc e LF CS v olume of L e ctur e Notes in Computer Scienc e pages Sain t P etersburg Russia Springer V erlag Nit b Ulric h Nitsc he Simple homomorphisms and linear temp oral logic Arb eitspapiere der GMD GMD F orsc h ungszen trum Informa tionstec hnik Darmstadt Decem b er Nit c Ulric h Nitsc he A v eri cation metho d based on homomorphic mo del abstraction In Pr o c e e dings of the th A nnual A CM Symp osium on Principles of Distribute d Computing PODC page Los An geles A CM Press Nit d Ulric h Nitsc he V erifying temp oral logic form ulas in abstractions of large reac habilit y graphs In J org Desel Andreas Ob erw eis and W olf gang Reisig editors National Workshop on A lgorithms and T o ols for Petri Nets A lgorithmen und Werkzeuge f ur Petrinetze A WP pages Hum b oldt Univ ersit at Berlin Nit Ulric h Nitsc he A nitary language seman tics for prop ositional linear temp oral logic abstract In Pr epr o c e e dings of the nd International Confer enc e on Developments in L anguage The ory DL T Univ er sit y of Magdeburg German y BIBLIOGRAPHY Nit a Ulric h Nitsc he A nitary language seman tics for prop ositional linear temp oral logic In J urgen Dasso w Grzegorz Rozen b erg and Arto Salomaa editors Pr o c e e dings of the nd International Confer enc e on Developments in L anguage The ory DL T pages Magde burg German y W orld Scien ti c Singap ore Nit b Ulric h Nitsc he V eri cation and b eha vior abstraction to w ards a tractable v eri cation tec hnique for large distributed systems Journal of Systems and Softwar e June Nit Ulric h Nitsc he In terpretation of the full computation tree logic CTL on sets of in nite sequences In Anil Nero de and Sergei Adian editors Pr o c e e dings of the th International Symp osium on L o gic al F oundations of Computer Scienc e LF CS v olume of L e ctur e Notes in Computer Scienc e pages Y arosla vl Russia Springer V erlag Nit Ulric h Nitsc he Application of formal v eri cation and b eha viour ab straction to the service in teraction problem in in telligen t net w orks Journal of Systems and Softwar e Marc h NNO F rank Nie ner Ulric h Nitsc he and P eter Oc hsensc hl ager Determin istic regular liv eness prop erties In Pr epr o c e e dings of the r d Inter national Confer enc e on Developments in L anguage The ory DL T Aristotle Univ ersit y of Thessaloniki Greece NNO F rank Nie ner Ulric h Nitsc he and P eter Oc hsensc hl ager Determinis tic regular liv eness prop erties In Symeon Bozapalidis editor Pr o c e e dings of the r d International Confer enc e on Developments in L an guage The ory DL T pages Thessaloniki Greece NO a Ulric h Nitsc he and P eter Oc hsensc hl ager Appro ximately satis ed prop erties of systems and simple language homomorphisms Ar b eitspapiere der GMD GMD F orsc h ungszen trum Information stec hnik Darmstadt Decem b er NO b Ulric h Nitsc he and P eter Oc hsensc hl ager Zwisc hen b eric h t des GMD T elek om Pro jekts F ormale Sp ezi k ations und V eri k ationsmetho den zur Behandlung der Service In teraction Problematik SER VINT Zwisc hen b eric h t GMD Juli NO a Ulric h Nitsc he and P eter Oc hsensc hl ager Appro ximately satis ed prop erties of systems and simple language homomorphisms In Pr o c e e dings of the st International Workshop on F ormal Metho ds for Industrial Critic al Systems FMICS Oxford U K Marc h BIBLIOGRAPHY NO b Ulric h Nitsc he and P eter Oc hsensc hl ager Appro ximately satis ed prop erties of systems and simple language homomorphisms Infor mation Pr o c essing L etters NOR Ulric h Nitsc he P eter Oc hsensc hl ager and J urgen Repp The SH Veri cation To ol Arb eitspapiere der GMD GMD F orsc h ungszen trum Informationstec hnik Darmstadt July NORR Ulric h Nitsc he P eter Oc hsensc hl ager J urgen Repp and Roland Riek e The SH v eri cation to ol In Pr o c e e dings of the nd Interna tional Workshop on F ormal Metho ds for Industrial Critic al Systems FMICS Cesena Italy NW Ulric h Nitsc he and Pierre W olp er Relativ e liv eness and b eha vior ab straction extended abstract In Pr o c e e dings of the th A CM Sym p osium on Principles of Distribute d Computing PODC pages San ta Barbara CA Oc h P eter Oc hsensc hl ager Die Pro duktnetzmasc hine Petri Net Newslet ter August Also app eared as a GMD Arb eitspapier Nr Oc h P eter Oc hsensc hl ager V eri k ation k o op erierender Systeme mit tels sc hlic h ter Homomorphisme n Arb eitspapiere der GMD Gesellsc haft f ur Mathematik und Daten v erarb eitung GMD Darm stadt Oktob er Oc h a P eter Oc hsensc hl ager Komp ositionelle Veri k ation k o op erierender Systeme Arb eitspapiere der GMD GMD F orsc h ungszen trum Informationstec hnik Darmstadt Dezem b er Oc h b P eter Oc hsensc hl ager V eri cation of co op erating systems b y sim ple homomorphisms using the pro duct net mac hine In Desel et al DOR pages Oc h P eter Oc hsensc hl ager Comp ositional v eri cation of co op erating sys tems using simple homomorphisms In J org Desel Hans Fleisc hhac k Andreas Ob erw eis and Mic hael Sonnensc hein editors Workshop A l gorithmen und Werkzeuge f ur Petrinetze pages Univ ersit at Old en burg OP P eter Oc hsensc hl ager and Rainer Prinoth Mo del lierung verteilter Systeme Konzeption F ormale Sp ezi kation und V eri kation mit Pr o duktnetzen View eg Wiesbaden BIBLIOGRAPHY P Eurescom Pro ject P Hand ling Servic e Inter action in the Servic e Life Cycle Deliv erable Annex B State of the Art in In teraction Handling Decem b er P et James L P eterson Petri Net The ory and the Mo deling of Systems Pren tice Hall rst edition Pn u Amir Pn ueli The temp oral logic of programs In Pr o c e e dings of the th A nnual IEEE Symp osium on F oundations of Computer Scienc e pages Q Draft Revised ITU T Recomme ndation Q Distribute d F unc tional Plane for Intel ligen t Network CS Marc h Q xx ITU T Recommendations Q xx Q series Intel ligent Network R e c ommendation Rei W olfgang Reisig Petri Nets A n Intr o duction v olume of EA TCS Mono gr aphs in The or etic al Computer Scienc e Springer V erlag rst edition SCORE SCORE Metho ds and T o ols R ep ort on Metho ds and T o ols for Servic e Cr e ation Se c ond V ersion V olume I Service In teraction Analysis Deliv erable D R SCO WP DS b SCORE Decem b er Sif Joseph Sifakis Prop ert y preserving homomorphisms of transition systems In Edm und Clark e and Dexter Kozen editors L o gics of Pr o gr ams v olume of L e ctur e Notes in Computer Scienc e pages Springer V erlag Sti Colin Stirling An in tro duction to mo dal and temp oral logics for CCS In A Y oneza w a and T Ito editors Concurr ency The ory L anguage and A r chite ctur e v olume of L e ctur e Notes in Computer Scienc e Springer V erlag Tho W olfgang Thomas Computation tree logic and languages In J W de Bakk er W P de Ro ev er and G Rozen b erg editors Line ar Time Br anching Time and Partial Or der in L o gics and Mo dels for Con curr ency v olume of L e ctur e Notes in Computer Scienc e pages Springer V erlag Tho W olfgang Thomas Automata on in nite ob jects In v an Leeu w en vL pages BIBLIOGRAPHY V al a An tti V almari A stubb orn attac k on state explosion In E M Clark e and R P Kurshan editors CA V Computer A ide d V eri c ation v olume of L e ctur e Notes in Computer Scienc e pages Springer V erlag V al b An tti V almari Stubb orn sets for reduced state space generation In Grzegorz Rozen b erg editor A dvanc es in Petri Nets v olume of L e ctur e Notes in Computer Scienc e pages Springer V erlag V ar Moshe Y V ardi Automatic v eri cation of probabilistic concurren t nite state programs In Pr o c e e dings of the th IEEE Symp osium on F oundations of Computer Scienc e pages P ortland Octob er vL Jan v an Leeu w en editor F ormal Mo dels and Semantics v olume B of Handb o ok of The or etic al Computer Scienc e Elsevier VW Moshe Y V ardi and Pierre W olp er An automata theoretic approac h to automatic program v eri cation In Pr o c e e dings of the st Symp o sium on L o gic in Computer Scienc e Cam bridge June VW Moshe Y V ardi and Pierre W olp er Reasoning ab out in nite compu tations Information and Computation No v em b er W G Pierre W olp er and P atrice Go defroid P artial order metho ds for tem p oral v eri cation In Best Bes pages W ol Pierre W olp er T emp oral logic can b e more expressiv e Information and Contr ol W ol Pierre W olp er On the relation of programs and computations to mo d els of temp oral logic In B Banieqbal H Barringer and A Pn ueli editors Pr o c e e dings of T emp or al L o gic in Sp e ci c ation v olume of L e ctur e Notes in Computer Scienc e pages Springer V erlag WVS Pierre W olp er Moshe Y V ardi and A Prasad Sistla Reasoning ab out in nite computation paths In Pr o c e e dings of the th A nnual IEEE Symp osium on F oundations of Computer Scienc e pages T uscon BIBLIOGRAPHY Leb enslauf geb oren in Jugenheim Studium der Informatik und Ph ysik an der Johann W olfgang Go ethe Univ ersit at F rankfurt am Main Diplom in Informatik Nac h wuc hswissensc haftler am Institut f ur T elek o op erationstec h nik der GMD Darmstadt Doktorand am F ac h b ereic h Informatik der Johann W olfgang Go ethe Univ ersit at F rankfurt am Main Gast wissensc haftler in der F orsc h ungsgrupp e v on Prof Pierre W olp er an der Univ ersit at Li ege Belgien Assisten t am Institut f ur Informatik der Univ ersit at Z uric h ab April Assistenzprofessur Lecturer am Departmen t of Electronics and Computer Science der Univ ersit at Southampton England Curriculum Vitae b orn in Jugenheim German y Studying Computer Science and Ph ysics at the Univ ersit y of F rankfurt German y Diploma in Computer Science Junior Scien tist at the Institute for T eleco op eration T ec hnology of GMD Darmstadt German y PhD studen t at the Departmen t of Computer Science of the Uni v ersit y of F rankfurt German y Visiting scien tist in the researc h group of Prof Pierre W olp er at the Univ ersit y of Li ege Belgium Researc h Assistan t at the Departmen t of Computer Science of the Univ ersit y of Zuric h Switzerland from April Univ ersit y Lecturer at the Departmen t of Electronics and Com puter Science of the Univ ersit y of Southampton U K Adresse ab address from April Ulric h Nitsc he Declarativ e Systems and Soft w are Engineering Group Departmen t of Electronics and Computer Science Univ ersit y of Southampton High eld Southampton SO BJ U K Email un ecs so ton ac u k