Deadlocks and Dihomotopy in Mutual Exclusion Models

Parallel processes in concurrency theory can be modelled in a geometric framework. A convenient model are the Higher Dimensional Automata of V. Pratt and E. Goubault with cubical complexes as their mathematical description. More abstract models are given by (locally) partially ordered topological spaces, the directed ($d$-spaces) of M.Grandis and the flows of P. Gaucher. All models invite to use or modify ideas from algebraic topology, notably homotopy. In specific semaphore models for mutual exclusion, we have developed methods and algorithms that can detect deadlocks and unsafe regions and give information about essentially different schedules using higher dimensional ``geometric'' representations of the state space and executions (directed paths) along it.