Algebraic Laws for Nondeterminism and Concurrency

Matthew Hennessy, Robin Milner

Research output: Contribution to journalArticlepeer-review

Abstract

Since a nondeterministic and concurrent program may, in general, communicate repeatedly with its environment, its meaning cannot be presented naturally as an input/output function (as is often done in the denotational approach to semantics). In this paper, an alternative is put forth. First, a definition is given of what it is for two programs or program parts to be equivalent for all observers; then two program parts are said to be observation congruent if they are, in all program contexts, equivalent. The behaviour of a program part, that is, its meaning, is defined to be its observation congruence class. The paper demonstrates, for a sequence of simple languages expressing finite (terminating) behaviours, that in each case observation congruence can be axiomatized algebraically. Moreover, with the addition of recursion and another simple extension, the algebraic language described here becomes a calculus for writing and specifying concurrent programs and for proving their properties.
Original languageEnglish
Pages (from-to)137-161
Number of pages25
JournalJournal of the ACM
Volume32
Issue number1
DOIs
Publication statusPublished - Jan 1985

Fingerprint Dive into the research topics of 'Algebraic Laws for Nondeterminism and Concurrency'. Together they form a unique fingerprint.

Cite this