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 connectivity of these path spaces. This paper presents an approach for such an estimation for particularly simple HDA arising from PV programs and modelling the access of a number of processors to a number of resources with given limited capacity each. It defines the spare capacity of a concurrent program with prescribed periods of access of the processors to the resources using only the syntax of individual programs and the capacities of shared resources. It shows that the connectivity 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 simple HDA. The key theoretical ingredient is a transition from the calculation of local connectivity 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örner.

Abstract Directed paths have been used by several authors to describe concurrent executions of a program. Spaces of directed paths in an appropriate state space contain executions with all possible legal schedulings. It is interesting to investigate whether one obtains different topological properties of such a space of executions if one restricts attention to schedulings with “nice” properties, e.g. involving synchronisations. This note shows that this is not the case, i.e. that one may operate with nice schedulings without inflicting any harm. Several of the results in this note had previously been obtained by Ziemiański in Ziemiański (2017. Applicable Algebra in Engineering, Communication and Computing28 497–525; 2020a. Journal of Applied and Computational Topology4 (1) 45–78). We attempt to make them accessible for a wider audience by giving an easier proof for these findings by an application of quite elementary results from algebraic topology; notably the nerve lemma.