Epistemic Logic for Distributed Systems with Crash Failures

Abstract

The possible states of a distributed system at a given time can be elegantly modeled using a simplicial complex, which consists of a downward-closed set of sets of vertices. In the context of distributed computing, each vertex of the simplicial complex represents the local view of a particular process (agent), whereas each of its maximal elements (facets) represents a global state of the system. Without crash failures, any facet contains exactly one vertex per agent, and the simplicial complex is called pure. Otherwise, when agents may be dead(have crashed), the system is represented by an impure simplicial complex. Recent works have explored a connection between epistemic logic and this topological modeling of distributed systems. It turns out that there is a categorical correspondence between chromatic simplicial complexes and a particular kind of Kripke frames. This led to a straightforward interpretationof epistemic logic on pure simplicial complexes and brought new insights into distributed computability. In particular, the framework has been successfully used to provide logical arguments for task unsolvability.In the case of impure simplicial complexes however, there are a number of design choices to be made. One of these concerns variables and knowledge of dead agents. In this thesis, we investigate the three-valued epistemic logic where such formulas are neither true nor false: they are undefined. A translation relating the three-valued to the two-valued semantics is given. As we consider two languages, with and without the global atoms expressing life and death of the agents, we study bisimulation for impure simplicial complexes. We find that the language with the global atoms is more expressive. Nevertheless, studying the logic for the language without global atoms provides essential insights. We present a sound and complete axiomatization for each of these languages.