Hostname: page-component-6bf8c574d5-qdpjg Total loading time: 0 Render date: 2025-02-21T04:05:26.905Z Has data issue: false hasContentIssue false

Transition and cancellation in concurrency and branching time

Published online by Cambridge University Press:  31 July 2003

VAUGHAN R. PRATT
Affiliation:
Stanford University
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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 $\T$ expressing transition. We prove the necessity of such a third value under mild assumptions about the nature of observable events, and show that the expansion of any complete Boolean basis $L$ to $L_{\T}$ with a third literal $\that a$ expressing $a=\T$ forms an expressively complete basis for the representation of acyclic HDAs. The main contribution is a new value $\cancel$ of cancellation, which is a sibling of $\T$, serving to distinguish $a(b+c)$ from $ab+ac$ while simplifying the extensional definitions of termination $\tick\A$ and sequence $\A\B$. We show that every HDAX (acyclic HDA with $\cancel$) is representable in the expansion of $L_{\T}$ to $L_{\T\cancel}$ with a fourth literal $\can a$ expressing $a=\cancel$.

Type
Paper
Copyright
2003 Cambridge University Press