Trees in Partial Higher Dimensional Automata

TL;DR

This paper introduces a new, more natural categorical definition of partial Higher Dimensional Automata (pHDA) and characterizes trees within pHDA as those with a unique path property, linking them to homotopy theory and concurrency models.

Contribution

It provides a simplified categorical definition of pHDA and characterizes trees as unfoldings and cofibrant objects, connecting automata with homotopy theory.

Findings

Trees in pHDA are exactly those with the unique path property modulo homotopy.

Trees are characterized as unfoldings of other pHDA.

Trees correspond to cofibrant objects in a model structure.

Abstract

In this paper, we give a new definition of partial Higher Dimension Automata using lax functors. This definition is simpler and more natural from a categorical point of view, but also matches more clearly the intuition that pHDA are Higher Dimensional Automata with some missing faces. We then focus on trees. Originally, for example in transition systems, trees are defined as those systems that have a unique path property. To understand what kind of unique property is needed in pHDA, we start by looking at trees as colimits of paths. This definition tells us that trees are exactly the pHDA with the unique path property modulo a notion of homotopy, and without any shortcuts. This property allows us to prove two interesting characterisations of trees: trees are exactly those pHDA that are an unfolding of another pHDA; and trees are exactly the cofibrant objects, much as in the language of Quillen's model structure. In particular, this last characterisation gives the premisses of a new understanding of concurrency theory using homotopy theory.