### Algebraic laws for nondeterminism and concurrencyAlgebraic laws for nondeterminism and concurrency

Access Restriction
Subscribed

 Author Hennessy, Matthew ♦ Milner, Robin Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Copyright Year ©1985 Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science 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 $\textit{behavior}$ 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) behaviors, 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. ISSN 00045411 Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 1985-01-01 Publisher Place New York e-ISSN 1557735X Journal Journal of the ACM (JACM) Volume Number 32 Issue Number 1 Page Count 25 Starting Page 137 Ending Page 161

#### Open content in new tab

Source: ACM Digital Library