article

Free access

Algebraic laws for nondeterminism and concurrency

Authors:

Matthew Hennessy,

Robin MilnerAuthors Info & Claims

Journal of the ACM (JACM), Volume 32, Issue 1

Pages 137 - 161

https://doi.org/10.1145/2455.2460

Published: 01 January 1985 Publication History

PDF eReader

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 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.

References

[1]

GORDON, M. J.l'tte Denotational Description oJ Programming Languages. Springer-Verlag, New York, 1979.

Crossref

Google Scholar

[2]

HENNESSY, M., AND MILNER, R.On observing nondeterminism and concurrency. In Proceedings of the 7th Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 85. Springer-Vedag, New York, Berlin, Heidelberg, 1980, pp. 299-309.

Crossref

Google Scholar

[3]

HENNESSY, M., AND PLOTKIN, G. D.Full abstraction for a simple parallel programming language. In Proceedings of the 8th MFCS Conference (Olomouc, Czechoslovakia). Lecture Notes in Computer Science, vol. 74. Springer-Verlag, New York, 1979, pp. 108-121.

Google Scholar

[4]

MILNE, G., AND MILNER, R.Concurrent processes and their syntax. J. ACM 26, (1979), 302-321.

Crossref

Google Scholar

[5]

MILNER, R.Synthesis of communicating behaviour. In Proceedings of the 7th MFCS Conference (Zacopane, Poland). Lecture Notes in Computer Science, vol. 64. Springer-Vedag, New York, 1978, pp. 71-83.

Google Scholar

[6]

MILNER, R.A Calculus of Communicating Systems. Lecture Notes in Computer Science, vol. 92. Springer-Verlag, New York, 1980.

Crossref

Google Scholar

[7]

PLOTKIN, G. D.A powerdomain construction. SIAM J. Comput. 5, 3 (1976), 452-487.

Google Scholar

[8]

PNUELI, A.The temporal logic of programs. In Proceedings of the 19th Annual Symposium on Foundations of Computer Science (Providence, R.I.). IEEE, New York, 1977, pp. 46-57.

Google Scholar

[9]

PRATT, V.R.Semantical considerations of Floyd-Hoare logic. In Proceedings of the 17th Annual Symposium on Foundations of Computer Science. IEEE, New York, 1976, pp. 109-121.

Google Scholar

[10]

SMYTH, M. Powerdomains. J. Comput. Syst. Sci. 15, 1 (1978), 23-36.

Google Scholar

[11]

STOY, J.E.Denotational Semantics: The Scott Strachey Approach to Programming Language Theory. MIT Press, Cambridge, Mass., 1977.

Crossref

Google Scholar

Cited By

View all

Stanković MStanimirović SĆirić M(2025)Approximate Hennessy-Milner type theorems for fuzzy multimodal logics over Heyting algebrasInternational Journal of Approximate Reasoning10.1016/j.ijar.2025.109362179(109362)Online publication date: Apr-2025
https://doi.org/10.1016/j.ijar.2025.109362
Stanković MĆirić MStanimirović SStakić Đ(2025)Approximate bisimulations for Kripke models of fuzzy multimodal logics over complete Heyting algebrasFuzzy Sets and Systems10.1016/j.fss.2025.109299507(109299)Online publication date: May-2025
https://doi.org/10.1016/j.fss.2025.109299
Bernardo MEsposito AMezzina C(2024)Expansion Laws for Forward-Reverse, Forward, and Reverse Bisimilarities via Proved EncodingsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.412.5412(51-70)Online publication date: 22-Nov-2024
https://doi.org/10.4204/EPTCS.412.5
Show More Cited By

Index Terms

Algebraic laws for nondeterminism and concurrency
1. Theory of computation
  1. Models of computation
  2. Semantics and reasoning
    1. Program semantics

Recommendations

Nondeterminism in Constructive Z

The abstraction inherent in most specifications and the need to specify nondeterministic programs are two well-known sources of nondeterminism in formal specifications. In this paper, we present a Z-based formalism by which one can specify bounded, ...
Nondeterminism in Constructive Z

The abstraction inherent in most specifications and the need to specify nondeterministic programs are two well-known sources of nondeterminism in formal specifications. In this paper, we present a Z-based formalism by which one can specify bounded, ...
An Algebraic Theory for Shared-State Concurrency
Programming Languages and Systems
Abstract
We present a monadic denotational semantics for a higher-order programming language with shared-state concurrency, i.e. global-state in the presence of interleaving concurrency. Central to our approach is the use of Plotkin and Power’s algebraic ...

Comments

Information & Contributors

Information

Published In

Journal of the ACM Volume 32, Issue 1

Jan. 1985

246 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/2455

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1985

Published in JACM Volume 32, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1,018
Total Citations
View Citations
2,877
Total Downloads

Downloads (Last 12 months)214
Downloads (Last 6 weeks)17

Reflects downloads up to 28 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Stanković MStanimirović SĆirić M(2025)Approximate Hennessy-Milner type theorems for fuzzy multimodal logics over Heyting algebrasInternational Journal of Approximate Reasoning10.1016/j.ijar.2025.109362179(109362)Online publication date: Apr-2025
https://doi.org/10.1016/j.ijar.2025.109362
Stanković MĆirić MStanimirović SStakić Đ(2025)Approximate bisimulations for Kripke models of fuzzy multimodal logics over complete Heyting algebrasFuzzy Sets and Systems10.1016/j.fss.2025.109299507(109299)Online publication date: May-2025
https://doi.org/10.1016/j.fss.2025.109299
Bernardo MEsposito AMezzina C(2024)Expansion Laws for Forward-Reverse, Forward, and Reverse Bisimilarities via Proved EncodingsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.412.5412(51-70)Online publication date: 22-Nov-2024
https://doi.org/10.4204/EPTCS.412.5
Bennouna APachamanova DPerakis GSkali Lami O(2024)Learning the Minimal Representation of a Continuous State-Space Markov Decision Process from Transition DataManagement Science10.1287/mnsc.2022.01652Online publication date: 26-Sep-2024
https://doi.org/10.1287/mnsc.2022.01652
Das SSharma A(2024)Embeddings Between State and Action Based Probabilistic LogicsFormal Aspects of Computing10.1145/369643137:2(1-58)Online publication date: 21-Sep-2024
https://dl.acm.org/doi/10.1145/3696431
Pflueger MMarti JKostylev ESobocinski PLago UEsparza J(2024)A Characterisation Theorem for Two-Way Bisimulation-Invariant Monadic Least Fixpoint Logic Over Finite StructuresProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662107(1-14)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662107
Acay CGancher JRecto RMyers A(2024)Secure Synthesis of Distributed Cryptographic Applications2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00021(433-448)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00021
Edixhoven LJongmans SProença JCastellani I(2024)Branching pomsets: Design, expressiveness and applications to choreographiesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100919136(100919)Online publication date: Jan-2024
https://doi.org/10.1016/j.jlamp.2023.100919
Nguyen LTran D(2024)Computing crisp bisimulations for fuzzy structuresInternational Journal of Approximate Reasoning10.1016/j.ijar.2024.109121166:COnline publication date: 1-Mar-2024
https://dl.acm.org/doi/10.1016/j.ijar.2024.109121
Bisping BMontanari L(2024)Characterizing contrasimilarity through games, modal logic, and complexityInformation and Computation10.1016/j.ic.2024.105191300:COnline publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1016/j.ic.2024.105191
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations

Nondeterminism in Constructive Z

Nondeterminism in Constructive Z

An Algebraic Theory for Shared-State Concurrency

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Share

Share this Publication link

Share on social media

Affiliations