On games and logics over dynamically changing structures [Elektronische Ressource] / vorgelegt von Philipp Rohde

Philipp Rohde

Sujets

• Informatik
• Mathematics

Informations

• Publié par: rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen
• Publié le: 01 janvier 2005
• Nombre de lectures: 6
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

OnGamesandLogicsover
DynamicallyChangingStructures
VonderFakultätfürMathematik,Informatikund
NaturwissenschaftenderRheinisch-WestfälischenTechnischen
HochschuleAachenzurErlangungdesakademischenGrades
einesDoktorsderNaturwissenschaftengenehmigteDissertation
vorgelegtvon
Diplom-Mathematiker
PhilippRohde
aus
Düsseldorf
Berichter: Univ.-Prof.Dr.Dr.h.c.WolfgangThomas
Univ.-Prof.Dr.JohanvanBenthem
TagdermündlichenPrüfung: 8. Dezember2005
DieseDissertationistaufdenInternetseitenderHochschulbibliothekonlineverfügbar.Abstract
Intheclassicalframeworkofgraphalgorithms,programlogics,andcorrespond-
ing model checking games, one considers changes of system states and move-
ments of agents within a system, but the underlying graph or structure is as-
sumed to be static. This limitation motivates a more general approach where
dynamicchangesofstructuresarerelevant.
In this thesis, we take up a proposal of van Benthem from 2002 and consider
games and modal logics over dynamically changing structures, where we focus
on the deletion of edges of a graph, resp., transitions of a Kripke structure. We
investigate two-player games where one player tries to reach a designated ver-
tex of a graph while the opponent sabotages this by deleting edges. It is shown
that adding the ‘saboteur’ makes these games algorithmically much harder to
solve. Further, we analyze corresponding modal logics which are augmented
with cross-model modalities referring to submodels from which a transition has
been removed. On the one hand, it turns out that these ‘sabotage modalities’ al-
readystrengthenstandardmodallogicinsuchawaythatmanynicealgorithmic
and model-theoretic properties get lost. On the other hand, the model checking
problemremainsdecidable.
Themainlimitationofmodallogicisthelackofamechanismforunbounded
iteration or recursion. To overcome this, we augment the ‘sabotage modal log-
ics’ of the first part of the thesis with constructors for forming least and great-
est monadic fixed-points. The resulting logic extends the well-known μ-calculus
andiscapableofexpressingiterativepropertieslikereachabilityorrecurrenceas
wellasbasicchanges oftheunderlying Kripkestructure, namely, thedeletionof
transitions. Finally,weintroduceextendedparitygameswhereinaddition,both
players are able to delete edges of the arena and to store, resp., restore the cur-
rentappearanceofthearenabyuseofafixednumberofregisters. Weshowthat
these games serve as model checking games for the aforementioned ‘sabotage
μ-calculus’.
Zusammenfassung
In der klassischen Theorie der Graph-Algorithmen und der Programm-Logiken
mit den damit verbundenen Model-Checking-Spielen betrachtet man dynami-
scheProzessewiedieZustandsänderungvonSystemenoderdieBewegungvon
Agenten innerhalb eines Systems. Doch werden in diesen Modellen die zugrun-
deliegenden Graphen oder Strukturen als unveränderlich angenommen. Diese
Einschränkung motiviert eine verallgemeinerte Betrachtungsweise, bei der dy-
namischeÄnderungenvonStrukturenberücksichtigtwerden.
In dieser Arbeit folgen wir einem Vorschlag von van Benthem aus dem Jahr
2002 und betrachten Spiele und Modallogiken über sich ändernden Strukturen.Dabei konzentrieren wir uns auf das Entfernen von Kanten eines Graphen bzw.
von Transitionen einer Kripke-Struktur. Wir untersuchen Zwei-Personen-Spiele,
bei denen ein Spieler versucht, einen ausgezeichneten Knoten eines Graphen zu
erreichen, während sein Gegenspieler dies zu verhindern sucht, indem er Kan-
ten des Graphen löscht. Es wird gezeigt, dass die algorithmische Komplexität
der Spiele durch die Hinzunahme dieses „Saboteurs“ deutlich erhöht wird. Im
Weiteren analysieren wir zugehörige Modallogiken, die um modellübergreifen-
de Modalitäten ergänzt sind. Diese neuen Modalitäten beziehen sich auf Unter-
strukturen, aus denen Transitionen entfernt worden sind. Es stellt sich heraus,
dass einerseits diese „Sabotage-Modalitäten“ die Ausdrucksfähigkeit der übli-
chenModallogiksoweitvergrößern,dassvielederangenehmenalgorithmischen
und modelltheoretischen Eigenschaften verloren gehen. Andererseits bleibt das
Model-Checking-Problementscheidbar.
Eine wesentliche Einschränkung der Modallogik ist das Fehlen eines allge-
meinen Mechanismus für unbeschränkte Iterationen oder Rekursion. Um diese
Schwäche zu beheben, erweitern wir die „Sabotage-Modallogiken“ des ersten
Teils der Arbeit um Operatoren zur Bildung von kleinsten und größten mona-
dischen Fixpunkten. Die daraus resultierende Logik stellt eine Erweiterung des
bekannten μ-Kalküls dar und ermöglicht es, sowohl iterative Eigenschaften wie
Erreichbarkeit oder Rekurrenz wie auch einfache Änderungen der zugrundelie-
genden Kripke-Struktur – hier das Entfernen von Transitionen – auszudrücken.
AbschließendführenwirerweiterteParitätsspieleein,beidenendiebeidenSpie-
ler neben der Bewegung durch den Spielgraphen zusätzliche Arten von Zügen
durchführen können: zum einen haben sie die Möglichkeit, Kanten des Spiel-
graphen zu löschen; zum anderen können sie das aktuelle Aussehen des Spiel-
graphen unter Verwendung einer festen Zahl von Registern speichern und ge-
gebenenfalls später wieder restaurieren. Wir werden zeigen, dass diese Spiele
alsModel-Checking-Spielefürdenobengenannten„Sabotage-μ-Kalkül“benutzt
werdenkönnen.Contents
Introduction ....................................................... 1
1. Preliminaries.................................................... 13
PartI FiniteSabotageGamesandSabotageModalLogics
2. SabotageGames................................................. 23
2.1 TheSabotageGame .......................................... 24
2.2 ComplexityofSolvingSabotageGames......................... 32
2.3 VariantsoftheGame ......................................... 44
2.4 AdditionalRemarks.......................................... 49
3. ModalLogicswithGlobalSabotage ............................... 51
3.1 SabotageModalLogic ........................................ 52
3.2 Model-TheoreticProperties.................................... 60
3.3 UndecidabilityoftheSatisfiabilityProblem...................... 67
3.4 ANormalForm: PrunedModels............................... 77
3.5 AdditionalRemarks.......................................... 85
4. GamesandLogicswithLocalSabotage............................. 89
4.1 AdjacentSabotage............................................ 91
4.2 PathSabotage ............................................... 111
4.3 AdditionalRemarks.......................................... 130
PartII InfiniteSabotageGamesandSabotageFixed-PointLogics
5. SabotageGameswithRestoration ................................. 133
5.1 BackupParityGames......................................... 134
5.2 ComplexityofSolvingBackupParityGames .................... 150
5.3 RandomAccessMemoryGames ............................... 162
6. SabotageModalLogicswithFixed-Points .......................... 173
6.1 Sabotageμ-calculus .......................................... 174
6.2 ModelCheckingviaBackupParityGames ...................... 182
6.3 CorrectnessoftheModelCheckingGame ....................... 187
6.4 AdditionalRemarks.......................................... 197
7. Conclusion...................................................... 199
Bibliography....................................................... 207
Index.............................................................. 213
iiiiv ContentsIntroduction
Theworldisoneofpermanence. Changeisanillusion.
—Parmenides,5thcenturyBC
IntheclassicalframeworkoflogicsandcorrespondingHintikkagamesformodel
checkingissues,oneconsiderschangesofsystemstatesandmovementsofagents
within a system, but the underlying structure is assumed to be static. For exam-
ple, the modalities of classical modal logic can be interpreted as local transitions
betweenstates(possibleworlds)ofastructure. Buttheevaluationofformulaeis
basedonimmutablesystems.
In some fields of computer science, engineering, and philosophy, an inter-
esting sort of tasks arises, which refers to temporal changes of the underlying
systems. Wemayconsiderfiveexamplescenarios. Thefirstsituationisrelatedto
protocolsforcomputernetworks:
Situation1. Consider a computer network where connections between servers
may break down or servers may stop working, for example, caused by technical
malfunction or wilful damage. Some natural questions arise for such networks:
Is it possible, regardless of the removed connections, to interchange information
between two designated servers? Is there a protocol that guarantees the reacha-
bilityofadestination?
The second scenario may be regarded as a natural question arising for routing
tasks:
Situation2. Consideracarnavigationsystem. Ausualtaskforthesystemisthe
dynamical calculation ofbestrouteswhileroadsareblockedduringtheride, for
instance,causedbyroadworksortrafficjams.
ThenextscenariowasproposedbyvanBenthem[Ben05]:
Situation3. Consider a traveling researcher who moves from one conference,
workshop, and research stay to another. He has to rely on a traffic network con-
sisting of railway routes, air routes, bus routes etc. We may ask whet