Simplicial models for the epistemic logic of faulty agents

Abstract 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 of Goubault et al. (Inf Comput 278:104597, 2021. https://doi.org/10.1016/j.ic.2020.104597 ), simplicial models are always assumed to be pure , meaning that all worlds have the same dimension. This is equivalent to the standard $$\mathbf {S5_n}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>S</mml:mi> <mml:msub> <mml:mn>5</mml:mn> <mml:mi>n</mml:mi> </mml:msub> </mml:mrow> </mml:math> 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 (van Ditmarsch, WoLLIC 2021, pp 31–46, 2021. https://doi.org/10.1007/978-3-030-88853-4_3 ; Goubault et al. STACS 2022, pp 33:1–33:20, 2022. https://doi.org/10.4230/LIPIcs.STACS.2022.33 ; Goubault et al. LICS, pp 1–13, 2023. https://doi.org/10.1109/LICS56636.2023.10175737 ), 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.