Simplicial approaches to crashing agents

Abstract

Kripke models have long been a preferred semantics for modeling knowledge and belief. For distributed systems, this is commonly done via the runs-and-systems framework, where the Kripke model is induced from a given interpreted system by abstracting away most low-level details, including agents' local states. Simplicial complexes provide an alternative algebraic-topological semantics that is categorically dual to Kripke models and treats agents' local states as primary objects. This is more in line with how agents' knowledge is determined in interpreted systems. One of the benefits of the tangible presence of agents and their local states is the ability to model the absence of some of the agents, which is necessary to faithfully represent distributed systems with crash failures. Modeling knowledge of crashed agents presents interesting dilemmas on the purely logical level. We outline the available choices, discuss the difficulties involved, e.g., the failure of modus ponens in one, and outline the benefits and pitfalls of the existing approaches.