h1

h2

h3

h4

h5
h6
http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png

On games and logics over dynamically changing structures = Über Spiele und Logiken über sich dynamisch ändernden Strukturen



Verantwortlichkeitsangabevorgelegt von Philipp Rohde

ImpressumAachen : Publikationsserver der RWTH Aachen University 2005

UmfangIV, 216 S.


Aachen, Techn. Hochsch., Diss., 2005

Prüfungsjahr: 2005. - Publikationsjahr: 2006


Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter


Tag der mündlichen Prüfung/Habilitation
2005-12-08

Online
URN: urn:nbn:de:hbz:82-opus-13802
URL: https://publications.rwth-aachen.de/record/60724/files/Rohde_Philipp.pdf

Einrichtungen

  1. Fakultät für Mathematik, Informatik und Naturwissenschaften (100000)

Inhaltliche Beschreibung (Schlagwörter)
Mathematik (frei) ; Erfüllbarkeitsproblem (frei) ; Dynamische Logik (frei) ; Modallogik (frei) ; Model checking (frei) ; My-Kalkül (frei) ; Sabotage-Spiel (frei) ; Paritätsspiel (frei) ; Dynamic Logic (frei) ; Modal Logic (frei) ; Mu-Calculus (frei) ; Parity Game (frei)

Thematische Einordnung (Klassifikation)
DDC: 510
ccs: F.4.1

Kurzfassung
In der klassischen Theorie der Graph-Algorithmen und der Programm-Logiken mit den damit verbundenen Model-Checking-Spielen betrachtet man dynamische Prozesse wie die Zustandsänderung von Systemen oder die Bewegung von Agenten innerhalb eines Systems. Doch werden in diesen Modellen die zugrundeliegenden Graphen oder Strukturen als unveränderlich angenommen. Diese Einschränkung motiviert eine verallgemeinerte Betrachtungsweise, bei der dynamische Änderungen von Strukturen berücksichtigt werden.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 Kanten 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übergreifende Modalitäten ergänzt sind. Diese neuen Modalitäten beziehen sich auf Unterstrukturen, aus denen Transitionen entfernt worden sind. Es stellt sich heraus, dass einerseits diese „Sabotage-Modalitäten” die Ausdrucksfähigkeit der üblichen Modallogik soweit vergrößern, dass viele der angenehmen algorithmischen und modelltheoretischen Eigenschaften verloren gehen. Andererseits bleibt das Model-Checking-Problem entscheidbar.Eine wesentliche Einschränkung der Modallogik ist das Fehlen eines allgemeinen 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 monadischen Fixpunkten. Die daraus resultierende Logik stellt eine Erweiterung des bekannten my-Kalküls dar und ermöglicht es, sowohl iterative Eigenschaften wie Erreichbarkeit oder Rekurrenz wie auch einfache Änderungen der zugrundeliegenden Kripke-Struktur – hier das Entfernen von Transitionen – auszudrücken. Abschließend führen wir erweiterte Paritätsspiele ein, bei denen die beiden Spieler 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 Spielgraphen zu löschen; zum anderen können sie das aktuelle Aussehen des Spielgraphen unter Verwendung einer festen Zahl von Registern speichern und gegebenenfalls später wieder restaurieren. Wir werden zeigen, dass diese Spiele als Model-Checking-Spiele für den oben genannten „Sabotage-my-Kalkül” benutzt werden können.

In the classical framework of graph algorithms, program logics, and corresponding model checking games, one considers changes of system states and movements of agents within a system, but the underlying graph or structure is assumed to be static. This limitation motivates a more general approach where dynamic changes of structures are relevant.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 vertex 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' already strengthen standard modal logic in such a way that many nice algorithmic and model-theoretic properties get lost. On the other hand, the model checking problem remains decidable.The main limitation of modal logic is the lack of a mechanism for unbounded iteration or recursion. To overcome this, we augment the 'sabotage modal logics' of the first part of the thesis with constructors for forming least and greatest monadic fixed-points. The resulting logic extends the well-known mu-calculus and is capable of expressing iterative properties like reachability or recurrence as well as basic changes of the underlying Kripke structure, namely, the deletion of transitions. Finally, we introduce extended parity games where in addition, both players are able to delete edges of the arena and to store, resp., restore the current appearance of the arena by use of a fixed number of registers. We show that these games serve as model checking games for the aforementioned 'sabotage mu-calculus'.

Fulltext:
Download fulltext PDF
(additional files)

Dokumenttyp
Dissertation / PhD Thesis

Format
online, print

Sprache
English

Externe Identnummern
HBZ: HT014643643

Interne Identnummern
RWTH-CONV-122417
Datensatz-ID: 60724

Beteiligte Länder
Germany

 GO


OpenAccess

QR Code for this record

The record appears in these collections:
Document types > Theses > Ph.D. Theses
Faculty of Mathematics, Computer Science and Natural Sciences (Fac.1) > No department assigned
Publication server / Open Access
Public records
Publications database
100000

 Record created 2013-01-28, last modified 2023-10-17


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)