Bisimulation for Impure Simplicial Complexes

TL;DR

This paper introduces a bisimulation concept for impure simplicial complexes, enabling comparison of models with dead agents in epistemic logic, and proves it has the Hennessy-Milner property.

Contribution

It defines a new bisimulation for impure simplicial complexes and establishes its theoretical properties, enhancing the semantic framework for epistemic logic with dead agents.

Findings

Bisimulation for impure complexes has the Hennessy-Milner property.

Expressive atoms for agent alive/dead status are essential for meaningful bisimulation.

Counterexamples show limited languages cannot support standard bisimulation.

Abstract

As an alternative to Kripke models, simplicial complexes are a versatile semantic primitive on which to interpret epistemic logic. Given a set of vertices, a simplicial complex is a downward closed set of subsets, called simplexes, of the vertex set. A maximal simplex is called a facet. Impure simplicial complexes represent that some agents (processes) are dead. It is known that impure simplicial complexes categorically correspond to so-called partial epistemic (Kripke) models. In this contribution, we define a notion of bisimulation to compare impure simplicial complexes and show that it has the Hennessy-Milner property. These results are for a logical language including atoms that express whether agents are alive or dead. Without these atoms no reasonable standard notion of bisimulation exists, as we amply justify by counterexamples, because such a restricted language is insufficiently expressive.