A Game Theoretic Approach to the Analysis of Dynamic Networks 1 Abstract

ofDynamicNetworks

1

FrankG.RadmacherandWolfgangThomas

RWTHAachen,LehrstuhlfürInformatik7,52056Aachen,Germany

{radmacher,thomas}@automata.rwth-aachen.de

Abstract

Amodelofdynamicnetworksisintroducedwhichincorporatesthreekindsofnetworkchanges:deletionofnodes(byfaultsorsabotage),restorationofnodes(byactionsof“repair”),andcreationofnodes(byactionsthatextendthenetwork).Theantagonismbetweentheoperationsofdeletionandrestorationresp.creationismodelledbyagamebetweenthetwoagents“Destructor”and“Constructor”.Inthisframeworkofdynamicmodel-checking,weconsiderasspecifications(“winningconditions”forConstructor)elementaryrequirementsonconnectivityofthosenetworkswhicharereachablefromsomeinitialgivennetwork.Weshowsomebasicresultsonthe(un-)decidabilityandhardnessofdynamicmodel-checkingproblems.Keywords:adaptivesystems,dynamicnetworks,dynamicgraphproblems,model-checking,gametheory.

1IntroductionandMotivation

Theclassicalmethodologyofmodel-checking(see[6])referstoafixedsystemandaspecificationofitsbehavior.Usuallythestatesandtransitionsofthesystemunderconsiderationarecollectedinatransitiongraph(Kripkestructure),andtheonlydynamicaspectisthechangeofstate(viaavailabletransitions)whichisthencap-turedbytheconceptofanexecutionpathor(ifbranchingbehaviorisconsidered)ofacomputationtree.Specificationsaredefinitionsofdesiredpropertiesofexecutionpathsorcomputationtrees.

Atheoryofmodel-checkingoverdynamicstructuresisstillverymuchinitsbe-ginnings.Somereferencesknowntousare[15,3,13]wherethedatastructureswithadynamicbehavior(likeprogramsorUMLstatemachines)areefficientlyencoded(e.g.aslistsortrees)fortheuseofwell-establishedmodel-checkingmethods.Theobjectiveofthispaperistointroduce(andproveinitialresultson)asimplebutquitegeneralmodelforstudyingnetworkswhichchangeovertime.Weconsidergraphsasmodelsofcommunicationnetworks.Suchanetworkisassumedtochangeovertime

1

ResearchwassupportedbytheRWTHAachenResearchClusterUMIC(UltraHighSpeedMobileInfor-mationandCommunication)oftheGermanExcellenceInitiative.

uvuv

Figure1.Movementofstrongnodewithrestoration.

bythedeletionandcreationofnodes.ThedifferentnetworksarisinginthiswayfromanoriginalnetworkGcanbecollectedinaKripkestructurewhoseelementsarenetworksreachablefromGbysuccessiveoperationsofnetworkmodification.Sowedealwithahierarchicalmodelinwhichthefirstlayercapturesnetworksandthesecond(representedbytheKripkestructure)thedynamicsofnetworks.Insteadofexecutionpathsweconsider“networkevolvementpaths”,andspecificationstyp-icallyareaddressingpropertiesofnetworksthatshouldholdthroughout(safetyproperties)orpropertiesthatshouldbeachieved(reachabilityconditions).Morecomplicatedspecificationsarepossible(e.g.,referringtostandardtemporallogicslikeLTL)butarenotpursuedinthepresentpaper.

Twolevelsofthedynamicshavetobedistinguished:Thefirstisconcernedonlywithinformationflowthroughanetwork,orachangeofstatesofthenodesofthenetwork.Nodesandedgesassuchstayfixed.Anaturalwaytodescribethisaspectistoassumealabelingofthenodesthatmaychangeovertime.Theclassicalmodel-checkingproblemcanbeseenasaspecialcaseofthisdynamiclabeling:WeconsidertheKripkestructureasanetworkandindicatethecurrentstateoftheKripkestructurebyaspeciallabelatthecorrespondingnode,or–inotherwords–asatokenonthisnode.Astepconsistsofashiftofthetokentoaneighbornodereachableviaatransition;thisobviouslyisaspecialcaseofre-labeling.Inthegeneralcasewehavelabelsandchangelabelssimultaneouslyinseveralnodesofthenetworkunderconsideration.Weshallcapturethisideaof“informationflow”byre-labelingrules.

Thesecondaspectofthedynamicsinvolvesachangeinthesetofnodesand/orthesetofedges.Inthepresentpaperweonlyconsiderchangesinthesetofnodes(andinducedchangesinthesetofedges).Themoregeneralcasethatariseswhenincludingedgesinthedynamicsinvolvesheaviernotationbutdoesnotaffectthegeneralresultsastheyappearinthispaper.Wedistinguishthreetypesofchanges,withan“original”networkGasareference.Wemaydeletenodes,wemayrestorenodesthathadbeeninexistencebefore,orwemaycreatecompletelynewnodes.Allthesestepsinvolvetheconceptof“strongness”ofanode:Astrongnodecannotbedeleted,anditistheprerequisiteforperformingtherestorationandcreationofnodes.Inthecontextofcommunicationnetworks,onecanviewthestrongnodesasstationswheremaintenanceresourcesarelocated.Theseresourcesmaytravelthroughedgestoexistingnodes,andtheymayatsomenodeurestoreadeletednodevbymovingtoitiftherewasanedge(u,v)inthenetworkbeforethedeletionofv(seeFig.1).

ForthecreationofanodewecanpicksomesetSofstrongnodes,createanewnodev(thatisorisnotstrong)andconnectitwitheachofthenodesinSbyatransition(seeFig.2).Thiscorrespondstotheassumptionthatcreationis“moreexpensive”thanrestoration.

Bothkindsofrulescanbeappliedeithergenerallyorsubjecttoconstraintswhichrefertothecurrentlabelingofnodes.

2

v

u1u2u3u1u2u3

Figure2.CreationofanewnodebyasetU={u1,u2,u3}ofstrongnodes.

Wemodelthenaturalantagonismbetweenthedeletionandrestorationresp.creationofnodesbyatwo-playergamebetweenthetwoagents“Destructor”(per-formingdeletionactionsanywhereinthenetwork)and“Constructor”(performingtheactionsofrestorationandcreation).NotethattheactionsofDestructoroc-curgloballyinthenetwork,whereastheactionsofConstructoroccurlocally(theyarebasedonshiftingstrongnessofnodestoneighbors).Thisasymmetrybetweendeletionandrestorationorcreationseemsadequateformodellingphenomenaoffault-tolerance:Faultsmayhappenanywhere,butactionsofrepairneedcoordi-nationofresources.Forsimplicity,weshallconsiderhereonlyturn-basedgameswhereDestructorandConstructoractinalternation(butbothhavetheoptiontoskip).AnothersimplificationistheassumptionthatConstructor’s(andDestruc-tor’s)movesaredecidedtakingintoaccountfullinformationaboutthecurrentnetwork.(Thissimplifyingassumptionistobedroppedinfuturework,usingthemechanismofinformationflow.)ThetaskofConstructoristoenforcethatproper-tiesgiveninaspecificationwillbereached(orpreserved)againstanysequenceofmovesbyDestructor.

Specificationsfordynamicnetworksaretypicallyconcernedwithguaranteeingdesirablepropertiesofnetworks.Inthepresentpaperweonlyconsidertheproper-tiesofconnectivityandbiconnectivity.(Agraphisbiconnectedifdeletionofanynodestillleadstoaconnectedgraph.)Therearemanysimilarproperties,likek-connectivity,havingasmalldiameter,havingacertainminimaldegreeforallnodes,etc.

Thedynamicmodel-checkingproblemnowtakestheformofaproblemofgamesolution,whereanetworkGandasetRofrulesforitsmodificationaregiven.WeassociatedeletionstepswithDestructorandallothermoveswithConstructor.

Forexamplewecanaskforasolutionofasafetygame,givenGandR:StartingfromG,doesConstructorhaveawinningstrategytoguaranteethatthenetworkalwaysstaysconnected?

Areachabilitygameisgivenbythefollowingproblem:

StartingfromGwhichisconnected,doesConstructorhaveawinningstrategythatwillleadtoabiconnectedgraph?

Thesearefirstexamplesofamuchwiderclassofproblemsthatarestudiedinthealgorithmictheoryofinfinitegames(see[9]).Theperspectiveofourworkistolinkthistheorytotheanalysisofdynamicnetworks.

Thepaperisstructuredasfollows.Inthenextsectionwebrieflydiscussrelatedwork.Thenwepresentourmodelinformaldetail.Afterthatwelistsomenaturalnetworkpropertiesthatarerelevantinthepresentcontextandshowsomeinitialresultsonthesolutionofdynamicmodel-checkingproblems.Notsurprisingly,it

3

turnsoutthatinthegeneralframeworkthereachabilityproblemisundecidable.Intherestrictedcaseof“non-expansive”dynamicnetworksweobtaindecidabilitybutestablishsomehardnessresults.Intheconcludingsectionweaddressperspectivesofthegametheoreticanalysisofdynamicnetworkswhicharetreatedinongoingwork.

2RelatedWork

Thegametheoreticframeworkdevelopedhereisanextensionofthetheoryof“sabotagegames”suggestedbyvanBenthem(cf.[22])anddevelopedbyPh.RohdeandC.LödingatRWTHAachen;see[17,18,16,19,20].Thenetworksinthesepapersaredirectedgraphswithpossiblymultipleedgesbetweennodes,onwhichaplayer“Runner”wantstoreachanodevfromagivenstartnodeu.AftereachmoveofRunner,theadversary,called“Blocker”,maydeleteanedge;andinthiswayRunnerandBlockermoveinalternation.ThealgorithmicproblemofsolvingthisgameasksforawinningstrategyforRunnerthatenableshimtoreachnodevagainstanychoiceofBlockerindeletingedges.Notethatthisgameinvolvesonlyre-labelings(shiftofpositionofRunner)and(edge-)deletions.Asinthegeneralgameabove,themovesofthe“good”playerarelocal(i.e.,transitionsthroughavailableedges),whereasthe“bad”player(theBlocker)canactgloballyandaccessanyexistingedgeinanymove.

AnotherinterestingapproacharisesfromthestudiesofdynamicversionsoftheDynamicLogicofPermission(DLP)whichisinturnanextensionoftheProposi-tionalDynamicLogic(PDL).InDLP,“computations”inaKripkestructurefromonestatetoanotherareconsideredwhicharesubjectto“permissions”.ThelogicDLP+dyn(see[5,8])extendsDLPwithformulaswhichallowupdatesofthepermissionsetandthuscanbeseenasadynamicallychangingKripkestructure.Nevertheless,allthedynamicshavetobespecifiedintheformula;anadversarialplayerisnotconsidered.

Previousstudiesofdynamicnetworksaddressingtheaspectofadversarialagentshavebeenconcernedwithroutingproblems.Insuchstudiesitwaseitherassumedthatthenetworkunderconsiderationstaysconnectedortheconnectivityofthenetworkisatleastgiveninfinitelyoftenovertime(cf.[6,1,2]).

Theideaofchangingnetworksisofcoursestudiedinconsiderabledepthinthetheoryofgraphgrammars,graphrewriting,andgraphtransformations(see[4,21]).Whiletheretheclassofgenerablegraphs(networks)isthefocusofstudy,wedealherewithamorerefinedviewwhenconsidering“evolvementpaths”andtheproper-tiesofgraphsoccurringinthem.Inthe“one-player”frameworkofmodel-checking,wementionthework[7]wheregraph-interpretedtemporallogicisintroducedasarule-basedspecification.ItextendsLTLbyinterpretingformulasontransitionsystemswhichnodesaregraphs.Atechniqueisdevelopedtomapthe“graphtran-sitionsystems”tofiniteKripkestructures,sothatclassicalLTL-model-checkingcanbeapplied.

Infinitemodeltheory,S.Patnaik,N.Immerman,andW.Hessedevelopedatheoryof“dynamiccomplexity”(cf.[11,10]).Forexample,thedecisionproblemDynREACHisthequestionwhether,giventwoverticesuandvandasequenceof

4

edgeinsertionsanddeletions(aswellaschangesofuandv),thereisapathfromutov.Thisproblemcorrespondstotherestrictionofourframeworktoone-playergames,whereConstructorcanaddanddeleteedgesfromnetworks.Forthisproblemtherearemotivationsindatabasetheory,buttheasymmetrybetweenDestructorandConstructor(asinsettingswherefaulttoleranceistheguidingmotivation)ismissing.

Inthetheoryoffullydynamicalgorithms,dynamicgraphsinwhichverticesandedgesareinsertedordeletedareconsidered,butthefocusofinvestigationisthecomputationalcomplexityofstaticgraphpropertieswithrespecttoagivenupdatestepresp.agivensequenceofupdatesteps(cf.[14,12]).

3

3.1

DynamicNetworksviaGames

TheBasicModel

WepresentnetworksintheformG=(V,E,A,S,(Pa)a∈Σ)with

•••••

afinitesetVofvertices(alsocallednodes),anundirectededgerelationE,asetA⊆Vof“activenodes”,asetS⊆Aof“strongnodes”,

apartitionofVintosetsPaforsomelabelalphabetΣ(AnodebelongstoPaifitcarrieslabela.Fortechnicalsimplicityweincludeablanksymbol󰀂󰀁inΣ(asadefaultfor“unlabeled”nodes).

ThedynamicsofanetworkarisesfromaninitialnetworkGbythepossiblemovesfromDestructorandConstructor(Constructor’smovesaresubjectofasetofrules)whicharechangingtherespectivecurrentnetwork.AgamearenawillbepresentedasapairG=(G,R),withaninitialnetworkGasaboveandafinitesetRofrulesforConstructor.(InthisworkwewillalwayshaveA=VfortheinitialgraphG;nonodesaredeletedatthebeginningoftheplay.)

ThetwoplayersDestructorandConstructorplayturnbyturn(Destructorstarts).Inourmodeltheplayersareallowedtoskipaswell.Playsareinfiniteingeneral,butmaybeconsideredfiniteinthecaseswhereneitheroftheplayerscanmove,oragivenwinningconditionissatisfied.

Letusdescribetherulesthatdefinethemoves.WhenitisDestructor’sturn,hecandoadeletionstepbydeletingsomenodev∈(A\\S);AischangedtoA\\{v}.

WhenitisConstructor’sturn,shecanmakeinaccordancewithhisrulesetRamoveofoneofthefollowingtypes:

Labelingrule:󰀐a,b−→c,d󰀑meanstochangethelabelsaandboftwoedge-connectednodesofAintocandd,respectively.Inthecaseof“pureinformationflow”wehaveb,c=󰀂󰀁anda=d.Formally,forapair(u,v)∈Ewithu∈Paandv∈PbthesetsPa,Pb,Pc,andPdareupdatedtoPa\\{u},Pb\\{v},Pc∪{u},andPd∪{v}.

Forlabelingruleswewillalsoconsiderruleswithmultiplere-labelingsinoneturn.Thiscorrespondstoourintuitionthattherecanbealotofinformation

5

flowinthenetworkatthesametime.Forexamplefortwolabelingrulesinoneturnweusethenotation󰀐a,b−→c,d;e,f−→g,h󰀑.Therulesareappliedoneaftertheotherbutinthesameturn.

Moveofstrongnoderesp.restorationofnode:Foranarbitraryu∈Swithanedge(u,v)∈Eandanodev∈S,updateSto(S\\{u})∪{v}andAtoA∪{v}.Incasev∈Athismeanstosimplyshiftstrongnesstov;incasev∈V\\Athismeansrestorationofv.Theabilityofastrongnodetomovemaybesubjectto

move

acertainlabeling(a,b)ofthepair(u,v).WeusetheNotation󰀐a−−−→b󰀑.Creationofnode:TakeanysetU⊆Sofstrongnodes,createanewnodewandconnectittothenodesofU.Formally,thesetsVandAareupdatedtoV∪{w},resp.A∪{w},andalsoEisupdatedbyaddingedgesbetweenwandeachnodeofU.Thecreationmaybesubjecttothenodelabelsa1,...,an(n=|U|)ofthenodesinU.AlsothelabelsofthenodesinUmaychangeaftercreation(to

󰀂󰀂a󰀂−−−−→a󰀂1,...,an).Weusethenotation󰀐a1,...,an−1,...,an󰀑,whenthenew

create󰀂−−→a󰀂nodewislabeledwithc.Bysimplywriting󰀐a1,...,an−1,...,an󰀑we

assumewgetsthelabel󰀂󰀁.Forthecreationofastrongnodeweusethenotation󰀂󰀐a1,...,an−−−−−−→a󰀂1,...,an󰀑.InthiscasealsoSisupdatedtoS∪{w}.Note

thatthesemovesaretheonlyonesthatchangeVandE.Thenewnodewiscreatedonlyonce;itcanhenceforthonlybedeletedandrestored.

s-create(c)

create(c)

ForagamearenaasgivenhereandanetworkpropertyP,wedistinguishtwotypesofgamesreferringtoP:

•

SafetyGamewithrespecttoP:DoesConstructorhaveawinningstrategytopreserve,startingfromGandproceedingbytherulesofR,thepropertyPforallnetworksreachedinaplay?

ReachabilityGamewithrespecttoP:DoesConstructorhaveawinningstrategytoguarantee,startingfromGandproceedingbytherulesofR,thatsomenetworkwithpropertyPisreached?

•

TheDynamicModel-CheckingProblem(inthesafety,respectivelyreachabilityformat)consistsofthequestion,givenGandRandnetworkpropertyP,whetherConstructorhasawinningstrategyinthesafetygame,respectivelyreachabilitygameforP.

Moregenerally,onecanintroduce,referringtonetworkpropertiesP1,...Pn,thetemporallogicLTLoverP1,...,Pnandaskforwinningstrategiesthatguar-anteesatisfactionofanLTL-formulaforaninfiniteplaybetweenDestructorandConstructor.

Example3.1ConsiderthegamearenaG=(G,R)withlabels⊥,󰀂󰀁inΣ.TheinitialgamegraphG=(V,E,A,S,(Pa)a∈Σ)withthesetS={s1,s2,u1,w1}ofstrongnodesisdepictedinFig.3.

ConsiderasrulesRonlymovesofstrongnodes(ifapplicablewithrestoration)

move

labeledwithablank:󰀐󰀂󰀁−−−→󰀂󰀁󰀑.Thestrongnodess1ands2arenotabletomove,becausetheirlabeldoesnotmatchthemoverule.Asascenarioforthisgamearenawecouldimaginetwoclientss1,s2whichcommunicateoveranetworkwithunreliableintermediatenodesbuttwomobilemaintenanceressources.

6

u3󰀂󰀁

u2󰀂󰀁

v1󰀂󰀁

w1󰀂󰀁

s2⊥

⊥s1

󰀂󰀁u1

󰀂󰀁v2

󰀂󰀁w2

󰀂󰀁w3

Figure3.Anexampleinitialgamegraph(boldnodesarestrong).

Weconsiderasafetygamewithconnectivityofs1ands2aspropertyP.So,weareinterestedinthequestionwhetherConstructorcanalwaysguaranteethatthereisapathfroms1tos2inthenetwork.IfwetakeacloserlookatthisexampleweseethatDestructorhasawinningstrategy.Hecandeletew3inhisfirstmove.Thenwedistinguishbetweentwocases:IfConstructorrestoresw3thenDestructordeletesv1inhisnextmoveandfinallyu1orv2.IfConstructordoesnotmovetheuppermovablestrongnodetow3thisnodehastoremainatw1,otherwiseConstructorlosesbydeletionofw1.InthiscaseitiseasytoseethatDestructorwinsbyasuitabledeletionofnodesin{u1,u2,v1,v2}.

Nowweconsiderthesamegame,butadditionallywiththerule󰀐󰀂󰀁,󰀂󰀁−−−→󰀂󰀁,󰀂󰀁󰀑.WeclaimthatnowConstructorhasawinningstrategy.IfDestructordeletesthevertexv1orv2Constructorcreatesanewvertexv3withthecreationrulewhichestablishesanewconnectionbetweenthetwostrongnodesu1andw1.IfDestructordeletesthenewvertexv3Constructorcreatesanewvertexagain,andsoon.NotethatinthiswaythesetVofverticesofthegraphcanincreasetoanunboundednumber.

Evenintheseverysmallexamplestheexactformalizationofthewinningstrate-giesisquitecomplex.So,thisexampleshouldalreadysufficeasamotivationforformalmodel-checkingmethods.3.2

RemarksonSpecialCasesandVariants

create

Themodelintroducedaboveisquitegeneral,andmanyspecialcasesandvariantscanbestudied.Weonlymentionthreeofthem.

(i)ClassicalModel-Checking:AsmentionedintheIntroduction,theclassical

model-checkingproblemforLTLcanbecapturedasaspecialcaseofthedy-namicmodel-checkingproblem(intheframeworkofLTL).Inthiscase,thegraphisdirectedandthepropertiesP1,...,Pnrefertopointedgraphs(G,v)(soPimaybeconsideredasavertexratherthanagraph).Destructorstayssilent–sowehaveasolitairegame–,andConstructorrealizesthechangeofthe“currentstate”byshiftingatokenthroughthegivengraph(usingonlyre-labelingrules).(ii)SolitaireGames:Inthiscase,onlyConstructormovesandkeepscontrolof

theevolvementofnetworks.Deletionandhencerestorationmovesarenotadmitted,andthemovesthatremainareeitherthecreationorthere-labelingofnodes.Avariantsuggestedbythesolitairemodelisthesituationwhere

7

Constructoralsocarriesoutthedeletionmoves.Thiscorrespondstoasituationwheretheevolvementofastructure(here:anetwork)iscontrolledcompletelybyoneagent.

(iii)Non-expansiveGames:ForpropergamesbetweenDestructorandConstructor,

wecanconsiderthespecialcasethatConstructordoesnotusecreationmoves.Thenwecalltherulesnon-expanding.ThissituationcorrespondstoanetworkevolvementwheretheoriginalsetVofnodesisneverextended.Obviously,thesetofnetworksreachablefromagiveninitialgraph–i.e.,theKripkestructurebuiltfromG–isfiniteinthiscase.Asaconsequence,the“non-expandingdynamicmodel-checkingproblem”(inthesafety-,reachability-,orevenLTL-format)isdecidable.Belowweshowthatdroppingtheconditionofnon-expansioncausesundecidability.Therearemanymorevariantsthatmighthavegoodmotivationsfromdifferentapplications.Anaturalvariantistoconsiderdeletionandinsertionofedgesratherthannodes(orevenofboth,nodesandedges).Thiswouldrequirecorrespondingconventionsregardingtherulesandtheirreferencetolabels.Notethatthesabotagegameswerebasedontheideaofedgedeletion.Forthegeneralresultsshowninthispaper,thisaspectisnotessential;sowedonotpursueit.However,itwillplayamajorroleforrefinedstudies,e.g.concerninginformationflow.

ApossiblecriticismaboutourframeworkmaybetheradicaldifferencebetweenDestructorandConstructor,whichputstheformerintoanadvantage.Thiscanberemediedbynaturalconventions,forexamplebytheassumptionthatDestructorkeepssilent(i.e.,skips)forcertainperiodsoftimeuntiladeletioniscarriedout.ItdependsontherespectiveareaofapplicationhowabalancebetweenConstructorandDestructorshouldbetuned.Inthecontextoffaulttolerance(whichisthemotivationofourwork),itisnaturaltoassumethatthatthedeletionactionsofDestructorareundesirableandthecreationandrestortationactionsofConstruc-toraredesirable.Inotherdomains,theconverseisconceivable.Thepurposeofthepresentpaperistoexhibitaframeworkwheresuchmodificationareeasytoincorporate.

4BasicResultsonDynamicModel-Checking

Letuslistsomebasicnetworkpropertiesthatarisenaturallyinourframework.WerefertotherestrictionofnetworksinthesimpleformatG=(V,E)ofplainundirectedgraphs.Asapreliminaryremarkwementionthatinmostpracticalapplicationsthedegreeofnetworksshouldbeboundedbyaconstantd(meaningthateachnodeisconnectedtoatmostdneighbors).

AgraphG=(V,E)isconnectedifforeachu,v∈Vthereisapathfromutov.Itisbiconnected(resp.k-connectedfork>2)ifforeachnodev(resp.foreachk−1-tuple(v1,...,vk−1)ofnodes)theinducedgraphoverV\\{v}(resp.V\\{v1,...,vk−1})isconnected.AgraphG=(V,E)isofdiameterdifforeachpairu,v∈Vthereisapathfromutovoflength≤d.

Inourfirstresultweshowthatthedynamicmodel-checkingproblemeveninthesolitaireversion(whereDestructoralwaysdecidestoskip)withrespecttoconnec-8

tivitypropertiesisundecidable.Theessentialfeatureoftheundecidabilityproofistheavailabilityofcreationmoves.

Theorem4.1Thedynamicmodel-checkingforsolitairegamesinreachabilityfor-matisundecidableinthefollowingversion:GivenaconnectednetworkGandafinitesetRofrulesforConstructor,isthereastrategyforConstructortoreachabiconnectednetwork?

ProofWeuseareductiontothehaltingproblemforTuringmachines.WepresentTuringmachinesintheformat

M=(Q,Γ,δ,q0,qstop)

withastatesetQ,tapealphabetΓ(weassumeQ∩Γ=∅),transitionfunctionδ:Q\\{qstop}×Γ→Q×Γ×{L,R},initialstateq0,andstopstateqstop.

ForeachsuchTuringmachineMweconstructasolitairegame(i.e.aninitialconnectednetworkGandasetRofrules)suchthatMhaltswhenstartedontheemptytapeiffConstructorcanreachabiconnectednetworkfromGbyapplyingtherulesofR.

TheideaoftheconstructionistorepresentaTuringmachineconfiguration[a1...anqb1...bm](here,[and]areleftandrightmarker,respectively)byase-quenceofn+m+3nodeslabeledwiththesesymbolsinsuccession.ThelabelalphabetthuscontainsthetapealphabetofM,thestatesofM,andtheendmark-ers.Forlateruseweallowalsotheletters[s,]s,p+foreachstatep∈Q,andasforeachletteraofthetapealphabet.

Asinitialgraphwetakethethreenodegraphwithnodeslabeled[,q0,].Wedefinethesethreenodesasstrong.

Itiseasytosupplyasetofre-labelingruleswhichallowtochangethislinegraphonlyinawaythatthecomputationofMstartingwiththeemptytapeissimulated.Formally,foreachpair(q,a,p,b,X)withδ(q,a)=(p,b,X)weaddthegamerules󰀐q,a−→p+,b󰀑and󰀐y,p+−→p,y󰀑ifX=L,and󰀐q,a−→b,p󰀑ifX=R(here,ydenotesanarbitrarylabelofΓ∪{󰀂󰀁}).

Forthecasethatmorespaceisneeded(beyondthecurrentendmarkers),weintroducecreationstepssubjecttolabelings,makingtheendmarkernodesstrongagain:󰀐[−−−−−−→󰀂󰀁󰀑and󰀐]−−−−−−→󰀂󰀁󰀑.

Finally,weallowspecialre-labelingrulesthatcanbeappliedwhenthefinalstateqstopisreached.Theextraindex“s”isnowpropagatedthroughtheexistinglinegraphtotherightandtotheleft,usingtheextralettersmentionedabove.Giventwostrongnodeswithlabels[s,]s,weallowtocreateanewnodewconnectedwithbothofthem,thusgeneratingacirclegraph(whichofcourseisbiconnected).2Theresultalsoholdsforthetwo-playergame.Sinceinoursimulationwehavedefinedallnodesasstrong,thepresenceofadestructiveplayerdoesnotchangetheplaysofthegame.

Notethattheproofreliesontheavailabilityofcreationmoves;ifthesearecancelled,theproblembecomestriviallydecidable:

9

s-create([)

s-create(])

Remark4.2Thedynamicmodel-checkingprobleminthereachabilityandthesafetyversionisdecidablefornon-expandingnetworks.

Fortheproofitsufficestoobservethatfromtheinitialnetworkonlyfinitelymanydistinctnetworks(overtheunchangedoriginalvertexsetV)canbegenerated.IfthereareNsuchnetworks,eachplaywillyieldarepetitionafteratmostNsteps.Hence,fordecidingthewinner(andprovidingawinningstrategy)itsufficestobuildupthegametreeuptodepthN.

Remark4.3Inordertokeepthemodelsimplewedonotconsiderscenarioswheredeletionandinsertionofedgesareallowed.Sincethenumberofpossibleedgesinthe󰀂|V|󰀁

non-expansivecaseisboundedby2,theabsenceofedgeinsertionanddeletionisinsignificantforthedecidabilityofthemodel-checkingproblem.

Inthefollowingwewillshowthatsolvabilityofnon-expansivegames(i.e.,with-outcreationrules)isPSPACE-hard.Weuseareductiontothesolutionofsabotagegamesasmentionedintheintroduction.LödingandRohdeshowedthatthesabo-tagegameproblemiscompleteforthePSPACE[17,18,20].Letusrecallthepreciseformulation.

AsabotagegameGs=(Gs,vin)isplayedonagamegraphGs=(V,E)whichchangesovertime;alsoadesignatedsetF⊆Visgiven.Thetwoplayers,calledRunnerandBlocker,playasfollows:Runnerstartstheplayinavertexvinandmovestoanodev󰀂with(vin,v󰀂)∈E.ThenplayerBlockererasesanedge(w,w󰀂)∈EresultinginagraphG󰀂.RunnercontinuestheplayonG󰀂,andsooninalternation.RunnerwinsiffshecancanreachavertexinthegivensetF⊆Voffinalvertices.

LödingandRohdeintroducedsabotagegameswithmulti-graphs(withpossiblymultipleedges),butshowedthatsingle-graphssuffice(seeLemma1in[18]).Theorem4.4Inthenon-expansivecase,thedynamicmodel-checkingprobleminthereachabilityversionisPSPACE-hard.

ProofConsiderasabotagegameGs=(Gs,vin)ontheinitialgamegraphGs=(Vs,Es)andasetF⊆Vsoffinalvertices.WeconstructagamearenaG=(G,R)withnodelabels‘vertex’,‘edge’,‘run’,‘acc’,‘reach’inthealphabetΣwiththepurposethatConstructorcanreachanetworkinGcontainingalabel‘reach’iffRunnerwinsthesabotagegameGs.

TheideaistosimulatetheRunnerbylabelingrulesoftheform󰀐run,∗−→∗,run󰀑.Wesimulateedgeremovalbynoderemovalasfollows:WemaketheverticesoftheoriginalinitialgraphGsunerasablebymakingthemtounmovablestrongnodes.ThenweaddonevertexforeachedgeinES.InsteadofdeletingedgesDestructormaydeletethesenewvertices.InordertoallowConstructorto“move”therunlabelfromoneunerasablevertextoanother,shemaketwore-labelingstepsinoneturn.

Figure4showstheinitialgraphGsofanexamplesabotagegameandtheequiv-alentinitialgamegraphGofourgame.

TheinitialgamegraphisG=(V,E,A,S,(Pa)a∈Σ)withV:=Vs∪Es,andEarisesfromEsasinthefigure.AdditionallyletPvertex:=Vs\\({vin}∪F),Pedge:=Es,Prun:={vin},Pacc:=F,Preach:=∅,andS:=Vs.

10

acc

edge

run

edge

vertex

edge

acc

Figure4.InitialgraphGsofasabotagegameandcorrespondinginitialgraphGofthereachabilitygame.

InordertosimulatethemovementofRunnerthesetRcontainstherules󰀐run,edge−→vertex,run;run,vertex−→edge,run󰀑and󰀐run,edge−→vertex,run;run,acc−→edge,reach󰀑.TheserulesallowConstructortopropagatethe‘run’labelfromone‘vertex’-labelednodetoanotherbypassingonenon-deleted‘edge’-labelednode.Ifthe‘run’-labelreachesthe‘acc’-labelitisre-labeledto‘reach’.Notethattherearenomovementresp.restorationrulesinR,sothatallstrongnodes(notlabeledwith‘edge’)areconsideredunerasable.

InthisproofweassumeConstructorstartsthegame(alikeRunnerstartsthesabotagegame).(Thiscouldbeeasilyachievedbyconnectingthe‘run’-nodetoone‘acc’-nodewithanadditional‘edge’-labelednode.So,Destructordeletesthisextra‘edge’-labelednodeinhisfirstturn.)

ThedeletionofthenodesinEsresp.thepropagationofthe‘run’-labelfromonnodeinVstoanothercorrespondstotheedge-deletionresp.tothemovementofRunnerinthesabotagegame.Hence,Constructorcanreachanetworkcontainingalabel‘reach’inGiffRunnerwinsthesabotagegameGs.2Notethatwedonothaveanymovementresp.restorationstepsintheproof,sotheproblemremainsPSPACE-hardforrestrictingourgamesbyprohibitingthoserules.

Onemighthavetheimpressionthatthehighcomplexityforthecasewithoutnodecreationisonlyduetoconsiderationofinformationflowresp.labelingrules.Butevenwithouttheserules,simplequestionslikeconnectivitycausecomputationalproblems.WepresentacorrespondingPSPACE-hardnessresultinThm.4.6belowusingareductiontosabotagegamesagain.Forreaderswhopreferareductiontoastandardproblem,weincludealsoaNP-hardnessproof(invokingthevertexcoverproblem).

Theorem4.5Inthenon-expansivecasewithoutconsiderationofinformationflow,thedynamicmodel-checkingproblemwithrespecttoconnectivityinthesafetyversionisNP-hard.

ProofWereducethevertexcoverproblemwhichiswell-knowntobeNP-hardtothequestionwhetherConstructorcanguaranteeconnectivityofthenetworkinthesafetygame.

Westatethevertexcoverprobleminthefollowingform:GivenagraphGVC=(V󰀂,E󰀂)andanintegerk,isthereavertexcoverofthesizekorlessforGVC?

WeconstructagamearenaG=(G,R)withlabels‘vertex’,‘edge’,‘keeper’,

11

󰀂󰀁

t1

edge

󰀂󰀁

t2

edge

edgeedge

vertexvertexvertexvertexvertex

keeperstoragestorage

rs1s2

Figure5.AnordinarygraphGVCandcorrespondinginitialgraphGofthesafetygamefortestingGVCforavertexcoverofsize2.

‘storage’,󰀂󰀁inΣ.TheideaistoadaptGVCfortheinitialgraphofGbyaddinganunmovablestrongnodeforeachedge.WekeeptheoriginalnodesofGVCaserasablenodes.Theseerasableverticesareconnectedwitha“storage”ofkmovablestrongnodess1,...,sk.Theerasableverticesarealsoconnectedwithanunmovablestrongnoderwhichkeepstheverticesconnected.So,inaplayDestructorcanonlytrytoisolatethe‘edge’-labelednodesbydeletingthe‘vertex’-labelednodes.ConstructorcanonlypreserveconnectivityofGbymovingthekstrongnodesofthestoragetotheverticeswhichareavertexcoverforGVC.

Additionally,knodeslabeledwith󰀂󰀁areconnectedwiththe‘edge’-labelednodestopreventDestructorfromwinningbeforeConstructorcanmovethenodesofthestoragetothevertexcover.Destructorcandeletethese󰀂󰀁-nodeswithinkturnsandthereisnowayforConstructortorestorethem.

ForexampleinthegraphinFig.5(ontheleft)thereexistsavertexcoverofsize2,sotwostrongstoragenodes(andtwoadditionalnodeslabeledwith󰀂󰀁)arenecessaryforConstructortopreservetheconnectivity(intheright-handgraph).

Formally,theinitialgamegraphisG=(V,E,A,(Pa)a∈Σ,S)withV:=V󰀂∪E󰀂∪{r,s1,...,sk,t1,...,tk},andEarisesfromE󰀂asinthefigure.AdditionallyletPvertex:=V󰀂Pedge:=E󰀂,Pkeeper:={r},Pstorage:={s1,...,sk},P󰀂󰀁:={t1,...,tk},andS:=E󰀂∪{r,s1,...,sk}.

Inordertoallowmovementofthestrongstoragenodestothenodeslabeled

move

with‘vertex’weaddarule󰀐storage−−−→vertex󰀑toR.NotethatthisistheonlyruleinR,sothattheotherstrongnodes(notlabeledwith‘storage’)areunmovable.

Clearly,ifforGVCavertexcoverofsizekexists,playerConstructorwinsbymovingkstrongnodestothevertexcover.

FortheotherdirectionnoticethatitisbestforConstructortomovenodestotheerasablenodeslabeledwith‘vertex’.Sinceonlythekstrongstoragenodesaremovable,ConstructorcanonlykeepthepersistenceofknodesofVGofherchoice.IfConstructorwins,thesenodesareavertexcoverofsizekforGVC.2Asannounced,wenowsharpenthisresulttoPSPACE-hardness,usingareduc-tiontothesolutionofsabotagegames(whichisPSPACE-complete[17,18,20]).WeshowthattheproblemisPSPACE-hardeveninthecaseweomitthedistinctionofnodelabels(i.e.,allnodesarelabeledwith󰀂󰀁).

12

󰀂󰀁···vtargetK|Vs|󰀂󰀁···󰀂󰀁󰀂󰀁···󰀂󰀁Figure6.InitialgraphGsofasabotagegameandcorrespondinginitialgraphGofthesafetygamewithrespecttoconnectivity.

Theorem4.6Inthenon-expansivecasewithoutconsiderationofinformationflowandwithoutdistinctionofnodelabels,thedynamicmodel-checkingproblemwithrespecttoconnectivityinthesafetyversionisPSPACE-hard.

ProofConsiderasabotagegameGs=(Gs,vin)ontheinitialgamegraphGs=(Vs,Es)withasetF⊆Vsoffinalvertices.WeconstructagamearenaG=(G,R)whereallverticesarelabeledwith󰀂󰀁,sothatConstructorcanpreservetheconnectivityofthegraphinGiffRunnerwinsthesabotagegameGs.

TheideaistosimulatethemovementofplayerRunnerbythemovementofastrongnode.Intuitively,Constructorshouldbeabletomoveastrongnodetoa“final”vertexinGiffRunnerreachesthisfinalvertexofFinthegameGs.Then,ConstructorcanpreventDestructorfromdestroyingtheconnectivityiffConstructorcanmoveastrongnodetoa“final”vertex.WewillensurethelatterbyconnectingthefinalverticeswithacompletegraphK|Vs|of|Vs|nodes.EachfinalvertexisconnectedwithallnodesofK|Vs|,andeachnodeofK|Vs|isconnectedwithanadditionalnodecalledvtarget.DestructorcanisolatevtargetbydeletingthecompletesubgraphK|Vs|iffConstructorcannotmoveastrongnodetowardsa“final”vertextoK|Vs|.FortherestofthearenaConstructorcanalwaysguaranteeconnectivityinG,butwiththehandicapthatastrongnodecanbemovedtoafinalvertexiffRunnerwinsinGs.

Inordertorealizetheconstruction,weshallreplacetheedgesofGsbyso-calledgateswhichwedepictbyaboldsquare;anexampleforthesimulationisdepictedinFig.6whichshowstheinitialgraphGsofanexamplesabotagegameandtheequivalentinitialgamegraphGofourgame.

ThereplacementgateforanedgebetweentwonodesuandvisdepictedinFig.7.Allgatesinthegraphsharethesameverticesz1andz2.EachnodeofthecompletesubgraphK|Vs|describedaboveisconnectedtoz1aswell.Thus,allverticesotherthanvtargetstayconnectedifConstructoralwaysskips.Thestrongnodez1isunmovable,otherwiseDestructorisolatesz2bydeletionofz1.ThemovementofRunnerfromutovissimulatedbythesituationthatConstructorcanmovethestrongnodeatwtovwithoutgivingDestructortheopportunitytoisolateoneofthenodesxi.ThereforeConstructorneedsastrongnodeatuwhichshecanmovetowardswinthecasethatDestructordeletesayi.Conversely,ifuisnotstrongandDestructordeletesoneofthenodesyi,Constructorcannotmovethestrongnodeatwtovanymore(eveninthecasethatubecomesstronglater),becauseDestructorcouldsubsequentlyisolatexibydeletionofw.Thexi-nodesandyi-nodesexist

13

uvu󰀂󰀁x1

󰀂󰀁

w󰀂󰀁x2

󰀂󰀁

v󰀂󰀁

y1󰀂󰀁z1

y2󰀂󰀁

󰀂󰀁

z2󰀂󰀁

Figure7.Anedgebetweennodesuandvinthesabotagegameanditsreplacementgate.

twicetopreventConstructorof“securing”thegatebymovingthestrongnodeatwtoaxinode.(IfConstructormovesthestrongnessofwtoonexi-node,Destructorcanachievetheisolationoftheotherone.)

Formally,weconstructtheinitialgamegraphG=(V,E,A,S,(P󰀂󰀁))withV:=Vs∪Es∪{w,x1,x2,y1,y2}×Es∪{z1,z2}∪V(K|Vs|)∪{vtarget},andEarisesfromEsasinthefigures.AdditionallyletP󰀂󰀁:=V,andS:={vin,z1}∪{w}×Es.WithV(K|Vs|)wedenotetheverticesofthecompletesubgraphK|Vs|,andvtargetisthenodewhichDestructortriestoisolate.ThevertexvtargetisonlyconnectedtothenodesinK|Vs|,andeachnodeofK|Vs|isadditionallyconnectedtoeach“final”

move

vertexandtothevertexz1.TheonlyruleinthesetRis󰀐󰀂󰀁−−−→󰀂󰀁󰀑whichallowsarbitrarymovementofstrongness(toweaknodes).

InthisproofweassumeConstructorstartsthegame(alikeRunnerstartsthesabotagegame).(ThiscouldbeeasilyachievedbyconnectingthestrongnodeinGwhichcorrespondstotheinitialnodeinGswithoneofthe“final”nodesbyanadditionalgate.So,Destructordeletesayi-nodeofthisgateinhisfirstturn.)

Assume,RunnerhasawinningstrategyinGs.ForeachturnwhereRunnermovesfromanodeutoanodevinGs,Constructormovesthestrongnessofwtovinthecorrespondingreplacementgatefortheedge(u,v)inG.IfDestructordeletesoneofthenodesy1,y2,orwinthisgatelateron,Constructorreactsbysecuringthisgatebymovingthestrongnessofutow(otherwisethismoveisnotnecessary).SinceRunnerreachesafinalstateinGswithin|Vs|−1turns,ConstructorcanmovethestrongnesstoaassociatednodeinGbeforeDestructorcandelete|Vs|−1verticesofK|Vs|.ConstructorcanfinallymovethisstrongnodetoanodeofK|Vs|,henceshewinsinG.

Conversely,assumethatBlockerhasawinningstrategyinGs.Foreachdeletionofanedge(u,v)inGs,Destructordeletesayi-nodeoftheassociatedgate.InthecasethatConstructormovesthestrongnessofaw-nodetoav-nodewithouthavingtherequiredstrongnessattheassociatedu-node,Destructorreactsbydeletingayi-nodeofthisgate(andsuccessivelythew-nodeifConstructordoesnotmoveback).Analogously,ifConstructormovesstrongnessofaw-nodetoaxi-nodeDestructortriestoisolatetheotherxi-node.AndinthecasethatConstructormovesthestrongnessofz1,Destructorwinsbydeletingz1.SinceRunnerlosesthesabotagegame,Constructorcannotmoveastrongnodetowardsa“final”nodetothecompletesubgraphK|Vs|withoutlosingthegame.Afterblockingthereplacement

14

gatesaccordingtoBlocker’sstrategyinGs,DestructorcandeleteallverticesofK|Vs|.InthiscasevtargetbecomesisolatedandDestructorwins,too.

Hence,ConstructorcanpreservetheconnectivityinGiffRunnerwinsthesab-otagegameGs.2Inthepresentpaperwedonotsettlethequestion,whethertheconsiderednon-expansivecasesofthemodel-checkingproblemareactuallysolvableinPSPACE.

5Perspectives

WehavepresentedinthispaperaveryflexiblemodelofdynamicnetworksbasedontheparadigmofagamebetweenthetwoplayersDestructorandConstructor.Weshowedsomepreliminaryresultsonthestatusofthedynamicmodel-checkingproblemassociatedwiththisgame.

Ourcurrentworkaddressesvariousrestrictionsoftheframework.Itisobviousthatinterestingalgorithmicsolutionscanonlybeobtainedinmoreconstrainedscenarios.

However,thisdoesnotapplytothespecifications.Inpracticeitmayberele-vanttoguaranteeabehaviorofdynamicalnetworkswhichtranscendstherangeofreachabilityorsafetyproperties.Alreadytheuseofthe“until”operatormaybein-teresting;itallowstoexpressreachabilitypropertiesunderanadditionalconstraint(whetheracertainpropertyisreachedanduntilthenanotherconstraintismet).

Anotherleadingaspectisthatyes/noquestionsasstudiedinthispaper(i.e.,whetheradynamicmodel-checkingspecificationissatisfiedornot)hastoberefined.Fromapracticalpointofviewtheformulationofoptimizationproblemsismoreuseful.Asanexampleconsideranetworkingridform,sayatwo-dimensionaln×narrayofnodes.Intheassociatedsafetygamewithoutlabelingconstraintstheconnectivityistobepreserved.Thequestionishowmanystrongnodesarerequiredtoensurethis.ItisclearthatDestructorwinsifaroundsomenodevallnodesofdistance<6(includingvitself)failtobestrong:Inthiscase,Destructorcansuccessivelydeletetheatmostfourneighborsofvandthusisolatevfromtherestofthenetwork,destroyingconnectivity.Todeterminethepreciseminimalnumberofstrongnodesnecessarytoensureconnectivityisanoptimizationissueextendingthequestionwhetheragivennetwork(withagivensetofstrongnodes)allowstosatisfyasafetyspecification.

References

[1]Awerbuch,B.,P.Berenbrink,A.BrinkmannandC.Scheideler,Simpleroutingstrategiesforadversarialsystems,in:ProceedingsofFOCS(2001),pp.158–167.[2]Awerbuch,B.,A.BrinkmannandC.Scheideler,Anycastinginadversarialsystems:Routingandadmissioncontrol,in:ProceedingsofICALP,LectureNotesinComputerScience2719(2003),pp.1153–1168.[3]Bouajjani,A.,P.Habermehl,A.RogalewiczandT.Vojnar,Abstractregulartreemodelcheckingofcomplexdynamicdatastructures,in:ProceedingsofSAS,LectureNotesinComputerScience4134(2006),pp.52–70.[4]Corradini,A.,GETGRATS:Asummaryofscientificresults(withannotatedbibliography),ElectronicNotesinTheoreticalComputerScience51(2001).

15

[5]Demri,S.,AreductionfromDLPtoPDL,JournalofLogicandComputation15(2005),pp.767–785.[6]EdmundM.Clarke,J.,O.GrumbergandD.A.Peled,“Modelchecking,”MITPress,Cambridge,MA,USA,1999.[7]Gadducci,F.,R.HeckelandM.Koch,Afullyabstractmodelforgraph-interpretedtemporallogic,in:ProceedingsofTAGT,LectureNotesinComputerScience17(1998),pp.310–322.[8]Göller,S.,Onthecomplexityofreasoningaboutdynamicpolicies,in:ProceedingsofCSL,LectureNotesinComputerScience46(2007),pp.358–373.[9]Grädel,E.,W.ThomasandT.Wilke,“Automata,Logics,andInfiniteGames,”LectureNotesinComputerScience2500,Springer,2002.[10]Hesse,W.,ThedynamiccomplexityoftransitiveclosureisinDynTC0,TheoreticalComputerScience

3(2003),pp.473–485.[11]Hesse,W.andN.Immerman,Completeproblemsfordynamiccomplexityclasses,in:Proceedingsof

LICS(2002),pp.313–322.[12]Holm,J.,K.deLichtenbergandM.Thorup,Poly-logarithmicdeterministicfully-dynamicalgorithms

forconnectivity,minimumspanningtree,2-edge,andbiconnectivity,JournaloftheACM48(2001),pp.723–760.[13]Jussila,T.,J.Dubrovin,T.Junttila,T.LatvalaandI.Porres,Modelcheckingdynamicandhierarchical

UMLstatemachines,in:ProceedingsofMoDeV2a(2006),pp.94–110,http://modeva.itee.uq.edu.au.[14]King,V.andG.Sagert,Afullydynamicalgorithmformaintainingthetransitiveclosure,Journalof

ComputerandSystemSciences65(2002),pp.150–167.[15]Lerda,F.andW.Visser,Addressingdynamicissuesofprogrammodelchecking,in:Proceedingsof

SPIN,LectureNotesinComputerScience2057(2001),pp.80–102.[16]Löding,C.andP.Rohde,Modelcheckingandsatisfiabilityforsabotagemodallogic,in:Proceedingsof

FSTTCS,LectureNotesinComputerScience2914(2003),pp.302–313.[17]Löding,C.andP.Rohde,SolvingthesabotagegameisPSPACE-hard,TechnicalReportAIB-05-2003,

RWTHAachen(2003).[18]Löding,C.andP.Rohde,SolvingthesabotagegameisPSPACE-hard,in:ProceedingsofMFCS,Lecture

NotesinComputerScience2747(2003),pp.531–540.[19]Rohde,P.,Movinginacrumblingnetwork:Thebalancedcase,in:ProceedingsofCSL,LectureNotes

inComputerScience3210(2004),pp.310–324.[20]Rohde,P.,“OnGamesandLogicsoverDynamicallyChangingStructures,”Ph.D.thesis,RWTHAachen

(2005).[21]Rozenberg,G.,editor,“HandbookofGraphGrammarsandComputingbyGraphTransformations,

Volume1:Foundations,”WorldScientific,1997.[22]vanBenthem,J.,Anessayonsabotageandobstruction,in:D.HutterandW.Stephan,editors,

MechanizingMathematicalReasoning,EssaysinHonorofJörgH.SiekmannontheOccasionofHis60thBirthday,LectureNotesinComputerScience2605(2005),pp.268–276.

16