Deadlocks and dihomotopy in mutual exclusion models

Higher dimensional automata (HDA) represent a promising tool for modelling (“true”) concurrency in a both combinatorial and topological framework. Within these models, fast algorithms investigating deadlocks and unreachable regions have been devised previously on a background of easily understandable “directed” geometric ideas. In this article, we modify notions and methods from homotopy theory to define and investigate “essentially different” schedules in a HDA and to detect whether two given runs are essentially different using an algorithm again based on “directed geometry”.