On symmetric higher-dimensional automata and bisimilarity

TL;DR

This paper demonstrates that symmetric higher-dimensional automata (HDAs) are equivalent in expressive power to ordinary HDAs under hereditary history-preserving bisimilarity, highlighting their suitability for modeling concurrency.

Contribution

It establishes the equivalence between symmetric and ordinary HDAs in terms of hereditary history-preserving bisimilarity, showing their interchangeable use in concurrency modeling.

Findings

Symmetric HDAs are hhp-bisimilar to free symmetric HDAs generated by them.

Ordinary HDAs and symmetric HDAs have the same expressive power for concurrency.

Symmetric HDAs can be generated from ordinary HDAs while preserving bisimilarity.

Abstract

It is shown that a higher-dimensional automaton is hhp-bisimilar to the free symmetric HDA generated by it. Consequently, up to hereditary history-preserving bisimilarity, ordinary HDAs and symmetric HDAs are models of concurrency with the same expressive power.