Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Bisimulation for Impure Simplicial Complexes

Marta Bílková, Hans van Ditmarsch, Roman Kuznets, Rojo Randrianomentsoa

TL;DR

This contribution defines a notion of bisimulation to compare impure simplicial complexes and shows that it has the Hennessy-Milner property, and results are for a logical language including atoms that express whether agents are alive or dead.

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.

Bisimulation for Impure Simplicial Complexes

TL;DR

This contribution defines a notion of bisimulation to compare impure simplicial complexes and shows that it has the Hennessy-Milner property, and results are for a logical language including atoms that express whether agents are alive or dead.

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.

Paper Structure

This paper contains 6 sections, 14 theorems, 20 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Epistemic Simplicial Semantics
  3. Bisimulation for Simplicial Models with Local Atoms?
  4. Bisimulation for Simplicial Models with Glocal Atoms
  5. Life Bisimulation for Partial Epistemic Models
  6. Conclusions and Future Work

Key Result

lemma 1

If eq:modeq_true holds for all $\varphi \in \mathcal{L}$ for pointed simplicial models $(\mathcal{C},Y)$ and $(\mathcal{C}',Y')$, then $(\mathcal{C},Y)\equiv_{\mathcal{L}}(\mathcal{C}',Y')$.

Figures (4)

  • Figure 1: Simplicial models and corresponding partial epistemic models
  • Figure 2: Differences between $(\mathcal{C},X)$, $(\mathcal{C}',X')$, and $(\mathcal{C}",X")$ are not local.
  • Figure 3: Life trees of three sample formulas
  • Figure 4: From right to left: life tree $\mathfrak{{T}}_{{\varphi}}$ of formula $\varphi = p_b \land \widehat{K}_c \widehat{K}_d p_a \land \widehat{K}_c \widehat{K}_e \neg p_a$; life tree $\mathfrak{{T}}_{{\psi}}$ of its subformula $\psi =\widehat{K}_d p_a$; and simplicial model $(\mathcal{C},X)$ such that $\mathcal{C}, X \not\bowtie \varphi$.

Theorems & Definitions (36)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • lemma 1: Criterion of modal equivalence
  • proof
  • proposition 1
  • proof
  • definition 5
  • theorem 1: Bisimilarity implies modal equivalence
  • ...and 26 more