Homotopy Bisimilarity for Higher-Dimensional Automata

TL;DR

This paper introduces a novel homotopy bisimilarity concept for higher-dimensional automata, utilizing unfoldings into higher-dimensional trees and open maps, providing a refined equivalence notion for concurrent systems.

Contribution

It defines a new category of higher-dimensional automata with homotopy bisimilarity, extending standard bisimilarity to higher dimensions and analyzing its relation to existing equivalences.

Findings

Homotopy bisimilarity is equivalent to a natural generalization of standard bisimilarity.

It is finer than split bisimilarity.

It is incomparable with history-preserving bisimilarity.

Abstract

We introduce a new category of higher-dimensional automata in which the morphisms are functional homotopy simulations, i.e. functional simulations up to concurrency of independent events. For this, we use unfoldings of higher-dimensional automata into higher-dimensional trees. Using a notion of open maps in this category, we define homotopy bisimilarity. We show that homotopy bisimilarity is equivalent to a straight-forward generalization of standard bisimilarity to higher dimensions, and that it is finer than split bisimilarity and incomparable with history-preserving bisimilarity.