Concurrent computing systems are those in which several events may happen in parallel; in fact that includes most modern systems. The verification of such systems is difficult: if one considers all possible interleavings of concurrent events, thus reducing concurrent systems to sequential systems which are well-understood, then the state space explodes; in addition it is not clear a priori which interleavings are possible (think out-of-order executions).

Perhaps surprisingly, geometry and topology may provide plenty of intuition for analysing concurrent systems in their own right, i.e. without reducing them to sequential systems. We will use this as a guiding principle for introducing several models for concurrent systems, exploring the relations between them, and using them for verification.

The tutorial will cover Petri nets, concurrent step transition systems, higher-dimensional automata, and directed topological spaces. We will see how to translate these formalisms into each other, how to analyse them, and how to use them to model concurrent systems. If time permits, we will also look at extensions such as Petri nets with inhibitor arcs or higher-dimensional timed automata.