TY - JOUR
T1 - Connectivity of spaces of directed paths in geometric models for concurrent computation
AU - Raussen, Martin
PY - 2023/2
Y1 - 2023/2
N2 - 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.
AB - 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.
KW - Connectivity
KW - Directed path
KW - Higher Dimensional Automata
KW - Nerve lemma
KW - Spare capacity
UR - https://arxiv.org/pdf/2106.11703.pdf
UR - http://www.scopus.com/inward/record.url?scp=85137165564&partnerID=8YFLogxK
U2 - 10.1016/j.comgeo.2022.101942
DO - 10.1016/j.comgeo.2022.101942
M3 - Journal article
SN - 0925-7721
VL - 109
JO - Computational Geometry
JF - Computational Geometry
M1 - 101942
ER -