In dieser Diplomarbeit verwenden wir temporal-epistemische Logik, um asynchrone Message-Passing-Systeme mit bis zu f Byzantinisch fehlerhaften Rechenknoten zu analysieren. Wir stellen die Kontextklasse Gamma_bamp vor, ein Modell für asynchrone Message-Passing-Systeme mit Byzantinischen Fehlern, in dem wir temporal-epistemische Logik verwenden können. Wir stellen eine anschauliche Möglichkeit vor, wie Wissen für Byzantinisch-fehlerhafte Akteure definiert werden kann. Mittels temporal-epistemischer Logik zeigen wir, dass ein Akteur in einem System mit bis zu f Byzantinisch-fehlerhaften Akteuren zu Beginn nur dann Wissen gewinnen kann, wenn er Nachrichten von mindestens f+1 Akteuren erhält. Wir versuchen, fehlertolerante verteilte Uhrensynchronisation mittels epistemischer Logik zu untersuchen. Zu diesem Zweck führen wir Firing Rebels ohne Relay ein, ein einfacheres, aber mit Uhrensynchronisation verwandtes Problem. Mit unserem Modell beweisen wir notwendiges und hinreichendes Wissen, mit dem Akteure in Firing Rebels ohne Relay agieren können. Davon ausgehend leiten wir eine untere Schranke für die Kommunikation zwischen Akteuren ab. Diese Arbeit wurde durch das Projekt RiSE/SHiNE (S11405) des ÖsterreichischenWissenschaftsfonds (FWF) unterstützt.
de
In this thesis, we use temporal-epistemic logic to analyze asynchronous message-passing systems with up to f Byzantine node failures. We introduce the class of contexts Gamma_bamp, a model for Byzantine asynchronous message-passing systems that allows us to apply temporal-epistemic logic. We propose an intuitive interpretation of knowledge for Byzantine-faulty agents. We use temporal-epistemic logic to prove that with up to f Byzantine-faulty agents, an agent can initially only gain knowledge by receiving messages from at least f+1 agents. We seek to apply temporal-epistemic logic to the analysis of fault-tolerant distributed clock synchronization. For this purpose we introduce Firing Rebels without Relay, a weaker problem related to clock synchronization. We apply our model to prove necessary and sufficient knowledge for the actions of agents in Firing Rebels without Relay. Based on necessary knowledge, we derive a lower bound on communication between agents. This work was supported through project RiSE/SHiNE (S11405) of the Austrian Science Fund (FWF).
