Epistemic Logic of Crash Failures

Explore the intersection of epistemic logic and distributed computing through this academic lecture that examines how knowledge and belief operate in multi-agent systems prone to crash failures. Learn about the fundamental concepts of epistemic logic, which investigates knowledge and belief in multi-agent systems using Kripke models and relational structures to represent agents' uncertainty about global system states. Discover how combinatorial topology, particularly simplicial complexes, provides a framework for modeling concurrency and asynchrony in distributed computing, where vertices represent local states of agents or processes. Examine the concept of impure simplicial complexes, which encode uncertainty about crashed processes in synchronous computation systems where not all facets contain information for all processes. Understand the development of a novel epistemic logic designed specifically for reasoning about distributed systems with crash failures, featuring a three-valued semantics where formulas can be true, false, or undefined - particularly relevant for knowledge of crashed processes and their local propositions. Analyze how this logic extends Paraconsistent Weak Kleene logic (PWK) with modal epistemic components derived from standard epistemic logic S5, enabling live processes to determine or remain uncertain about whether other processes have crashed. Compare this approach with other recent methods for encoding distributed systems using impure complexes, including both two-valued systems where dead processes know false propositions and other three-valued but less expressive alternatives. Gain insights into cutting-edge research that bridges formal logic, distributed computing theory, and multi-agent systems through collaborative work spanning multiple institutions and research domains.