Simplicial Models for the Epistemic Logic of Faulty Agents
This work addresses foundational issues in modeling epistemic logic for faulty agents, with applications in fault-tolerant distributed computing, but it is incremental as it builds on existing impure simplicial model frameworks.
The paper tackles the challenge of classifying design choices in impure simplicial models for epistemic logic, which allow varying numbers of agents per world, and it axiomatizes the resulting logics, demonstrating this with examples from synchronous distributed systems where processes may crash.
In recent years, several authors have been investigating simplicial models, a model of epistemic logic based on higher-dimensional structures called simplicial complexes. In the original formulation, simplicial models were always assumed to be pure, meaning that all worlds have the same dimension. This is equivalent to the standard S5n semantics of epistemic logic, based on Kripke models. By removing the assumption that models must be pure, we can go beyond the usual Kripke semantics and study epistemic logics where the number of agents participating in a world can vary. This approach has been developed in a number of papers, with applications in fault-tolerant distributed computing where processes may crash during the execution of a system. A difficulty that arises is that subtle design choices in the definition of impure simplicial models can result in different axioms of the resulting logic. In this paper, we classify those design choices systematically, and axiomatize the corresponding logics. We illustrate them via distributed computing examples of synchronous systems where processes may crash.