Modern concurrent systems are considered challenging to reason about because of the nature of concurrent behaviour. Concurrency is highly pervasive and often found on all levels of computation. Since concurrency is unambiguous and pervasive, mathematical models are necessary for reasoning about concurrent behaviour. Non-interleaving models are promising when considering the incremental development of concurrent systems. The incremental development considers a method known as action refinement. Action refinement is the method of developing a system by starting with an abstract specification and gradually refining its action by providing more details. However, non-interleaving models lack a tractable algebraic theory. Algebraic topology has been used to define a geometric model of concurrency that has a natural algebraic structure, that is, overcoming the lack of a tractable algebraic theory. This model was named higher-dimensional automata and is a geometric model of concurrency shown to capture main characteristics of both interleaving and non-interleaving models, that is, higher-dimensional automata are highly expressive.
Sculpting is a method of identifying events in a higher-dimensional automaton. Intuitively, a higher-dimensional automaton is an automaton with nicely incorporated squares, cubes and higher-dimensional cubes, which represent the independence of events. In this thesis we show, by following the intuition of Pratt, that the process of modelling a concurrent system using higher-dimensional automata as a sculpting process − take one single higher-dimensional cube, having enough concurrency, that is, enough events, and remove cells until the desired concurrent behaviour is obtained.
We also investigate a conjecture posed by Vaughan Pratt. The conjecture is that any higher-dimensional automata can be obtained using the sculpting method. We first need to define precisely the sculpting method, following again the intuition of Pratt that sculpting is similar to subalgebras. We answer in negative by giving examples of higher-dimensional automata which are not sculptures. We also identify precisely the class of higher-dimensional automata for which events can be identified using the standard method used in the literature, that is, as transitions opposite in a square.
| supervisors | Christian Johansen, Ulrich Fahrenberg, Martin Steffen, Olaf Owe |
| IFI links | abstract, thesis, presentation |