Connectivity of spaces of directed paths in geometric models for concurrent computation
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örner.