Weak morphisms of higher dimensional automata

TL;DR

This paper introduces weak morphisms for higher dimensional automata (HDAs) to define new preorder relations, analyzing their properties and invariance of trace languages under these abstractions.

Contribution

It defines weak morphisms for HDAs and explores their role in preorder relations, including homeomorphic and trace equivalent abstractions, with invariance results for trace languages.

Findings

Homeomorphic abstraction is generally stronger than trace equivalent abstraction.

Trace language is invariant under trace equivalent abstraction for many HDAs.

Weak morphisms help formalize abstraction relations in higher dimensional automata.

Abstract

We introduce weak morphisms of higher dimensional automata and use them to define preorder relations for HDAs, among which homeomorphic abstraction and trace equivalent abstraction. It is shown that homeomorphic abstraction is essentially always stronger than trace equivalent abstraction. We also define the trace language of an HDA and show that, for a large class of HDAs, it is invariant under trace equivalent abstraction.