Wissensbasierte Analyse byzantinischer verteilter Systeme

Verteilte fehlertoleranter Systeme, in denen netzwerkgekoppelte Prozessoren ohne zentrale Koordination ein vorgegebenes Problem lösen müssen, sind notorisch schwierig zu beschreiben: Zahlreiche Unsicherheiten wie variierende Ausführungsgeschwindigkeiten, unvorhersehbare Nachrichtenverzögerungen und Komponentenfehler erschweren es den Prozessoren, ausreichendes lokales Wissen für die Ausführung von korrekten Aktionen zu gewinnen. Design und Analyse verteilter fehlertoleranter Algorithmen ist daher eine herausfordernde und fehleranfällige Aufgabe, die praktisch ausschließlich händisch und von Fall zu Fall unterschiedlich gelöst werden muß: Eine brauchbare Abstraktion, die sowohl (1) auf ausreichend hohem Niveau für das Design neuer Algorithmen ist, (2) rigoros und formal genug ist, um eine Grundlage für zukünftige Werkzeuge zu bilden, existiert derzeit noch nicht. Wie auch in der formalen Verifikation ist eine präzise logische Sprache für die Spezifikation von Algorithmen, Verhaltenmustern und Eigenschaften eine der wichtigsten Voraussetzungen dafür. Statt sich auf klassische temporale Logiksprachen wie LTL oder CTL zu verlassen, die viel zu dem großen Erfolg von Modelchecking-Ansätzen beigetragen haben, möchten wir die Eignung von epistemische Logik für die automatisierte Entscheidungsfindung in Multiagentensystemen erforschen. Insbesondere ist bislang sehr wenig über die Modellierung und Analyse von solchen Systemen bekannt, deren Agents beliebiges ("byzantinisches") Fehlverhalten zeigen können. Das betrifft ganz besonders die Evolution des lokalen Wissens, also des Lernens, im Zuge der Ausführung komplexer Protokolle in solchen Systemen. Das konkrete Ziel des gegenständlichen Projekts ist es, diese Lücke zu schließen, indem epistemische Logik um beliebig fehlerhafte Agenten erweitert und die übliche Kripke- Semantik durch eine geeignete topologische Semantik für verteilte Systeme ersetzt wird. Besondere Beachtung soll dynamischer epistemische Logik geschenkt werden, die sich in der jüngeren Vergangenheit als vielversprechender Kandidat für die Beschreibung der Dynamik des Lernens in modaler Logik erwiesen hat.

Das Projekt widmete sich der Untersuchung verteilter fehlertoleranter Systeme, die aus netzwerkgekoppelten Prozessoren ohne zentrale Koordination bestehen, die ein vorgegebenes Problem lösen müssen. Die beiden wichtigsten angewandten Methoden waren logische Methoden, die das notwendige und ausreichende Wissen für verteilte Agenten untersuchen, um das vorgegebene Problem lösen zu können, und topologische Methoden, die die verteilten Konfigurationen und Protokolle über geeignete topologische Objekte, beispielsweise sogenannte simpliziale Komplexe, kodieren und die Lösbarkeit des vorgegebenen Problems in topologischer Begriffe charakterisieren. Auf der logischen Seite wurde unter Verwendung des Formalismus der epistemischen Modallogik der erste epistemische Rahmen, der vollständig byzantinische Agenten umfasst, verwendet, um zu zeigen, dass selbst korrekte Agenten sich nicht auf ihre eigene Korrektheit verlassen können, sodass die Entscheidungsfindung auf dem Begriff des Glaubens basieren muss, der schwächer als Wissen ist und Wissen modulo der eigenen Korrektheit darstellt. Gleichzeitig wurde gezeigt, dass der Informationsgehalt von Nachrichten in Gegenwart byzantinischer Agenten eine noch schwächere Modalität der Hoffnung erfordert, die die Unsicherheit des Empfängers hinsichtlich der Zuverlässigkeit des Absenders widerspiegelt. Da sowohl Korrektheit als auch Glaube durch Wissen und Hoffnung ausgedrückt werden können, lassen sich byzantinische verteilte Systeme in einer logischen Sprache beschreiben, die zwei Modalitäten pro Agent enthält: Wissen und Hoffnung. Probleme, die koordinierte Aktionen erfordern, erfordern geeignete Fixpunktversionen dieser Modalitäten. Beispielsweise hat die epistemische Analyse der vereinfachten Version der weit verbreiteten konsistenten Broadcasting-Primitive dazu geführt, dass die letztendlich gemeinsame Hoffnung als notwendige Bedingung angesehen wird. Dynamische Versionen dieser Logiken wurden ebenfalls untersucht, wobei die Selbstkorrektur der Agenten durch die Aktualisierung des Zustands der Hoffnungsmodalität auf einer Agent-für-Agent-Basis implementiert wurde. Die Rolle des A-priori-Wissens sowohl des Systementwicklers als auch der Agenten bei der Entwicklung verteilter Systeme wurde sowohl philosophisch als auch logisch untersucht. Insbesondere wurde im Stil der dynamischen epistemischen Logik eine Methode entwickelt, mit der Agenten Inkonsistenzen durch unabhängige und autonome Aktualisierung ihrer eigenen A-priori-Glaubens auflösen können. Auf der topologischen Seite wurde eine kombinatorische und topologische Modellierung des Konsenses unter vergesslichen Nachrichtengegnern bereitgestellt und eine besonders interessante Verallgemeinerung des berühmten Asynchronous Computability Theorem auf kontinuierliche Aufgaben erreicht. Schließlich wurde an der Schnittstelle zwischen Logik und Topologie die Logik der simplizialen Komplexe für verteilte Systeme mit Abstürze entwickelt, die eine stärker agentenorientierte Perspektive bietet und eine differenziertere Darstellung des Wissens sowohl der abgestürzten Agenten als auch der aktiven Agenten über die abgestürzten Agenten ermöglicht, wobei ein möglicher dritter Wahrheitswert "undefiniert" benützt ist.