Connectivity of spaces of directed paths in geometric models for concurrent computation

TL;DR

This paper develops a topological approach to analyze the connectivity of execution spaces in higher dimensional automata modeling concurrent systems, using spare capacities to estimate path connectedness and detect deadlocks.

Contribution

It introduces a method to estimate the connectedness of path spaces in simple HDAs via spare capacities, linking local and global topological properties.

Findings

Connectedness of path spaces can be bounded by spare capacities.

Spare capacities help identify deadlocks and critical states.

The approach applies a nerve lemma to relate local and global topology.

Abstract

Higher Dimensional Automata (HDA) are higher dimensional relatives to transition systems in concurrency theory taking into account to which degree various actions commute. Mathematically, they take the form of labelled cubical complexes. It is important to know, and challenging from a geometric/topological perspective, whether the space of directed paths (executions in the model) between two vertices (states) is connected; more generally, to estimate higher connectedness of these path spaces. This paper presents an approach for such an estimation for particularly simple HDA modelling the access of a number of processors to a number of resources with given limited capacity each. It defines a spare capacity for a concurrent program with prescribed periods of access of the processors to the resources. It shows that the connectedness of spaces of directed paths can be estimated (from above) by spare capacities. Moreover, spare capacities can also be used to detect deadlocks and critical states in such a HDA. The key theoretical ingredient is a transition from the calculation of local connectedness bounds (of the upper links of vertices of an HDA) to global ones by applying a version of the nerve lemma due to Anders Bj\"orner.