03/04/2003
Vaughan Pratt (Stanford University)
Transition and Cancellation in Concurrency and Branching

We review the conceptual development of (true) concurrency and branching time starting from Petri nets and proceeding via Mazurkiewicz traces, pomsets, bisimulation, and event structures up to higher dimensional automata (HDAs), whose acyclic case may be identified with triadic event structures and triadic Chu spaces. Acyclic HDAs may be understood as extending the two truth values of Boolean logic with a third value expressing transition. We prove the necessity of such a third value under mild assumptions about the nature of observable events [...]. The main contribution is a new value × of cancellation, sibling to [the third value], serving to distinguish a(b + c) from ab + ac while simplifying the extensional definitions of termination and sequence. [...]