# A Theory of Communicating Sequential Processes

@article{Brookes1984ATO, title={A Theory of Communicating Sequential Processes}, author={Stephen D. Brookes and Charles Antony Richard Hoare and Andrew William Roscoe}, journal={J. ACM}, year={1984}, volume={31}, pages={560-599} }

A mathematical model for communicating sequential processes isgiven, and a number of its interesting and useful properties arestated and proved. The possibilities of nondetermimsm are fullytaken into account.

#### 1,389 Citations

A state-based approach to communicating processes

- Computer Science
- Distributed Computing
- 2005

Communicating processes, which may exhibit nondeterministic behaviour, are specified as state-transition systems. Equivalence and refinement relations are defined in terms of the failures model of… Expand

A calculus for communicating systems with time and probabilities

- Computer Science
- [1990] Proceedings 11th Real-Time Systems Symposium
- 1990

A process algebra that extends R. Milner's (1983) calculus of communicating systems (CCS) with probabilities and time is presented. With this calculus it is possible to describe real-time and… Expand

A Process Algebra of Concurrent Constraint Programming

- Computer Science
- JICSLP
- 1992

We develop an algebraic theory for the observational equivalence of concurrent constraint programs which identifies processes which have the same final results for all possible executions.

Communicating sequential processes

- Computer Science
- CACM
- 1983

This paper suggests that input and output are basic primitives of programming and that parallel composition of communicating sequential processes is a fundamental program structuring method. When… Expand

An Improved Failures Model for Communicating Processes

- Computer Science
- Seminar on Concurrency
- 1984

The failures model of communicating processes is extended to allow a more satisfactory treatment of divergence in addition to deadlock, and some connections are made with various models proposed by other authors. Expand

Quantales, Observational Logic and Process Semantics

- Mathematics, Computer Science
- Math. Struct. Comput. Sci.
- 1993

General completeness criteria are stated, and proved in applications, in which observations are taken as constituting a quantale. Expand

Process Realizability

- Computer Science, Mathematics
- Electron. Notes Theor. Comput. Sci.
- 1999

A notion of realizability for Classical Linear Logic is introduced, and a number of examples are described, including one based on concurrent games, and onebased on the process calculus CCS. Expand

Bounded Nondeterminism and the Approximation Induction Principle in Process Algebra

- Computer Science, Mathematics
- STACS
- 1987

A new semantics of ACPτ, the Algebra of Communicating Processes with abstraction is presented which is isomorphic to the model of process graphs modulo rooted τδ-bisimulation of Baeten, Bergstra & Klop. Expand

Descriptive and analytical process algebras

- Mathematics, Computer Science
- European Workshop on Applications and Theory in Petri Nets
- 1988

The notion of process equivalence is introduced and its complete axiomatization is proposed. Expand

A Complete Proof System for Timed Observations

- Computer Science
- TAPSOFT, Vol.1
- 1991

Timed Observations is a failure and divergence semantic model for concurrent processes, suitable for real-time systems that expresses true concurrency by action multisets (bags). Expand

#### References

SHOWING 1-10 OF 46 REFERENCES

Communicating sequential processes

- Computer Science
- CACM
- 1978

This paper suggests that input and output are basic primitives of programming and that parallel composition of communicating sequential processes is a fundamental program structuring method. When… Expand

An Improved Failures Model for Communicating Processes

- Computer Science
- Seminar on Concurrency
- 1984

The failures model of communicating processes is extended to allow a more satisfactory treatment of divergence in addition to deadlock, and some connections are made with various models proposed by other authors. Expand

A Proof System for Communicating Sequential Processes

- Computer Science
- TOPL
- 1980

An axiomatic proof system is presented for proving partial correctness and absence of deadlock of communicating sequential processes, the key (meta) rule introduces cooperation between proofs, and CSP's new convention for distributed termination of loops is dealt with. Expand

A mathematical theory of communicating processes

- Computer Science
- 1982

This thesis introduced much of the theory for Hoare's CSP, including the failures and failures-divergences model and methods of proving properties of processes based on metric, order and topological structures. Expand

A Complete Set of Axioms for a Theory of Communicating Sequential Processes

- Mathematics, Computer Science
- FCT
- 1983

This work defines formally this preorder and proves that it can be characterized as the smallest relation satisfying a particular set of axioms and shed lights on problems arising from the way divergence and underspecification are handled. Expand

Testing Equivalence for Processes

- Mathematics, Computer Science
- ICALP
- 1983

This work shows how to define in a natural way three different equivalences on processes that are applied to a particular language CCS and gives associated complete proof systems and fully abstract models. Expand

Testing Equivalences for Processes

- Computer Science, Mathematics
- Theor. Comput. Sci.
- 1984

This work shows how to define in a natural way three different equivalences on processes that are applied to a particular language CCS and gives associated complete proof systems and fully abstract models. Expand

A Calculus of Communicating Systems

- Mathematics, Computer Science
- Lecture Notes in Computer Science
- 1980

A case study in synchronization and proof techniques, and some proofs about data structures in value-communication as a model of CCS 2.0. Expand

Proof rules for communicating sequential processes

- Mathematics
- 1980

This thesis presents proof rules for an extension of Hoare's Communicating Sequential Processes (CSP). CSP is a notation for describing processes that interact through communication, which provides… Expand

Proving the Correctness of Multiprocess Programs

- Computer Science
- IEEE Transactions on Software Engineering
- 1977

The inductive assertion method is generalized to permit formal, machine-verifiable proofs of correctness for multiprocess programs, represented by ordinary flowcharts, and no special synchronization mechanisms are assumed. Expand