Two normal form theorems for CSP programs

DOI10.1016/0020-0190(87)90001-9MaRDI QIDQ1094869zbMATH OpenOpenAlexFDO

Authors Luc Bougé, Ph. Clermont, Krzysztof R. Apt

Publication date 1987

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://ir.cwi.nl/pub/10291

zbMATH Keywords

deadlock freedompartially interpreted computationsyntactic equivalence

Mathematics Subject Classification ID

Theory of operating systems (68N25)

Review text

We define two normal forms for CSP programs. In the first normal form, each process contains only one I/O repetitive command and all its I/O commands appear as guards of this command. In the second normal form, all guards of this I/O repetitive command are I/O guards. We describe an inductive method that transforms any CSP program into an equivalent program in first or second normal form. The notion of equivalence is discussed. It is shown that no transformation into second normal form can preserve deadlock freedom.

Recommendations

• Normalform-Transformationen für CSP-Programme. (Normal form transformations for CSP-programs)
• scientific article; zbMATH DE number 3911719
• Finite-state concurrent programs can be expressed in pairwise normal form
• Normal forms in total correctness for while programs and action systems
• scientific article; zbMATH DE number 3892585

Cites work

• Closed Covers: To Verify Progress for Communicating Finite State Machines
• Communicating sequential processes
• Correctness proofs of distributed termination algorithms
• Distributed Termination
• scientific article; zbMATH DE number 3808928 (Why is no real title available?)
• scientific article; zbMATH DE number 3903947 (Why is no real title available?)
• scientific article; zbMATH DE number 3744520 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• Normalform-Transformationen für CSP-Programme. (Normal form transformations for CSP-programs)
• On folk theorems
• Some Properties of Predicate Transformers
• Two normal form theorems for CSP programs

Cited in

(10)

• Two normal form theorems for CSP programs
• Normalform-Transformationen für CSP-Programme. (Normal form transformations for CSP-programs)
• Fairness and the axioms of control predicates
• Appraising fairness in languages for distributed programming
• Design and verification of fault tolerant systems with CSP
• Fairness and hyperfairness in multi-party interactions
• Repeated snapshots in distributed systems with synchronous communications and their implementation in CSP
• Fifty years of Hoare's logic
• Finite-state concurrent programs can be expressed succinctly in triple normal form
• Finite-state concurrent programs can be expressed in pairwise normal form

Describes a project that uses

Uses Software

• CESAR

This page was built for publication: Two normal form theorems for CSP programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1094869)