Modeling concurrency with geometry

Abstract

The phenomena of branching time and true or noninterleaving concurrency find their respective homes in automata and schedules. But these two models of computation are formally equivalent via Birkhoff duality, an equivalence we expound on here in tutorial detail. So why should these phenomena prefer one over the other? We identify dimension as the culprit: l-dimensional automata are skeletons permitting only interleaving concurrency, whereas true n-fold concurrency resides in transitions of dimension n. The truly concurrent automaton dual to a schedule is not a skeletal distributive lattice but a solid one! We introduce true nondeterminism and define it as monoidal homotopy; from this perspective nondeterminism in ordinary automata arises from forking and joining creating nontrivial homotopy, The automaton dual to a poset schedule is simply connected whereas that dual to an event structure schedule need not be, according to monoidal homotopy though not to group homotopy. We conclude with a formal definition of higher dimensional automaton as an n-complex or n-category, whose two essential axioms are associativity of concatenation within dimension and an interchange principle between dimensions. 1 Background A central problem in the semantics of imperative computation is the construction of convenient models of computation embodying the apparent aspects of both branching time and true or noninterleaving or causal