Reasoning about Knowledge in Byzantine Distributed Systems
Reasoning about fault-tolerant distributed systems, which consist of networked processors without a central control that need to achieve a common goal, is notoriously difficult due to the many sources of uncertainty: varying execution speeds, unpredictable transmission delays, and partial failures make it difficult for a processor to establish local knowledge sufficient to safely perform required actions. The design and analysis of distributed algorithms is, hence, a difficult and error-prone task, which has to be done manually, on a case-by-case basis. A suitable abstraction that is both
- high-level enough to facilitate the design of new algorithms and
- rigorous and formal enough to form the basis of future tools
does not exist today.
Like in automated formal verification, one of the mandatory prerequisites for automated reasoning and decision making in multi-agent systems are precise logical languages for specifying algorithms, behaviors, and properties. Rather than just resorting to classic temporal logic languages such as LTL or CTL, which contributed much to the tremendous success of model checking approaches, we will explore the suitability of epistemic logic for this purpose. Very little is known about modeling and analysis of multi-agent systems where agents may be arbitrarily ("byzantine") faulty, and about the evolution of knowledge of the agents, i.e., learning, in the course of the information exchange caused by complex protocols.
The goal of the proposed project is to close the above gaps by incorporating arbitrarily misbehaving agents into an epistemic reasoning framework and by supplementing the standard Kripke semantics with a suitable topological semantics for distributed systems, while exploiting, and being informed by, the success of Dynamic Epistemic Logic in capturing the dynamics of knowledge evolution in modal logic.
Keywords: epistemic logic, fault-tolerant distributed algorithms, topology, knowledge-based reasoning
Selected key publications:
- Krisztina Fruzsa, Roman Kuznets, and Ulrich Schmid. Fire! Accepted to TARK 2021: Theoretical Aspects of Rationality and Knowledge.
- Thomas Schlögl, Ulrich Schmid, and Roman Kuznets. The persistence of false memory: Brain in a vat despite perfect clocks. PRIMA 2020: Principles and Practice of Multi-Agent Systems. Lecture Notes in Artificial Intelligence, v. 12568, pp. 403—411. Springer, 2021. (doi:10.1007/978-3-030-29007-8_15)
- Roman Kuznets, Laurent Prosperi, Ulrich Schmid, and Krisztina Fruzsa. Epistemic Reasoning with Byzantine-Faulty Agents. FroCoS 2019: Frontiers of Combining Systems. Lecture Notes in Artificial Intelligence, v. 11715, pp. 259—276. Springer, 2019. (doi:10.1007/978-3-030-29007-8_15)
- Roman Kuznets, Laurent Prosperi, Ulrich Schmid, and Krisztina Fruzsa. Causality and Epistemic Reasoning in Byzantine Multi-Agent Systems. TARK 2019: Theoretical Aspects of Rationality and Knowledge. Electronic Proceedings in Theoretical Computer Science, v. 297, pp. 293—312. Open Publishing Association, 2019. (doi:10.4204/EPTCS.297.19)
Project duration: 2020—2025
Project leaders: Roman Kuznets, Ulrich Schmid
Supported by the Austrian Science Fund (FWF) under project number P 33600.
