Graph transformation planning with time and concurrency / vorgelegt von Steffen Ziegert, M.Sc.

G aph T ans o ma ion Planning wi h Time and Concu ency Disse a ion zu E langung des akademischen G ades eines Dok o s de Na u wissenscha en an de Fakul ä ü Elek o echnik, In o ma ik und Ma hema ik de Uni e si ä Pade bo n o geleg on S e en Ziege , M.Sc. Pade bo n 2016 iii Abs ac The inc easing complexi y o echnical sys ems inspi es so wa e and sys- ems enginee ing scien is s o imp o e he s a e o he a in designing such sys ems. Among hese imp o emen s is he in eg a ion o cogni i e unc ions in o app oaches o model-d i en so wa e de elopmen . Such cogni i e unc ions enable an au onomous ope a ion o he sys em, e.g., by planning econ igu a ion beha io a ec ing he so wa e a chi ec u e o he sys em. In his con ex , his hesis is conce ned wi h he au oma ed gene a ion o econ igu a ion plans. By p o iding a o mal amewo k o he ule-based modi ica ion o g aphs o g aph-like s uc u es, g aph ans o ma ion sys ems enable o model he dynamics o s uc u es. As a consequence, hey a e pa icula ly con enien o modeling econ igu a ion beha io o so wa e a chi ec u es. Howe e , g aph ans o ma ion sys ems ha e only a ely been employed as sys em models o planning echniques. Mo i a ed by di e en equi emen s a ising om wo undamen ally di e en applica ion examples, wo app oaches o g aph ans o ma ion planning ha e been de eloped in his hesis. The i s app oach p ese es he exp essi eness o g aph ans o ma ion sys ems by di ec ly wo king on a g aph ans o ma ion sys em’s s a e space. As a esul , i can handle sys em models wi h an in ini e s a e space. I employs a domain-speci ic heu is ic unc ion ha uses he solu ion leng h o a elaxed planning p oblem as heu is ic es ima e. Taking bo h he s uc u e o g aphs and applicable g aph ans o ma ions in o accoun , his is a conside able imp o emen o e ela ed wo k. The second app oach pu s i s ocus on iming aspec s and concu ency. I comes wi h a new o malism o he speci ica ion o du a i e g aph ans o ma- ions. This o malism ensu es ha mul iple du a i e g aph ans o ma ions wi h con lic ing beha io canno be execu ed concu en ly. Fu he mo e, i enables he explici , ule-based speci ica ion o equi emen s ega ding hei concu en and u gen execu ion. By being based on imed g aph ans o ma ion sys ems, i also allows o employ a ailable e i ica ion p ocedu es. Sys em models ha ha e been designed in his o malism can be ansla ed in o planning domains, o which p oblem ins ances can be sol ed by employing o - he-shel planning sys ems. E alua ion esul s gi e insigh on how o decide be ween di e en ansla ion a ian s and con oy an idea how ce ain aspec s o planning domains in luence planning pe o mance. i Zusammen assung Die zunehmende Komplexi ä on echnischen Sys emen mo i ie Fo sche im So wa e und Sys ems Enginee ing den S and de Technik de En wicklung solche Sys eme zu e besse n. Zu diesen Ve besse ungen gehö die In eg a ion kogni i e Funk ionen in Ansä ze de modellge iebenen So wa een wicklung. Solche kogni i e Funk ionen e möglichen einen au onomen Be ieb des Sys ems, z.B. du ch eine Planung on Rekon igu a ionen, die die So wa ea chi ek u des Sys ems beein lussen. In diesem Zusammenhang beschä ig sich diese A bei mi de au oma ischen E s ellung on Plänen solche Rekon igu a ionen. Indem sie ein o males F amewo k ü die egelbasie e Modi ika ion on G aphen und G aph-ähnlichen S uk u en zu Ve ügung s ellen, e möglichen es G aph ans o ma ionssys eme, die Dynamik on S uk u en zu modellie en. Sie sind dami besonde s zu Modellie ung on Rekon igu a ionen eine So - wa ea chi ek u geeigne . Bishe wu den G aph ans o ma ionssys eme jedoch nu sel en als Modelle ü Planungs e ah en eingese z . Mo i ie du ch die un e schiedlichen An o de ungen zweie g und e - schiedene Anwendungsbeispiele, wu den in diese A bei zwei Ve ah en zu Planung mi G aph ans o ma ionen en wickel . Das e s e Ve ah en e häl die Ausd ucksk a on G aph ans o ma ions- sys emen, indem es di ek au dem Zus ands aum eines G aph ans o ma- ionssys ems a bei e . Aus diesem G und kann es mi Modellen umgehen, die einen unendlichen Zus ands aum au spannen. Es e wende eine domänenunab- hängige Heu is ik, die die Länge de Lösung eines elaxie en Planungsp oblems als Schä zwe lie e . Sie be ücksich ig sowohl die S uk u des G aphen als auch die anwendba en G aph ans o ma ionen, was eine deu liche Ve besse ung gegenübe e wand en A bei en da s ell . Das zwei e Ve ah en leg seinen Fokus au Zei aspek e und Nebenläu igkei . Es b ing einen neuen Fo malismus zu Spezi ika ion on zei konsumie enden G aph ans o ma ionen mi sich. Diese Fo malismus s ell siche , dass meh e e zueinande im Kon lik s ehende zei konsumie ende G aph ans o ma ionen nich nebenläu ig ausge üh we den können. Des Wei e en e möglich e die explizi e, egelbasie e Spezi ika ion on An o de ungen bezüglich ih e neben- läu igen und eiligen Aus üh ung. Indem e au zei beha e en G aph ans o ma- ionen au se z , e möglich e auße dem die Ve wendung be ei s e ügba e Ve i ika ions e ah en. In diesem Fo malismus en wickel e Modelle können in Planungsdomänen übe se z we den, dessen P oblemins anzen mi S anda d- Planungssys emen gelös we den können. Auswe ungse gebnisse hel en zwi- schen un e schiedlichen Va ian en diese Übe se zung zu en scheiden und e - mi eln eine Idee, inwie e n die Pe o manz de Planung du ch e schiedene Aspek e de Planungsdomäne beein luss wi d. Acknowledgmen s Fi s o all, I would like o hank my PhD ad iso P o . D . Heike Weh heim o he suppo and guidance du ing hese pas i e yea s and he oppo uni y o w i e his PhD hesis. I would u he like o hank P o . D . Wilhelm Schä e o his ime and in e es in he e ala ion o my hesis and D . Theo Le mann, P o . D . Leena Suhl, and P o . D . Ch is ian Plessl o se ing as hesis comi ee membe s. Special hanks go o D . Dominik S eenken, D . Claudia P ies e jahn, D . Ch is ian Heinzemann, Oli e Sudmann, Tobias Meye , Ch is oph Rasche, and P o . D . Ma hias Tichy o he p oduc i e and enjoyable collabo a ion wi hin he Collabo a i e Resea ch Cen e 614 and o e lapping esea ch in e es s. I would also like o hank he ( o me ) membe s o ou esea ch g oup D . Thomas Ruh o h, D . Nils Timm, D . Galina Beso a, Daniel Wonisch, S en Wal he , Alexande Sch emme , Oleg T a kin, Tobias Isenbe g, Ma ie-Ch is ine Jakobs, Manuel Töws, Julia K äme , and Elisabe h Schla o p o iding a wa m and inspi ing a mosphe e. A simila con ibu ion has been made by a ious colleagues om ac oss he loo . Thank you o making co ee b eaks mo e enjoyable! Addi ionally, I would like o hank my s uden assis an s Shayan Ahmadian and Johannes Geismann o suppo ing me in de eloping pa s o he hesis implemen a ion and my hesis ad isees Ma cel F ied ich, Thomas Hauck, and Johannes Heil o in e es ing discussions in esea ch hemes ela ed o his PhD hesis. Finally, I would like o hank my wi e and pa en s o hei suppo and pa ience du ing hese yea s o esea ch (and all hose yea s be o e) and my b o he o spa king my in e es in compu e science in he i s place. Con en s Lis o Figu es xi Lis o Tables x Lis o Algo i hms x ii Lis o Lis ings xix 1 In oduc ion 1 1.1 Au oma edPlanning............................. 3 1.2 Rule-Based Modi ica ion o G aphs . . . . . . . . . . . . . . . . . . . . 4 1.3 Resea ch Tasks and Con ibu ions . . . . . . . . . . . . . . . . . . . . . 5 1.4 Applica ionExamples ............................ 8 1.5 ThesisOu line................................. 11 2 Backg ound on G aph T ans o ma ions 13 2.1 G aphs, G aph Mo phisms, and Pushou s . . . . . . . . . . . . . . . . . 15 2.2 Double Pushou App oach . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.3 Single Pushou App oach . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.4 NACs, Types, and Visual Rep esen a ion . . . . . . . . . . . . . . . . . 21 2.5 Pa allel and Sequen ial Independence . . . . . . . . . . . . . . . . . . . 23 3 Backg ound on AI Planning 27 3.1 PDDLFundamen als............................. 28 3.2 Nume icExp essions............................. 31 3.3 Du a i eAc ions ............................... 32 3.4 Requi edConcu ency............................ 33 4 Planning wi h G aph T ans o ma ions 35 4.1 P oblemS a emen .............................. 37 ii iii CONTENTS 4.2 Applica ion Example: Recon igu a ion o ECUs . . . . . . . . . . . . . 38 4.3 Relaxed Planning Heu is ic . . . . . . . . . . . . . . . . . . . . . . . . . 40 4.3.1 Abs ac S a e Sequences . . . . . . . . . . . . . . . . . . . . . . 40 4.3.2 Rule Applica ion Labels . . . . . . . . . . . . . . . . . . . . . . . 44 4.3.3 P og amCode ............................ 46 4.4 E alua ion................................... 50 4.5 Rela edWo k ................................. 56 4.6 Discussion................................... 59 5 Du a i e G aph T ans o ma ion Sys ems 65 5.1 Applica ion Example: RailCab Sys em . . . . . . . . . . . . . . . . . . . 67 5.2 Du a i e G aph T ans o ma ion Rules . . . . . . . . . . . . . . . . . . . 68 5.2.1 Syn ax ................................. 72 5.2.2 Timed G aphs and Clock Ins ances . . . . . . . . . . . . . . . . 73 5.2.3 Locking Edges and Applica ion Indica o s . . . . . . . . . . . . 76 5.2.4 Timed G aph T ans o ma ion Rules . . . . . . . . . . . . . . . . 79 5.2.5 Clock Ins ance and In a ian Rules . . . . . . . . . . . . . . . . 84 5.2.6 Ope a ional Seman ics . . . . . . . . . . . . . . . . . . . . . . . . 87 5.3 P ope ies o Du a i e G aph T ans o ma ion Rules . . . . . . . . . . . 90 5.3.1 Co espondence o a Du a i e G aph T ans o ma ion . . . . . . 90 5.3.2 Rule Te mina ion and In e lea ing T ansi ion Sequences . . . . 92 5.4 Suppo o Nega i e Applica ion Condi ions . . . . . . . . . . . . . . . 102 5.5 Concu encyRules ..............................107 5.5.1 Syn ax .................................108 5.5.2 Seman ics ...............................114 5.6 U gencyRules.................................120 5.6.1 Syn ax .................................122 5.6.2 Seman ics ...............................124 5.7 Rela edWo k .................................131 5.8 Discussion...................................134 6 Tempo al PDDL-Based Planning o Du a i e G aph T ans o ma ion Sys ems 139 6.1 P oblemS a emen ..............................141 6.2 Applica ion Example: RailCab Sys em (Emphasis on NACs) . . . . . . 143 6.3 T ansla ionScheme..............................146 6.3.1 TypeG aph ..............................148 6.3.2 Du a i e G aph T ans o ma ion Rules . . . . . . . . . . . . . . . 149 6.3.3 Fo biddenPai s............................151 6.3.4 DanglingEdges............................154 6.3.5 Locking Func ionali y . . . . . . . . . . . . . . . . . . . . . . . . 155 6.3.6 Locks in Du a i e Rules . . . . . . . . . . . . . . . . . . . . . . . 156 6.3.7 Concu ency Rules . . . . . . . . . . . . . . . . . . . . . . . . . . 161 6.3.8 U gencyRules ............................164 6.4 P o o ype and T ansla ion Wo k low . . . . . . . . . . . . . . . . . . . . 167 CONTENTS ix 6.5 E alua ion o T ansla ion Va ian s . . . . . . . . . . . . . . . . . . . . . 168 6.6 E alua ion o Concu ency and U gency Rules . . . . . . . . . . . . . . 171 6.7 Rela edWo k .................................177 6.8 Discussion...................................178 7 Conclusion and Fu u e Wo k 181 Bibliog aphy 185 Lis o Algo i hms 4.1 RelaxedNACma ching ............................. 47 4.2 Collec ing ule applica ion labels om an LHS ma ch . . . . . . . . . . . . 48 4.3 Heu is ic unc ion yielding he leng h o a elaxed plan . . . . . . . . . . . 49 x ii Lis o Lis ings 3.1 An example domain descip ion in PDDL [FL03] . . . . . . . . . . . . . . . 29 3.2 A p oblem desc ip ion o he domain o Lis ing 3.1 [FL03] . . . . . . . . . 30 3.3 A domain desc ip ion wi h nume ic exp essions [FL03] . . . . . . . . . . . 31 6.1 Exce p o a plan o 4 RailCabs . . . . . . . . . . . . . . . . . . . . . . . . . 146 6.2 Gene a ed decla a ion o ypes, p edica es, and unc ions . . . . . . . . . 149 6.3 Gene a ed du a i e ac ion o he du a i e ule joinCon oy ........150 6.4 Gene a ed nega i e exis en ial quan i ica ion o a o bidden pai . . . . . 152 6.5 Gene a ed decla a ions o he coun ing unc ionali y . . . . . . . . . . . . 153 6.6 Gene a ed nume ic ac s and assignmen s o o bidden pai s . . . . . . . 153 6.7 Gene a ed uni e sal quan i ica ion o dele ing dangling edges (in he SPO a ian wi h quan i ica ions) . . . . . . . . . . . . . . . . . . . . . . . . 154 6.8 Gene a ed du a i e ac ion o dele ing dangling edges (in he SPO a ian wi hcoun ing unc ions).............................155 6.9 Gene a ed decla a ions o he locking unc ionali y . . . . . . . . . . . . . 156 6.10 Gene a ed locks o suppo ( equi ed) nodes . . . . . . . . . . . . . . . . . 157 6.11 Gene a ed locks o suppo equi ed and o bidden edges . . . . . . . . . 158 6.12 Gene a ed adjacency locks o suppo o bidden pai s . . . . . . . . . . . 160 6.13 Gene a ed decla a ions o suppo concu ency ules . . . . . . . . . . . . 162 6.14 Gene a ed concu ency demand in he ule changePublica ion ......163 6.15 Gene a ed concu ency sa is ac ion in he ule mo eRailCab ........163 6.16 Gene a ed decla a ions o suppo u gency ules . . . . . . . . . . . . . . . 165 6.17 Clip ac ion o suppo u gency ule immedia elyMo eRailCab .......166 6.18 Gene a ed u gency demand in he ule accele a eRailCab ........166 6.19 Gene a ed u gency sa is ac ion in he ule b akeRailCab ..........166 xix 1 In oduc ion In oday’s economy, mo e and mo e echnical sys ems con ain la ge amoun s o so wa e. The inc easing complexi y o hese sys ems ga e ise o he use o modeling languages, which allow o c ea e a model o he sys em ha is o be de eloped. Such a model usually abs ac s de ails o he sys em away o allows o hide hem in di e en iews, hus making he model easie o unde s and. Howe e , he oppo uni ies o employing modeling languages du ing he de elopmen o so wa e sys ems go a beyond ha o abs ac ly ep esen ing sys ems o easie discussion and documen a ion. Model-D i en So wa e De elopmen (MDSD) [SV06] ies o bene i om he exis- ence o models by conside ing hem as i s -class a i ac s du ing he de elopmen o so wa e sys ems. The aim o MDSD is o enable he gene a ion o code om models, e.g., ia model ans o ma ion echniques [OMG11], making a leng hy and e o -p one di ec implemen a ion unnecessa y. A ela ed goal is o enable he analysis o he same models, e.g., o e i y hei co ec ness o o ensu e a ce ain le el o quali y. The bene i s o a well- unc ioning MDSD app oach a e ob ious: so wa e sys ems a e much easie o de elop and e o s can be ound ea lie in he de elopmen p ocess. Fo an MDSD app oach o unc ion p ope ly, i s sys em models need o ha e a o mal ounda ion, i.e., a ma hema ical basis ha unambiguously de ines a model’s meaning. De elopmen echniques in he a ea o so wa e enginee ing and ha dwa e design ha p o ide such a o mal ounda ion a e called o mal me hods. Examples o o mal me hods include p ocess calculi, like Hoa e’s Communica ing Sequen ial P ocesses (CSP) [Hoa78] and Milne ’s Calculus o Communica ing Sys ems (CCS) [Mil80], o mal speci ica ion languages, like he Z no a ion [Spi92; ISO02] and Alloy [Jac06], and au oma a heo y. MDSD app oaches, like Mecha onicUML [Bec+12], a e likely o combine mul- iple domain-speci ic modeling languages, each specialized o a ce ain kind o modeling ask. Examples o such modeling asks include modeling he s uc u al 1 2CHAPTER 1. INTRODUCTION ela ionship o so wa e componen s, communica ion beha io be ween di e en com- ponen s, and econ igu a ion beha io . The la e s a es how he s uc u al ela ionship o so wa e componen s may change o e ime. Because econ igu a ion impac s he so wa e a chi ec u e o a sys em, i is usually ea ed sepa a ely om o he beha io . The inc easing complexi y o echnical sys ems also inspi ed so wa e and sys- ems enginee ing scien is s o look in o di e en ields, like con ol heo y, op imiza- ion, and a i icial in elligence, o imp o e he s a e o he a in designing hose sys ems, c . [GRS14]. Among hese imp o emen s is he in eg a ion o cogni i e unc ions in o MDSD app oaches. This enables subsys ems o he sys em unde conside a ion o ope a e au onomously and hus ensu es ha hey equi e only low main enance. These cogni i e unc ions allow o pe cei e si ua ions and add some kind o pa ial in elligence o he echnical sys em. To enable a echnical sys em o ope a e au onomously, one has o in eg a e a means o making decisions in o his sys em. Fo each decision, he e may be a la ge se o al e na i es. Selec ing which al e na i e o pu in o p ac ice should no be done in isola ion om o he decisions. Sys ems ope a ing au onomously usually ha e goals ha a e supposed o be eached du ing ope a ion, like op imizing he consump ion o ime o esou ces, o achie ing use -speci ied objec i es. These goals ha e o be aken in o accoun when deciding which al e na i es o ealize. Howe e , ecognizing hose al e na i es ha a e likely o help in achie ing he goal can be a complex ask. I hese decisions we e o be made by humans, he esponse- ime equi emen s o many echnical sys ems would no be me . As a consequence, he sys em needs a so wa e componen ha plans which al e na i es o ake. Execu ing some o he chosen al e na i es may in ol e econ igu a ions o he sys em’s so wa e a chi ec u e, such as he c ea ion and dele ion o so wa e compo- nen ins ances o communica ion links be ween hem. Sys ems ha au onomously decide when and how o pe o m hese econ igu a ions, a e said o ha e a sel - o ganizing [GMK02] o sel -managing [B a+04] a chi ec u e. Mul iple a chi ec u al models ha e been p oposed o he de elopmen o such sys ems, e.g., he Ope a o - Con olle Module (OCM) [HOG04], which was de eloped as pa o he Collabo a i e Resea ch Cen e “Sel -Op imizing Concep s and S uc u es in Mechanical Enginee ing” (CRC 614), o K ame and Magee’s e e ence model o sel -managing sys ems [KM07]. A schema ic ep esen a ion o he OCM is gi en in Figu e 1.1. Bo h a chi ec u al models consis o h ee laye s. The bo om laye , called con- olle (in he OCM) o componen con ol (in he e e ence model), accomplishes he mos basic asks o he sys em. I essen ially p o ides he implemen a ion o p imi i e ea u es ela ed o senso s and ac ua o s. The middle laye , called e lec i e ope a o (in he OCM) o change managemen (in he e e ence model), has he capa- bili y o modi y he sys em’s a chi ec u e, e.g., i selec s ope a ing pa ame e s o he bo om laye o execu es so wa e a chi ec u e econ igu a ions. The op laye , called cogni i e ope a o (in he OCM) o goal managemen (in he e e ence model), accomplishes ime-consuming asks, like he compu a ion o a plan ha de e mines which decision al e na i es o ealize. In a sys em wi h a sel -managing a chi ec u e, 1.1. AUTOMATED PLANNING 3 Ac ion Le el Planning Le el Moni o ing Sequence Re lec i e Ope a o Con olle Ope a o -Con olle -Module (OCM) ... Con igu a ion- Con ol Eme gency So Real Time Ha d Real Time Model-based Sel -Op imiaza ion Beha io -based Sel -Op imiza ion Cogni i e In o ma ion P ocessing Cogni i e Ope a o Cogni i e Loop Re lec i e Loop Re lec i e In o ma ion P ocessing Mo o In o ma ion P ocessing Con igu a ions Con olled Sys em Mo o Loop A C B C B A Figu e 1.1: S uc u e o he Ope a o -Con olle Module such a plan s a es which a chi ec u e econ igu a ions o pe o m and when. This hesis is speci ically conce ned wi h his las laye o hose a chi ec u al models, i.e., wi h he au oma ed gene a ion o econ igu a ion plans. 1.1 Au oma ed Planning Au oma ed planning is a discipline in he a ea o a i icial in elligence, coming along in many di e en a ian s. In mos o hese a ian s, some kind o agen has o choose among some se o ac i i ies which one o pe o m. Usually, he e is a no ion 4CHAPTER 1. INTRODUCTION o a s a e o con igu a ion, and each ac i i y de ines a ansi ion be ween wo such s a es. S a es and s a e ansi ions can be ep esen ed in almos any kind o o m. Independen ly o he manne chosen o ep esen sys em s a es, a planning ask always has some kind o ini ial s a e and a goal speci ica ion. The goal speci ica ion de e mines whe he a s a e o he s a e space is a alid end s a e o he pu pose o he planning ask. I a planning sys em inds such an end s a e in he s a e space o igina ing om he ini ial s a e o a planning ask, hen he pa h om he ini ial s a e o he end s a e cons i u es a alid plan. Usually, he e is also some kind o objec i e in ol ed, e.g., s a e changes can ha e cos s, which a e o be minimized. In he mos simple case, hese cos s a e dis ibu ed uni o mly, i.e., he objec i e is o each he goal in as ew s eps as possible. I ime is o he essence, he objec i e is usually o each he goal in as li le ime as possible. A con en ional ep esen a ion o ac ions and s a es o planning p oblems, which is used h oughou he AI planning esea ch communi y, is based on (quan i ie - ee) p edica e calculus. In his ep esen a ion, an ac ion is schema ically de ined ia a se o a omic o mulas ha a e equi ed o hold, a se o a omic o mulas ha a e asse ed as ue, and a se o a omic o mulas ha a e asse ed as alse. This classical o malism is called STRIPS, named a e a planning sys em de eloped by Fikes and Nilsson [FN71] in 1971. I is s ill in use oday wi hin he planning esea ch communi y and has been in eg a ed in o a common language, called he Planning Domain De ini ion Language (PDDL), by McDe mo and he AIPS-98 Planning Compe i ion Commi ee [MA98] in 1998. PDDL has since been ex ended by se e al o he con ibu o s. The mos ele an ex ensions wi h ega d o his hesis a e yping, which allows o employ a ype hie a chy o objec s appea ing as e ms in a omic o mulas, and du a i e ac ions [FL03], which in oduce a no ion o ime and concu en execu ion in o PDDL. Fu he ex ensions ha a e made use o in his hesis include he suppo o nume ic o mulas and quan i ica ion. Na u ally, he applica ion o planning echniques is no es ic ed o such classical ep esen a ions. Planning has also been applied o g aphical models such as Pe i ne s [Pe 62], e.g., o sol ing assembly p oblems in manu ac u ing [Zha89; McC94], and in mo e ecen imes, o g aph ans o ma ion sys ems [Eh +06], e.g., o sol ing econ igu a ion p oblems in he con ex o cybe -physical sys ems [EW11]. Bo h Pe i ne s and g aph ans o ma ion sys ems a e o mal modeling languages wi h igo ous ma hema ical de ini ions and execu ion seman ics. Pe i ne s a e e y well sui ed o modeling he concu en beha io o dis ibu ed sys ems, and g aph ans o ma ion sys ems enable o model he dynamics o s uc u es by p o iding a o - mal amewo k o a ule-based modi ica ion o g aphs o g aph-like s uc u es. The la e is pa icula ly con enien o modeling econ igu a ion beha io o so wa e a chi ec u es. 1.2 Rule-Based Modi ica ion o G aphs In g aph ans o ma ion sys ems, he modi ica ion o g aphs is speci ied ia g aph ans o ma ion ules. Each g aph ans o ma ion ule de ines a condi ion ha has o 1.3. RESEARCH TASKS AND CONTRIBUTIONS 5 be ul illed by a g aph so ha he ule may be applied o his g aph. I he condi ion is ul illed, he ule gi es one o mo e op ions how he g aph may be ans o med in o a new g aph. Since g aphs p o ide an in ui i e way o desc ibe complex concep s and ela ions, g aph ans o ma ions o e a wide ange o applica ion a eas. Resea ch on g aph ans o ma ion s a ed in he la e 1960s in he ields o pa e n ecogni ion and compile cons uc ion. Since hen, g aph ans o ma ions ha e been applied in so wa e enginee ing, da abase design, modeling o concu en sys ems, logical p og amming, model ans o ma ion, and many o he a eas. Thei s eng h lies in hei abili y o model he dynamics o g aphical s uc u es. Fo his eason, g aph ans o ma ions ha e been conside ed a new pa adigm o de eloping so wa e, especially i his so wa e is o complex s uc u e. A lo o s uc u al in o ma ion appea s in he ields o so wa e de elopmen and isual modeling. In objec -o ien ed design, o example, he e is s uc u al in o ma ion in he ela ionship be ween di e en classes and objec s. Compu e ne wo ks and componen -based so wa e sys ems a e also buil using a la ge amoun o s uc u al in o ma ion. All his s uc u al in o ma ion can be exp essed ia g aphs, and hei e olu ion can be exp essed ia g aph ans o ma ions. Due o i s abili y o speci y how s uc u es e ol e o e ime, g aph ans o ma- ions ha e been used o he speci ica ion o so wa e a chi ec u e econ igu a ion, e.g., by We melinge and Fiadei o [WF99; WF02], by Taen ze a al. [TGM00], o by Le Mé aye [Le 98]. Since g aph ans o ma ions ha e a o mal ounda ion, hey ha e also been used o e i ica ion. A p ominen example is he ool se GROOVE [Ren04], which p o ides explici CTL and LTL model checking o g aph ans o ma ion sys ems [KR06; Ren08]. The e a e also app oaches o he mo e speci ic case o e i ying so wa e a chi ec u e econ igu a ion, e.g., a symbolic in a ian checking echnique by Becke e al. [Bec+06], which allows o p o e he absence o o bidden g aph pa e ns, and a composi ional e i ica ion app oach by Ecka d e al. [Eck+13], which includes he e i ica ion o imed p ope ies. Howe e , g aph ans o ma ion sys ems ha e only a ely been employed as sys em models o planning echniques. 1.3 Resea ch Tasks and Con ibu ions The main pu pose o his hesis is o design planning echniques based on g aph ans o ma ions. The use o g aph ans o ma ions ende s hese planning echniques sui able o so wa e a chi ec u e econ igu a ion and allows o an in eg a ion wi h MDSD app oaches. Depending on he applica ion scena ios o in e es , e.g., whe he o no hey in ol e iming aspec s and concu en beha io , he e a e di e en equi emen s o such g aph ans o ma ion planning sys ems. In gene al, econ igu a ions o a sys em’s so wa e a chi ec u e ake ime. I mul i- ple such empo al econ igu a ions a e non-con lic ing, hey can p obably be ca ied ou in pa allel. Requi ing a s ic ly sequen ial execu ion o econ igu a ions migh e en be coun e in ui i e in ce ain applica ion domains, e.g., whe e econ igu a ions 2 Backg ound on G aph T ans o ma ions In g aph g amma s and g aph ans o ma ion sys ems, he modi ica ion o g aphs is speci ied ia g aph ans o ma ion ules 1 . Each ule consis s o a pai o g aphs, called le -hand side (LHS) and igh -hand side (RHS), which schema ically de ine how a g aph may be ans o med in o a new g aph. Applying a g aph ans o ma ion ule o a g aph can be seen as eplacing a subg aph co esponding o he ule’s LHS wi h a copy o i s RHS. Mo e p ecisely, elemen s ha a e speci ied in bo h LHS and RHS a e p ese ed by he ule applica ion, elemen s speci ied only in he LHS a e dele ed, and elemen s speci ied only in he RHS a e c ea ed. When a g aph ans o ma ion ule is applied o a g aph, his g aph is called hos g aph o no con use i wi h he LHS and RHS o he ule, which a e also g aphs. Na u ally, he possibili y o applying a g aph ans o ma ion ule o a hos g aph unde lies he condi ion ha a subg aph co esponding o he ule’s LHS can be ound. Fu he mo e, i is also possible ha mul iple ma ching subg aphs exis in a hos g aph. In such a case, mul iple ule applica ions o he same ule can be pe o med. These ule applica ions a e no necessa ily independen . I migh be he case ha a choice has o be made a which ma ch o ans o m he hos g aph, e.g., when di e en ma ches o e lap and each hei espec i e g aph ans o ma ion modi ies elemen con ained in he o he ma ch. A se o g aph ans o ma ion ules oge he wi h an ini ial g aph spans a ansi ion sys em. In his ansi ion sys em, g aphs a e ep esen ed as s a es and g aph ans o ma ions as ansi ions be ween s a es. I is impo an o ealize ha he nonde e minism indica ed by mul iple ou going ansi ions o a s a e has wo sou ces: mul iple ules may be applicable o a g aph and hey may po en ially be applied a mul iple ma ches. The e exis a ious app oaches o ealize g aph ans o ma ions. They a e b oadly classi ied in o connec ing app oaches and gluing app oaches. The main di e ence o hese app oaches is how hey a ach a new eplacemen subg aph o he emainde 1A g aph ans o ma ion ule is also known as g aph p oduc ion, c . [Co +97; Eh +06]. 13 14 CHAPTER 2. BACKGROUND ON GRAPH TRANSFORMATIONS o he hos g aph. Connec ing app oaches in oduce new edges o connec he new subg aph o he emainde g aph. Gluing app oaches iden i y o “glue oge he ” ce ain elemen s o he new subg aph wi h elemen s o he emainde g aph. In he node eplacemen app oach [JR80; ER97], a g aph ans o ma ion eplaces a single node in a g aph wi h a new subg aph. This subg aph is connec ed wi h new edges o he emainde g aph acco ding o an embedding ela ion. The e a e a ious ways o de ine such an embedding ela ion. Consequen ly, he e a e se e al ex ensions and a ia ions o his app oach. All o hese a ia ions belong o he connec ing app oaches. In he hype edge eplacemen app oach [Fed71; Pa 72; DKH97], a hype edge is eplaced by a new hype g aph. This app oach does no equi e an embedding ela ion. The new hype g aph is glued o he emainde hype g aph by iden i y- ing designa ed a achmen nodes wi h nodes o he emainde hype g aph. This app oach belongs o he g oup o gluing app oaches. The e a e wo no able algeb aic app oaches, he double pushou (DPO), which was in en ed by Eh ig e al. [EPS73; Co +97; Eh +06] and he single pushou (SPO) app oach, which was in en ed by Löwe e al. [Löw93; Eh +97]. Bo h app oaches a e based on ca ego y heo y and he ca ego ical e m o a pushou . In DPO, a ans o ma ion is o malized ia wo pushou s in he ca ego y o g aphs and ( o al) g aph mo phisms. One o he pushou s ealizes he dele ion o elemen s and he o he one ealizes hei addi ion. In SPO, only a single pushou is used, which is a pushou in he ca ego y o g aphs and pa ial g aph mo phisms. Bo h app oaches belong o he gluing app oaches. The wo algeb aic app oaches di e in how hey handle ce ain si ua ions. In DPO, he applica ion o a ule is no allowed a a ma ch i i causes one o mo e dangling edges. The DPO app oach also equi es ha no elemen in he hos g aph may ha e mo e han one p eimage unde he ma ch i any o hese p eimages is o be dele ed. The e o e, a ans o ma ion dele es exac ly as many elemen s as speci ied in he ule. The SPO app oach has no such es ic ions on he applicabili y o ules. Dangling edges a e simply dele ed, and si ua ions whe e an elemen in he hos g aph has mul iple p eimages unde he ma ch, one o hem speci ied o be dele ed and he o he one o be p ese ed, a e also esol ed by dele ing he elemen in ques ion. The algeb aic app oaches also ha e al e na i e se - heo e ic p esen a ions, which a e commonly seen in u o ial in oduc ions, e.g. [EKL91; BH02], and include explici cons uc ions o successo g aphs. As o p ac ical ma e s, hei wo kings and ou come a e he same. The successo g aphs o he se - heo e ic and hose o he algeb aic e sions a e equi alen up o isomo phism. We adhe e o he algeb aic e sions, which a e deemed mo e sui able o p oo s han he explici cons uc ions, c . [Co +97, p. 187]. O he well-known app oaches o g aph ans o ma ion a e Cou celle’s monadic second-o de logic o g aphs [Cou90; Cou97], which uses logical o mulas o speci y g aph p ope ies and g aph ans o ma ions, he heo y o 2-s uc u es by Eh en euch el al. [EHR97], which is a ela ional amewo k o he decomposi ion and ans o - 2.1. GRAPHS, GRAPH MORPHISMS, AND PUSHOUTS 15 ma ion o g aphs, as well as app oaches o p og ammed g aph eplacemen [Sch97], which employ con ol p og ams o s ee he applica ion o g aph ans o ma ion ules. The o mal seman ics o imed and du a i e g aph ans o ma ion sys ems, which is p o ided in Chap e 5, ollows he SPO app oach. Howe e , he e is no concep ual es ic ion o he SPO app oach; he p esen ed concep s wo k pe ec ly well in a DPO con ex . This is why he ansla ion o du a i e g aph ans o ma ion sys em models in o PDDL allows o choose whe he o comply wi h he DPO o SPO seman ics. The nex sec ions p esen he undamen als o hese wo app oaches. Sec ion 2.1 lays he algeb aic ounda ion o bo h app oaches. I in oduces he no ions o g aphs, g aph mo phisms, and pushou s. Sec ions 2.2 and 2.3 explain he wo kings o g aph ans o ma ions in he DPO and SPO app oach, espec i ely. Sec ion 2.4 in oduces nega i e applica ion condi ions and illus a es he g aphical ep esen a ion used o g aph ans o ma ion ules in his hesis. The las sec ion, Sec ion 2.5, in oduces he no ions o pa allel and sequen ial independence o g aph ans o ma ions. These no ions play a i al ole in p o ing p ope ies o he seman ics o du a i e g aph ans o ma ion sys ems. The de ini ions p o ided in his chap e a e loosely based on he monog aph Fundamen als o Algeb aic G aph T ans o ma ion [Eh +06] and he i s olume o he Handbook o G aph G amma s and Compu a ion by G aph T ans o ma ion, in pa icula he chap e s on he DPO app oach [Co +97] and he SPO app oach [Eh +97]. The DPO app oach p ima ily ollows he o maliza ion p o ided in [Eh +06]; he SPO app oach ollows ha p o ided in [Eh +97]. The no ions o pa allel and sequen ial independence ollow ha o Habel e al. [HHT96]. We also p o ide less s ic a ian s o pa allel and sequen ial independence ha ake ad an age o he exis ence o isomo phic ma ches. Al hough he idea o g aph ew i ing modulo isomo phism is no new, c . [Plu05], we did no ind de ini ions o pa allel and sequen ial independence modulo isomo phism in ela ed wo k. 2.1 G aphs, G aph Mo phisms, and Pushou s A g aph is a s uc u e ha ep esen s a se o objec s along wi h ela ions be ween hem. He e, we conside only di ec ed g aphs. Undi ec ed g aphs can be simula ed by adding bo h di ec ed edges o each undi ec ed edge. De ini ion 2.1.1 (G aph) . A(di ec ed) g aph G= (VG , EG , s cG , g G) consis s o a se o nodes VG , a se o edges EG , and sou ce and a ge unc ions s cG , g G:EG→VG . This de ini ion o a g aph allows pa allel edges, i.e., edges whose pai o sou ce and a ge node is iden ical o he pai o sou ce and a ge node o ano he edge. Ou seman ics o du a i e g aph ans o ma ions makes use o pa allel edges. Each ead access o a node o edge is ealized as ano he (possibly pa allel) edge. Mul iple concu en ead accesses o he same node o edge hus esul in mul iple pa allel edges. Ano he common de ini ion o g aphs de ines he se o edges such ha 16 CHAPTER 2. BACKGROUND ON GRAPH TRANSFORMATIONS E⊆V×V . Such a de ini ion does no allow pa allel edges. Howe e , i can be used o simula e g aphs ha do suppo pa allel edges, c . [Bon+07]. Rela ions be ween g aphs can be exp essed h ough g aph mo phisms. A g aph mo phism is a mapping o nodes and edges o one g aph o nodes and edges o ano he g aph such ha he sou ce and a ge nodes o edges a e p ese ed. Such mo phisms a e used in g aph ans o ma ion ules o de ine which nodes and edges a e c ea ed, dele ed, o p ese ed when he ule is applied o a g aph. De ini ion 2.1.2 (G aph mo phism, pa ial g aph mo phism) . Ag aph mo phism :G→H be ween wo g aphs is a pai o mappings = ( E , V) wi h E:EG→ EH and V:VG→VH ha commu es wi h he sou ce and a ge unc ions, i.e., V◦s cG=s cH◦ E and V◦ g G= g H◦ E . A g aph mo phism = ( E , V) is called injec i e i E and V a e injec i e and called isomo phic i E and V a e bijec i e. Asubg aph S o G , w i en S⊆G o S,→G , is a g aph wi h VS⊆VG and ES⊆EG such ha s cS=s cG|ES and g S= g G|ES . A pa ial g aph mo phism g om G o H is a ( o al) g aph mo phism om a subg aph o G o H . This subg aph is called he es ic ed domain o g , w i en dom(g) . The ange o a g aph mo phism g0:G→H , w i en an(g0) , is a subg aph S0 o H whe e VS0 is he image se o g0 V and ES0is he image se o g0 E. The applica ion o g aph ans o ma ion ules is based on he concep o “gluing” g aphs oge he . Two di e en g aphs sha ing a common subg aph can be glued oge he by adding he uncommon nodes and edges o bo h g aphs o he common subg aph. This is o malized by he ca ego ical no ion o a pushou . De ini ion 2.1.3 (Pushou ) . Le :A→B and g:A→C be wo mo phisms in a ca ego y C . A pushou (D , 0 , g0) o e and g is de ined by a pushou objec D and mo phisms 0:C→Dand g0:B→Dsuch ha •g0◦ = 0◦gand (commu a i i y) • o all objec s X and mo phisms h:B→X and k:C→X wi h h◦ =k◦g , he e is a unique mo phism x:D→Xsuch ha x◦g0=hand x◦ 0=k. (uni e sal p ope y) AB CD g 0 g0 X x h k = = = 2.2. DOUBLE PUSHOUT APPROACH 17 He e, A is he common subg aph. The pushou objec D is he esul o gluing B and C ia A , , and g . The commu a i i y ensu es ha all elemen s o B and C ha ha e a common p eimage in A a e glued oge he in D . The uni e sal p ope y ensu es ha • elemen s o B and C ha do no ha e a common p eimage in A a e no glued oge he in Dand •Ddoes no con ain elemen s ha nei he exis in Bno C. I elemen s o B and C we e glued oge he in D , hen he e would exis a g aph X o which no mo phism x:D→X sa is ies x◦g0=h and x◦ 0=k , because x had o map he glued elemen simul aneously o di e en elemen s in X o x◦g0=h and x◦ 0=k o hold. I D did con ain elemen s ha exis nei he in B no C , he e would also exis such a g aph, e.g., a subg aph o D ha does no con ain hese elemen s. 2.2 Double Pushou App oach In he double pushou app oach, a g aph ans o ma ion ule connec s i s LHS and RHS ia a so-called gluing g aph 2 , which is a common subg aph o he LHS and RHS. The gluing g aph ep esen s hose nodes and edges ha a e p ese ed du ing he applica ion o he ule. To iden i y hese nodes and edges in he LHS and RHS, wo o al g aph mo phisms a e used. Elemen s o he LHS and RHS ha a e ou side o he ange o hese mo phisms ep esen hose elemen s ha a e being dele ed and c ea ed by he applica ion o he ule, espec i ely. De ini ion 2.2.1 (G aph ans o ma ion ule (DPO)) . Ag aph ans o ma ion ule p= (L , K , R , l , ) consis s o h ee g aphs L , K , and R , called le -hand side (LHS),gluing g aph, and igh -hand side (RHS), espec i ely, and wo injec i e g aph mo phisms l:K→Land :K→R. The seman ics o he applica ion o a ule is gi en by wo pushou s in G aph , he ca ego y o g aphs and ( o al) g aph mo phisms, c . [Eh +06]. The i s pushou handles he dele ion o nodes and edges, he second pushou hei addi ion. Howe e , whe he o no he i s pushou can be cons uc ed depends on he hos g aph and he ma ch o he LHS o he hos g aph. De ini ion 2.2.2 (Applicabili y o a ule (DPO)) . A g aph ans o ma ion ule p= (L , K , R , l , ) is applicable a a ma ch m:L→G , i and only i a con ex g aph D can be cons uc ed such ha he e exis s a pushou (G , l∗ , m) o e l:K→L and k:K→D in G aph. 2The gluing g aph o a g aph ans o ma ion ule is also known as in e ace, c . [Co +97]. 18 CHAPTER 2. BACKGROUND ON GRAPH TRANSFORMATIONS K R D k L G l l∗ m(PO) The con ex g aph is unique up o isomo phism i i exis s. Howe e , i he dele ion o nodes esul s in he exis ence o dangling edges, he con ex g aph canno be cons uc ed. This is because he de ini ion o a g aph does no allow any dangling edges. The pushou can also no be cons uc ed i he images o elemen s in L ha e been me ged by m in o he same elemen in G and a leas one o hese elemen s is no going o be p ese ed. In such a case he uni e sal p ope y o he pushou does no hold. Un o una ely, his de ini ion makes i a he di icul o see whe he a g aph ans o ma ion ule is applicable a a gi en ma ch. Fo una ely, he e exis s an equi alen no ion o a ule’s applicabili y, called he gluing condi ion, c . [Eh +06]. De ini ion 2.2.3 (Gluing condi ion (DPO)) . Le p= (L , K , R , l , ) be a g aph ans o - ma ion ule, Ga g aph, and m:L→Ga ma ch. Then, •GP deno es hose nodes and edges in L , called gluing poin s, ha a e no dele ed by p, i.e., GP =l(K), •IP deno es hose nodes and edges in L , called iden i ica ion poin s, whose images unde m ha e been me ged in o he same elemen in G , i.e., IP ={ ∈ VL|∃w∈VL , w6= :m( ) = m(w)} ∪ {e∈EL|∃ ∈EL , 6=e:m(e) = m( )} , and •DP deno es hose nodes in L , called dangling poin s, whose images unde m a e he sou ce o a ge o an edge in G ha is no con ained in m(L) , i.e., DP ={ ∈VL|∃e∈EG m(EL):s c(e) = m( )∨ g (e) = m( )}. I all iden i ica ion poin s and all dangling poin s a e also gluing poin s, i.e., IP ∪DP ⊆ GP, hen pand msa is y he gluing condi ion (and hus pis applicable a m). I a DPO g aph ans o ma ion ule is applicable a a ma ch m , i s g aph ans o - ma ion is de ined by a double pushou in G aph. De ini ion 2.2.4 (G aph ans o ma ion (DPO)) . Le p= (L , K , R , l , ) be a g aph ans o ma ion ule and m:L→G a ma ch o i s LHS L o a g aph G such ha p is applicable a m . The (di ec ) g aph ans o ma ion 3 om G o H ia p a m , w i en Gp,m =⇒H, is gi en by he pushou s (G,l∗,m)and (H, ∗,m∗)in G aph. 3A (di ec ) g aph ans o ma ion is also known as (di ec ) de i a ion, c . [Co +97] 2.3. SINGLE PUSHOUT APPROACH 19 K R D H ∗ km∗ L G l l∗ m(PO) (PO) The i s pushou esul s in he cons uc ion o a con ex g aph D , which co - esponds o a empo a y, in e media e g aph whe e all dele ion bu no c ea ion is pe o med. Then, he second pushou , which always exis s i he i s pushou exis s, adds new elemen s o he ule’s RHS by gluing hem oge he wi h he con ex g aph. 2.3 Single Pushou App oach In he single pushou app oach, g aph ans o ma ion ules a e de ined by only one mo phism. This mo phism di ec ly maps om he LHS o he RHS, wi hou he use o a gluing g aph. To allow he dele ion o elemen s, his mo phism is pa ial ins ead o o al. In ui i ely, elemen s o he LHS ha a e ou side o he mo phism’s es ic ed domain a e dele ed, and elemen s o he RHS ha a e ou side o he mo phism’s ange a e c ea ed. De ini ion 2.3.1 (G aph ans o ma ion ule (SPO)) . Ag aph ans o ma ion ule p= (L , R , ) consis s o wo g aphs L and R , called le -hand side (LHS) and igh -hand side (RHS), and an injec i e pa ial g aph mo phism :L→R , called ule mo phism. In an SPO g aph ans o ma ion ule, he ule mo phism speci ies bo h addi ion and dele ion. The e o e, he pushou cons uc ion o he SPO app oach is mo e complica ed han o he DPO app oach. In addi ion o he concep o gluing, i has o ealize dele ion. Dele ion is ealized in he SPO app oach by “equalizing” wo pa ial mo phisms ha a e de ined on he same domain o de ini ion bu on di e en es ic ed domains. This is done by emo ing all elemen s om hei ange ha ha e di e en p eimages unde bo h mo phisms. This concep is o malized by he ca ego ical no ion o a co-equalize . The SPO app oach cons uc s a speci ic co-equalize , c . [Eh +97]. I s cons uc ion assumes ha , o each elemen ha is con ained in he es ic ed domains o bo h mo phisms, bo h mo phisms map o he same image. We will see ha his is su icien o he cons uc ion o a pushou in G aphP , he ca ego y o g aphs and pa ial g aph mo phisms, in De ini ion 2.3.3. De ini ion 2.3.2 (Speci ic co-equalize in G aphP ) . Le a , b:A→B be wo (pa ial) mo phisms such ha ∀x∈dom(a)∩dom(b):a(x) = b(x) . The co-equalize o a and bin G aphPis he uple (C,c)whe e •C⊆Bis he la ges subg aph o B a(dom(b)) b(dom(a)) and •c:B→C, wi h dom(c) = C, is he iden i y mo phism on C. 20 CHAPTER 2. BACKGROUND ON GRAPH TRANSFORMATIONS To cons uc C , he co-equalize il e s ou om B all elemen s o which he e is a p eimage unde one o he mo phisms a o b ha is no de ined unde he o he mo - phism. The e o e, only elemen s emain in C ha ha e ei he he same p eimage(s) unde bo h mo phisms o no p eimages a all. Dangling edges a e dele ed because he de ini ion cons uc s C as he g ea es subg aph o B a(dom(b)) b(dom(a)) , which is a g aph-like s uc u e con aining dangling edges. The cons uc ion o a pushou in G aphP is ealized ia wo pushou s in G aph and a co-equalize , c . [Eh +97]. The o al mo phisms o he wo pushou s in G aph a e de ined in dependence on he pa ial mo phism o he pushou in G aphP . The co-equalize is used o ealize dele ion in he cons uc ion o a pushou in G aphP. De ini ion 2.3.3 (Pushou in G aphP ) . Le b:A→B and c:A→C be wo pa ial g aph mo phisms. The pushou o e b and c in G aphP always exis s and can be cons uc ed in h ee s eps: 1. Cons uc he pushou (C0 , A→C0 , C→C0) o he o al mo phisms dom(c)→ Cand dom(c)→Ain G aph. (gluing 1) 2. Cons uc he pushou (D , B→D , C0→D) o he o al mo phisms dom(b)→ A→C0and dom(b)→Bin G aph. (gluing 2) 3. Cons uc he co-equalize (E , D→E) o he pa ial mo phisms A→B→D and A→C→C0→Din G aphP. (dele ion) The pushou o e b and c in G aphP is he uple (E , C→C0→D→E , B→D→E) . dom(c)A CC0 dom(b)B D E (PO) (PO) Since he pushou in G aphP always exis s, he e is no coun e pa o he gluing condi ion in SPO. We can simply de ine he applica ion o an SPO g aph ans o ma- ion ule as a pushou in G aphP. De ini ion 2.3.4 (G aph ans o ma ion (SPO)) . Le p= (L , R , ) be a g aph ans- o ma ion ule and m:L→G a ma ch o i s LHS L o a g aph G . The g aph ans o ma ion om G o H ia p a m , w i en as Gp,m =⇒H , is gi en by he pushou (H, ∗,m∗)o e and min G aphP. L R GH m ∗ m∗ (PO) The mo phisms ∗ and m∗ a e called he de i a ion mo phism and he co-ma ch o Gp,m =⇒H, espec i ely. 2.4. NACS, TYPES, AND VISUAL REPRESENTATION 21 The ma ch m and he ule mo phism co espond o A→C and A→B o De ini ion 2.3.3, espec i ely. Since he ma ch o an LHS o a hos g aph is always o al, he i s pushou in G aph does no do any hing. The second pushou in G aph adds elemen s, simila o he second pushou du ing he applica ion o a DPO ule. Due o he second pushou , A→B→D and A→C→C0→D commu e, which allows o cons uc hei co-equalize . A he end, he co-equalize dele es all elemen s o which he e is a p eimage unde m ha is no de ined unde . Rega dless o whe he o no such an elemen has ano he p eimage unde m ha is de ined unde , he elemen is dele ed. The exis ence o ano he p eimage is no ele an , see De ini ion 2.3.2. To end up in a alid g aph, he co-equalize dele es dangling edges as well. 2.4 Nega i e Applica ion Condi ions, Types, and Visual Rep esen a ion The isual ep esen a ion o g aph ans o ma ion ules used in his hesis ollows he s o y pa e n o malism [De +12]. A s o y pa e n ep esen s a g aph ans o ma ion ule by in eg a ing he LHS and RHS in o one g aph and using s e eo ypes o indica e elemen s ha a e only p esen in he LHS o RHS. :RailCab :T ack:T ack:T ack :RailCab:RailCab :Con oy:Con oy «++» on «++» membe membe on nex on membe nex «- -» on Figu e 2.1: An example o a s o y pa e n Figu e 2.1 shows a s o y pa e n om one o he wo RailCab domains used in his hesis. The s o y pa e n shows a RailCab joining a con oy o RailCabs. Nodes and edges ha a e being c ea ed by he applica ion o he s o y pa e n, i.e., appea only in he RHS, o dele ed, i.e., appea only in he LHS, a e labeled wi h s e eo ypes «++» and «--» and d awn in g een and ed, espec i ely. Elemen s being c ea ed a e also e e ed o as c ea ion node/edge and elemen s being dele ed as dele ion node/edge. This s o y pa e n speci ies he c ea ion o a membe edge ep esen ing he RailCab’s pa icipa ion in he con oy ope a ion simul aneously wi h i s mo emen o he nex ack segmen . To es ic he applicabili y o a ule, a nega i e applica ion condi ion (NAC) can be used. A nega i e applica ion condi ion o bids speci ic g aph s uc u es om being p esen in he hos g aph. The s o y pa e n o malism also allows o exp ess nega i e applica ion condi ions. In Figu e 2.1, he c ossed ou Con oy node and 28 CHAPTER 3. BACKGROUND ON AI PLANNING (RDDL) [San10]. I is he planning language cu en ly used in p obabilis ic acks o IPCs. Fo dis ibu ed and mul i-agen planning, mul iple planning languages ha e been p oposed, some o hem ex ensions o PDDL. The mos ecen and p omising one is Mul i-Agen PDDL (MA-PDDL) [Ko 12]. I suppo s bo h planning o and planning by mul iple agen s, was used in 2015 du ing a mul i-agen planning compe i ion o ganized by he ICAPS Wo kshop on Dis ibu ed and Mul i-Agen Planning (DMAP 2015), and is expec ed o become he inpu language o possible mul i-agen planning acks on u u e IPCs. Fo a bi a y planning p oblems in he p oposi ional STRIPS o malism, deciding he exis ence o a plan is PSPACE-comple e, c . [Byl94]. I ac ions a e only allowed o add bu no o dele e a omic o mulas, i is NP-comple e. Fo una ely, in many anspo a ion domains (whe e he consump ion o uel is no cons ained), a sa is y- ing plan can be ound in polynomial ime, c . [Hel14]. Howe e , inding a sa is ying plan i uel is es ic ed and inding an op imal plan bo h a e NP-comple e. 3.1 PDDL Fundamen als In PDDL, a planning ask is sepa a ed in o a domain and a p oblem desc ip ion. A domain desc ip ion cha ac e izes he mechanics o a domain, i.e., i de ines (pa am- e e ized) ope a ions, called ac ion schema a, as well as objec ypes and p edica es, which a e used wi hin hose ac ion schema a. He e, a p edica e means he se - heo e ic meaning o a p edica e, i.e., a Boolean- alued unc ion. As usual, he e m p edica e e e s o a p edica e symbol (o name), and he e m li e al e e s o an a omic o mula, which is a p edica e symbol oge he wi h a lis o a gumen s, o i s nega ion. P oblem ins ance in o ma ion, like speci ic objec s a ailable in he planning ask’s “wo ld”, a e de ined in p oblem desc ip ions. Such a p oblem desc ip ion also de ines an ini ial s a e, which is ep esen ed as a se o g ound a omic o mulas, and a goal speci ica ion. Mul iple p oblem desc ip ions can be associa ed wi h he same domain desc ip ion, hus yielding di e en planning asks on he same applica ion domain. No e ha s a es ollow he closed-wo ld assump ion: any a omic o mula ha is no known o be ue in a s a e is indeed alse. An ac ion schema wi hin a domain desc ip ion consis s o a lis o pa ame e s, a p econdi ion, and an e ec . In he p econdi ion, a lis o li e als ha a e equi ed o applying he ac ion can be speci ied. Simila ly, he e ec o an ac ion speci ies a lis o li e als ha a e ob ained when he ac ion is applied. An ac ion schema is ins an ia ed – in he con ex o PDDL, his is called g ounding – by subs i u ing he lis o pa ame e s wi h objec s de ined in he p oblem desc ip ion. Since he a gumen s o all li e als a e con ained in he lis o pa ame e s, his ans o ms he li e als in o g ound li e als, which do no con ain any ee a iables. Examples o a domain and an associa ed p oblem desc ip ion a e gi en in Lis ings 3.1 and 3.2. Acco ding o he domain desc ip ion, ehicles can mo e be ween loca ions by consuming uel. To cap u e his possibili y, he domain decla es he 3.1. PDDL FUNDAMENTALS 29 Lis ing 3.1: An example domain descip ion in PDDL [FL03] 1: (de ine (domain ehicle) 2: (: equi emen s :s ips : yping) 3: (: ypes ehicle loca ion uel-le el) 4: (:p edica es 5: (a ? - ehicle ?p - loca ion) 6: ( uel ? - ehicle ? - uel-le el) 7: (accessible ? - ehicle ?p1 ?p2 - loca ion) 8: (nex ? 1 ? 2 - uel-le el) 9: ) 10: (:ac ion d i e 11: :pa ame e s (? - ehicle ? om ? o - loca ion ? be o e ? a e - ⤦ ↪ uel-le el) 12: :p econdi ion (and 13: (a ? ? om) 14: (accessible ? ? om ? o) 15: ( uel ? ? be o e) 16: (nex ? be o e ? a e ) 17: ) 18: :e ec (and 19: (no (a ? ? om)) 20: (a ? ? o) 21: (no ( uel ? ? be o e)) 22: ( uel ? ? a e ) 23: ) 24: ) 25: ) ypes ehicle , loca ion , and uel-le el and ou p edica es ha s a e a which loca ion each ehicle is (line 5), which uel le el each ehicle has (line 6), which loca ion is accessible om which o he loca ion o each ehicle (line 7), and which uel le el ollows which uel le el a e uel has been consumed (line 8). The ac ion schema’s p econdi ion ensu es ha he ehicle is a he s a ing posi ion assumed by he g ound ac ion (line 13), he end posi ion is accessible by he ehicle om he s a ing posi ion (line 14), he ehicle has he uel le el assumed by he g ound ac ion (line 15), and a nex lowe uel le el exis s (line 16). I s e ec changes he ehicles posi ion o he end loca ion (lines 19 and 20) and educes he uel le el o he ehicle (lines 21 and 22). No e ha a iable names always s a wi h a ques ion ma k, and pa ame e s o p edica es o ac ions a e deno ed by a iable names ollowed by hei ype. The gi en p oblem desc ip ion de ines wo ehicles, h ee uel le els, and ou loca ions as a ailable objec s (lines 4 o 6). I s ini ial s a e de ines dynamic s a e in o ma ion, like he posi ions o ehicles and hei uel le el (lines 9 o 12), bu 30 CHAPTER 3. BACKGROUND ON AI PLANNING Lis ing 3.2: A p oblem desc ip ion o he domain o Lis ing 3.1 [FL03] 1: (de ine (p oblem ehicle-example) 2: (:domain ehicle) 3: (:objec s 4: uck ca - ehicle 5: ull hal emp y - uel-le el 6: Pa is Be lin Rome Mad id - loca ion 7: ) 8: (:ini 9: (a uck Rome) 10: (a ca Pa is) 11: ( uel uck hal ) 12: ( uel ca ull) 13: (nex ull hal ) 14: (nex hal emp y) 15: (accessible ca Pa is Be lin) 16: (accessible ca Be lin Rome) 17: (accessible ca Rome Mad id) 18: (accessible uck Rome Pa is) 19: (accessible uck Rome Be lin) 20: (accessible uck Be lin Pa is) 21: ) 22: (:goal (and 23: (a uck Pa is) 24: (a ca Rome) 25: )) 26: ) also s a ic p oblem ins ance in o ma ion, like he connec ions be ween di e en uel le els and loca ions (lines 13 o 20). PDDL p o ides se e al ex ensions o he co e unc ionali y explained abo e, which essen ially cons i u e he STRIPS o malism. The only ex ension al eady used in he examples shown abo e is yping, which allows o use a ype hie a chy o objec s. This ex ension is suppo ed by e e y ele an PDDL-based planning sys em oday. Un o una ely, o he ex ensions a e no suppo ed uni e sally; hei suppo depends on he employed planning sys em. Fo example, he ex ension nega i e p econdi ions enables he use o nega i e li e als in an ac ion’s p econdi ion, which is a e y use ul ea u e in domain modeling. Ano he ex ension, which is made use o in Chap e 6, is equali y. I allows o use he equal sign as a p edica e ha is in e p e ed as equali y. Disjunc ions and quan i ie s can be used in p econdi ions and goals ia he ex ensions disjunc i e p econdi ions and quan i ied p econdi ions, espec i ely. Uni e sally quan i ied and condi ional e ec s can bo h be suppo ed ia he ex ension condi ional e ec s. 3.2. NUMERIC EXPRESSIONS 31 3.2 Nume ic Exp essions To suppo planning domains in ol ing non-bina y esou ces, e sion 2.1 o PDDL in oduced nume ic exp essions. Nume ic exp essions use nume ic- alued unc ions o associa e alues wi h objec s o he domain. The decla a ion o hese unc ions wo ks analogously o ha o p edica es: i equi es only a unc ion name and a lis o a gumen ypes. The suppo o nume ic exp essions can be enabled ia he ex ension luen s. The alue o a nume ic- alued unc ion o a speci ic lis o a gumen s cons i u es a p imi i e nume ic exp ession. Values a e no es ic ed o dis inguished in wha hey ep esen ; hey can ep esen quan i ies o esou ces, coun e s, indices, o some dimension o u ili y. Using a i hme ic ope a o s, a nume ic exp ession can be cons uc ed om se e al p imi i e nume ic exp essions. Nume ic exp essions a e only allowed o appea as pa o nume ic ac s o nume ic assignmen s. A nume ic ac can be used o compa e he alues o wo nume ic exp essions in an ac ion’s condi ion o he condi ion o a condi ional e ec . A nume ic assignmen can be used in he e ec o an ac ion o assign a new alue o a p imi i e nume ic exp ession. Nume ic exp essions a e no allowed in ac ion pa ame e s o as a gumen s o li e als o o he nume ic exp essions. Lis ing 3.3: A domain desc ip ion wi h nume ic exp essions [FL03] 1: (de ine (domain jug-pou ing) 2: (: equi emen s : yping : luen s) 3: (: ypes jug) 4: (: unc ions 5: (amoun ?j - jug) 6: (capaci y ?j - jug) 7: ) 8: (:ac ion pou 9: :pa ame e s (?jug1 ?jug2 - jug) 10: :p econdi ion (>= (- (capaci y ?jug2) (amoun ?jug2)) (amoun ?jug1)) 11: :e ec (and 12: (assign (amoun ?jug1) 0) 13: (inc ease (amoun ?jug2) (amoun ?jug1)) 14: ) 15: ) 16: ) An example using nume ic exp essions is gi en in Lis ing 3.3. The domain models an ac ion o he jugs-and-wa e p oblem, whe e jugs o di e en sizes a e a ailable, and he goal is o achie e a ce ain illing le el o each jug. The e a e wo nume ic- alued unc ion in his domain: a unc ion ha yields he illing le el o each jug (line 5) as well as a unc ion ha yields hei holding capaci y (line 6). The modeled ac ion allows o pou he wa e con ained in one jug in o a second jug unde he condi ion ha he second jug has enough emp y space le o hold he 32 CHAPTER 3. BACKGROUND ON AI PLANNING addi ional wa e . The p econdi ion speci ies his condi ion by use o a nume ic ac calcula ing he emp y space o he second jug and compa ing i wi h he amoun o wa e in he i s (line 10). The e ec speci ies wo nume ic assignmen s: he i s is an absolu e assignmen ha emp ies he i s jug (line 12); he second is a ela i e assignmen inc easing he amoun o wa e in he second jug by ha o he i s jug (line 13). Along wi h nume ic exp essions came plan me ics, which e alua e he quali y o plans based on nume ic exp essions. A plan me ic can be p o ided in he p oblem desc ip ion o de ine an objec i e o he planning p ocess di e en om minimizing he numbe o used ac ions (in sequen ial planning) o he imespan o he en i e plan (in empo al planning). An example o a plan me ic o he ehicles domain is o minimize he amoun o uel used by each ehicle. Ob iously, he domain has o speci y a sui able unc ion o ep esen ing his quan i y and upda e i s alues each ime uel is consumed. No e ha his hesis does no make use o plan me ics o he han he buil -in me ic o al- ime, which e e s o he plan’s imespan. 3.3 Du a i e Ac ions Like nume ic exp essions, du a i e ac ions ha e been in oduced in e sion 2.1 o PDDL. The e a e wo kinds o du a i e ac ions: disc e ized and con inuous du a i e ac ions. He e, we conside disc e ized du a i e ac ions only. Du a i e ac ions spli he li e als, nume ic ac s, and nume ic assignmen s used in each hei p econdi ion and e ec in o di e en se s acco ding o hei ime o e alua ion. They can be equi ed a _s a , o e _all , and a _end when used in he p econdi ion and be e ec i e a _s a and a _end when used in he e ec . While a _s a and a _end e e o he beginning and ending o an ac ion, o e _all e e s o he (open) in e al du ing he ac ion’s execu ion. As a esul , a du a i e ac ion beha es like wo un imed bu empo ally linked ac ions wi h an in a ian condi ion ha mus be me by all s a es occu ing du ing hei applica ion in e al. Wi hou a no ion o ime, plans we e simply in e p e ed as sequences o s a es. Wi h du a i e ac ions, he applica ion in e als o ac ions can o e lap, which leads o he ques ion unde wha cons ain s hey a e allowed o do so. To answe his ques ion, we i s ake a look a he no ion o s a es in his empo al con ex . S a es a e s e ched o e in e als, which a e sepa a ed by poin s in ime on a global clock. S a e change occu s only a hose poin s in ime, and all s a e change a a gi en ime poin occu s ins an aneously. The ime poin s whe e s a e changes occu a e gi en by he beginnings and endings o du a i e ac ions. Mul iple beginnings o endings o di e en ac ions may all a he same poin in ime i hei condi ions and e ec s do no in e e e. In he seman ics o du a i e ac ions, such a se o ac ion beginnings and endings is called a happening and ea ed like an o dina y un imed ac ion. Wi hin a happening, i is no allowed o asse a li e al and i s nega ion a he same ime. I is also o bidden o asse a li e al a he same ime i is equi ed by ano he ac ion’s beginning o ending in he same happening. No condi ion may ely on an e ec in he same happening. E en i he condi ion is ue be o e and 3.4. REQUIRED CONCURRENCY 33 a e execu ing a concu en e ec , i may no ely on he alue o a li e al i he e ec upda es he alue. Fox and Long [FL03] called his he no mo ing a ge s ule. No e ha he beginning o ending o a single ac ion is allowed o access a alue in i s condi ion and upda e i in i s e ec a he same ime. This is only o bidden i pe o med by di e en ac ions, essen ially like mu ual exclusion o sha ed a iables. A simila es ic ion holds o nume ic ac s and assignmen s in happenings. The only di e ence is ha mul iple simul aneous upda es a e allowed i hey commu e, i.e., each o hem is a ela i e assignmen . A consequence o he no mo ing a ge s ule is a non-ze o sepa a ion be ween each pai o happenings: unlike imed au oma a and ela ed cons uc s, whe e he passing o ime is no equi ed be ween wo successi e changes o he logical s a e, wo happenings ha e o occu a leas a minimum ime o ε> 0 apa om each o he . Tempo al planning sys ems o en use a alue o 0.001 as minimum uni o ime. Du a i e ac ions complica e he pic u e o a planning ask’s s a e space in ha hey in ol e a commi men . A du a i e ac ion ha has been s a ed in a s a e, has o be inished a a la e poin in ime. All s a es up o his poin in ime ha e o ul ill he o e _all condi ions o he du a i e ac ion, and he s a e a his poin in ime has o ul ill i s a _end condi ions. Howe e , since he a _end condi ion does no ha e o be ul illed when he ac ion s a s, i can be achie ed by concu en ac ions. Fo his eason, he decision whe he a du a i e ac ion is applicable canno be made alone by looking a all ac ions ha ha e been applied al eady. Ins ead o de ining he seman ics o du a i e ules in e ms o s a e space con- s uc ion, Fox and Long [FL03] de ined i in e ms o execu abili y o happening sequences. Each happening has o ul ill he no mo ing a ge s ule, hei accumu- la ed ac ion beginnings and endings ha e o be execu able in he o de gi en by he happening sequence, and he s a e esul ing by execu ing he comple e happening sequence has o sa is y he goal speci ica ion o he planning ask. The happen- ing sequence also con ains a i icial moni o ing ac ions esponsible o checking in a ian condi ions. These moni o ing ac ions do no con ain any e ec s. They a e placed a e a du a i e ac ion wi h in a ian condi ions has been s a ed and a e each o he happening occu ing du ing i s applica ion in e al. No e ha he sea ch h ough he s a e space migh also conside happening sequences ha a e no execu able, because addi ional du a i e ac ions enabling hei execu abili y ha e no ye been scheduled. 3.4 Requi ed Concu ency The in oduc ion o du a i e ac ions in o planning domains added a scheduling p oblem o he planning asks. A widely used app oach o sol e hese planning asks is o sepa a e logical om empo al easoning and sol e he planning and scheduling p oblems sepa a ely. By ea ing du a i e ac ions as single ins an aneous ac ions – his is called ac ion comp ession [LF03] – and hus neglec ing any oppo uni ies o he concu en execu ion o ac ions, a plan is compu ed by employing a classical 34 CHAPTER 3. BACKGROUND ON AI PLANNING sequen ial planne . A e wa ds, ac ions a e scheduled in a pos -p ocess o achie e a be e plan leng h. As one migh expec , such a p agma ic app oach is e y as . Un o una ely, app oaches ha sepa a e planning and scheduling a e no com- ple e. The e a e planning p oblems o which no sequen ial solu ion exis s. A planning p oblems whe e a leas one ac ion has o be applied concu en ly o ano he ac ion in o de o each he goal is said o ha e equi ed concu ency. Such a planning p oblem canno be sol ed by a sequen ial planning sys em. I a planning p oblem wi h equi ed concu ency can be o mula ed on a planning domain, his domain is said o suppo equi ed concu ency. No e ha a planning p oblem on a domain suppo ing equi ed concu ency does no au oma ically ha e equi ed concu ency i sel ; i is easily possible o model a planning p oblem wi hou equi ed concu ency on any domain. While he e m equi ed concu ency was coined by Cushing e al. [Cus+07] in 2007, i has been known be o e ha planning sys ems sol ing empo al plan- ning asks ia ac ion comp ession and sequen ial planning, like SGPlan [CWH06] o MIPS [Ede03], a e as bu no comple e. Tempo al planning sys ems ha did no pe - o m ac ion comp ession, like LPGP [LF03] o VHPOP [YS03], we e no compe i i e. Fo his eason, Halsey e al. [HLF04] de eloped a planning sys em ha in eg a es scheduling phases in o he planning phase. I s idea is o in eg a e scheduling phases only whe e necessa y, bu pos pone scheduling whe e possible, wi hou sac i icing comple eness. Thei planne CRIKEY and i s successo s CRIKEY SHE [Col+09b] and CRIKEY3 [Col+08] de ec si ua ions whe e his in eg a ion is necessa y by iden i y- ing speci ic pa e ns in condi ions and e ec s o ac ions. I such a pa e n is ound in an ac ion, i s ending is conside ed a choice poin o s a e space explo a ion; o he wise i is simply applied di ec ly o as soon as i is needed [Col+09a]. CRIKEY3 p o ides he code base o se e al s a e-o - he-a planning sys ems de eloped by he Planning G oup a King’s College London 1 , among hem he empo al planning sys em POPF [Col+10], which is used in Chap e 6 o e alua ing di e en planning domains wi h equi ed concu ency. 1 The Planning G oup o Ma ia Fox and De ek Long mo ed om he Uni e si y o S a hclyde o King’s College London in 2011. 4 Planning wi h G aph T ans o ma ions This chap e p esen s an app oach ha allows echnical sys ems o au onomously decide how o econ igu e hei so wa e a chi ec u e by pe o ming planning asks on g aph ans o ma ion sys ems. Focusing solely on s uc u al aspec s, his ap- p oach excludes any iming and concu ency issues. This allows o use o dina y ( yped) g aph ans o ma ion ules o model possible econ igu a ions o he sys em. Classical planning app oaches o ully obse able and de e minis ic en i on- men s wo k wi h no ions o s a e and ac ion: he execu ion o an ac ion esul s in a s a e change. In he case o g aph ans o ma ion planning, s a es a e ep esen ed as g aphs, and hose ac ions a ailable in a planning domain esul om a se o g aph ans o ma ion ules. Mo e p ecisely, a g aph ans o ma ion ule is a pa ame e ized ac ion and g aph ans o ma ions a e g ounded ac ions in which elemen s o he LHS ha e been subs i u ed wi h elemen s om he hos g aph. The ansi ion sys em o a g aph ans o ma ion sys em can be cons uc ed by successi ely applying g aph ans o ma ions o he ini ial g aph and i s successo g aphs. The planning ask is o ind a pa h in his ansi ion sys em ending in a g aph sa is ying a goal speci ica ion. The ansi ions on his pa h cons i u e he plan. Since he ansi ion sys em su e s om a s a e explosion p oblem, i.e., a combina o ial blowup o he s a e space, cons uc ing he comple e ansi ion sys em is no an app op ia e op ion o ind a plan. To ind a plan e icien ly, we need a sui able planning echnique. Planning wi h g aph ans o ma ions has been co e ed be o e, e.g., in [EW11] o coo dina ing beha io in cybe -physical sys ems and in [TK11] o planning a sel -healing p ocess in au omo i e sys ems. The planning p oblems a e usually sol ed by one o he ollowing wo app oaches: ei he a ansla ion in o a dedica ed planning language, like PDDL, is pe o med o a planning sys em is de eloped ha wo ks di ec ly on a g aph ans o ma ion sys em. Un o una ely, bo h app oaches ha e hei d awbacks. Employing a ansla ion-based app oach is emp ing because i exploi s decades 35 36 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS o esea ch in AI planning by applying s a e-o - he-a planning sys ems. Howe e , ansla ion-based app oaches su e om a di e en exp essi eness o GTSs and PDDL: while he c ea ion and dele ion o nodes is a undamen al ea u e o g aph ans o ma ion sys ems, he e is no such hing in PDDL. By no suppo ing he ins an ia ion and deins an ia ion o objec s, PDDL main ains a ini e s a e space. In o de o handle he objec ins an ia ion and deins an ia ion in PDDL ne e heless, a modeling wo ka ound can be used ha decla es all unins an ia ed objec s in he ini ial s a e, bu uses a p edica e o s a e hei ac ual exis ence. Howe e , he wo ka ound is based on he assump ion ha a maximal numbe o objec s is known be o ehand o can be deduced om he g aph ans o ma ion sys em. Un o una ely, planning sys ems wo king di ec ly on he ansi ion sys em o a g aph ans o ma ion sys em a e no highly e ol ed. Up un il oday, he e a e only ew sys ems ha use domain-independen heu is ics o guide hei sea ch h ough he s a e space o a g aph ans o ma ion sys em. Thei domain-independen heu is- ics a e a he simple: hey compu e alues o he s uc u al simila i y o he cu en con igu a ion and he goal speci ica ion. Mul iple such simila i y-based heu is ics a e p esen ed in [EJL06]. Se e al o hem a e di e en a ian s o coun ing hose nodes and edges ha ha e o be c ea ed o dele ed o each a a ge con igu a ion, e.g., hey di e in whe he o no i is allowed o ely on he iden i y o nodes and edges, and hen using his numbe as a dis ance measu e. A sligh ly di e en a ian o such a heu is ic has also been p esen ed in [Sni11]. Ano he idea o a simila i y-based heu is ics gi en in [EJL06] is o ans o m he goal speci ica ion in o a o mula and e alua e how many p edica es o his o mula a e alse in a gi en s a e. O he g aph ans o ma ion planning sys ems no employing domain-independen heu is ics, e.g., semi-au oma ically deducing domain-speci ic heu is ics based on expe knowledge [EW11] o pe o ming en i ely di e en kinds o analyses o guide he sea ch in he s a e space [HHV11], a e explained in mo e de ail in Sec ion 4.5, he ela ed wo k sec ion o his chap e . A p oblem o he a o emen ioned simila i y-based heu is ics is ha hey do no ake any g aph ans o ma ion ules in o accoun . A high simila i y be ween he cu en s a e and he goal speci ica ion is i ele an i he e a e no ules a ailable ha can e icien ly ans o m he cu en s a e in o a s a e sa is ying he goal speci ica ion. The e o e, we belie e ha i is manda o y o an e icien planning sys em wo king di ec ly wi h g aph ans o ma ions o look in o sea ch echniques o s a e-o - he- a AI planning sys ems. Adap ing al eady es ablished echniques om mode n PDDL-based planne s o g aph ans o ma ion sys ems migh be s aigh o wa d in some cases o impossible due o he di e en exp essi eness o g aph ans o ma ion sys ems and PDDL in o he cases, e.g., due o he possibili y o ins an ia ing nodes in g aph ans o ma ion sys ems. Fu he mo e, he p ocess o adap ing such echniques migh lead o ideas ha we e impossible o e y unin ui i e in PDDL-based ep e- sen a ions, e.g., me ging o nodes. This ende s he adap a ion o known planning app oaches o g aph ans o ma ion sys ems an in e es ing esea ch pe spec i e. We de eloped a new planning sys em wo king wi h g aph ans o ma ions, c . [Zie14]. I employs a domain-independen heu is ic unc ion, which can be used 4.1. PROBLEM STATEMENT 37 in combina ion wi h di e en sea ch algo i hms. The heu is ic unc ion is mainly inspi ed by he planning sys em Fas -Fo wa d (FF) [HN01], which is a o wa d- chaining planne wi h a heu is ic unc ion ha uses he solu ion leng h o a elaxed p oblem as heu is ic es ima e. I won he 2nd In e na ional Planning Compe i ion (IPC-2000), which led o a shi o planning esea ch owa ds heu is ic-guided app oaches. Va ian s o i s echniques a e used in many o oday’s s a e-o - he-a planne s, e.g., LAMA [RW10a]. In ou app oach, he elaxa ion is pe o med by ein e p e ing ce ain pa s o he ules’ applica ion condi ions. Thanks o his ein e p e a ion, he elaxed p oblem is easie o sol e han he o iginal p oblem. As pa o his con ibu ion, we compa e he pe o mance o ou heu is ic agains he pe o mance o a simila i y-based heu is ic. The nex sec ion in oduces he no ion o planning p oblems on g aph ans- o ma ions sys ems. The econ igu a ion o ECUs se es as a unning example o his chap e . I s g aph ans o ma ion sys em is p esen ed in Sec ion 4.2 and used in Sec ion 4.3 o explain ou heu is ic app oach. An e alua ion compa ing he pe o mance o ou heu is ic agains he pe o mance o a simila i y-based heu is ic is gi en in Sec ion 4.4. We discuss ela ed wo k in he na ow a ea o g aph ans o - ma ion planning in Sec ion 4.5. Then, we conclude his chap e wi h a discussion on he di e ences o ou heu is ic unc ion o ha employed by FF and an ou look on u he possibili ies o g aph ans o ma ion planne s in Sec ion 4.6. 4.1 P oblem S a emen To de ine he g aph ans o ma ion planning p oblem, we i s need a means o speci y a goal. Such a goal speci ica ion can, o example, be a g aph, which has o be ound by he planning sys em by applying g aph ans o ma ions o he ini ial g aph. In gene al, we do no sea ch o he exac g aph bu o a la ge g aph ha con ains he g aph we a e looking o as a subg aph. We also do no equi e he same iden i y o nodes and edges, i.e., we sea ch o a subg aph isomo phism. Goal speci ica ions also suppo s NACs. The e o e, a goal speci ica ion is so o like a g aph ans o ma ion ule wi hou an RHS. We call his a g aph pa e n. De ini ion 4.1.1 (G aph pa e n) . Ag aph pa e n P= (L , N) consis s o a g aph L and a se o NACs N whe e each NAC ∈ N is a uple NAC = (N , n) wi h n:L→Nand nbeing injec i e. NAC sa is ac ion is de ined as in De ini ion 2.4.1. Ha ing a means o speci ying a ge con igu a ions o a planning p oblem, we can now de ine he planning p oblem i sel . De ini ion 4.1.2 (G aph ans o ma ion planning p oblem) . Ag aph ans o ma ion planning p oblem P= (G0,R,P g )consis s o • an ini ial g aph G0, • a se o g aph ans o ma ion ules R, and • a a ge g aph pa e n P g = (L g ,N g ). 44 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS Table 4.1: Rule applica ion labels o he i s abs ac successo s a e Elemen A ached labels i1 ‹#1, ’des oyIns .’, #1› i2 ‹#1, ’des oyIns .’, #2› ins (c1,i1) ‹#1, ’des oyIns .’, #1› ins (c2,i2) ‹#1, ’des oyIns .’, #2› unning(i1,n1) ‹#1, ’des oyIns .’, #1› unning(i2,n2) ‹#1, ’des oyIns .’, #2› deployed(c1,n2) ‹#1, ’deployComp.’, #1› deployed(c2,n1) ‹#1, ’deployComp.’, #2› gene a ed x successo s a es, whe e x is wo imes he heu is ic alue o he ini ial s a e o he conc e e planning p oblem. This ensu es ha he compu a ion o a heu is ic alue e mina es and ha he sea ch algo i hm can con inue wi h o he s a es i he elaxed p oblem is no sol able om a ce ain s a e. 4.3.2 Rule Applica ion Labels Ou planning sys em pe o ms a s a e space explo a ion by successi ely choosing a s a e and expanding i , i.e., applying each ule a each possible ma ch o gene a e i s successo s a es. To decide which s a e o expand nex , he sys em calcula es a heu is ic alue o each unexpanded s a e. Calcula ing a heu is ic alue o a s a e in ol es gene a ing he abs ac s a e sequence s a ing in his s a e un il we each a s a e ha sa is ies he a ge g aph pa e n. Ha ing cons uc ed he abs ac s a e sequence, a nai e idea would be o use i s leng h as heu is ic es ima e. Al hough he abs ac s a e sequence is expec ed o be sho e o s a es which a e nea o a goal s a e and longe o s a es which a e u he away om a goal s a e, his alue is s ill a he imp ecise. A be e idea is o gi e he app oxima e numbe o indi idual g aph ans o ma ions needed o eaching he (abs ac ) goal s a e. Howe e , we canno simply coun all applied ans o ma ions pe ansi ion o calcula e his numbe , because his would include a lo o ans o ma ions ha we e no needed o each he (abs ac ) goal s a e. The ans o ma ions ha we e needed o each he (abs ac ) goal s a e a e called a elaxed plan and hei numbe is called he leng h o he elaxed plan. Ou app oach o calcula e his numbe inco po a es ule applica ion in o ma ion in o he newly c ea ed elemen s o each successo g aph. Each c ea ed elemen is labeled wi h in o ma ion abou he ans o ma ion ha caused i s c ea ion. This label consis s o he i e a ion numbe o he successo g aph c ea ion loop, he name o he applied ule, and a dis inc iden i ie o he ma ch o he ule o he hos g aph. As an example, he deployed edge om componen c1 o ECU n2 is labeled wi h ‹i e a ion #1, ’ deployComponen ’, ma ch #1›, see Table 4.1 and he second s a e in Figu e 4.5. When he goal ma ch is ound, we can coun he numbe o dis inc ule appli- 4.3. RELAXED PLANNING HEURISTIC 45 Table 4.2: Rule applica ion labels o he second abs ac successo s a e Elemen Di ec ly a ached labels P opaga ed labels i1 ‹#1, ’des oyIns .’, #1› i2 ‹#1, ’des oyIns .’, #2› ins (c1,i1) ‹#1, ’des oyIns .’, #1› ins (c2,i2) ‹#1, ’des oyIns .’, #2› unning(i1,n1) ‹#1, ’des oyIns .’, #1› unning(i2,n2) ‹#1, ’des oyIns .’, #2› deployed(c1,n2) ‹#1, ’deployComp.’, #1› deployed(c2,n1) ‹#1, ’deployComp.’, #2› i3 ‹#2, ’c ea eIns .’, #1› ‹#1, ’des oyIns .’, #1› i4 ‹#2, ’c ea eIns .’, #2› ‹#1, ’des oyIns .’, #2› i5 ‹#2, ’c ea eIns .’, #3› ‹#1, ’deployComp.’, #1› i6 ‹#2, ’c ea eIns .’, #4› ‹#1, ’deployComp.’, #2› ins (c1,i3) ‹#2, ’c ea eIns .’, #1› ‹#1, ’des oyIns .’, #1› ins (c2,i4) ‹#2, ’c ea eIns .’, #2› ‹#1, ’des oyIns .’, #2› ins (c1,i5) ‹#2, ’c ea eIns .’, #3› ‹#1, ’deployComp.’, #1› ins (c2,i6) ‹#2, ’c ea eIns .’, #4› ‹#1, ’deployComp.’, #2› unning(i3,n1) ‹#2, ’c ea eIns .’, #1› ‹#1, ’des oyIns .’, #1› unning(i4,n2) ‹#2, ’c ea eIns .’, #2› ‹#1, ’des oyIns .’, #2› unning(i5,n2) ‹#2, ’c ea eIns .’, #3› ‹#1, ’deployComp.’, #1› unning(i6,n1) ‹#2, ’c ea eIns .’, #4› ‹#1, ’deployComp.’, #2› down(n1,n1) ‹#2, ’shu downEcu’, #1› ‹#1, ’des oyIns .’, #1› down(n2,n2) ‹#2, ’shu downEcu’, #2› ‹#1, ’des oyIns .’, #2› ca ion labels ha a e con ained in he elemen s o he goal ma ch. This numbe is he numbe o ans o ma ions needed o c ea e he elemen s in he goal ma ch. Howe e , hese labels con ains only labels o elemen s ha appea di ec ly in he goal ma ch. I does no ye con ain labels o elemen s ha we e needed o a i e a he goal ma ch. An example o his is he label o he a o emen ioned deployed edge om componen c1 o ECU n2 . While he deployed edge is no con ained in he goal ma ch, i s c ea ion du ing he i s ansi ion was necessa y o he applica ion o ano he ans o ma ion du ing he second ansi ion o c ea e an elemen in he goal ma ch. In his example, he applica ion o c ea eIns ance ha c ea es componen ins ance i5 du ing he second ansi ion equi ed he deployed edge om c1 o n2 . Ou app oach includes labels o such elemen s when coun ing he ule applica ion labels in he goal ma ch: each elemen c ea ed by a ans o ma ion – in addi ion o i s own label – inhe i s he labels o all elemen s in he LHS ma ch o he ule applica ion. In he example abo e, he ule applica ion label o he deployed edge c ea ed du ing he i s ansi ion is p opaga ed o he newly c ea ed ins ance i5 du ing he second ansi ion, see Table 4.2 and he hi d s a e in Figu e 4.5. Elemen s ha ha e been ma ked as dele ed a e handled simila ly. Fo exam- ple, he componen ins ance i1 ecei es he ule applica ion label ‹i e a ion #1, 46 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS ’ des oyIns ance ’, ma ch #1› when i is ma ked as dele ed by he applica ion o he des oyIns ance ule, see Table 4.1. Labels o elemen s being ma ked as dele ed a e p opaga ed o newly c ea ed (o dele ed) elemen s i he labeled elemen is con ained in a NAC ma ch, e.g., he label o i1 is p opaga ed o he down edge a ECU n1 when shu downNode is applied du ing he second ansi ion, see Table 4.2. No e ha elemen s being ma ked as dele ed inhe i labels in he same manne as elemen s ma ked as c ea ed: hey inhe i labels o c ea ed elemen s i con ained in he LHS ma ch and labels o dele ed elemen s i con ained in he NAC ma ch. By inhe i ing he labels o o he elemen s, he elemen s in he goal ma ch do no only con ain labels o ans o ma ions ha di ec ly c ea ed hem, bu also abou all p io ans o ma ions ha made hei c ea ion possible – whe he by means o elemen c ea ion o dele ion. The heu is ic alue is now simply de ined as he numbe o ule applica ion labels ha a e a ached o all elemen s in he goal ma ch. This is easonable because ule applica ion labels ha e been p opaga ed o elemen s in he goal ma ch i he e e enced ule applica ion assis ed in es ablishing he goal ma ch. In doing so, coun ing ule applica ion labels ollows se seman ics, i.e., i elemen s ha we e c ea ed om di e en ans o ma ions sha e he same inhe i ed labels, hese labels a e coun ed only once. In gene al, he ule applica ion label se con ains a leas one label o each i e a ion o he successo g aph c ea ion loop. Applied o he example o Figu e 4.5, he goal ma ch con aining i5 and i2 esul s in a heu is ic alue o 4. This alue comes om wo ule applica ion labels o i5 and he wo o n1 ’s down edge. The ule applica ion label o i2 is no coun ed, because i2 is ma ked as dele ed. I would ha e been coun ed i i2 was con ained in a NAC. When he e exis mul iple goal ma ches p esen in an abs ac s a e, we use he smalle alue. This p e en s om basing he heu is ic alue on a goal ma ch con aining i4 ins ead o i2 . I we had no used he NAC o he unning edge be ween he componen ins ance o c1 and n1 in he a ge g aph pa e n, a goal ma ch con aining i1 and hus a heu is ic alue o 2 would also ha e been possible. Howe e , since we knew om he ini ial con igu a ion ha i1 is unning on an ECU ha is supposed o be shu down, speci ying his NAC was easonable o p e en such an un a o able goal ma ch om being possible. 4.3.3 P og am Code The heu is ic unc ion inco po a es wo impo an unc ionali ies. The i s unc- ionali y is he use o ma kings du ing he c ea ion o abs ac successo g aphs. These ma kings allow o ein e p e NAC ma ching such ha an elemen con ained in he ma ch o a NAC can be dis ega ded i i is ma ked as c ea ed o dele ed. As a consequence, he use o hese ma kings elaxes NAC ma ching and enables – oge he wi h he elaxed LHS ma ching, which esul s om no dele ing elemen s when ans o ma ions a e applied – he pa allel execu ion o all applicable ans- o ma ions. The second unc ionali y is he use o ule applica ion labels and hei p opaga ion o newly c ea ed o dele ed elemen s. These labels allow o coun hose 4.3. RELAXED PLANNING HEURISTIC 47 ule applica ions ha assis ed in eaching he (abs ac ) goal s a e, which cons i u es he heu is ic alue. Nex , we p o ide p og am code o his heu is ic unc ion. I is di ided in o h ee p ocedu es. The i s p ocedu e implemen s he elaxed NAC ma ching unc ionali y. The second p ocedu e is a simple helpe unc ion ha collec s ule applica ion labels om elemen s in he LHS ma ch. The hi d p ocedu e ealizes he heu is ic unc ion and calls he o he wo p ocedu es o do so. Algo i hm 4.1: Relaxed NAC ma ching Inpu : Ma ch m:L→G, NACs N, Se labels Ou pu : Boolean allNacsOk, Se labels 1: p ocedu e checkAllNacMa ches(m,N,labels) 2: o all q:N→Gwi h (N,n)∈ N and q◦n=mdo 3: hisNacOk ← alse 4: o all e∈ an(q)wi h e/∈ an(m)do 5: i eis ma ked as c ea ed hen 6: hisNacOk ← ue 7: b eak .no need o check o he elemen s 8: end i 9: i eis ma ked as dele ed hen 10: hisNacOk ← ue 11: inse labels a ached o ein o labels 12: b eak .no need o check o he elemen s 13: end i 14: end o 15: i ¬ hisNacOk hen 16: e u n alse .no need o check o he NAC ma ches 17: end i 18: end o 19: e u n ue 20: end p ocedu e The i s p ocedu e, checkAllNacMa ches, is gi en in Algo i hm 4.1. Gi en an LHS ma ch and he NACs o a g aph ans o ma ion ule, i checks o each ma ch o a NAC (line 2) whe he i con ains an elemen (line 4) ha may be dis ega ded because i has been ma ked as c ea ed (line 5) o dele ed (line 6). I such an elemen has been ound, he cu en NAC ma ch can be neglec ed unde elaxed NAC ma ching. This also means ha i is no necessa y o check any emaining elemen s in his NAC ma ch (lines 7 and 12). No e ha elemen s ha a e al eady con ained in he LHS a e no conside ed by his check (line 4), because i is no easonable o ega d hem as exis ing o LHS ma ching bu as no p esen o NAC ma ching. As soon as a single NAC ma ch is ound ha con ains no elemen ma ked as ei he c ea ed o dele ed, we know ha his NAC is no sa is ied, despi e he applied elaxa ion. In such a case, he e is no need o check any emaining NACs and 48 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS he p ocedu e e u ns alse (line 16). I each NAC ma ch can be neglec ed due o ma ked elemen s, he p ocedu e e u ns ue (line 19). As a side e ec , his p ocedu e collec s ule applica ion labels om hose elemen s ha allowed neglec ing a NAC ma ch (line 11). This is only done o elemen s ma ked as dele ed bu no o elemen s ma ked as c ea ed, because you need o apply a ans o ma ion o dele ing elemen s bu no o no c ea ing hem. No e ha he se o ule applica ion labels is gi en as a e e ence, i.e., he e is no need o e u n his se . Algo i hm 4.2: Collec ing ule applica ion labels om an LHS ma ch Inpu : Ma ch m:L→G, Se labels Ou pu : Se labels 1: p ocedu e collec RuleApplica ionLabels(m,labels) 2: o all e∈ an(m)do 3: i eis ma ked as c ea ed hen 4: inse labels a ached o ein o labels 5: end i 6: end o 7: end p ocedu e The second p ocedu e, collec RuleApplica ionLabels, is gi en in Algo- i hm 4.2. All i does is collec ule applica ion o hose elemen s ha a e ma ked as c ea ed. I is called om he hi d p ocedu e, ei he wi h an LHS ma ch o wi h a goal ma ch as pa ame e . The p ocedu e ealizing he heu is ic unc ion, compu eHeu is icValue, is gi en in Algo i hm 4.3. Gi en he se o g aph ans o ma ion ules, an ini ial g aph o he elaxed p oblem, he a ge g aph pa e n, and an uppe bound o he leng h o he abs ac s a e sequence, i cons uc s successo s a es un il ei he he mos ecen ly c ea ed successo s a e sa is ies he a ge g aph pa e n o he uppe bound is eached (line 4). The successo g aph c ea ion loop is oughly di idable in o wo pa s. The i s pa (lines 5 o 20) cons uc s he nex abs ac successo s a e. The second pa (lines 22 o 29) checks whe he i sa is ies he a ge g aph pa e n. To cons uc an abs ac successo s a e, he p ocedu e i s sea ches all LHS ma ches o all g aph ans o ma ion ules and checks whe he all hei NAC ma ches a e sa is ied unde elaxed NAC ma ching by calling he p ocedu e checkAllNac- Ma ches (line 9). Fo all LHS ma ches ha sa is y hei NAC ma ches, new elemen s a e c ea ed acco ding o he ule mo phism, bu none a e dele ed (line 11). Then, hese new elemen s a e ma ked as c ea ed (line 12), and elemen s supposed o be dele ed acco ding o he ule mo phism a e ma ked as ‹(line 13). No e ha each o hese elemen s is only ma ked i i has no been ma ked be o e. A e he ma king o elemen s is comple ed, he p ocedu e a aches ule ap- plica ion labels o newly ma ked elemen s. Labels o elemen s ha enabled he ule applica ion by being ma ked as dele ed, i.e., hey allowed o neglec one o he 4.3. RELAXED PLANNING HEURISTIC 49 Algo i hm 4.3: Heu is ic unc ion yielding he leng h o a elaxed plan Inpu : Rules R, G aph G0, G aphPa e n G g , In ege maxLeng h Ou pu : In ege heu is icValue 1: p ocedu e compu eHeu is icValue(R,G0,G g ,maxLeng h) 2: G←G0 3: leng h ←0 4: while leng h ≤maxLeng h do 5: Gsucc ←G 6: o all p= (L,R, ,N)∈Rdo 7: o all m:L→Gdo 8: labels ←∅ 9: allNacsOk ←checkAllNacMa ches(m,N,labels) 10: i allNacsOk hen 11: add c ea ed elemen s o Gp,m =⇒H o Gsucc 12: ma k c ea ed elemen s o Gp,m =⇒Hin Gsucc as c ea ed 13: ma k dele ed elemen s o Gp,m =⇒Hin Gsucc as dele ed 14: collec RuleApplica ionLabels(m,labels) 15: inse ‹leng h,p.name, m.id› in o labels 16: a ach labels o newly ma ked elemen s in Gsucc 17: end i 18: end o 19: end o 20: G←Gsucc 21: leng h ←leng h +1 22: o all g:L g →Gwi h G g = (L g ,N g )do 23: labels ←∅ 24: allNacsOk ←checkAllNacMa ches(g,N g ,labels) 25: i allNacsOk hen 26: collec RuleApplica ionLabels(g,labels) 27: e u n ca dinali y o labels 28: end i 29: end o 30: end while 31: e u n highes possible alue o In ege 32: end p ocedu e NAC ma ches, a e al eady con ained in he se labels due o a side e ec o he p ocedu e checkAllNacMa ches (line 9). Now, he p ocedu e also collec s labels om elemen s ha made he LHS ma ch possible, i.e., elemen s ha a e ma ked as c ea ed and con ained in he LHS ma ch, by calling he p ocedu e collec RuleAp- plica ionLabels (line 14). Then, i also pu s a label o he ule applica ion ha was jus execu ed in o he se labels (line 15) and a aches his se o all elemen s ha ha e been ma ked as c ea ed o dele ed by his ule applica ion (line 16). As 50 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS a consequence, each elemen is labeled wi h bo h a label o he ule applica ion ha c ea ed he elemen and/o i s ma king as well as labels ha made his ule applica ion possible. A e he nex abs ac successo s a e has been c ea ed, he p ocedu e checks whe he his s a e sa is ies he a ge g aph pa e n. Like he applica ion o g aph ans o ma ion ules, his check is pe o med unde elaxed NAC ma ching (line 24). In case i does sa is y he a ge g aph pa en, he p ocedu e collec s labels om elemen s ha a e ma ked as c ea ed and con ained in he goal ma ch be o e e u ning he size o his se as heu is ic alue. Labels om elemen s ma ked as dele ed ha e al eady been collec ed when checking elaxed NAC ma ching. 4.4 E alua ion We compa ed he pe o mance o ou elaxed planning heu is ic ( h p ) agains ha o a simila i y-based heu is ic ( hsim ), which esembles hose heu is ic unc ions employed by Edelkamp e al. [EJL06] and Snippe [Sni11]. The simila i y-based heu is ic coun s he numbe o nodes and edges ha exis in bo h he cu en con igu a ion and he a ge con igu a ion. I elies on he ypes o nodes and edges o judge whe he a node o edge is coun ed as exis ing. Mo e p ecisely, i pu s he ype o each node and edge o a con igu a ion in o a mul ise and akes he ca dinali y o he in e sec ion o he cu en con igu a ion’s mul ise and he a ge con igu a ion’s mul ise as a simila i y measu e. The heu is ic alue is hen de ined as he addi i e in e se o his measu e. Bo h heu is ics ha e been implemen ed in GROOVE [Ren04]. To elimina e any po en ial side e ec s wi h a pa icula sea ch algo i hm, each o he heu is ics was employed mul iple imes in combina ion wi h a di e en sea ch algo i hm. This e alua ion was pe o med on wo di e en p oblem domains. Sea ch algo i hms Bo h heu is ic unc ions we e e alua ed in combina ion wi h g eedy bes - i s and a a ian o en o ced hill-climbing. G eedy bes - i s (GBF) [RN03] is a well-known sea ch algo i hm o in o med sea ch. I uses a closed lis and an open lis o s a es. A e expanding a s a e, i.e., all successo s a es ha e been gene a ed, his s a e is placed in he closed lis . Fo each new successo s a e ound, i s heu is ic alue is compu ed and hen he s a e is placed in he open lis . The decision which s a e o expand nex is solely based on he heu is ic alues o he s a es in he open lis . The cos s o each he cu en s a e a e no conside ed. As a esul , he algo i hm g eedily chooses among all known s a es ha s a e wi h he smalles expec ed dis ance o he goal s a e. We also es ed a a ian o GBF ha di e s om his app oach in ha i also g eedily expands he nex s a e, c . [CS07, Sec . 3.2]. I a successo s a e wi h a be e heu is ic han he cu en s a e is ound, his a ian immedia ely chooses his s a e o expand, wi hou checking any emaining sibling s a es. When his happens, he cu en s a e is no placed in he closed lis ; i emains in he open lis , di ec ly behind he new s a e. By doing so, he heu is ic alues o i s emaining successo 4.4. EVALUATION 51 s a es can be compu ed la e i he new s a e u ns ou o lead o wo se successo s a es. Since he e was no signi ican di e ence in pe o mance be ween hose wo a ian s o GBF, his sec ion includes only esul s o he adi ional a ian . En o ced hill-climbing (EHC) [HN01] is a local sea ch algo i hm. In each i e a ion i pe o ms a b ead h- i s sea ch om he cu en s a e un il i inds a s a e wi h a be e heu is ic alue. When such a s a e is ound, i upda es he cu en s a e and con inues wi h he nex i e a ion. We use a modi ied EHC ha applies bes - i s sea ch ins ead o b ead h- i s sea ch in each i e a ion. This esul s in di e en beha io i EHC encoun e s pla eaus, i.e., egions in he s a e space whe e he heu is ic alues o all successo s a es a e no lowe han he cu en bes heu is ic alue. Using a bes - i s sea ch a he han a b ead h- i s sea ch is expec ed o esul in sho e planning imes o yield sho e plans on some domains, c . [CS07, Sec . 6.3]. P oblem domains The wo p oblem domains used o ou expe imen s a e Blocks Wo ld and ECUs. Blocks Wo ld is a classical p oblem domain in he a ea o AI planning. I consis s o a able wi h a se o cubes ha can be s acked upon each o he . A cube can only be mo ed i he e a e no o he cubes on op o i , and he e is only one a m ha can hold a cube, i.e., wo cubes canno be mo ed simul aneously. Finding an op imal solu ion in his domain has been shown o be NP-ha d [GN92]. The ECUs domain wo ks as explained in Sec ion 4.2. In con as o he Blocks Wo ld domain, which does no in ol e he objec ins an ia ion, he ECUs domain con ains ules c ea ing new nodes. Expe imen se up Fo he Blocks Wo ld domain, we used 8 di e en p oblem sizes (4, 6, 8, 10, 12, 14, 16, and 18 blocks) and 4 di e en p oblem ins ances (2 andom ini ial and 2 andom a ge con igu a ions) pe p oblem size. Fo he ECUs domain, we used 4 di e en p oblem sizes (2, 3, 4, and 5 ECUs), each wi h 4 di e en p oblem ins ances. Two o hese p oblem ins ances had he same numbe o componen ins ances unning in he ini ial con igu a ion as ECUs we e a ailable. The o he wo p oblem ins ances had an addi ional componen ins ance unning. Each a ge con igu a ion speci ied e e y second ECU ( ounding down a odd numbe s o ECUs) o be shu down. The expe imen s we e conduc ed on a Dual In el Xeon E5520 compu e se e wi h 16 ( i ual) co es unning a 2.27GHz. Each expe imen was gi en 4 co es and 4GB o RAM. I no plan could be compu ed wi hin 20 minu es, he job was e mina ed. Resul s Fi s , we gi e an o e iew o he numbe o explo ed s a es o each combina ion o heu is ic unc ion and sea ch algo i hm. The numbe o explo ed s a es coun s only hose s a es ha ha e been chosen o expansion and is gene ally less han he numbe o all gene a ed s a es. The e o e, i is a sui able measu e o 52 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS 1 10 100 1000 10000 100000 1e+06 4blocks 6blocks 8blocks 10 blocks 12 blocks 14 blocks 16 blocks 18 blocks No. o explo ed s a es GBF/hsim EHC/hsim GBF/h p EHC/h p Figu e 4.6: His og am o he numbe o explo ed s a es in Blocks Wo ld domains 1 10 100 1000 10000 100000 1e+06 2ECUs 3ECUs 4ECUs 5ECUs No. o explo ed s a es GBF/hsim EHC/hsim GBF/h p EHC/h p Figu e 4.7: His og am o he numbe o explo ed s a es in ECUs domains 4.4. EVALUATION 53 how well he employed heu is ic p unes he s a e space. No e ha his numbe also does no include abs ac s a es compu ed by h p. Figu e 4.6 shows a his og am o he a e age numbe o s a es o he BlocksWo ld domain, Figu e 4.7 o he ECUs domain. No e he loga i hmic scale in bo h his- og ams. Wi h inc easing p oblem size h p makes i s supe io i y clea . Combina ions wi h hsim ailed o p o ide a solu ion wi hin 20 minu es o he p oblems o size 10 blocks and abo e (on he BlocksWo ld domain) and 5 ECUs (on he ECUs domain). The e is no signi ican di e ence in pe o mance be ween GBF and EHC. Conside ing he a e age planning imes in Figu es 4.8 and 4.9, we can obse e ha hsim pe o ms be e han h p on small domains. The pe o mance o h p on small domains is wo se han ha o hsim because he compu a ion cos s o inding a elaxed plan is in gene al much highe han he compu a ion cos s o coun ing he numbe o nodes and edges in a s a e. Howe e , he pe o mance changes o he a o o h p as he p oblem size inc eases: he planning ime o h p scales be e han he planning ime o hsim . This is expec ed because he numbe o gene a ed s a es also scales be e . No e he small disc epancy be ween he numbe o explo ed s a es and he o al planning ime in he case o 5 ECUs. The numbe o explo ed s a es did no inc ease when swi ching om ins ances wi h 4 ECUs o ins ances wi h 5 ECUs, whe eas he planning ime did inc ease. This can be explained ia he numbe o gene a ed s a es. The numbe o gene a ed s a es inc eased when swi ching om ins ances wi h 4 ECUs o ins ances wi h 5 ECUs. This led o mo e heu is ic alues being calcula ed, which in u n led o mo e and be e candida es being a ailable o u he explo a ion. Be e candida es led o a smalle numbe o s a es chosen o explo a ion due o a smalle a e age plan leng h. Table 4.3: Pe cen age o ime spen calcula ing heu is ic alues in BlocksWo ld domains #blocks 4 6 8 10 12 14 16 18 GBF/hsim 4,58 3,44 4,97 — — — — — EHC/hsim 4,83 3,56 4,18 — — — — — GBF/h p 89,80 93,65 94,31 95,16 97,28 97,81 99,40 99,02 EHC/h p 88,10 92,67 94,62 95,24 97,32 97,77 99,14 99,37 Table 4.4: Pe cen age o ime spen calcula ing heu is ic alues in ECUs domains #ECUs 2 3 4 5 GBF/hsim 3,70 5,02 3,95 — EHC/hsim 3,99 6,74 9,87 — GBF/h p 87,32 94,15 98,38 99,58 EHC/h p 81,60 91,88 98,46 99,74 Nex , we ake a de ailed look a he ime spen o calcula ing heu is ic alues. Tables 4.3 and 4.4 show hese imes in pe cen age o o al planning ime. While hsim consumes only app ox. 4% o he o al planning ime, h p consumes o e 81%, 60 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS li e al laye and an ac ion laye oge he o m a so-called s ep o he planning g aph. Each la e s ep also con ains wo such laye s. The i - h li e al laye con ains hose li e als ha can be asse ed wi hin i s eps. The i - h ac ion laye con ains hose ac ions ha a e applicable gi en he i - h li e al laye . No e ha he i s wo laye s o m s ep 0. A planning g aph has edges be ween nodes o di e en laye s ha mi o he condi ions and e ec s o ac ions. I a li e al in s ep i is con ained in he p econdi ion o an ac ion in s ep i , he e is an edge om he li e al o he ac ion. I an ac ion in s ep i asse s a li e al in s ep i+ 1, he e is an edge om he ac ion o he li e al. These edges enable o conside he ela ion be ween li e als and ac ions when sea ching h ough he planning g aph o a plan. In gene al, planning g aphs also ha e mu ual exclusion edges be ween ac ions ha in e e e wi h one ano he and be ween li e als ha canno be achie ed a he same s ep simul aneously. Howe e , in he case o a elaxed planning ask, he e a e no mu ual exclusion edges because no li e al is e e dele ed, i.e., he elaxed planning g aph is a bipa i e g aph. I a laye is eached ha con ains all goal li e als, a backwa d sea ch o a plan is pe o med. This is done by selec ing an achie e , i.e., a (g ound) ac ion asse ing he li e al, o each li e al in he goal se . Then, his selec ion is ecu si ely applied o all li e als in he p econdi ions o he selec ed ac ions. When his sea ch eaches he i s s ep, no ac ions need o be selec ed anymo e and he se o selec ed ac ions cons i u es he plan. No e ha in gene al, he backwa d sea ch o a plan can equi e back acking when no ac ion can be selec ed ha is no exclusi e o ac ions selec ed ea lie . Since he e a e no mu ual exclusion edges in a elaxed planning g aph, no back acking occu s he e. This is wha makes he sea ch o a elaxed plan in a planning g aph much mo e e icien han he sea ch o a non- elaxed plan. By applying he idea o elaxed planning o g aph ans o ma ion sys ems ins ead o PDDL’s p oposi ional s a e ep esen a ions, we ace mul iple di e ences. These di e ences s em om he ac ha g aph ans o ma ion sys ems, unlike PDDL, suppo objec ins an ia ion and om he in eg a ion o NACs in o he abs ac planning algo i hm. Achie e s and admissibili y In FF’s elaxed planning g aph, a li e al can ha e mul iple achie e s. A elaxed plan is ound by choosing an achie e o each li e al in he goal ma ch and o each un ul illed li e al in he p econdi ion o o he achie e s. Finding he op imal elaxed plan, which esul s in an admissible heu is ic, is NP-ha d, c . [Byl94]. The e o e, FF uses a heu is ic o selec ing achie e s, which p e e s hose ac ions whose p econdi ions a e easie o ul ill. While his does no esul in an admissible heu is ic anymo e, i wo ks well in p ac ice and allows o ind a elaxed plan in polynomial ime. In ou case, he e a e no mul iple achie e s o c ea ed elemen s. Each c ea ed elemen has a ule applica ion label iden i ying he g aph ans o ma ion ha c ea ed i . The e o e, no sea ch o an op imal se o achie e s is necessa y o c ea ed elemen s. Elemen s ma ked as dele ed also ha e only one ule 4.6. DISCUSSION 61 applica ion label, i.e., he label om he i s ule applica ion ha in ended o dele e he elemen . When inding an elemen ma ked as dele ed in a NAC ma ch while collec ing all ule applica ion labels, his amoun s o choosing he i s ans o ma ion ha in ended o dele e his elemen and hus esul ed in his elemen being ma ked. This is simila o FF’s app oach o p e e ing hose ac ions whose p econdi ions a e easie o ul ill. Like he heu is ic o FF, ou heu is ic is no admissible. We can easily c ea e an example domain whe e ou heu is ic unc ion coun s h ee g aph ans- o ma ions, e.g., g aph ans o ma ions ha ha e been applied in pa allel o each he (abs ac ) goal s a e in one i e a ion, al hough a plan o leng h wo exis s, e.g., a plan ha equi es i s wo g aph ans o ma ions o be applied in sequence. In such an example, he o e es ima ion o he cos s o eaching a a ge con igu a ion is essen ially caused by he ea ly e mina ion o he successo g aph c ea ion loop. Objec ins an ia ion The c ea ion o nodes can lead o an explosion o he g aph size du ing he c ea ion o successo g aphs in he abs ac ion. Du ing each i e a ion o he successo g aph c ea ion loop, he size o he nex abs ac s a e g ows. This is because o each applicable ans o ma ion c ea ing one o mo e nodes, all hose nodes a e c ea ed by he pa allel execu ion o hese ans o ma ions. Fu he mo e, each c ea ion o an elemen esul s in a new elemen e en i such an elemen does al eady exis , possibly e en c ea ed by he same ule in an ea lie i e a ion. This inc eases he g aph size o each abs ac successo s a e and hus he ma ching cos s. This is also he eason ha a ge g aph pa e ns a e likely o ha e mul iple ma ches in an abs ac s a e, each wi h a di e en heu is ic alue. Such an explosion o he size o a s a e is no an issue in PDDL-based planne s because hey do no suppo objec ins an ia ion. An idea o educe he numbe o new elemen s pe i e a ion is o me ge all new nodes o he same ype in o a single node. This, howe e , a ec s he p opaga ion o ule applica ion labels. I is no possible anymo e o dis inc ly iden i y he ule applica ion ha was esponsible o c ea ing a new node i he e was mo e han one applicable ans o ma ion c ea ing a node o he new node’s ype. In such a case, we can again p e e hose g aph ans o ma ions whose p econdi ions a e easie o ul ill, i.e., whose LHS ma ches needed less newly c ea ed elemen s and less g aph ans o ma ions o c ea e hem, simila o FF’s heu is ic o selec ing achie e s. Nega i e applica ion condi ions The equi alen o NACs in PDDL a e nega i e exis en ial quan i ica ions o e conjunc i e ac s. They a e usually sol ed by compiling hem away, i.e., ansla ing hem in o DNF, which esul s in a blowup o he p oposi ional domain ep esen a ion, c . [HN01]. In ou app oach, we a oid such a blowup by building he suppo o NACs di ec ly in o he abs ac planning algo i hm. As soon as a g aph elemen ma ked as 62 CHAPTER 4. PLANNING WITH GRAPH TRANSFORMATIONS c ea ed o dele ed is ound wi hin a NAC ma ch, he e is no need o check any emaining elemen s in he same NAC ma ch. We mo i a ed he de elopmen o ou app oach o g aph ans o ma ion planning by a guing abou he need o e ain he exp essi eness o g aph ans o ma ion sys ems when sol ing g aph ans o ma ion planning p oblems and he chances o adap ing al eady known echniques om PDDL-based planning sys ems. Adap ing he idea o FF’s heu is ic unc ion, i.e., using he solu ion leng h o a elaxed p oblem as heu is ic es ima e, is only one o he possibili ies. Ano he possibili y ha we deem p omising is he adap a ion o landma k ecogni ion echniques. Alandma k is a li e al o a se o li e als ha occu s in e e y alid plan. Po eous, Sebas ia, and Ho mann [PSH14] in oduced he no ion o landma ks in 2001. They iden i y landma k candida es ia a backwa d sea ch h ough a elaxed planning g aph and e i y ha hey a e indeed landma ks by checking whe he a elaxed planning g aph wi hou hose ac ions achie ing a landma k candida e eaches a s a e sa is ying he goal. This app oach, which can be pe o med in polynomial ime, is sound bu no comple e. Since checking whe he o no a li e al is a landma k is PSPACE-comple e, c . [HPS04], a comple e app oach is no conside ed wo h he e o . By now, he e a e se e al echniques on inding landma ks. The wo k o Ma zal e al. [MSO11] p esen s a g ea o e iew o he mos ele an echniques and combines hese echniques in o one o inc ease he pe cen age o landma ks ound. When employing a heu is ic based on landma ks, i is also impo an o ind use ul o de ings among landma ks. Landma ks can hen be conside ed as subgoals ha ha e o be eached in sequence o each he goal. They can ei he be used o decompose he planning p oblem in o se e al subp oblems, c . [PSH14], o o de i e a heu is ic ha s a es how many landma ks s ill ha e o be achie ed in he co ec o de . The LAMA planne [RW10a], which won he sequen ial sa is icing ack o he 6 h In e na ional Planning Compe i ion (IPC-2008), uses such a heu is ic in a mul i-heu is ic sea ch, i.e., i al e na es be ween di e en heu is ics, he landma k heu is ic and he heu is ic o FF, o bene i om bo h app oaches o hogonally. The success o he LAMA planne ga e mo i a ion o adap landma ks-based echniques o g aph ans o ma ion planning. A i s s ep in o his di ec ion was made by Ahmadian [Ahm12], who also de eloped a p edecesso e sion o ou g aph ans o ma ion planning app oach, which uses he leng h o he pa allel elaxed plan as heu is ic es ima e. He adap ed a echnique o Zhu and Gi an [ZG03], which p opaga es landma k in o ma ion h ough a planning g aph ia labels. An impo an aspec o his adap a ion conce ns he ep esen a ion o landma ks i sel . In p oposi ional s a e ep esen a ions, a landma k is a li e al. Such a li e al can include in o ma ion abou ela ed objec s, e.g., a li e al wi h wo pa ame e s can exp ess which so wa e componen is deployed on which ECU. This is no as easy in g aph ans o ma ion sys ems, because i is no possible o ely on he iden i y o nodes ha do no ye exis . The e o e, Ahmadian de ined landma ks on he ype le el. Un o una ely, his makes hem imp ecise because hey do no p o ide any s uc u al in o ma ion. A node landma k only s a es ha a node o a ce ain ype has o exis , and an edge landma k only s a es ha an edge o a ce ain edge ype has o 4.6. DISCUSSION 63 exis be ween wo nodes o ce ain ypes. An idea o in eg a e s uc u al in o ma ion in o such landma ks is o conside he combina ion o mul iple edge landma ks in ol ing he same nodes as a landma k on i s own. Such a “highe -o de ” landma k con o ms o wha is known in ela ed wo k as a conjunc i e landma k, c . [KRH10]. 5 Du a i e G aph T ans o ma ion Sys ems This chap e p esen s a o malism o g aph ans o ma ions wi h ime in concu - en con ex s. This o malism, called du a i e g aph ans o ma ion sys ems (DGTS), p o ides concep s o speci y s uc u al econ igu a ions whose execu ion consumes ime as well as dependencies be ween such econ igu a ions. These concep s enable an in ui i e speci ica ion o empo al econ igu a ions on a high le el o abs ac ion. Thei o mal seman ics ha e been designed such ha planning and e i ica ion echniques can be applied easonably. Du a i e g aph ans o ma ion sys ems p o ide h ee kinds o ules: du a i e g aph ans o ma ion ules,concu ency ules, and u gency ules. F om hese h ee kinds o ules, du a i e g aph ans o ma ion ules a e he mos in elligible concep . Syn ac ically, hey a e a s aigh o wa d ex ension o o dina y g aph ans o ma ion ules, i.e., each g aph ans o ma ion ule is anno a ed wi h a na u al numbe ep esen ing i s execu ion ime. The o mal seman ics employs a locking mechanism. The idea o his locking mechanism is simila o concu ency con ol me hods implemen ed by da abase managemen sys ems. Basically, i es ic s ead o w i e access o nodes and edges while hey a e in ol ed in a du a i e g aph ans o ma ion. This gua an ees ha mul iple du a i e g aph ans o ma ions can no be execu ed concu en ly i hey ha e con lic ing needs, c . [ZH13b] Concu ency ules and u gency ules o malize empo al dependencies be ween di e en du a i e g aph ans o ma ion ules. The idea o concu ency ules is inspi ed by he no ion o en elope ac ions [HLF03] in PDDL planning domains. An en elope ac ion is an ac ion whose execu ion ac s as a ime window o ano he ac ion, i.e., he o he ac ion equi es he en elope ac ion o be applied concu en ly. In du a i e g aph ans o ma ion sys ems, we employ concu ency ules o speci y such dependencies. In doing so, we allow he en elope o be a disjunc ion o mul iple ans o ma ions: he e may be mul iple du a i e g aph ans o ma ions 2 ac ing as a ime window o a du a i e g aph ans o ma ion 1 and execu ing any one o hem is su icien o allow he execu ion o 1. 65 66 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS The idea o u gency ules is inspi ed by ha o u gen loca ions, c . [BDL04], and u gen ansi ions, c . [BST99; BT04], bo h concep s o imed au oma a. An u gency ule speci ies ha a ce ain du a i e g aph ans o ma ion 2 has o ollow ano he du a i e g aph ans o ma ions 1 u gen ly, i.e., wi hin a gi en ime ame since he execu ion o 1 inished. No e ha he empo al dependencies speci ied ia concu ency and u gency ules appea on he le el o ans o ma ions, no he le el o ules. Conside an example o wo obo ic a ms: one ule implemen s a obo ic a m o con inuously o a e an objec , ano he ule speci ies a obo ic a m o apply adhesi e o an objec ha is con inuously being o a ed by ano he obo ic a m. In his example, he second ule depends on a concu en applica ion o he i s ule. Howe e , i he e a e mul iple obo ic a ms and objec s, i ma e s which obo ic a m o a es which objec . The e o e, a concu ency ule ha speci ies such a dependency has o include in o ma ion ha de ines how he ma ches o di e en ules ha e o ela e o each o he . The same holds o u gency ules. The o mal seman ics o all hese ules a e based on imed g aph ans o ma ion sys ems, i.e., any gi en du a i e g aph ans o ma ion sys em can be ansla ed in o a imed g aph ans o ma ion sys em. Ob iously, ins ead o speci ying a sys em model as a du a i e g aph ans o ma ion sys ems, a modele could decide o speci y he sys em model di ec ly as a imed g aph ans o ma ion sys ems. Howe e , his would be much less con enien . In he TGTS o malism, he applica ion o ules is imed, bu ins an aneous, i.e., imed g aph ans o ma ions do no consume ime. Ins ead, ime passes in be ween wo consecu i e g aph ans o ma ions. A du a i e g aph ans o ma ion ule could be simula ed ia wo imed g aph ans o ma ion ules, bu his would mean sol ing a p oblem manually and epea edly ha has al eady been sol ed by he seman ics o du a i e g aph ans o ma ion sys ems. Fu he mo e, i would equi e he use o o he cons uc s o imed g aph ans o ma ion sys em, i.e., clock ins ance ules, which enable he measu emen o ime, and in a ian ules, which speci y imed condi ions. Howe e , he manual handling o clock ins ances is a edious du y and can be an e o -p one endea o . Du a i e g aph ans o ma ion sys ems ha e he ad an age ha such clock ins ances a e abs ac ed away and concu en and u gen beha io a e made explici . Due o being based on imed g aph ans o ma ion sys ems, we can make use o he e i ica ion p ocedu es o imed g aph ans o ma ion sys ems p o ided by Heinzemann e al. [HE10] and Suck e al. [SHS11]. The app oach by Heinzemann e al. [HE10] enables o check whe he o no a o bidden g aph exis s in any s a e o a imed g aph ans o ma ion sys em’s s a e space, i.e., i is possible o e i y CTL o mulas o he o m EFφ and AG¬φ . In his app oach, he absence o a o bidden g aph is e i ied by a backwa d ule applica ion om he o bidden g aph o he s a g aph. This has p e iously been done ( o un imed g aph ans o ma ion sys ems) by Becke e al. [Bec+06] bo h ia an explici sea ch and he use o symbolic encodings. The app oach by Suck e al. [SHS11] in oduces a i s -o de a ian o TCTL [ACD93] and enables a e i ica ion o i s -o de TCTL o mulas by ansla ing hem in o TCTL model checking p oblems o imed au oma a. 5.1. APPLICATION EXAMPLE: RAILCAB SYSTEM 67 A e in oducing he unning example o his chap e in he nex sec ion, he syn ax and seman ics o du a i e g aph ans o ma ion ules is p esen ed in Sec- ion 5.2. Being based on imed g aph ans o ma ion sys ems, his sec ion also explains he concep s a ailable in he TGTS o malism. Fo easons o cla i y, he suppo o nega i e applica ion condi ions is le ou o now. Then, Sec ion 5.3 co e s how a du a i e g aph ans o ma ion co ela es wi h an un imed g aph ans o ma ion, he e mina ion o du a i e ules, and possible in e lea ings among mul iple du a i e ules. The DGTS o malism is ex ended successi ely in Sec ion 5.4 o suppo o bidden edges and o bidden pai s, in Sec ion 5.5 o suppo concu - ency ules, and in Sec ion 5.6 o suppo u gency ules. Rela ed wo k in he a ea o g aph ans o ma ions wi h ime is co e ed in Sec ion 5.7. E en ually, Sec ion 5.8 concludes his chap e wi h a discussion on design decisions ega ding he syn ax and seman ics o concu ency and u gency ules. 5.1 Applica ion Example: RailCab Sys em Each o he h ee kinds o ules in he DGTS o malism can be mo i a ed wi h he help o he RailCab sys em, see Sec ion 1.4, which is why we use a domain o he RailCab sys em as a unning example in his chap e . Ins ead o p o iding all ules o he RailCab sys em a once, we show hem as needed, i.e., in in oduc o y pa ag aphs and syn ax sec ions wi hin he emainde his chap e . He e, we gi e a gene al o e iew on how he RailCab sys em is modeled. RailCab d i ing i s las T ack ee S a ion Con oy d i ing Publica ion Base on a pa O membe on publishe dis ibu o moni o s on nex Figu e 5.1: Type g aph o he RailCab domain Figu e 5.1 shows a ype g aph o he ules in he du a i e g aph ans o ma ion sys em ha models he RailCab domain. RailCabs ope a e on a ailway sys em whose physical s uc u e is speci ied as pa o he sys em con igu a ion. The ailway sys em consis s o ack segmen s ha a e connec ed o each o he ia nex edges. A RailCab can occupy one such ack segmen a a ime, which is ep esen ed by an on edge o he ack segmen . Fu he mo e, RailCabs can coo dina e wi h o he RailCabs o o m a con oy. Such an ac i e con oy ope a ion is ep esen ed in a con igu a ion 68 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS by a node o he Con oy ype. A Con oy node has a membe edge o each pa icipa ing RailCab and ep esen s an ac i e ins ance o he RTCP Con oyCoo dina ion as well as one ins ance o he RTCP Dis anceCon ol o each pai o neighbo ing RailCabs in he con oy. The posi ion o each RailCab in he con oy is gi en by he i s edge, las edge, and on edges in a con igu a ion. Wi hin a con oy, he e is a on edge be ween each pai o neighbo ing RailCabs. The i s and las edge a e sel edges ha ep esen he head and ail o he con oy. The applica ion scena io mainly consis s o econ igu a ions o mo e RailCabs o con oys o RailCabs as well as econ igu a ions ela ed o con oy ins an ia ion, deins an ia ion, and membe ship change. Each o hese econ igu a ions will be speci ied as a du a i e g aph ans o ma ion ule. RailCabs d i e slowe i hey a e on hei own because d i ing alone is less ene gy e icien han d i ing in a con oy. The e o e, hese ules will ha e di e en du a ions. Remembe ha RailCabs also ha e o communica e wi h base s a ions o he RailCab sys em. Each RailCab has o be egis e ed a a base s a ion ha moni o s he ack segmen ha he RailCab occupies. This is ep esen ed by an ins ance o he RTCP Publica ion. When a RailCab mo es om a ack segmen moni o ed by one base s a ion o a ack segmen moni o ed by ano he base s a ion, i has o deins an ia e his RTCP and ins an ia e a new one wi h he new base s a ion. This change o he RailCab’s egis a ion is a econ igu a ion ha is equi ed o be execu ed concu en ly o he mo emen o he RailCab. The e o e, his equi emen will be modeled as a concu ency ule. In his applica ion scena io, a RailCab is no allowed o s op ab up ly i i is in d i ing mo ion. To be allowed o s op, a RailCab i s has o b ake while s ill mo ing o one ack segmen ahead. Being no allowed o s op ab up ly means ha he e may be no pause be ween mul iple consecu i e ans o ma ions mo ing a RailCab; hey ha e o be applied con inuously wi hou in e mission. Technically, as soon as a econ igu a ion ha mo es a RailCab o ano he ack segmen inishes (and he RailCab did no b ake du ing his econ igu a ion), ano he econ igu a ion mo ing his RailCab has o s a . This equi emen will be speci ied by means o u gency ules. 5.2 Du a i e G aph T ans o ma ion Rules Adding a no ion o du a ions o g aph ans o ma ion ules is i ial i he execu ion o hese ules is assumed o be s ic ly sequen ial. Howe e , de ining a imed seman ics o g aph ans o ma ion ules allowing a concu en execu ion is di icul due o he many ways mul iple ans o ma ions can in e ac wi h each o he . While unp oblema ic in some cases, he execu ion o mul iple g aph ans o ma ion ules simul aneously, i.e., applying hem o he same con igu a ion in pa allel, can lead o con lic s in o he cases. Technically, du a i e g aph ans o ma ions can be ealized by ansla ing hem in o wo disc e e g aph ans o ma ions ha a e empo ally linked o each o he . One g aph ans o ma ion ep esen s he s a o he du a i e ans o ma ion; a 5.2. DURATIVE GRAPH TRANSFORMATION RULES 69 second one ep esen s i s end. In doing so, du a i e g aph ans o ma ions ha e applica ion in e als, and as a esul , i is possible o apply mul iple du a i e g aph ans o ma ions concu en ly. The ques ion is when o ac ually pe o m he econ igu a ion ha is speci ied by he du a i e g aph ans o ma ion ule. Pe o ming i as pa o he disc e e g aph ans o ma ion ha ep esen s he s a o he du a i e g aph ans o ma ion would no be a easonable solu ion. The s a e o he sys em would be changed long be o e he du a i e ans o ma ion inished i s execu ion. The e o e, we execu e he econ igu a ion as pa o he second disc e e g aph ans o ma ion. Un o una ely, he e migh be con lic s be ween wo du a i e g aph ans o ma- ions i hei ma ches a e allowed o o e lap a bi a ily. Such a con lic can cause disc e e g aph ans o ma ions ep esen ing he end o a du a i e g aph ans o - ma ion no o be applicable when hey a e due. Conside a nai e app oach, which simply uses he applica ion condi ions o hose disc e e g aph ans o ma ions ha ep esen he s a o a du a i e ans o ma ion o decide whe he o no mul iple du a i e g aph ans o ma ions may be applied concu en ly. In his case, a disc e e g aph ans o ma ion ep esen ing he end o a du a i e g aph ans o ma ion migh no be applicable when i is due, because o he g aph ans o ma ions ha ha e been applied concu en ly may ha e in alida ed i s applica ion condi ion. 1:T ack 2:T ack 3:T ack ee 4:T ack ee 1:RailCab d i ing 2:RailCab las 3:RailCab i s c:Con oy d i ing nex nex nex on on membe membe on Figu e 5.2: A con igu a ion in he RailCab domain As an example, conside he con igu a ion gi en in Figu e 5.2 and he wo g aph ans o ma ion ules joinCon oy and dissol eCon oy gi en in Figu es 5.3 and 5.4. Each o hese ules has only one ma ch in he con igu a ion. The ma ch o joinCon oy maps o he Con oy node c , RailCab nodes 1 and 2 , and T ack nodes 1 o 3 , ha o dissol eCon oy o Con oy node c , RailCab nodes 2 and 3 , and T ack nodes 2 o 4 . Le us assume ha one o he wo ules, dissol eCon oy , is cu en ly being applied. This means ha i s condi ion has al eady been checked bu i s ac ual econ igu a ion no ye been execu ed. Le us u he assume ha an execu ion o joinCon oy is scheduled o s a while dissol eCon oy is being execu ed and o end a e he execu ion o dissol eCon oy inished. Since dissol eCon oy ends be o e 76 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS 5.2.3 Locking Edges and Applica ion Indica o s In imed g aphs, locking o nodes and edges is done ia he c ea ion and dele ion o addi ional edges, called locking edges. Elemen s o a con igu a ion a e locked by applying s a ules and unlocked by applying end ules o p e en a concu en access. The e a e sepa a e locking edges o eading nodes, eading edges, w i ing nodes, and w i ing edges. All hese locking edges also ha e espec i e edge ypes in a ype g aph. To gua an ee ha he ma ch o an end ule con o ms wi h an ea lie ma ch o a s a ule, he ma ch o each s a ule has o be emembe ed in a con igu a ion. This is done by adding designa ed nodes, called applica ion indica o s, when applying a s a ule. Such an applica ion indica o has an edge o each node in he ma ch o he s a ule. These nodes indica e he applica ion scope o he du a i e ule ha induced he s a ule. When applying he end ule, we can ensu e con o mi y wi h he s a ule’s ma ch by equi ing he same applica ion scope. To p ope ly indica e o which du a i e ule an applica ion indica o belongs, i s ype is dis inc o each du a i e ule. All induced ules men ioned ea lie a e yped ia a ype g aph o he TGTS o malism. This ype g aph is induced by he ype g aph o he du a i e g aph ans o ma ion sys em unde conside a ion and con ains equi alen ypes and edge ypes. In addi ion o hese ypes and edge ypes, i needs ypes and edge ypes o allow o he c ea ion and dele ion o locking edges and applica ion indica o s. These ypes and edge ypes p o ide he basis o ealizing he locking mechanism and indica ing he ongoing applica ion o a du a i e ule in a con igu a ion. The nex pa ag aphs explain he cons uc ion o an induced TGTS ype g aph ia examples, wi h special a en ion paid o locking edges and applica ion indica o s. I s o mal de ini ion is gi en a e wa ds. To con enien ly e e o locking edge ypes, we use he unc ions lnode :VTG → ETG , wlnode :VTG →ETG , ledge :ETG →ETG , and wledge :ETG →ETG . Each node ype n has wo locking edge ypes, lnode(n ) and wlnode(n ) , as sel edges in he TGTS ype g aph. Fo e e y edge ype e ha is no locking edge ype i sel , he e a e locking edges ypes ledge(e ) and wledge(e ) adjacen o he same sou ce and a ge node ypes. An example o he inducemen o locking edge ypes is shown in Figu e 5.7. In a con igu a ion, an edge o ype lnode(n ) depic s an ob ained ead lock o a node ha has he ype n , and an edge o ype wlnode(n ) depic s an ob ained w i e lock. Simila ly, an edge o ype ledge(e ) depic s an ob ained ead lock o an edge ha has he ype e , and an edge o ype wledge(e )depic s an ob ained w i e lock. Applica ion indica o s a e used o indica e he ongoing execu ion o a du a i e g aph ans o ma ion in a con igu a ion. Thei ou going edges, called applica ion in- dica o edges, ma k he ma ch o he du a i e g aph ans o ma ion ule ha has been used, i.e., he subg aph o he con igu a ion ha is changed by he ans o ma ion. Fo a du a i e g aph ans o ma ion ule wi h he name name , he node ype o he applica ion indica o s i ins an ia es is gi en by aiType(name) ; he edge ype o an edge connec ing he applica ion indica o wi h a node is gi en by aiEdgeType( ). 5.2. DURATIVE GRAPH TRANSFORMATION RULES 77 A B x (a) A DGTS ype g aph A B x wl wl l l wl(x) l(x) (b) I s induced TGTS ype g aph (incomple e, shows only locking edge ypes) Figu e 5.7: Inducemen o locking edge ypes The induced TGTS ype g aph shown in Figu e 5.7(b) is no ye comple e. In addi ion o locking edges, i con ains node ypes o applica ion indica o s: he e is a node ype o each du a i e ule and edge ypes om his node ype o e e y o he node ype used wi hin he ule, i.e., he TGTS ype g aph depends on he se o du a i e ules con ained in he du a i e g aph ans o ma ion sys em. Figu e 5.8 shows he inducemen o a TGTS ype g aph o a du a i e g aph ans o ma ion sys em con aining only a single ule. :A :B :B x«--» x B name := “ExABB” d := 5 (a) A du a i e ule wi h he name ExABB and a du a ion o 5 A B x wl wl l l wl(x) l(x) ExABB unde App1 unde App1 unde App2 (b) An induced TGTS ype g aph o a DGTS con- aining only he ule ExABB Figu e 5.8: Inducemen o a TGTS ype g aph 78 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS Applica ion indica o edges o di e en nodes o he same ype ha e o be dis inguishable o gua an ee ha he ma ch o he s a ule can be in e ed om hem. This is impo an because he end ule o a du a i e ule is supposed o ma ch he same nodes and edges as i s s a ule did. I he e was no possibili y o dis inguish applica ion indica o edges, he end ule would s ill ma ch he co ec se o nodes bu no necessa ily wi h a co ec s uc u e, i.e., i migh no necessa ily ma ch he co ec se o edges. The e o e, applica ion indica o edges o nodes o he same ype a e indi idualized wi h numbe s ha a e dis inc wi hin he ule. Consequen ly, he TGTS ype g aph con ains mul iple applica ion indica o edge ypes om a single applica ion indica o ype o a single node ype n i he applica ion indica o ’s ule speci ies mul iple nodes o ype n , see Figu e 5.8(b). Now, we gi e a o mal de ini ion o he induced TGTS ype g aph. Such a ype g aph is needed by he a ious kinds o ules o he TGTS o malism. In addi ion o he ypes and edge ypes de ined by he DGTS ype g aph, he induced TGTS ype g aph p o ides locking edge ypes and ypes o applica ion indica o s and i s edges. De ini ion 5.2.8 (Induced TGTS ype g aph).Le T G be a ype g aph o a du a i e g aph ans o ma ion sys em. The induced TGTS ype g aph o T G is a ype g aph TG whe e •VTG =VT G ∪VAI, •ETG =ET G ∪EAI ∪ERL.node ∪EWL.node ∪ERL.edge ∪EWL.edge, •|VAI|=|DR| ∧ ∀D ∈ DR :aiType(name)∈VAI, •|EAI|=∑D∈DR |VG,L| ∧ ∀D ∈ DR :∀ ∈VT G :∃EAI0⊆EAI : |EAI0|=|{ ∈VG,L| ype( ) = }| ∧ s c(EAI0) = aiType(name)∧ g (EAI0) = , •|ERL.node|=|VT G | ∧ ∀ ∈VT G : lnode( )∈ERL.node ∧ s c ◦ lnode( ) = g ◦ lnode( ) = , •|EWL.node|=|VT G | ∧ ∀ ∈VT G :wlnode( )∈EWL.node ∧ s c ◦wlnode( ) = g ◦wlnode( ) = , •|ERL.edge|=|ET G| ∧ ∀e ∈ET G : ledge(e )∈ERL.edge ∧ s c ◦ ledge(e ) = s c(e )∧ g ◦ ledge(e ) = g (e ), and •|EWL.edge|=|ET G| ∧ ∀e ∈ET G :wledge(e )∈EWL.edge ∧ s c ◦wledge(e ) = s c(e )∧ g ◦wledge(e ) = g (e ). 5.2. DURATIVE GRAPH TRANSFORMATION RULES 79 The e is exac ly one applica ion indica o o each du a i e ule, and each node in i s LHS has an own applica ion indica o edge ype, which connec s i s ype wi h he applica ion indica o . The la e is so ha applica ion indica o edges o di e en nodes o he same ype a e dis inguishable, which ensu es a co ec ma ch o he end ule. Fo each node ype, he induced TGTS ype g aph has wo locking edge ypes as sel edges, one o eading and one o w i ing. The e a e also wo locking edge ypes o each edge ype ha is no locking edge ype i sel . These locking edge ypes ha e he same sou ce and a ge node as he edge ype. 5.2.4 Timed G aph T ans o ma ion Rules The induced s a ule and end ule o a du a i e g aph ans o ma ion ule a e bo h de ined on op o a imed g aph ans o ma ion ule. A imed g aph ans o ma ion ule is simila o an o dina y g aph ans o ma ion ule, excep ha i ope a es on imed g aphs ins ead o o dina y g aphs. Finding a ma ch o a imed g aph ans o ma ion ule wo ks exac ly in he same way as inding a ma ch o an o dina y g aph ans o ma ion ule. In addi ion o he LHS, RHS, and ule mo phism, a imed g aph ans o ma ion ule speci ies a imed gua d as well as a se o clock ins ances o be ese . The ime gua d is a clock ins ance cons ain ha is exp essed ia clock ins ances con ained in he ule’s LHS. Fo he ule o be applicable, he ime gua d has o be e alua ed o ue. When he ule is applied, hose clock ins ances speci ied in he se a e ese o ze o. De ini ion 5.2.9 (Timed g aph ans o ma ion ule) . A imed g aph ans o ma ion ule = (L,R, ,N,z,V es)consis s o • wo imed g aphs Land R, • an injec i e ule mo phism :L→R wi h (VCI,L) = VCI,R and |VCI,L|= |VCI,R|, • a se o NACs Nwhe e each NAC is a uple (N,n)∈ N wi h n:L→N, • a clock ins ance cons ain z∈ Z(VCI,L), called ime gua d, and • a se o clock ins ances V es ⊆VCI,R. This imed g aph ans o ma ion ule is u he specialized by he induced s a and end ule. In ui i ely, he induced s a ule se es wo pu poses. Fi s , i adds in o ma ion abou he execu ion o he du a i e ule in o he hos g aph. This is needed o he anno a ion o ime and o he end ule o ind a ma ch ha co esponds o he ma ch o he s a ule. Finding a co esponding ma ch is impo an because oge he bo h ules a e supposed o ep esen he applica ion in e al o he du a i e g aph ans o ma ion. Wi h a w ong ma ch he e would be no meaning ul in e p e a ion o he applica ion o a du a i e ule. Second, i adds locking edges in o he hos g aph such ha subsequen ules do no ma ch i hey access he same elemen s in a con lic ing manne . 80 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS De ini ion 5.2.10 (Induced s a ule) . Le D= (LD , RD , D , name , d) be a du a i e ule. The induced s a ule o Dis a imed ule s = (L,R, ,N,z,V es)whe e •VG,L=VLD∧EG,L=ELD, •VG,R=VLD∪ {ai} ∧ ype(ai) = aiType(name)∧EG,R=ELD∪ {e|s c(e) = ai ∧ g (e)∈VG,R {ai} ∧ ype(e) = aiEdgeType ◦ g (e)} ∪ ERL.node,R∪EWL.node,R∪ERL.edge,R∪EWL.edge,R, •VCI,L=VCI,R=∅∧ECI,L=ECI,R=∅, •iL:LD→Lis he iden i y mo phism on LD∧ is o al, •N=NWL.node ∪ NRL.node ∪ NWL.edge ∪ NRL.edge, •z=∅∧V es =∅, •ERL.node,R={le|∃ ∈VG,L:s c(le) = g (le) = ( )∧ ype(le) = lnode ◦ ype( )}, •EWL.node,R={le|∃ ∈VG,L iL◦dom( D):s c(le) = g (le) = ( )∧ ype(le) = wlnode ◦ ype( )}, •ERL.edge,R={le|∃e∈EG,L:s c(le) = s c ◦ (e)∧ g (le) = g ◦ (e)∧ ype(le) = ledge ◦ ype(e)}, •EWL.edge,R={le|∃e∈EG,L iL◦dom( D):s c(le) = s c ◦ (e)∧ g (le) = g ◦ (e)∧ ype(le) = wledge ◦ ype(e)}, •NWL.node ={(N,n)|∃ ∈VG,L:VN=VG,L∧ EN=EG,L∪ {ne} ∧ s c(ne) = g (ne) = n( )∧ ype(ne) = wlnode ◦ ype( )∧nis injec i e}, •NRL.node ={(N,n)|∃ ∈VG,L iL◦dom( D):VN=VG,L∧ EN=EG,L∪ {ne} ∧ s c(ne) = g (ne) = n( )∧ ype(ne) = lnode ◦ ype( )∧nis injec i e}, •NWL.edge ={(N,n)|∃e∈EG,L:VN=VG,L∧ EN=EG,L∪ {ne} ∧ s c(ne) = s c ◦n(e)∧ g (ne) = g ◦n(e)∧ ype(ne) = wledge ◦ ype(e)∧ nis injec i e}, and •NRL.edge ={(N,n)|∃e∈EG,L iL◦dom( D):VN=VG,L∧ EN=EG,L∪ {ne} ∧ s c(ne) = s c ◦n(e)∧ g (ne) = g ◦n(e)∧ ype(ne) = ledge ◦ ype(e)∧ nis injec i e}. The LHS o he induced s a ule is he same as he LHS o he du a i e ule. I s RHS is a copy o he LHS wi h an addi ional node ai , which is i s applica ion indica o , addi ional applica ion indica o edges om ai o all o he nodes in he RHS, and addi ional locking edges ERL.node,R , EWL.node,R , ERL.edge,R , and EWL.edge,R . In ui i ely, he exis ence o an applica ion indica o in he hos g aph indica es he 5.2. DURATIVE GRAPH TRANSFORMATION RULES 81 applica ion o i s du a i e ule, i s applica ion indica o edges ma k he subg aph ha is being changed by he ule applica ion, and locking edges in he hos g aph indica e whe he ead o w i e access o speci ic nodes and edges is locked. The s a ule shall no dele e any node o edge. The e o e, he ule mo phism ( es ic ed o g aph nodes and edges) is o al. Acco ding o he de ini ion o a imed g aph ans o ma ion ule, i is also injec i e, and as a consequence o i s LHS and RHS, unique (up o isomo phism). This allows o a de e minis ic inducemen o s a ules. The se s o clock ins ances, clock ins ance edges, ime gua ds, and clock ins ance ese s a e emp y because a s a ule does no add a clock ins ance measu ing he execu ion ime i sel . Ins ead, he addi ion o a clock ins ance o he execu ion o a du a i e ule is done by a clock ins ance ule, which is p esen ed in Sec ion 5.2.5. The emainde condi ions implemen he locking unc ionali y. The locking edge se s ERL.node,R and ERL.edge,R speci y he c ea ion o a ead lock o e e y equi ed node o edge, espec i ely. The se s EWL.node,R and EWL.edge,R speci y he c ea ion o a w i e lock o e e y node o edge ha is dele ed acco ding o he syn ax o he du a i e ule, i.e., ha is no con ained in iL◦dom( D) . The las ou se s NWL.node , NRL.node , NWL.edge , and NRL.edge de ine NACs ha a e used o check o he exis ence o locking edges. Fo each ead lock, he e is a NAC ha o bids he exis ence o a w i e lock and ice e sa. I he hos g aph con ains pa allel edges, he locking mechanism ope a es mo e es ic i e han necessa y. I any one o mul iple pa allel edges is accessed, his has he e ec o locking all hose pa allel edges. Fo una ely, a less es ic i e locking o pa allel edges can be achie ed wi hou changing he seman ics: g aphs ha suppo pa allel edges can simply be simula ed by g aphs ha do no suppo hem, as done in [Bon+07]. Thus, we can p ep ocess a du a i e g aph ans o ma ion sys em employing pa allel edges by mapping i in o an equi alen du a i e g aph ans o ma ion sys em wi hou pa allel edges. The pu pose o he induced end ule is o ac ually ealize he ans o ma ion ha is syn ac ically speci ied by he du a i e ule and o emo e hose locking edges ha ha e been c ea ed by he s a ule. De ini ion 5.2.11 (Induced end ule) . Le D= (LD , RD , D , name , d) be a du a i e ule. The induced end ule o Dis a imed ule e = (L,R, ,N,z,V es)whe e •VG,L=VLD∪ {ai} ∧ ype(ai) = aiType(name)∧EG,L=ELD∪ {e|s c(e) = ai ∧ g (e)∈VG,L {ai} ∧ ype(e) = aiEdgeType ◦ g (e)} ∪ ERL.node,L∪EWL.node,L∪ERL.edge,L∪EWL.edge,L, •VG,R=VRD∧EG,R=ERD, •VCI,L=VCI,R={ci} ∧ ECI,L={(ci,ai)} ∧ ECI,R=∅, •iL:LD→Lis a subg aph isomo phism ∧ iR:RD→Ris he iden i y mo phism on RD∧ |{VG,L,EG,L}=iR◦ D◦i−1 L∧ |{VCI,L}is o al, 82 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS •N=∅, •z={ci ≥d} ∧ V es =∅, •ERL.node,L={le|∃ ∈VG,L:s c(le) = g (le) = ∧ ype(le) = lnode ◦ ype( )}, •EWL.node,L={le|∃ ∈VG,L dom( ):s c(le) = g (le) = ∧ ype(le) = wlnode ◦ ype( )}, •ERL.edge,L={le|∃e∈EG,L:s c(le) = s c(e)∧ g (le) = g (e)∧ ype(le) = ledge ◦ ype(e)}, and •EWL.edge,L={le|∃e∈EG,L dom( ):s c(le) = s c(e)∧ g (le) = g (e)∧ ype(le) = wledge ◦ ype(e)}. The LHS o he induced end ule is de ined analogously o he RHS o he induced s a ule, i.e., i co esponds o he LHS o he du a i e ule plus an applica ion indica o node, applica ion indica o edges, and locking edges. The RHS o he induced end ule is he same as he RHS o he du a i e ule. The e o e, he applica ion o he end ule emo es he applica ion indica o , he applica ion indica o edges, and he locking edges ha we e c ea ed when he s a ule was applied. The ule mo phism is de ined in con o mi y wi h D , i.e., he end ule ealizes he g aph ans o ma ion syn ac ically speci ied by he du a i e ule. The end ule also includes a ime gua d on he alue o clock ins ance ci , which gua an ees ha he p ope amoun o ime is consumed be o e he end ule is applied. No e ha ci , which is connec ed ia only one edge o ai , is no emo ed by he end ule. This is because imed g aph ans o ma ions may nei he add no emo e clock ins ances o o om a imed g aph. Adding clock ins ances is subjec o clock ins ance ules and emo ing hem is subjec o a single on clock ins ance emo al ule. Bo h a e co e ed in Sec ion 5.2.5. Figu e 5.9 shows an example o a du a i e g aph ans o ma ion ule and i s induced s a and end ule. The du a i e ule is named ExAB and speci ies he emo al o an edge x du ing an in e al o 5 ime uni s, see Figu e 5.9(a). I s induced s a ule speci ies an applica ion indica o node ExAB o be c ea ed, along wi h wo applica ion indica o edges, one o he node o ype A and one o he node o ype B , see Figu e 5.9(b). He e, he a ge nodes o bo h applica ion indica o edges a e o di e en ype. The e o e, bo h edges a e labeled wi h unde App1 . I bo h a ge nodes we e o he same ype, one o he applica ion indica o edges would ha e been labeled wi h unde App2 ins ead. Since bo h o hese nodes a e p ese ed in he du a i e ule, only hei ead access is locked by an a ached c ea ion edge l in he s a ule. Fo he edge, which is dele ed in he du a i e ule, bo h i s ead and w i e access a e locked by a ached c ea ion edges l(x) and wl(x) . Fu he mo e, o bidden edges allow he applica ion o he s a ule only i w i e access o he p ese ed nodes and bo h w i e and ead access o he dele ion edge a e no locked. The end ule dele es he applica ion indica o node, i s adjacen edges, and all locking edges ha he s a ule c ea es, see Figu e 5.9(c). The applica ion indica o 5.2. DURATIVE GRAPH TRANSFORMATION RULES 83 :A :B «--» x name := “ExAB” d := 5 (a) A du a i e ule wi h he name ExAB and a du a ion o 5 :A :B x wl wl «++» l «++» l wl(x) l(x) «++» l(x) «++» wl(x) «++» :ExAB «++» unde App1 «++» unde App1 (b) I s induced s a ule :A :B «--» x «--» l «--» l «--» l(x) «--» wl(x) «--» :ExAB «--» unde App1 «--» unde App1 ci:Clock «--» hasNode z := {ci ≥5} (c) I s induced end ule Figu e 5.9: Inducemen o s a and end ule edges ensu e ha he ma ch o he end ule co esponds o he ma ch o he s a ule when he end ule is applied. No e ha i he e we e mul iple nodes o he same ype in he du a i e ule, he applica ion indica o edges being added o hese nodes by he induced s a ule would be o di e en edge ypes o ensu e a co ec ma ch o he end ule. The ime gua d z={ci ≥ 5 } is a condi ion o he ule’s applica ion. I gua an ees ha he ule canno be applied be o e 5 ime uni s ha e been passed on he clock ins ance ci . In he g aphical ep esen a ion, he clock ins ance he ime gua d e e s o can be iden i ied ia i s objec name. In he o mal syn ax, we can simply use a iable names o make clea o which clock ins ance a ime gua d e e s 84 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS o. The e o e, we did no de ine such objec names in he syn ax o imed g aphs o imed g aph ans o ma ion ules. The ime gua d only gua an ees ha he induced end ule is no applied oo ea ly. We also need o ensu e ha i is no applied oo la e. Mo e p ecisely, we need o en o ce he applica ion o he ule as soon as i s ime gua d is ul illed. In o de o do his, we use in a ian ules, which a e o mally explained in he nex sec ion. 5.2.5 Clock Ins ance and In a ian Rules In Sec ion 5.2.2, we explained ha clock ins ances pe ain o pa s o a con igu a ion – as opposed o imed au oma a, whe e clocks pe ain o he comple e au oma on. Since i is impossible o decide a design ime how many clock ins ances a imed g aph ans o ma ion sys em needs, clock ins ances ha e o be ins an iable. Thei ins an ia ion could simply be suppo ed by allowing imed ules o add clock ins ances; howe e , he designe s o he imed g aph ans o ma ion o malism decided o pu his unc ionali y in o sepa a e ules, called clock ins ance ules. This decision can easily be explained by looking a he implemen a ion o in a ian s. In a ian s a e ealized as in a ian ules in he TGTS o malism. In a ian ules s a e how long a speci ic s uc u e is allowed o exis . This s uc u e ep esen s a pa o a con igu a ion. I does no ma e which ans o ma ions esul ed in his con igu a ion o whe he i is he esul o a single o mul iple ans o ma ions. Since an in a ian does no ca e which imed ans o ma ion led o a con igu a ion, why should a clock ins ance ca e? By pu ing he c ea ion and dele ion o clock ins ances in o sepa a e ules, he exis ence o a clock ins ance in a con igu a ion depends en i ely on i s s uc u e, no on wha happened be o e. Clock ins ance ules iden i y hose pa s o a con igu a ion ha clock ins ances pe ain o. They wo k simila o imed ules; howe e , hey a e speci ied such ha hey do no dele e any hing and c ea e only a single clock ins ance as well as edges adjacen o his clock ins ance. To p e en he c ea ion o mo e han one clock ins ance o he same pa o he con igu a ion, he ule speci ies a NAC ha is iden ical o i s RHS. De ini ion 5.2.12 (Clock ins ance ule) . Aclock ins ance ule c = (L , R , , N) consis s o wo imed g aphs L and R , a ule mo phism :L→R , and a nega i e applica ion condi ion (N,n)∈ N whe e •VG,L=VG,R∧EG,L=EG,R, •VCI,L=∅∧ |VCI,R|=1∧ |ECI,R| ≥ 1, • is o al, and •N=R∧n= ∧ |N | =1. In ea ly a ian s o he imed g aph ans o ma ion o malism [Neu07; Hi 08], clock ins ance ules ha e been de i ed om imed ules and in a ian ules. La e a ian s, such as [SHS11; Eck+13], also allow hei explici speci ica ion. Bo h a ian s 5.2. DURATIVE GRAPH TRANSFORMATION RULES 85 a e sui able o a seman ics o du a i e ules. He e, we ollow he la e app oach, i.e., we explici ly de ine he induced clock ins ance ule o a gi en du a i e ule. An induced clock ins ance ule has only an applica ion indica o node in i s LHS. The e o e, i a aches a clock ins ance only i a s a ule ha has been induced by he same du a i e ule has been applied be o e. Since he applica ion indica o is yped ia he name o he du a i e ule, he e is exac ly one induced clock ins ance ule o each du a i e ule. De ini ion 5.2.13 (Induced clock ins ance ule) . Le D= (LD , RD , D , name , d) be a du a i e ule. The induced clock ins ance ule o Dis a ule c = (L,R, ,N)whe e •VG,L=VG,R={ai} ∧ ype(ai) = aiType(name)∧EG,L=EG,R=∅and •VCI,L=∅∧ECI,L=∅∧VCI,R={ci} ∧ ECI,R={(ci,ai)}. The ope a ional seman ics in Sec ion 5.2.6 is designed such ha all applicable clock ins ance ules a e applied immedia ely a e a imed ule has been applied. Upon applica ion, an induced clock ins ance ule a aches a clock ins ance o an applica ion indica o node ha is no ye connec ed o a clock ins ance. Since s a ules c ea e applica ion indica o nodes, a clock ins ance ule c ea es a clock ins ance di ec ly a e a s a ule has been applied. I he pa o he con igu a ion ha he clock ins ance pe ains o is no longe p esen , he clock ins ance needs o be emo ed as well. This is he case when an end ule is applied because each applica ion o an end ule emo es an applica ion indica o . Remo ing he clock ins ance is subjec o a clock ins ance emo al ule. Fo a gi en se o clock ins ance ules, a clock ins ance emo al ule can be de i ed au oma ically. I has a single clock ins ance as i s LHS and an emp y RHS. In addi ion, i speci ies he RHSs o all clock ins ance ules as NACs. As a consequence, he clock ins ance emo al ule dele es a clock ins ance i he pa o he con igu a ions ha he clock ins ance pe ains o is no longe p esen . The e is only one clock ins ance emo al ule o he comple e imed g aph ans o ma ion sys em. De ini ion 5.2.14 (Clock ins ance emo al ule) . Le CR be a se o clock ins ance ules. A clock ins ance emo al ule o CR is a ule CR = (L,R, ,N)whe e •VG,L=VG,R=∅∧EG,L=EG,R=∅, •VCI,L={ci} ∧ VCI,R=∅∧ECI,L=ECI,R=∅, •N={(N , n)|∃c = (Lc , Rc , c , Nc )∈CR :N=Rc ∧n:L→N wi h n(ci)∈VCI,Rc }. In a ian ules, which s a e how long a speci ic pa o a con igu a ion is allowed exis , speci y only an LHS. The e is no need o an RHS, because in a ian ules do no pe o m ans o ma ions. The LHS o an in a ian ule con ains an a bi a y numbe o g aph node and edges, bu exac ly one clock ins ance. They also speci y a clock ins ance cons ain . 92 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS p= (LD , RD , D) and he g aph G= (VG , EG) be a p ojec ion o D and TiG o he un imed case. I and only i he e is a ma ch g:LD→G and a (di ec ) g aph ans o ma ion GD,g =⇒H , hen he e a e ma ches m:Ls →TiG and x:Le →TiG0 and ansi ions hTiG,νis ,m ==⇒ hTiG0,ν0id =⇒ hTiG0,ν00ie ,x =⇒ hTiH,νisuch ha H= (VH,EH)and TiH = (HTiH, ypeTiH)wi h HTiH = (VH,∅,EH,∅). P oo . Le iG:G→TiG deno e he isomo phism be ween Gand TiG|{VG,EG}. Fi s , we show ha , gi en he ma ch g:LD→G , we can de ine he ma ches m:Ls →TiG and x:Le →TiG0 such ha H=TiH|{VH,EH} . Since Ls =LD and TiG|{VG,EG}=G hold, we can de ine m=iG◦g◦i−1 L,s . Then, we can cons uc TiG0 and ν0 acco ding o he ope a ional seman ics gi en in De ini ion 5.2.21. TiG0 now con ains one clock ins ance ci and ν0(ci) = 0. Acco ding o Lemma 5.3.1, he e is a unique (up o isomo phism) ma ch x:Le →TiG0 wi h x◦iL,e = ∗ m◦m◦iL,s and ansi ions hTiG0 , ν0id =⇒ hTiG0 , ν00ie ,x =⇒ hTiH , νi . Since m=iG◦g◦i−1 L,s and x◦iL,e = ∗ m◦m◦iL,s hold, we ha e x= ∗ m◦iG◦g◦i−1 L,e . Since ∗ m is o al, H=TiH|{VH,EH}holds. Second, we show ha , gi en he ma ches m:Ls →TiG and x:Le →TiG0 , we can de ine he ma ch g:LD→G such ha H=TiH|{VH,EH} . Since LD⊆Le holds, we can de ine g=i−1 G◦x◦iL,e . Then, we can cons uc H acco ding o he SPO app oach. Since D=i−1 R,s ◦ e |{VG,L,EG,L}◦iL,e and g=i−1 G◦x◦iL,e hold, we ha e H=TiH|{VH,EH}. In ui i ely, he esul ing g aphs H and TiH|{VH,EH} a e iden ical due o h ee ac s. Fi s , execu ing he s a ans o ma ion lea es he essen ial pa s o he g aph unchanged. Second, all locking edges and special nodes, i.e., applica ion indica o s and clock ins ances, ha a e c ea ed by execu ing he s a ans o ma ion a e dele ed again by execu ing he end ans o ma ion. Thi d, he end ans o ma ion ealizes a g aph ans o ma ion ha con o ms o he un imed g aph ans o ma ion – o be p ecise, hei RHSs a e he same. 5.3.2 Rule Te mina ion and In e lea ing T ansi ion Sequences The applica ion in e al o a du a i e g aph ans o ma ion is de ined by he delay ansi ion ha is execu ed be ween he applica ion o i s induced s a and end ule. A an a bi a y poin in ime du ing i s applica ion in e al, an induced s a o end ule o ano he du a i e ule can be applied. This is in ended; o he wise, no concu en execu ion would be possible. The ques ion is whe he he end ule o an ongoing du a i e ans o ma ion can s ill be applied i one o mo e s a o end ules induced by o he du a i e ules ha e been applied du ing i s applica ion in e al. The DGTS seman ics is designed such ha his wo ks, i.e., du a i e ans o ma ions a e gua an eed o inish once hey ha e been s a ed. This is o malized in Theo em 5.3.6. 5.3. PROPERTIES OF DURATIVE GRAPH TRANSFORMATION RULES 93 The concu en applica ion o wo du a i e g aph ans o ma ion ules means ha hei induced s a and end ules a e applied in an in e lea ing manne . Mul iple such in e lea ings a e possible and each such in e lea ing esul s in he same con igu a ion. This is o malized in Theo em 5.3.7. Bo h o hese p ope ies build upon some lemmas, which a e o malized i s . Each o hese lemmas gi es he sequen ial o pa allel independence be ween wo applica ions o induced ules. We can hen apply he Local Chu ch-Rosse Theo em, see Theo em 2.5.1, which s a es ha wo sequen ial o pa allel independen (di ec ) g aph ans o ma ions can be applied in any o de and bo h o de ings esul in he same g aph. This is use ul when p o ing Theo ems 5.3.6 and 5.3.7. The i s lemma conside s wo induced s a ules ha a e applied in sequence. Lemma 5.3.3 (Sequen ial independence be ween wo s a ans o ma ions) . Le D1 and D2 be wo du a i e ules, TiG = (GTiG , ypeTiG) a imed g aph wi h GTiG = (VG , VCI , EG , ECI) , and ν a clock ins ance alue assignmen such ha ν|=TiG . The induced s a ules o D1 and D2 a e deno ed by s 1 and s 2 , espec i ely. Fu he , ci1 deno es he clock ins ance exis ing du ing he applica ion in e al o D1 and d1 i s du a ion. I he e a e wo ac ion ansi ions hTiG , νis 1,m1 ===⇒ hTiH1 , ν0i wi h ν0(ci1) = 0and hTiH1 , ν00is 2,x2 ==⇒ hTiX , ν000i wi h 0 ≤ν00(ci1)≤d1 , hen hey a e sequen ially indepen- den . P oo . We ha e o show ha (i) hTiH1 , ν00is 2,x2 ==⇒ hTiX , ν000i is weakly sequen ially independen o hTiG , νis 1,m1 ===⇒ hTiH1 , ν0i and (ii) hTiG , νis 1,m1 ===⇒ hTiH1 , ν0i is weakly pa allel independen o hTiG,νis 2,m2 ===⇒ hTiH2,ˆ νi. (i) TiG TiX Ls 1 Rs 1 s 1 Ls 2 Rs 2 s 2 TiH1 m1 m∗ 1 ∗ m1 TiH2 m2 m∗ 2 ∗ m2 x2 x∗ 2 ∗ x2 Since he e a e no applica ion indica o s o locking edges in he LHS o s 2 (and hus he e a e none in he ange o x2 ) and hTiG , νis 1,m1 ===⇒ hTiH1 , ν0i c ea es only such elemen s, an(x2)∩TiH1 an( ∗ m1) = ∅ holds. Thus, we can cons uc m2:Ls 2→TiG such ha ∗ m1◦m2=x2. NACs Fu he mo e, m2 ul ills each NAC in Ns 2 because hTiG , νis 1,m1 ===⇒ hTiH1 , ν0i does no dele e any elemen s o TiG when de i ing TiH1 and x2 al eady ul ills each NAC in Ns 2by de ini ion. 94 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS (ii) TiG TiX Ls 1 Rs 1 s 1 Ls 2 Rs 2 s 2 TiH1 m1 m∗ 1 ∗ m1 TiH2 m2 m∗ 2 ∗ m2 x1 x∗ 1 ∗ x1 Since hTiG , νis 2,m2 ===⇒ hTiH2 , ˆ νi does no dele e any elemen s o TiG when de i ing TiH2 , an(m2)∩TiG dom( ∗ m1) = ∅ holds. Thus, we can cons uc x1:Ls 1→TiH2such ha x1= ∗ m2◦m1. NACs We show ha x1 ul ills each NAC in Ns 1 by con adic ion. Le us assume ha hTiG , νis 2,m2 ===⇒ hTiH2 , ˆ νi c ea es locking edges ha con lic wi h a NAC in Ns 1 , i.e., he e is a ma ch q1:Ns 1→TiH2 wi h q1◦ns 1=x1 and (Ns 1,ns 1)∈ Ns 1such ha an(q1)∩TiH2 an( ∗ m2)6=∅. Acco ding o De ini ion 5.2.10, each NAC ha ealizes a check o a ead lock [w i e lock] is accompanied by a aching a w i e lock [ ead lock] o he same elemen and ice e sa. Thus, hTiG , νis 1,m1 ===⇒ hTiH1 , ν0i c ea es locking edges ha con lic wi h a NAC o s 2 , i.e., he e is a ma ch q2:Ns 2→TiH1 wi h q2◦ns 2=x2 and (Ns 2 , ns 2)∈ Ns 2 such ha an(q2)∩TiH1 an( ∗ m1)6=∅ . This is a con adic ion o he applicabili y o hTiH1,ν00is 2,x2 ==⇒ hTiX,ν000i. In ui i ely, Lemma 5.3.3 holds due o wo ac s: 1. The la e s a ans o ma ion only adds elemen s o he hos g aph bu dele es none, hus canno con lic wi h he applicabili y o he ea lie s a ans o ma ion. In o he wo ds, he e canno be a use-dele e con lic . 2. Since no NAC o he la e s a ans o ma ion ma ches, i.e., he wo ans- o ma ions a e ee o p oduce- o bid con lic s, and he locking mechanism is designed symme ically, hey also ha e o be ee o o bid-p oduce con lic s. The nex lemma conside s an end ans o ma ion being applied a e a s a ans o ma ion. Ins ead o “o dina y” sequen ial independence, i s a es sequen- ial independence modulo isomo phism. O dina y sequen ial independence is no su icien due o he sha ed ead locks. A locking edge c ea ed by he s a ans o - ma ion can be dele ed by he end ans o ma ion i bo h ans o ma ions ead he same elemen . Howe e , in such a case, he e exis s ano he locking edge, which is isomo phic o he i s one. Lemma 5.3.4 (Sequen ial independence modulo isomo phism be ween a s a and an end ans o ma ion) . Le D1 and D2 be wo du a i e ules, TiG = (GTiG , ypeTiG) a imed g aph wi h GTiG = (VG , VCI , EG , ECI) , and ν a clock ins ance alue assignmen such ha ν|=TiG and hTiG , νi is eachable om he ini ial con igu a ion. The induced s a ule 5.3. PROPERTIES OF DURATIVE GRAPH TRANSFORMATION RULES 95 o D1 and end ule o D2 a e deno ed by s 1 and e 2 , espec i ely. Fu he , ci1 deno es he clock ins ance exis ing du ing he applica ion in e al o D1 and d1 i s du a ion. Also, ais 1 and aie 2 deno e he applica ion indica o in he RHS o s 1 and he LHS o e 2 , espec i ely. I he e a e wo ac ion ansi ions hTiG , νis 1,m1 ===⇒ hTiH1 , ν0i wi h ν0(ci1) = 0and hTiH1 , ν00ie 2,x2 ==⇒ hTiX , ν000i wi h 0 ≤ν00(ci1)≤d1 and x2(aie 2)6=m∗ 1(ais 1) , hen hey a e sequen ially independen modulo isomo phism. P oo . We ha e o show ha (i) hTiH1 , ν00ie 2,x2 ==⇒ hTiX , ν000i is weakly sequen ially in- dependen modulo isomo phism o hTiG , νis 1,m1 ===⇒ hTiH1 , ν0i and (ii) hTiG , νis 1,m1 ===⇒ hTiH1 , ν0i is weakly pa allel independen modulo isomo phism o hTiG , νie 2,m2 ===⇒ hTiH2,ˆ νi. (i) TiG TiX Ls 1 Rs 1 s 1 Le 2 Re 2 e 2 TiH1 m1 m∗ 1 ∗ m1 TiH2 m2 m∗ 2 ∗ m2 x2 x∗ 2 ∗ x2 I hTiH1 , ν00ie 2,x2 ==⇒ hTiX , ν000i does no dele e any locking edges ha ha e been c ea ed by hTiG , νis 1,m1 ===⇒ hTiH1 , ν0i , we ha e an(x2)∩TiH1 an( ∗ m1) = ∅ and can hus cons uc m2 such ha ∗ m1◦m2=x2 . Fo he case i does, we ha e o show ha m2 can be cons uc ed such ha ∗ m1◦m2=e x2 whe e e x2 is isomo phic o x2. Since x2 is o al, he e exis s an applica ion indica o x2(aie 2) in TiG . This applica ion indica o mus ha e been c ea ed by he induced s a ule s 2 o D2 . Thus, he e has o be an applica ion o s 2 in he ansi ion sequence om he ini ial con igu a ion o TiG . Le y2:Ls 2→TiF deno e i s ma ch and seq he ansi ion sequence om TiF o TiG. Now we ha e wo cases: ei he none o he locking edges c ea ed by he s a ule ans o ma ion s 2,y2 ==⇒ has been dele ed by any o he ans o ma ions in seq o a leas one o he locking edges has been dele ed. a) None o he locking edges has been dele ed by any o he ans o ma ions in seq . In his case, we can cons uc m2 such ha ∗ m1◦m2=e x2 whe e e x2 is isomo phic o x2 because TiG con ains locking edges which a e isomo phic o he ones c ea ed by hTiG,νis 1,m1 ===⇒ hTiH1,ν0i. b) A leas one o he locking edges has been dele ed by a leas one o he ans o ma ions in seq . To cons uc m2 such ha ∗ m1◦m2=e x2 whe e e x2 is isomo phic o x2 , locking edges ha e o exis ha a e isomo phic o he locking edges ha ha e been c ea ed by s 2,y2 ==⇒ bu dele ed by a 96 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS ans o ma ion in seq . Le ¯ e i deno e he ules o ans o ma ions dele ing he locking edges and ¯ mi:L¯ e i→TiEi hei ma ches wi h i= 1, . . . , n whe e nis he numbe o ans o ma ions dele ing he locking edges. Each ans o ma ion ¯ e i,¯ mi ==⇒ mus ha e been he applica ion o an end ule because s a ules do no dele e any hing. Thus, o each ¯ e i,¯ mi ==⇒ , he e mus ha e been a s a ule ans o ma ion ¯ s i,¯ yi ==⇒ wi h ¯ yi:L¯ s i→TiDi c ea ing he applica ion indica o ha ¯ e i,¯ mi ==⇒ dele es. Acco ding o De ini ions 5.2.10 and 5.2.11, each ¯ s i,¯ yi ==⇒ also c ea es locking edges which a e isomo phic o he ones ha ¯ e i,¯ mi ==⇒dele es. Again we ha e wo cases: ei he hey s ill exis in TiG o hey ha e been dele ed. I hey s ill exis in TiG , we can cons uc m2 as in (a). I no , hey ha e been dele ed by ans o ma ions in he ansi ion sequences om TiDi o TiG . In such a case, we can epea he a gumen o (b). This a gumen loop e mina es because he sequence o ansi ions om he ini ial con igu a ion o TiG is ini e. Thus, locking edges exis in TiG ha a e isomo phic o he ones c ea ed by hTiG , νis 1,m1 ===⇒ hTiH1 , ν0i and m2 can be cons uc ed such ha ∗ m1◦m2=e x2whe e e x2is isomo phic o x2. NACs Fu he mo e, m2|=Ne 2 holds ob iously because e 2 does no con ain any NACs. (ii) TiG TiX Ls 1 Rs 1 s 1 Le 2 Re 2 e 2 TiH1 m1 m∗ 1 ∗ m1 TiH2 m2 m∗ 2 ∗ m2 x1 x∗ 1 ∗ x1 We show ha hTiG , νis 1,m1 ===⇒ hTiH1 , ν0i is weakly pa allel independen o hTiG , νie 2,m2 ===⇒ hTiH2 , ˆ νi . This implies i s weak pa allel independence modulo isomo phism. We show ha he ma ch x1 such ha x1= ∗ m2◦m1 can be cons uc ed by con adic ion. Le us assume ha hTiG , νie 2,m2 ===⇒ hTiH2 , ˆ νi dele es elemen s o TiG which a e equi ed o x1 o be o al, i.e., an(m1)∩TiG dom( ∗ m2)6=∅. Acco ding o De ini ion 5.2.11, he dele ion o elemen s is accompanied by eleasing a w i e lock, i.e., dele ing a locking edge ha cons i u es a w i e ope a ion. Thus, each o he elemen s in an(m1)∩TiG dom( ∗ m2) has a w i e lock a ached. Acco ding o De ini ion 5.2.10, each elemen in he ange o he LHS’s ma ch is accompanied by a NAC ha checks o w i e locks. Since he elemen s 5.3. PROPERTIES OF DURATIVE GRAPH TRANSFORMATION RULES 97 in an(m1)∩TiG dom( ∗ m2) a e ob iously con ained in he ange o m1 and hese elemen s ha e w i e locks a ached, m1 does no ul ill each NAC in Ns 1 . This is a con adic ion o he applicabili y o hTiG,νis 1,m1 ===⇒ hTiH1,ν0i. NACs Fu he mo e, x1 ul ills each NAC in Ns 1 because hTiG , νie 2,m2 ===⇒ hTiH2 , ˆ νi does no c ea e any locking edges when de i ing TiH2 , Ns 1 con ains only NACs ha cons i u e checks o locking edges, and m1 al eady ul ills each NAC in Ns 1by de ini ion. In ui i ely, Lemma 5.3.4 holds due o wo ac s: 1. The end ans o ma ion consuming locking edges implies he exis ence o ano he s a ans o ma ion ha c ea ed such locking edges ea lie , hus p o iding exac ly he same (up o isomo phism) locking edges as i none o he wo ans o ma ions we e applied. 2. Elemen s supposed o be dele ed by a u u e end ans o ma ion, i.e., he coun e pa o he s a ans o ma ion, canno be dele ed by any o he ans- o ma ion because he s a ans o ma ion a ached locking edges o hem. The nex lemma conside s wo end ans o ma ions being applicable in he same con igu a ion. Fo he i s wo lemmas, we assumed a si ua ion whe e he ans o ma ions a e applied in sequence. This ensu ed hei sequen ial independence. I hey we e no sequen ially independen , he second ans o ma ion would no ha e been applicable a all. When conside ing wo end ans o ma ions, his is no necessa y. He e, hei applicabili y alone al eady ensu es ha hey a e pa allel independen . Lemma 5.3.5 (Pa allel independence modulo isomo phism be ween wo end ans o - ma ions) . Le D1 and D2 be wo du a i e ules, TiG = (GTiG , ypeTiG) a imed g aph wi h GTiG = (VG , VCI , EG , ECI) , and ν a clock ins ance alue assignmen such ha ν|=TiG and hTiG , νi is eachable om he ini ial con igu a ion. The induced end ules o D1 and D2 a e deno ed by e 1 and e 2 , espec i ely. Fu he , ci1 and ci2 deno e he clock ins ance exis ing du ing he applica ion in e al o D1 and D2 , espec i ely. Also, aie 1 and aie 2 deno e he applica ion indica o in he LHS o e 1and e 2, espec i ely. I he e a e wo ac ion ansi ions hTiG , νie 1,m1 ===⇒ hTiH1 , ν0i wi h ν0(ci1) = 0and hTiG , νie 2,m2 ===⇒ hTiH2 , ν00i wi h ν00(ci2) = 0and m2(aie 2)6=m1(aie 1) , hen hey a e pa allel independen modulo isomo phism. P oo . We ha e o show ha (i) hTiG , νie 2,m2 ===⇒ hTiH2 , ν00i is weakly pa allel inde- penden modulo isomo phism o hTiG , νie 1,m1 ===⇒ hTiH1 , ν0i and (ii) hTiG , νie 1,m1 ===⇒ hTiH1 , ν0i is weakly pa allel independen modulo isomo phism o hTiG , νie 2,m2 ===⇒ hTiH2,ν00i. 98 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS (i) TiG TiX Le 1 Re 1 e 1 Le 2 Re 2 e 2 TiH1 m1 m∗ 1 ∗ m1 TiH2 m2 m∗ 2 ∗ m2 x2 x∗ 2 ∗ x2 I ∗ m1◦m2 is o al, i.e., an(m2)∩TiG dom( ∗ m1) = ∅ , we can simply cons uc x2:Le 2→TiH1 such ha x2= ∗ m1◦m2 . O he wise, we ha e o show ha he e exis a o al mo phism e m2:Le 2→TiG such ha e m2 is isomo phic o m2 and hen cons uc x2such ha x2= ∗ m1◦e m2o he e is a con adic ion. The e a e wo cases: ei he an(m2)∩TiG dom( ∗ m1) con ains only locking elemen s o i also con ains o he elemen s han locks. a) an(m2)∩TiG dom( ∗ m1) con ains only locking elemen s. In his case, he e exis a e m2:Le 2→TiG which is isomo phic o m2 . Thus, we can cons uc x2:Le 2→TiH1 such ha x2= ∗ m1◦e m2 . The p oo ha e m2 exis s is analogous o he p oo o Lemma 5.3.4 (i). b) an(m2)∩TiG dom( ∗ m1) con ains elemen s o he han locks. Acco ding o De ini ion 5.2.11, he dele ion o elemen s is accompanied by eleasing a w i e lock, i.e., dele ing a locking edge ha cons i u es a w i e ope a ion. Thus, each o he elemen s in TiG dom( ∗ m1)has a w i e lock a ached. These w i e locks (o isomo phic ones) mus ha e been c ea ed by an applica ion o a s a ule s 1 o D1 ha also c ea ed he applica ion indica o ha e 1,m1 ===⇒ dele es. Simila ly, each o he elemen s in an(m2) has a ead lock a ached, which (modulo isomo phism) mus ha e been c ea ed by an applica ion o a s a ule s 2 o D2 . Le y1:Ls 1→TiF1 and y2:Ls 2→TiF2 deno e he he ma ch o s 1 and s 2 , espec i ely. Since m2(aie 2)6=m1(aie 1)holds, we ha e s 16=s 2∨y16=y2. Now, he e a e wo possible o de ings: ei he s 1,y1 ==⇒ happens be o e o a e s 2,y2 ==⇒ in he ansi ion sequence om he ini ial con igu a ion o TiG . In case o he o me , s 1,y1 ==⇒ c ea es a w i e lock ha s ill exis s in TiF2 . In case o he la e , s 2,y2 ==⇒ c ea es a ead lock ha s ill exis s in TiF1 . The exis ence o hese locking elemen s (o isomo phic ones) can be shown analogously o he a gumen loop in he p oo o Lemma 5.3.4 (i). Acco ding o De ini ion 5.2.10, each c ea ion o a w i e lock [ ead lock] is accompanied by a NAC ha ealizes a check o a ead lock [w i e lock]. Thus, he w i e lock [ ead lock] exis ing in TiF2 [ TiF1 ] con lic s wi h a NAC o s 2 [ s 1 ]. Bo h cons i u e a con adic ion o he applicabili y o he second ans o ma ion. 5.3. PROPERTIES OF DURATIVE GRAPH TRANSFORMATION RULES 99 NACs Fu he mo e, x2|=Ne 2 holds ob iously because e 2 does no con ain any NACs. (ii) TiG TiX Le 1 Re 1 e 1 Le 2 Re 2 e 2 TiH1 m1 m∗ 1 ∗ m1 TiH2 m2 m∗ 2 ∗ m2 x1 x∗ 1 ∗ x1 This p oo is analogous o he p oo o (i). In ui i ely, he pa allel independence o he end ans o ma ions esul s om he independence o hei s a ans o ma ion coun e pa s. I he s a ans o ma ions we e no independen , hey could no ha e been applied du ing he ansi ion sequence om he ini ial con igu a ion o he cu en con igu a ion. Now, we o malize he p ope y ha ensu es ha each du a i e g aph ans o - ma ion e mina es p ope ly, i.e., no o he ans o ma ion can cause he induced end ule o he ongoing du a i e g aph ans o ma ion no o be applicable anymo e. As a consequence, du a i e g aph ans o ma ions can only be execu ed i hey do no in e e e wi h ongoing du a i e g aph ans o ma ions. Theo em 5.3.6 (Te mina ion o a du a i e ule) . Le D1 be a du a i e ule, TiG = (GTiG , ypeTiG) a imed g aph wi h GTiG = (VG , VCI , EG , ECI) , and ν a clock ins ance alue assignmen such ha ν|=TiG and hTiG , νi is eachable om he ini ial con igu a ion. The induced s a and end ule o D1 a e deno ed by s 1 and e 1 , espec i ely. Fu he , iL,s 1 and iL,e 1 deno e he mo phisms iden i ying he elemen s o LD1 in Ls 1 and Le 1 , espec i ely. Also, ais 1 and aie 1 deno e he applica ion indica o in he RHS o s 1 and he LHS o e 2 , espec i ely. I he e exis s a ansi ion sequence hTiG , νis 1,m1 ===⇒ hTiH1 , ν0iseq hTiX , ν00i wi h hTiA , ˆ νie 1,a1 ==⇒ hTiB , ˆ ν0i/∈seq o any ma ch a1:Le 1→TiA such ha a1(aie 1) = ∗ p e ◦ m∗ 1(ais 1) whe e ∗ p e deno es he de i a ion mo phism o a p e ix ansi ion sequence o seq ending in TiA , hen he e exis s a unique (up o isomo phism) ma ch g1:Le 1→TiX such ha g1◦iL,e 1= ∗ seq ◦ ∗ m1◦m1◦iL,s 1 and an ac ion ansi ion hTiX , ν00ie 1,g1 ==⇒ hTiY , ν000i . Ls 1Rs 1 TiG TiH1 Le 1Re 1 TiX TiY s 1 m1m∗ 1 ∗ m1 ∗ seq e 1 g1g∗ 1 ∗ g1 P oo . We show his p ope y by induc ion o e he numbe o ansi ions in seq. 100 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS Basis s ep. The ansi ion sequence seq is emp y. Thus, hTiH1 , ν0i=hTiX , ν00i holds. Now, we only ha e o show ha he e exis s a ma ch g1:Le 1→TiH1 such ha g1◦iL,e 1= ∗ m1◦m1◦iL,s 1 . Acco ding o De ini ions 5.2.10 and 5.2.11, Le 1=Rs 1 holds. Thus, we can simply de ine g1 such ha g1◦iL,e 1=m∗ 1◦ s 1◦ iL,s 1= ∗ m1◦m1◦iL,s 1. Induc ion s ep. Le 2,x2 ==⇒ deno e he i s ansi ion in seq . Tha way, we ha e hTiG , νis 1,m1 ===⇒ hTiH1 , ν0i 2,x2 ==⇒ hTiI , ξiseq0hTiX , ν00i . Acco ding o Lem- mas 5.3.3 and 5.3.4 he ans o ma ions hTiG , νis 1,m1 ===⇒ hTiH1 , ν0i 2,x2 ==⇒ hTiI , ξi a e sequen ially independen (modulo isomo phism). Theo em 2.5.1 s a es ha se- quen ially independen ans o ma ions can be eo de ed and s ill esul in he same g aph. Thus, we ge hTiG , νi 2,m2 ===⇒ hTiH2 , ξ0is 1,x1 ==⇒ hTiI , ξiseq0hTiX , ν00i . Now, we can apply he induc ion hypo hesis, which esul s in he exis ence o g1:Le 1→TiX such ha g1◦iL,e 1= ∗ seq0◦ ∗ x1◦x1◦iL,s 1 . Using m1 ins ead o x1 , we ge g1◦iL,e 1= ∗ seq0◦ ∗ x2◦ ∗ m1◦m1◦iL,s 1 . Since ∗ seq = ∗ seq0◦ ∗ x2 holds, we ge g1◦iL,e 1= ∗ seq ◦ ∗ m1◦m1◦iL,s 1. While Theo em 5.3.6 ensu es ha each du a i e g aph ans o ma ion e mina es p ope ly, e en when o he ans o ma ions a e applied du ing i s applica ion in e al, i does no s a e any hing abou he con igu a ion ha esul s in such cases. The nex p ope y does. I s a es ha each in e lea ing o wo du a i e g aph ans o ma ions esul s in he same con igu a ion when bo h ans o ma ions inished (and no o he ans o ma ion is in ol ed). F om a mo e abs ac pe spec i e, his p ope y cha ac e izes all possible in e lea ings o wo du a i e g aph ans o ma ions ha a e independen o each o he . Theo em 5.3.7 (Exis ence o in e lea ing ansi ion sequences) . Le D1 and D2 be wo du a i e ules, TiG = (GTiG , ypeTiG) a imed g aph wi h GTiG = (VG , VCI , EG , ECI) , and ν a clock ins ance alue assignmen such ha ν|=TiG and hTiG , νi is eachable om he ini ial con igu a ion. The induced s a and end ules o D1 and D2 a e deno ed by s 1 , e 1 , s 2, and e 2, espec i ely. I hTiG , νis 1,m1 ===⇒ hTiH1 , ν0i and hTiG , νis 2,m2 ===⇒ hTiH2 , ν00i a e pa allel independen , he e exis ma ches ms1 , me1 , ms2 , and me2 o s 1 , e 1 , s 2 , and e 2 , espec i ely, such ha each o he ansi ion sequences ul illing he pa ial o de • • s 1,ms1 e 1,me1 s 2,ms2 e 2,me2 exis s and esul s in he same g aph TiZ. 5.3. PROPERTIES OF DURATIVE GRAPH TRANSFORMATION RULES 101 TiG TiH1TiH2 TiI1TiX TiI2 TiY1TiY2 TiZ s 1,m1 s 1,x1 s 1,y1 e 1, 1 e 1,g1 e 1,h1 s 2,m2 s 2,x2 s 2,y2 e 2, 2 e 2,g2 e 2,h2 P oo . Acco ding o he Local Chu ch-Rosse Theo em, bo h sequen ializa ions o wo pa allel independen ans o ma ions esul in he same g aph. Thus, we ha e he ansi ion sequence shown in Figu e 5.11(a). Acco ding o De ini ions 5.2.10 and 5.2.11, Le 1=Rs 1 holds. Thus, he ma ch g1:Le 1→TiX can be de ined such ha g1◦iL,e 1=x∗ 1◦ s 1◦iL,s 1= ∗ x1◦x1◦iL,s 1 . The ma ch g2:Le 2→TiX can be de ined analogously. Now, we ha e he ansi ion sequence shown in Figu e 5.11(b). Acco ding o Lemma 5.3.4, he ans o ma ions s 2,x2 ==⇒ and e 1,g1 ==⇒ a e sequen ially independen . Since he Local Chu ch-Rosse Theo em also wo ks o sequen ially independen ans o ma ions, we ge he ansi ion sequence shown in Figu e 5.11(c). · · · · · · (a) · · · · · · (b) · · · · · · · · (c) · · · ··· · · · · ? = (d) · · · ··· · · · ? = (e) Figu e 5.11: Visual aid o he p oo o Theo em 5.3.7 108 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS base s a ion. Mo e p ecisely, a RailCab has o be egis e ed a a base s a ion ha moni o s he ack segmen ha he RailCab is cu en ly occupying. The eal- ime communica ion be ween a RailCab and he base s a ion i is egis e ed a is speci ied by he RTCP Publica ion, which is ep esen ed wi hin con igu a ions and ules as a node o ype Pub. When a RailCab mo es om a ack segmen ha is moni o ed by one base s a ion o a ack segmen ha is moni o ed by ano he base s a ion, i has o change i s publica ion. This is cap u ed by he du a i e ule changePublica ion , which is shown in Figu e 5.13. I speci ies he e oca ion o a publica ion a one base s a ion and he announcemen o a publica ion a ano he base s a ion. :RailCab:Base :Base «--» :Pub «++» :Pub «++» publishe «++» dis ibu o «--» publishe «--» dis ibu o d := 2 Figu e 5.13: Du a i e ule changePublica ion A condi ion o he applica ion o he du a i e ule changePublica ion is he concu en applica ion o ano he du a i e ule ha mo es he RailCab om one ack segmen o he nex . Besides mo eRailCab , possible candida es p o iding such a econ igu a ion a e mo eCon oy and all du a i e ules ela ed o membe ship change, e.g., o mCon oy o joinCon oy , since hey also change he posi ion o RailCabs. All hese du a i e ules a e modeled independen ly om changePublica ion and hei applica ions exis independen ly om applica ions o changePublica ion. Including he mo emen o a RailCab in changePublica ion is no ad isable due o wo easons. Fi s , he e is mo e han one econ igu a ion ha mo es a RailCab o he nex ack segmen . A modele would ha e o model a sepa a e ule o each such econ igu a ion. Second, changing a publica ion and mo ing a RailCab a e di e en conce ns, and modeling hem as one econ igu a ion can be conside ed bad de elopmen s yle. Since econ igu a ions add essing di e en conce ns a e modeled independen ly om one ano he , we need an ex e nal means o speci ying equi emen s o hei concu en execu ion. Concu ency ules p o ide his means by e e encing du a i e ules and speci ying how hese ules ha e o ma ch ela i ely o one ano he . 5.5.1 Syn ax A concu ency ule speci ies a dependency be ween wo se s o du a i e ules: an applica ion o a du a i e ule in he i s se equi es a concu en applica ion o a du a i e ule in he second se . Vice e sa, he applica ion in e al o a du a i e ule in he second se can be seen as a window o oppo uni y o ules in he i s 5.5. CONCURRENCY RULES 109 se . The in ol ed du a i e ules o bo h se s ha e o ma ch in a ce ain way o his dependency o be ul illed. This ma ching cons ain is o malized in he syn ax o concu ency ules ia wo in e ace g aphs and g aph mo phisms o he in ol ed du a i e ules. De ini ion 5.5.1 (Concu ency ule) . Le DR be a se o du a i e ules. A concu ency ule C= (GT,DT,ST,D,S,name)consis s o • a yped g aph GT , called connec ing g aph, wi h wo subg aphs DT and ST , called (concu ency) demande in e ace and (concu ency) sa is ie in e ace, espec- i ely, • a non-emp y se o uples D , called (concu ency) demande uples, whe e each uple (D , d)∈D e e ences a du a i e ule D ∈ DR and de e mines a sub- g aph o i s LHS ia an injec i e mo phism d:DT→LD , called (concu ency) demande cons ain mo phism, • a non-emp y se o uples S , called (concu ency) sa is ie uples, whe e each uple (D , s)∈S e e ences a du a i e ule D ∈ DR and de e mines a subg aph o i s LHS ia an injec i e mo phism s:ST→LD , called (concu ency) sa is ie cons ain mo phism, and • a dis inc name name. Fo a du a i e g aph ans o ma ion sys em DS = (T G , GT 0 , DR) wi h a se o concu ency ules CR, we also w i e DS = (T G,GT 0,DR,CR). A connec ing g aph has wo dedica ed subg aphs, which se e as in e aces o he du a i e ules in ol ed wi h a concu ency ule. They a e called demande in e ace and sa is ie in e ace. So-called cons ain mo phisms om hese subg aphs o du a i e ules de ine which du a i e ules ul ill hese in e aces and how hey ha e o ma ch ela i ely o each o he . All hese cons ain mo phisms a e – oge he wi h he ules hey map o – con ained in he se o demande and sa is ie uples. Each ule e e enced by a demande o sa is ie uple ul ills he demande o sa is ie in e ace, espec i ely. An applica ion o a du a i e ule e e enced by a demande uple demands a concu en ans o ma ion, and an applica ion o a du a i e ule e e enced by a sa is ie uple sa is ies his demand. The e o e, we call a du a i e ule ha is e e enced by a demande uple a demanding ule. I i is e e enced by a sa is ie uple, we call i a sa is ying ule. The demande and sa is ie cons ain mo phisms cons i u e ma ching cons ain s o all in ol ed du a i e ules. Fo a demanding and a sa is ying ule o be applicable concu en ly, elemen s con ained in he images o hei demande and sa is ie cons ain mo phism ha o igina e om he same elemen in he connec ing g aph GTalso ha e o ma ch o he same elemen in he hos g aph. Elemen s ha ha e a p eimage in only one o he in e ace subg aphs DT and ST also es ic he ma ching: i an elemen o DT is somehow connec ed in GT o an elemen o ST , hen he same connec ion has o exis o hei images in he hos g aph. 110 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS :RailCab:Base :Base «--» :Pub «++» :Pub «++» publish. «++» dis i. «--» publish. «--» dis i. :RailCab :T ack :T ack :Base :Base moni o s moni o s (a) A demande cons ain mo phism o allowChangePublica ion o changePublica ion :RailCab d i ing :T ack + ee :T ack – ee «++» on «--» on nex :RailCab :T ack :T ack :Base :Base moni o s moni o s (b) A sa is ie cons ain mo phism o allowChangePublica ion o mo eRailCab Figu e 5.14: A demande and a sa is ie cons ain mo phism o he concu ency ule allowChangePublica ion As an example, Figu e 5.14 shows a demande and a sa is ie cons ain mo - phism o he concu ency ule allowChangePublica ion . A RailCab is only allowed o change i s publica ion i i is mo ing om one ack segmen o he nex . The e- o e, changePublica ion is a demanding ule and mo eRailCab a sa is ying ule. To be p ecise, changePublica ion is he only demanding ule, while mo eRailCab is one o mul iple sa is ying ules. All du a i e ules ha mo e a RailCab om one ack segmen o he nex a e alid sa is ying ules o allowChangePublica ion . He e, mo eRailCab is exempla y o all sa is ying ules o allowChangePublica ion . The ele an node in his example is he RailCab node, which is why i is con ained in bo h in e ace subg aphs and hus de ined unde bo h demande and sa is ie cons ain mo phisms. Howe e , he ac ha he RailCab nodes o bo h ules ha e o ma ch he same node in he hos g aph is no he only ma ching cons ain o he concu en applica ion o bo h ules. The new base s a ion also has o moni o he ack segmen ha he RailCab is mo ing o. This is nei he speci ied in changePublica ion no in mo eRailCab . I is no speci ied in changePublica ion , 5.5. CONCURRENCY RULES 111 because changePublica ion is no conce ned wi h he mo emen o RailCabs a all, and i is no speci ied in mo eRailCab , because mo eRailCab is no conce ned wi h base s a ions and publica ions. Ins ead, his cons ain is exp essed ia he s uc u e o he connec ing g aph and bo h in e ace subg aphs: each Base node is connec ed o one o he T ack nodes ia a moni o s edge, and while he Base nodes a e con ained in he demande in e ace, he T ack nodes a e con ained in he sa is ie in e ace. Fo he concu en applica ion o bo h ules, his s uc u e also has o exis in he hos g aph. No e ha he e can be mul iple demande o sa is ie cons ain mo phisms o he same demanding o sa is ying ule. I he e a e mul iple demande cons ain mo phisms o a single demanding ule, his means ha he demande in e ace is ul illed in mul iple di e en ways, each wi h a di e en ma ching cons ain , and an applica ion o his ule causes mul iple demands. I he e a e mul iple sa is ie cons ain mo phisms o a single sa is ying ule, his means ha he sa is ie in e ace can be ul illed in mul iple di e en ways, i.e., mul iple ma ches can lead o a sa is ac ion o he demand in concu en execu ion. An example o his is he ule o mCon oy , which models wo RailCabs d i ing in he same di ec ion. In his ule, a ea wa d RailCab ca ches up o a on wa d RailCab by co e ing a dis ance o wo ack segmen s. Figu e 5.15 shows wo sa is ie cons ain mo phisms mapping o his ule. The i s cons ain mo phism maps he concu ency ule’s RailCab node o he ea wa d RailCab and he second cons ain mo phism o he on wa d RailCab. No e ha he second T ack node does no ha e o be he di ec successo o he i s T ack node o he cons ain mo phisms o ma ch. When employing concu ency ules in so wa e de elopmen , a modele po en- ially has o de ine a lo o demande and sa is ie cons ain mo phisms. While hese cons ain mo phism can be de ined con enien ly using colo s o highligh ing, a g aphical ep esen a ion o a concu ency ule in ol ing mul iple cons ain mo - phisms, like he ones in Figu es 5.14 and 5.15, is a he imp ac ical as an o e iew because i is no p esen ed cohe en ly in a single diag am. Fo una ely, he la e can be done: by employing objec names in du a i e ules, we allow o e e ence hei nodes di ec ly om he connec ing g aph o a concu ency ule. Figu e 5.16 illus a es such a compac ep esen a ion o he cons ain mo phisms o Figu es 5.14 and 5.15. As an example, conside he RailCab node in he cen e o he connec ing g aph. The label #dc::‘ c’ means ha he node maps o he node wi h he objec name c unde he cons ain mo phism dc , which is a demande cons ain mo phism o he du a i e ule changePublica ion . The o he h ee labels de ine images o his node unde he h ee sa is ie cons ain mo phisms o Figu es 5.14(b), 5.15(a) and 5.15(b). 112 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS «++» :Con oy +d i ing :RailCab –d i ing +las :RailCab + i s :T ack + ee :T ack + ee :T ack – ee nex «--» on «++» on «++» membe «--» on «++» membe nex «++» on :RailCab :T ack :T ack :Base :Base moni o s moni o s (a) Fi s sa is ie cons ain mo phism o allowChangePublica ion o o mCon oy «++» :Con oy +d i ing :RailCab –d i ing +las :RailCab + i s :T ack + ee :T ack + ee :T ack – ee nex «--» on «++» on «++» membe «--» on «++» membe nex «++» on :RailCab :T ack :T ack :Base :Base moni o s moni o s (b) Second sa is ie cons ain mo phism o allowChangePublica ion o o mCon oy Figu e 5.15: Two sa is ie cons ain mo phisms o concu ency ule allowChangePub- lica ion mapping o he same du a i e ule 5.5. CONCURRENCY RULES 113 «d/s» :RailCab #dc::‘ c’ #sm::‘ c’ #s 1::‘ c1’ #s 2::‘ c2’ «dem» :Base #dc::‘b1’ «dem» :Base #dc::‘b2’ «sa » :T ack #sm::‘ 1’ #s 1::‘ 1’ #s 2::‘ 2’ «sa » :T ack #sm::‘ 2’ #s 1::‘ 3’ #s 2::‘ 3’ moni o s moni o s #dc →dem “changePublica ion” #sm →sa “mo eRailCab” #s 1 →sa “ o mCon oy” #s 2 →sa “ o mCon oy” Figu e 5.16: Compac ep esen a ion o demande and sa is ie cons ain mo phisms o Figu es 5.14 and 5.15 o concu ency ule allowChangePublica ion 114 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS 5.5.2 Seman ics The seman ics o concu ency ules is de ined by ex ending hose imed g aph ans o ma ion ules ha ha e been induced by du a i e g aph ans o ma ion ules. This can be seen as modi ying he seman ics o all du a i e ules in ol ed in concu ency ules. Each s a o end ule whose inducing du a i e ule is e e enced by a concu ency ule is ex ended. To mo i a e how hese ules a e ex ended, we ake a look a hei in e ac ion. demanding ule sa is ying ule equi es concu en applica ion o ha e s a ed equi es concu en applica ion o ha e inished (i exis ing) sequence o ule applica ions Figu e 5.17: Concu en execu ion o a demanding and a sa is ying ule Figu e 5.17 illus a es he dependency be ween a demanding and a sa is ying ule, e.g., changePublica ion and mo eRailCab . In e ms o ime, he demanding ule has he “inne ” and he sa is ying ule he “ou e ” applica ion in e al. The seman ics o a concu ency ule ex ends he induced s a and end ules o all in ol ed du a i e ules such ha hei applica ion imes ha e o be empo ally o de ed as in he igu e. Mo e p ecisely, he demanding ule equi es he applica ion o he sa is ying ule bo h o ha e s a ed ea lie and o end la e . To equi e he o me , we ex end he induced ules o bo h ules such ha he demanding ans o ma ion checks whe he he sa is ying ans o ma ion is cu en ly being applied. When equi ing he la e , we ha e o make su e ha he cu en sa is ying ans o ma ion is indeed he same ans o ma ion as be o e. To p e en a second sa is ie ans o ma ion (o he same o a di e en ule) om aking he place o he i s , we apply a lock and e e se he di ec ion o he dependency, i.e., by checking o po en ial locks, he sa is ying ule gua an ees ha no demanding ans o ma ion is being applied concu en ly. No e ha a sa is ying ule can s ill be applied independen ly o a demanding ule, which is why he igh a ow in Figu e 5.17 has a di e en meaning han he le . To p ope ly ex end he induced ules, we ha e o be able o check whe he a demand in concu en execu ion, as speci ied by a concu ency ule, is sa is ied. The sa is ac ion o such a demand is indica ed by a sa is ac ion indica o , which is a concep ha is analogous o an applica ion indica o . Since concu ency ules a e no applied in he sense o g aph ans o ma ions, sa is ac ion indica o s a e no c ea ed and dele ed by concu ency ules bu by hei e e enced sa is ying ules. As a consequence o he use o sa is ac ion indica o s, he induced TGTS ype g aph has o be ex ended. This ex ension is made analogously o ha o applica ion indica o s. The TGTS ype g aph has o include a ype o each sa is ac ion indica o . Fo a concu ency ule wi h he name name , i s sa is ac ion indica o ype is gi en by siType(name) . Fu he mo e, he e has o be a dis inc sa is ac ion indica o edge 5.5. CONCURRENCY RULES 115 ype o each node in he sa is ie in e ace o he concu ency ule. Fo a node , i s sa is ac ion indica o edge ype is gi en by siEdgeType( ). Fo a sa is ying ule, a sa is ac ion indica o is simply a ached ia sa is ac ion indica o edges o hose nodes ha a e in he ange o i s sa is ie cons ain mo - phism. Un o una ely, he appea ance o sa is ac ion indica o s in demanding ules is sligh ly mo e complica ed han in sa is ying ules. Since demande and sa is ie cons ain mo phisms a e de ined unde di e en subg aphs o he connec ing g aph, hose nodes ha he sa is ac ion indica o has o be a ached o do no necessa ily exis in a demanding ule’s LHS. The e o e, he LHSs o a demanding ule’s in- duced s a and end ule a e ex ended wi h hose elemen s in he connec ing g aph ha a e no de ined unde he demande cons ain mo phism. Technically, his is implemen ed ia a pushou . Adding hese elemen s o he induced ules’ LHSs does no es ic he applica- bili y o he demanding ule. The added elemen s ha e o exis in he hos g aph in ei he case because he sa is ying ule, which is applied concu en ly, equi es hem. Nex , we gi e de ini ions ha s a e how he induced ules o demanding and sa is ying ules a e ex ended. A e each de ini ion, we gi en an example o he ex ended induced ule. These ex ensions ollow he example o he concu - ency ule allowChangePublica ion wi h changePublica ion as demanding ule and mo eRailCab as sa is ying ule. Fi s , we ex end he induced s a and end ule o a concu ency demanding ule such ha hey equi e he exis ence o a sa is ac ion indica o in he hos g aph. De ini ion 5.5.2 (Ex ension o a concu ency demande ’s induced s a ule) . Le C= (GT , DT , ST , D , S , name) be a concu ency ule and DR a se o du a i e ules. Fo each concu ency demande uple (D , d)∈D , he induced s a ule s = (L , R , , N , z , V es) o D ∈ DR is ex ended in o a imed ule s 0= (L0 , R0 , 0 , N0 , z , V es) whe e •(Lx,g,i∗), wi h g:GT→Lxand i∗:L→Lx, is he pushou o e d:DT→Land he subg aph isomo phism i:DT→GT, •VSI ={si} ∧ ype(si) = siType(name)∧ ESI ={e|s c(e) = si ∧ g (e)∈g(ST)∧ ype(e) = siEdgeType ◦g−1◦ g (e)}, •VG,L0=VG,Lx∪VSI ∧EG,L0=EG,Lx∪ESI, •VG,R0=VG,R∪VSI ∧EG,R0=EG,R∪ESI ∪ERL.node,R0, •VCI,L0=VCI,Lx∧ECI,L0=ECI,Lx∧VCI,R0=VCI,R∧ECI,R0=ECI,R • 0= ∪ {∀x∈Vg(GT DT)∪Eg(GT DT):x7→ x} ∪ {si 7→ si} ∪ {∀y∈Vg(ST):(si,y)7→ (si,y)}, and •N0is de ined analogously o De ini ion 5.2.10 such ha ∀(N,n)∈ N 0: dom(n) = L0, and •ERL.node,R0={e|s c(e) = g (e) = si ∧ ype(e) = lnode ◦ ype(si)} 116 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS The pushou adds hose elemen s ha a e exis ing in he connec ing g aph bu no in he subg aph cons i u ing he demande in e ace o he LHS o he ex ended s a ule. This is necessa y so ha we can a ach he sa is ac ion indica o a i s app op ia e place. Besides equi ing his sa is ac ion indica o and i s sa is ac ion indica o edges, he ex ended s a ule c ea es a ead lock on he sa is ac ion indica o . The ead lock is used o ensu e ha he execu ion o a demanding ule inishes be o e he execu ion o a sa is ying ule. Apa om ha , he ex ended s a ule is almos iden ical o he o iginal ule. The ule mo phism and he NAC mo phisms a e changed such ha hey a e o al on hei new domain L0 . This is necessa y only o easons o echnical co ec ness; i does no change hei in ended pu pose. :RailCab + l :Base + l :Base + l «++» :Pub + l +wl publish. dis i. «++» l(dis i.) «++» wl(dis i.) «++» l(publish.) «++» wl(publish.) :T ack moni o s :T ack moni o s :SI + l Figu e 5.18: Demanding ule changePublica ion ’s induced s a ule ex ended acco ding o concu ency ule allowChangePublica ion Figu e 5.18 shows he ex ended induced s a ule o changePublica ion . The ex ension was done acco ding o he demande cons ain mo phism o Figu e 5.14(a). Fo easons o cla i y, he ex ended ule does no show any NACs o locks ha ha e been gene a ed o suppo NACs on he le el o du a i e ules. The wo T ack nodes along wi h he wo moni o s edges, which connec he T ack nodes o he Base nodes, ha e been added in o he ule by he pushou . Then, he sa is ac ion indica o is connec ed o hese T ack nodes and he only RailCab node. The sa is ac ion indica o also ecei es a ead lock. No e ha he new T ack nodes do no ha e any locks, because hey we e no p esen in he o iginal ule. The end ule o a concu ency demanding ule is ex ended in a simila manne as he s a ule. The LHS and RHS include hose elemen s om he connec ing g aph needed o he sa is ac ion indica o , he sa is ac ion indica o i sel , and i s sa is ac ion indica o edges. The LHS also includes a ead lock on he sa is ac ion indica o . 5.5. CONCURRENCY RULES 117 De ini ion 5.5.3 (Ex ension o a concu ency demande ’s induced end ule) . Le C= (GT , DT , ST , D , S , name) be a concu ency ule and DR a se o du a i e ules. Fo each concu ency demande uple (D , d)∈D , he induced end ule e = (L , R , , N , z , V es) o D ∈ DR is ex ended in o a imed ule e 0= (L0 , R0 , 0 , N , z , V es) whe e •(Lx,g,i∗), wi h g:GT→Lxand i∗:L→Lx, is he pushou o e d:DT→Land he subg aph isomo phism i:DT→GT, •VSI ={si} ∧ ype(si) = siType(name)∧ ESI ={e|s c(e) = si ∧ g (e)∈g(ST)∧ ype(e) = siEdgeType ◦g−1◦ g (e)}, •VG,L0=VG,Lx∪VSI ∧EG,L0=EG,Lx∪ESI ∪ERL.node,L0, •VG,R0=VG,R∪VSI ∧EG,R0=EG,R∪ESI, •VCI,L0=VCI,Lx∧ECI,L0=ECI,Lx∧VCI,R0=VCI,R∧ECI,R0=ECI,R • 0= ∪ {∀x∈Vg(GT DT)∪Eg(GT DT):x7→ x} ∪ {si 7→ si} ∪ {∀y∈Vg(ST):(si,y)7→ (si,y)}, and •ERL.node,L0={e|s c(e) = g (e) = si ∧ ype(e) = lnode ◦ ype(si)}. Figu e 5.19 shows he ex ended induced end ule o changePublica ion . I s ex ension is done analogously o ha o he induced s a ule in Figu e 5.18. :RailCab – l :Base – l :Base – l «--» :Pub – l –wl «++» :Pub «++» publish. «++» dis i. «--» publish. «--» dis i. «--» l(dis i.) «--» wl(dis i.) «--» l(publish.) «--» wl(publish.) :T ack moni o s :T ack moni o s :SI – l Figu e 5.19: Demanding ule changePublica ion ’s induced end ule ex ended ac- co ding o concu ency ule allowChangePublica ion The induced ules o a demanding ule equi e he exis ence o a sa is ac ion indica o . The only ules able o c ea e (and dele e) his speci ic sa is ac ion indica o a e induced s a (and end) ules o hose sa is ying ules ha a e e e enced by he same concu ency ule as he demanding ule. 124 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS «d/s» RailCab #dm::‘ c’ #sm::‘ c’ #sb::‘ c’ d/sd i ing «d/s» :T ack #dm::‘ ’ #sm::‘ 1’ #sb::‘ 1’ «d/s» on #dm →dem “mo eRailCab” #sm →sa “mo eRailCab” #sb →sa “b akeRailCab” Figu e 5.25: Compac ep esen a ion o demande and sa is ie cons ain mo phisms o Figu e 5.24 o u gency ule immedia elyMo eRailCab mo eRailCab in Figu e 5.24. When e e encing he same ule as demanding and sa is ying ule, he demande and sa is ie cons ain mo phisms should be di e en , which is he case he e; o he wise, a ule applica ion would sa is y i s demand i sel . A compac ep esen a ion o hese h ee cons ain mo phisms is shown in Figu e 5.25. As opposed o he cons ain mo phisms o he concu ency ule allowChangePublica ion , o which a compac ep esen a ion was shown in Fig- u e 5.16, he cons ain mo phisms he e also in ol e edges. Fo una ely, we do no ha e o s a e he image o an edge unde each cons ain mo phism. I is su icien o s a e which edge is in ol ed in he demande and sa is ie in e ace because he co ec sou ce and a ge nodes o he edge’s image unde each cons ain mo phism can be deduced om he con ex , i.e., om he connec ing g aph and he nodes’ images. In he example gi en he e, he demande and sa is ie in e ace a e iden ical. In gene al, he demande and sa is ie in e ace o u gency ules a e, o cou se, also allowed o be di e en . An example whe e hey a e equi ed o be di e en migh be he elease o a d i e ’s sa e y bel and he subsequen unlocking o he d i e ’s doo . 5.6.2 Seman ics As in concu ency ules, he seman ics o u gency ules a e de ined by ex ending hose s a and end ules whose du a i e ules a e e e enced by u gency ules. In con as o concu ency ules, u gency ules also induce new imed ules, in a ian ules, and clock ins ance ules di ec ly. To mo i a e hei pu pose, we ake an abs ac look a how he seman ics o an u gency ule is implemen ed. Figu e 5.26 illus a es how he applica ion o a sa is ying ule, e.g., b akeRailCab , is en o ced by he applica ion o a demanding ule, e.g., mo eRailCab . Fi s , he demanding ule indica es a demand in u gen execu ion. This is done by adding a demand indica o in o he hos g aph. To equi e ha he demand is sa is ied, 5.6. URGENCY RULES 125 demanding ule sa is ying ule sa is ie - i ing ule sa is ie -cleaning ule equi es concu en applica ion o ha e s a ed u gen applica ion en o ced ia in a ian ule sequence o ule applica ions Figu e 5.26: U gen execu ion o a sa is ying ule a e a demanding ule i.e., he demand indica o is dele ed again, wi hin he ime ame speci ied by he u gency ule, we use an in a ian ule o e he demand indica o . The only ule able o dele e his demand indica o is he imed ule shown abo e he sa is ying ule in Figu e 5.26. This ule is called sa is ie - i ing imed ule. I s applica ion is en o ced ia he in a ian ule. The pu pose o he sa is ie - i ing imed ule is o en o ce he applica ion o a sa is ying ule. To do so, he ule equi es a sa is ac ion indica o o exis in he hos g aph. Since he applica ion o he sa is ie - i ing imed ule is i sel en o ced ia an in a ian ule, a compa ible sa is ac ion indica o has o be c ea ed be o e i s applica ion. This is wha causes a sa is ying ule o be applied. No e ha a sa is ying ule can also be applied when he e is no demand in u gen execu ion. In such a case, he sa is ying ule c ea es a sa is ac ion indica o ha is no dele ed by a sa is ie - i ing imed ule. I le behind in he hos g aph, a sa is ac ion indica o migh cause a p oblem when an u gency demanding ule is applied a second ime: since he old sa is ac ion indica o is s ill a ailable, he e is no need o a sa is ying ule o be applied. The e o e, sa is ac ion indica o s a e dele ed by ano he imed ule, called sa is ie -cleaning imed ule. This ule, shown below he sa is ying ule in Figu e 5.26, has o be applied o e e y sa is ac ion indica o in he hos g aph ha is no dele ed by an applica ion o he sa is ie - i ing imed ule. As wi h he sa is ie - i ing imed ule, we en o ce he applica ion o he sa is ie -cleaning imed ule ia an in a ian ule. The demand and sa is ac ion indica o can simply be a ached o he RHS o he demanding ule and he LHS o he sa is ying ule, espec i ely. Thei p ope ela i e posi ioning in a con igu a ion, i.e., he ma ching cons ain s o malized ia he demande and sa is ie cons ain mo phisms, is gua an eed by he sa is ie - i ing imed ule. The e is no need o ex end he demanding ule wi h addi ional nodes and edges as done in he case o concu ency ules. Ex ending he demanding ule was necessa y o concu ency ules because concu ency ules do no ha e demand indica o s. 126 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS The induced TGTS ype g aph is ex ended by u gency ules o suppo hei demand and sa is ac ion indica o s. Fo each demand and sa is ac ion indica o , i includes a sepa a e ype. Fo an u gency ule wi h he name name , i s demand and sa is ac ion indica o ype a e gi en by diType(name) and siType(name) , espec i ely. Fu he mo e, he e a e dis inc demand and sa is ac ion indica o edge ypes o each node in he in e ace subg aphs o he u gency ule. Fo a node , i s demand and sa is ac ion indica o edge ype a e gi en by diEdgeType( ) and siEdgeType( ) , espec i ely. Nex , we gi e he o mal de ini ions o he seman ics o u gency ules. Be ween hose de ini ions, we gi e examples o he ex ended induced ules and he imed ules di ec ly induced by u gency ules. They ollow he example o u gency ule immedia elyMo eRailCab wi h mo eRailCab as demanding ule and b akeRailCab as sa is ying ule. Fi s , we ex end he induced end ule o an u gency demanding ule such ha i c ea es a demand indica o in he hos g aph. De ini ion 5.6.2 (Ex ension o an u gency demande ’s induced end ule) . Le U= (GT , DT , ST , D , S , name , dl) be an u gency ule and DR a se o du a i e ules. Fo each u gency demande uple (D , d)∈D , he induced end ule e = (L , R , , N , z , V es) o D ∈ DR is ex ended in o a imed ule e 0= (L , R0 , , N , z , V es) whe e •VDI ={di} ∧ ype(di) = diType(name)∧ EDI ={e|s c(e) = di ∧ g (e)∈ an(d)∧ ype(e) = diEdgeType ◦d−1◦ g (e)}, •VG,R0=VG,R∪VDI ∧EG,R0=EG,R∪EDI, and •VCI,R0=VCI,R∧ECI,R0=ECI,R. Figu e 5.27 shows he ex ended induced end ule o mo eRailCab . This ex ension is done acco ding o he demande cons ain mo phism o Figu e 5.24(a). As wi h he las sec ion, he ex ended ule does no show any NACs o locks ha ha e been :RailCab d i ing – l – l(d i ing) :T ack + ee – l :T ack – ee – l – l( ee) –wl( ee) «--» on «--» l(on) «--» wl(on) «++» on nex «--» l(nex ) «++» :DI Figu e 5.27: Demanding ule mo eRailCab ’s induced end ule ex ended acco ding o u gency ule immedia elyMo eRailCab 5.6. URGENCY RULES 127 gene a ed o suppo NACs on he le el o du a i e ules. The only new elemen is a demand indica o , which is connec ed o he RailCab node and he igh T ack node. To en o ce he applica ion o he sa is ying ule, he u gency ule induces a sa is ie - i ing imed ule. De ini ion 5.6.3 (Induced sa is ie - i ing imed ule) . Gi en an u gency ule U= (GT , DT , ST , D , S , name , dl) , he induced sa is ie - i ing imed ule o U is a imed ule s = (L,R, ,N,z,V es)whe e •VDI ={di} ∧ ype(di) = diType(name)∧ EDI ={e|s c(e) = di ∧ g (e)∈VDT∧ ype(e) = diEdgeType ◦ g (e)}, •VSI ={si} ∧ ype(si) = siType(name)∧ ESI ={e|s c(e) = si ∧ g (e)∈VST∧ ype(e) = siEdgeType ◦ g (e)}, •VG,L=VGT∪VDI ∪VSI ∧EG,L=EGT∪EDI ∪ESI, •VG,R=VGT∧EG,R=EGT, •VCI,L=VCI,R=∅∧ECI,L=ECI,R=∅, • :L→R, wi h dom( ) = R, is he iden i y mo phism on R, •N=∅, and •z=∅∧V es =∅. The placemen o he demand and sa is ac ion indica o in a sa is ie - i ing imed ule is de e mined by he demande and sa is ie in e ace o i s inducing u gency ule. This ensu es ha he sa is ying ule is applied a a compa ible ma ch, i.e., a ma ch ha is compa ible wi h he s uc u e speci ied in he u gency ule. :RailCab d i ing :T ack on «--» :DI «--» :SI Figu e 5.28: Induced sa is ie - i ing imed ule o u gency ule immedia elyMo e- RailCab Figu e 5.28 shows he sa is ie - i ing imed ule ha has been di ec ly induced by immedia elyMo eRailCab . I consis s o he connec ing g aph o immedia ely- Mo eRailCab wi h an addi ional demand and sa is ac ion indica o in i s LHS. He e, bo h indica o s a e connec ed o bo h nodes because bo h in e ace subg aphs a e iden ical o he connec ing g aph. 128 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS The applica ion o a sa is ie - i ing imed ule is coupled o he applica ion o a demanding ule’s induced end ule ia a sa is ie - i ing in a ian ule. No e ha he in e play be ween a sa is ie - i ing imed ule and a sa is ie - i ing in a ian ule is analogous o ha o a du a i e ule’s induced end ule and in a ian ule. Howe e , ins ead o a du a ion gi en by a du a i e ule, his in a ian ule speci ies a deadline o i ing he sa is ie - i ing imed ule acco ding o he deadline gi en in he u gency ule. De ini ion 5.6.4 (Induced sa is ie - i ing in a ian ule) . Gi en an u gency ule U= (GT , DT , ST , D , S , name , dl) , he induced sa is ie - i ing in a ian ule o U is an in a ian ule s i = (L,z)whe e •VG,L={di} ∧ ype(di) = diType(name)∧EG,L=∅, •VCI,L={ci} ∧ ECI,L={(ci,di)}, and •z={ci ≤dl}. Bo h a sa is ie - i ing imed ule and a sa is ie - i ing in a ian ule need a clock ins ance o ope a e on. Such a clock ins ance is c ea ed by a sa is ie - i ing clock ins ance ule. De ini ion 5.6.5 (Induced sa is ie - i ing clock ins ance ule) . Gi en an u gency ule U= (GT , DT , ST , D , S , name , dl) , he induced sa is ie - i ing clock ins ance ule o U is a clock ins ance ule s c = (L,R, ,N)whe e •VG,L=VG,R={di} ∧ ype(di) = diType(name)∧EG,L=EG,R=∅and •VCI,L=∅∧ECI,L=∅∧VCI,R={ci} ∧ ECI,R={(ci,di)}. Now, we ex end he induced s a ule o an u gency sa is ying ule such ha i c ea es a sa is ac ion indica o in he hos g aph. This ex ension is done analogously o he ex ension o he u gency demanding ule’s end ule. De ini ion 5.6.6 (Ex ension o an u gency sa is ie ’s induced s a ule) . Le U= (GT , DT , ST , D , S , name) be an u gency ule and DR a se o du a i e ules. Fo each u gency sa is ie uple (D , s)∈S , he induced s a ule s = (L , R , , N , z , V es) o D ∈ DR is ex ended in o a imed ule s 0= (L,R0, ,N,z,V es)whe e •VSI ={si} ∧ ype(si) = siType(name)∧ ESI ={e|s c(e) = si ∧ g (e)∈ an(s)∧ ype(e) = siEdgeType ◦s−1◦ g (e)}, •VG,R0=VG,R∪VSI ∧EG,R0=EG,R∪ESI, and •VCI,R0=VCI,R∧ECI,R0=ECI,R. Figu e 5.29 shows he ex ended induced s a ule o (u gency) sa is ying ule b akeRailCab . The ex ension is done acco ding o he sa is ie cons ain mo phism o Figu e 5.24(c). I is analogous o he ex ension o he induced end ule o he 5.6. URGENCY RULES 129 :RailCab d i ing + l + l(d i ing) :T ack + l :T ack ee + l + l( ee) +wl( ee) on «++» l(on) «++» wl(on) nex «++» l(nex ) «++» :SI Figu e 5.29: Sa is ying ule b akeRailCab ’s induced s a ule ex ended acco ding o u gency ule immedia elyMo eRailCab demanding ule. The only new elemen is a sa is ac ion indica o , which is connec ed o he RailCab node and he le T ack node. I he induced s a ule o a sa is ying ule is applied in a si ua ion whe e he e was no demand in u gen execu ion, i c ea es a sa is ac ion indica o ha is no needed and hus no consumed by a sa is ie - i ing imed ule. To p e en such a sa is ac ion indica o om emaining in he sys em un il an un ela ed sa is ie - i ing imed ule is applied, we dele e i immedia ely. This is done by a sa is ie -cleaning imed ule. De ini ion 5.6.7 (Induced sa is ie -cleaning imed ule) . Gi en an u gency ule U= (GT , DT , ST , D , S , name) , he induced sa is ie -cleaning imed ule o U is a imed ule sc = (L,R, ,N,z,V es)whe e •VSI ={si} ∧ ype(si) = siType(name)∧ ESI ={e|s c(e) = si ∧ g (e)∈VST∧ ype(e) = siEdgeType ◦ g (e)}, •VG,L=VST∪VSI ∧EG,L=EST∪ESI, •VG,R=VST∧EG,R=EST, •VCI,L=VCI,R=∅∧ECI,L=ECI,R=∅, • :L→R, wi h dom( ) = R, is he iden i y mo phism on R, •N=∅, and •z=∅∧V es =∅. Figu e 5.30 shows he sa is ie -cleaning imed ule ha has been di ec ly induced by immedia elyMo eRailCab . While his ule looks simila o he sa is ie - i ing imed ule, excep o he missing demand indica o , his does no ha e o be he case o an a bi a y u gency ule. Ins ead o he comple e connec ing g aph, sa is ie - cleaning imed ules only use he subg aph cons i u ing he sa is ie in e ace. The demande in e ace is i ele an o sa is ie -cleaning imed ules, because he e was no applica ion o a demanding ule when a sa is ie -cleaning imed ule is applied. 130 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS :RailCab d i ing :T ack on «--» :SI Figu e 5.30: Induced sa is ie -cleaning imed ule o u gency ule immedia elyMo e- RailCab The applica ion o a sa is ie -cleaning imed ule is coupled o he applica ion o a sa is ying ule’s induced s a ule ia a sa is ie -cleaning in a ian ule. De ini ion 5.6.8 (Induced sa is ie -cleaning in a ian ule) . Gi en an u gency ule U= (GT , DT , ST , D , S , name) , he induced sa is ie -cleaning in a ian ule o U is an in a ian ule sci = (L,z)whe e •VG,L={si} ∧ ype(si) = siType(name)∧EG,L=∅, •VCI,L={ci} ∧ ECI,L={(ci,si)}, and •z={ci =0}. Bo h a sa is ie -cleaning imed ule and a sa is ie -cleaning in a ian ule ope a e on a clock ins ance ha is c ea ed by a sa is ie -cleaning clock ins ance ule. De ini ion 5.6.9 (Induced sa is ie -cleaning clock ins ance ule) . Gi en an u gency ule U= (GT , DT , ST , D , S , name) , he induced sa is ie -cleaning clock ins ance ule o U is a clock ins ance ule scc = (L,R, ,N)whe e •VG,L=VG,R={si} ∧ ype(si) = siType(name)∧EG,L=EG,R=∅and •VCI,L=∅∧ECI,L=∅∧VCI,R={ci} ∧ ECI,R={(ci,si)}. As wi h a du a i e g aph ans o ma ion sys em wi hou u gency ules, he seman ics o a du a i e g aph ans o ma ion sys em wi h u gency ules is gi en by i s induced imed g aph ans o ma ion sys em. Since De ini ions 5.2.18 and 5.5.6 do no ega d u gency ules, we ha e o p o ide a new de ini ion o a du a i e g aph ans o ma ion sys em wi h u gency ules. De ini ion 5.6.10 (Induced imed g aph ans o ma ion sys em espec ing u gency ules) . Le DS = (T G , GT 0 , DR , CR , UR) be a du a i e g aph ans o ma ion sys em ha con ains a se o concu ency ules CR and a se o u gency ules UR and T S = (TG , TiG0 , TR , IR , CR) i s induced imed g aph ans o ma ion sys em espec ing concu ency ules acco ding o De ini ion 5.5.6. I s induced imed g aph ans o ma ion sys em espec ing u gency ules T S0= (TG0 , TiG0 , TR0 , IR0 , CR0) di e s om T S in ha 5.7. RELATED WORK 131 • he induced TGTS ype g aph TG has been ex ended in o a ype g aph TG0 ha con ains a demand indica o ype and a sa is ac ion indica o ype o each u gency ule in UR as well as hei demand indica o edge ypes and sa is ac ion indica o edge ypes, • each imed ule ∈TR whose inducing du a i e ule D is e e enced by an (u gency) demande o (u gency) sa is ie uple o an u gency ule in UR has been ex ended in o a imed ule 0∈TR0 as de ined in De ini ions 5.6.2 and 5.6.6, and i D is e e enced by mul iple (u gency) demande o (u gency) sa is ie uples (o one o mo e u gency ules in UR ), hen he imed ule is ex ended successi ely, and • in addi ion o he ex ended a ian s o hose imed ules in TR , he in a ian ules in IR , and he clock ins ance ules in CR , he induced imed g aph ans o ma ion sys em T S0 also con ains hose imed ules, in a ian ules, and clock ins ance ules ha ha e been induced by UR acco ding o De ini- ions 5.6.3 o 5.6.5 and 5.6.7 o 5.6.9. No e ha i he e is no compa ible sa is ying ule ha can be applied wi hin he u gency ule’s deadline a e he demanding ule’s applica ion (and he e is no imed ule making a sa is ying ule applicable wi hou passing mo e ime han allowed), a ime-s opping deadlock occu s. Du ing ope a ion o he sys em, his is no a p oblem pe se, because he sys em does no ha e o ake a pa h o he s a e space ha leads in o a ime-s opping deadlock. A e all, i is he ask o he sys em’s planning componen o ind a pa h leading o a ce ain goal speci ica ion, and i such a pa h exis s, i i ob iously ee o deadlocks. 5.7 Rela ed Wo k Gyapay e al. [GHV02] p oposed an app oach o g aph ans o ma ion wi h ime ha anno a es codes wi h imes amps, called ch onos alues. Such ch onos alues can be ead and w i en upon applica ion o a g aph ans o ma ion ule. When his is done, all w i en ch onos alues a e se o he same ime, i.e., he i ing ime o he g aph ans o ma ion, which has o be highe han all ch onos alues ead. Whe he o no a node has a ch onos alue is de ined ia he ype g aph, i.e., ei he all nodes o a ce ain ype ha e a ch onos alue o none o hem. By assigning ch onos alues ( ia he RHS) ela i ely o hei alues ead ( ia he LHS), a g aph ans o ma ion ule can be seen as ha ing some so o i ing du a ion, al hough i s applica ion is a omic. The e a e i al di e ences be ween g aph ans o ma ions wi h ime and du a i e g aph ans o ma ions. I he e a e ypes wi hou ch onos alues o ch onos alues o some nodes in he RHS a e no upda ed by a ule applica ion, hen he e can be nonsensical sequences o g aph ans o ma ions, whe e i ing imes a e no mono onically inc easing. I no , hen no concu en applica ion o wo ules is possible i he ma ches o bo h ules o e lap. The eason o his is ha each ule 132 CHAPTER 5. DURATIVE GRAPH TRANSFORMATION SYSTEMS applica ion inc eases he ch onos alues o nodes in i s ma ch by i s i ing du a ion. This is clea ly mo e es ic i e han he DGTS o malism. Since g aph ans o ma ion wi h ime also do no ha e any concep s analogous o ime gua d and in a ian ules, hey would no ha e been a sui able al e na i e o TGTS o implemen ing he a ious concep s o he DGTS o malism. Sy iani and Vangheluwe [SV11; SV08] de eloped a modula language o imed g aph ans o ma ion, called MoTi . I s seman ics is based on Disc e e EVen sys em Speci ica ion (DEVS) [Zei84], whe e g aph a e embedded in e en s being ansmi ed be ween scheduling uni s, called a omic DEVS models, which un in pa allel. In MoTi , a omic DEVS models a e ans o ma ion en i ies, which can ha e di e en execu ion seman ics, e.g., applying a ule once, a all ma ches, o as many imes as possible. These ans o ma ion en i ies ha e a so-called ime ad ance speci ying a delay a e which he ule applica ion occu s, i.e., g aph ans o ma ion ules a e applied ins an aneously. As wi h mos ela ed app oaches, MoTi is mo e simila o imed g aph ans- o ma ion sys ems han o du a i e g aph ans o ma ion sys ems. Howe e , a downside compa ed o he TGTS o malism is ha i is no possible o main ain a single consis en ep esen a ion o he hos g aph when ules a e being applied con- cu en ly, because each ans o ma ion en i y wo ks on i s own copies ansmi ed ia e en s. As a consequence, concu ency issues a e di icul o handle. In he app oach o de La a e al. [La +14; La +10], g aph ans o ma ion ules can schedule he applica ion o o he g aph ans o ma ion ules a a la e poin in ime. The app oach is based on disc e e e en simula ion, i.e., he applica ion o a g aph ans o ma ion ule is conside ed an e en , and he scheduling o e en s is de ined in a s uc u e simila o an e en g aph. This s uc u e con ains so-called in oca ion edges and canceling edges. An in oca ion edge schedules u u e ule applica ions o i s a ge ule when i s sou ce ule has been applied. Canceling edges disca d scheduled ule applica ions o hei a ge ules. A scheduled ule applica ion is also disca ded when i s ma ch is in alida ed by ano he ule applica ion. As a esul o his, he e is no gua an ee ha a scheduled ule applica ion will be execu ed. On he plus side, scheduled ule applica ions may also include ma ching con- s ain s. Fo mally, hese ma ching cons ain s a e de ined simila o cons ain mo phisms in he DGTS o malism. Howe e , he e is no connec ing g aph wi h indi idual in e ace subg aphs. As a consequence, ma ching cons ain s can only be o malized ia elemen s exis ing in bo h ules. Bo ona and Öl eczky [BÖ10] p esen ed MOMENT2, a model ans o ma ion amewo k suppo ing imed beha io . I is based on Maude [Cla+07], which is a speci ica ion language and ool based on ew i ing logic and capable o e i ying in a ian s and LTL p ope ies. MOMENT2 in oduces se e al imed cons uc s: a clock, which inc eases i s alue acco ding o he elapsed ime, a imed alue, which is a clock wi h a (posi i e o nega i e) weigh ing ac o , and a ime , which is a clock unning backwa ds. Time s can be deac i a ed o ese by g aph ans o ma ion ules. I a ime eaches ze o, ime is no allowed o pass anymo e, i.e., a g aph 5.7. RELATED WORK 133 ans o ma ion ule has o be applied be o e he passing o ime may con inue. The pu pose o ime s is hus simila o ha o in a ian ules in he TGTS o malism. The app oach o Ri e a e al. [RDV10] is simila o MOMENT2 in ha i ex- ends in-place model ans o ma ions wi h imed beha io . In hei ool e-Mo ions, du a ions o g aph ans o ma ion ules a e speci ied as in e als ep esen ing he minimum and maximum amoun o ime needed o execu e he g aph ans o - ma ion. I s seman ics is gi en by a mapping o Real-Time Maude [ÖM07]. Simila o a du a i e g aph ans o ma ion ule in DGTS, a ule in e-Mo ions is compiled in o wo ew i e ules, he so-called igge ing and ealiza ion ule. The use o ime s ensu es ha he amoun o ime consumed be ween execu ing hese wo ew i e ules sa is ies he du a ion in e al. As opposed o MOMENT2, his app oach is mo e high-le el because ime s do no ha e o be managed manually. Checking he ule’s applicabili y is implemen ed bo h in he igge ing and ealiza ion ule. Addi ional in a ian checks a e op ional, c . [RVV09]. The ule’s execu ion is implemen ed in he ealiza ion ule. I he LHS ma ch does no exis anymo e when he ealiza ion ule is scheduled o be applied, i s execu ion is being canceled. This migh lead o e oneous beha io i he execu ion o a concu en g aph ans o ma ion elied on his ule. In he DGTS o malism, such a cancella ion o du a i e ules is p e en ed by he use o a locking mechanism. A dis inguishing ea u e o e-Mo ions is he possibili y o e e o pas and concu en ule applica ions, called ac ion execu ions, in g aph ans o ma ion ules. As he e is no equi alen o a locking mechanism, his ea u e has o be used by a designe o p e en con lic ing g aph ans o ma ions om being execu ed concu en ly. Using his ea u e o equi e a concu en ule applica ion sha es simila i ies wi h concu ency ules in he DGTS o malism. Howe e , i is less exp essi e o h ee easons: 1. While he ma ch o a equi ed concu en ule applica ion can be es ic ed o con ain ce ain nodes, i is no possible o speci y he posi ion o hese nodes in he concu en ule’s LHS. As a esul , he concu ency ule allowChangePub- lica ion canno be speci ied co ec ly in e-Mo ions, because i s sa is ying ule o mCon oy has mul iple nodes o he RailCab ype bu only one o hem sa is ies he demand in concu en execu ion. 2. Ma ching cons ain s can only be o malized o nodes appea ing in bo h ules. In he DGTS o malism, ma ching cons ain s a e exp essed ia he s uc u e o he connec ing g aph, which enables o ela e Base nodes in changePublica ion o T ack nodes in mo eRailCab al hough mo eRailCab has no Base nodes and changePublica ion has no T ack nodes. 3. Unlike concu ency ules in he DGTS o malism, i is no possible o speci y a disjunc ion o sa is ying concu en ule applica ions in e-Mo ions. Baldan e al. [Bal+08] p o ide a heo e ical amewo k o he de ini ion o ansac ional g aph ans o ma ion sys ems. A ansac ional g aph ans o ma ion sys ems di e en ia es be ween g aph elemen s ha a e s able and uns able. The s able