Cubical complexes in concurrency theory, discrete and continuous models for directed lifting problems

In recent years, methods from algebraic topology and geometry have entered computer science. These methods are used in many different areas of computer science, and various traditional methods of geometry and algebraic topology are applied directly or costumized to fit the applications. Among the computer science disciplines which attract geometric methods is concurrency. Modern computers have more than one processor, and hence the execution of a program will often be distributed to different processors who then have to exchange information, to share memory, printers etc. For a fast execution, it is preferable that many processors work concurrently. On the other hand, the non-determinism introduced by various processors with their own local time and pace is problematic in verification that executions will do what they are expected to. Another problem introduced is the vast number of states in such a concurrent program - to check that a program will always behave correctly involves checking that all possible states are acceptable. This problem is referred to as the state space explosion problem. To discuss the problems, one needs a good model for concurrency. A model describing a program with just one process is a labelled directed graph with loops and branchings - an automaton. In 1991, V. Pratt [9] introduced a Higher Dimensional Automaton, an HDA, the higher dimensional analogue of an automaton as a model for concurrency. An HDA is a cubical set, where a solid cube of dimension n represents n actions which may be executed concurrently. Fig. 1 shows two different representations of the execution of actions a and b. The first figure, with only boundary edges of the square, represents a choice between “a then b” or “b then a”. The second figure with the full 2-cube has the interpretation that a and b may be executed concurrently by two processors. In particular, a and b do not interfer with each other and the result of the execution does not depend on the order in which a and b are executed.