In: Theoretical Computer Science Vol. 153, No. 1--2, pages 95-128. 1996.
Abstract: The box calculus is a process algebra with a simple Petri net semantics. We show that it provides for the concise translation of parallel programs and for the combination of verification techniques from process algebra and Petri nets. This is done by proving some properties of mutual exclusion algorithms.