Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Bisimulations and Logics for Higher-Dimensional Automata

Safa Zouari, Krzysztof Ziemiański, Uli Fahrenberg

TL;DR

This work introduces Ipomset modal logic, a Hennessy-Milner type logic over HDAs, and shows that it characterizes Path-bisimulation, a variant of the standard ST-bisimulation, and defines a notion of Cell-bisimulation, using the open-maps framework of Joyal, Nielsen, and Winskel.

Abstract

Higher-dimensional automata (HDAs) are models of non-interleaving concurrency for analyzing concurrent systems. There is a rich literature that deals with bisimulations for concurrent systems, and some of them have been extended to HDAs. However, no logical characterizations of these relations are currently available for HDAs. In this work, we address this gap by introducing Ipomset modal logic, a Hennessy-Milner type logic over HDAs, and show that it characterizes Path-bisimulation, a variant of the standard ST-bisimulation. We also define a notion of Cell-bisimulation, using the open-maps framework of Joyal, Nielsen, and Winskel, and establish the relationship between these bisimulations (and also their "strong" variants, which take restrictions into account). In our work, we rely on the new categorical definition of HDAs as presheaves over concurrency lists and on track objects.

Bisimulations and Logics for Higher-Dimensional Automata

TL;DR

This work introduces Ipomset modal logic, a Hennessy-Milner type logic over HDAs, and shows that it characterizes Path-bisimulation, a variant of the standard ST-bisimulation, and defines a notion of Cell-bisimulation, using the open-maps framework of Joyal, Nielsen, and Winskel.

Abstract

Higher-dimensional automata (HDAs) are models of non-interleaving concurrency for analyzing concurrent systems. There is a rich literature that deals with bisimulations for concurrent systems, and some of them have been extended to HDAs. However, no logical characterizations of these relations are currently available for HDAs. In this work, we address this gap by introducing Ipomset modal logic, a Hennessy-Milner type logic over HDAs, and show that it characterizes Path-bisimulation, a variant of the standard ST-bisimulation. We also define a notion of Cell-bisimulation, using the open-maps framework of Joyal, Nielsen, and Winskel, and establish the relationship between these bisimulations (and also their "strong" variants, which take restrictions into account). In our work, we rely on the new categorical definition of HDAs as presheaves over concurrency lists and on track objects.
Paper Structure (15 sections, 17 theorems, 14 equations, 9 figures)

This paper contains 15 sections, 17 theorems, 14 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Higher Dimensional Automata
  3. Interval pomsets with interfaces vs. track objects
  4. Background
  5. The category of interval ipomsets
  6. Defining the HDA-path category
  7. Paths and tracks
  8. Background: Paths and their labels
  9. The categories of tracks and paths
  10. Bisimulation and modal logic
  11. Overview
  12. Bisimulation from open maps for HDA
  13. Modal characterization
  14. Particular case
  15. Omitted Proofs

Key Result

lemma 1

Let $X$ be a precubical set, $S$ be a conclist, and $x \in X$. If $\textup{ev}(x)=S$, then there exists a unique precubical map $\iota_x: \square^S \to X$ such that $\iota_x(\mathbf{y}_S)=x$.

Figures (9)

  • Figure 1: How HDA models concurrency: The filled-in cube models the events $[a_1,a_2,a_3]$. The 2-dimensional faces with the same color model the same 2 events. The uncolored faces model the events $[a_2,a_3]$.
  • Figure 2: HDA models distinguishing interleaving $a. b + b. a$ (left) from non-interleaving concurrency $a \parallel b$ (right).
  • Figure 3: Two-dimensional cell with its faces. The labels of each cell are shown on the left.
  • Figure 4: Hierarchy of notions of equivalence.
  • Figure 5: Interval ipomsets (below) with their corresponding interval representations (above). An event with a dot on the left (resp. on the right) is an element of a source (resp. target) interface. Full arrows indicate precedence order, while dashed arrows indicates event order.
  • ...and 4 more figures

Theorems & Definitions (59)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • definition 5
  • lemma 1
  • definition 6
  • definition 7
  • proposition 1
  • definition 8
  • ...and 49 more