A Calculus of Communicating Systems

Frontmatter

0. Introduction

1. Experimenting on nondeterministic machines

2. Synchronization

3. A case study in synchronization and proof techniques

4. Case studies in value-communication

5. Syntax and semantics of CCS

6. Communication trees (CTs) as a model of CCS

Abstract

In this chapter we have

(i)

Constructed CTs as an intuitive model of CCS;

 

(ii)

Shown that, in considering atomic actions and strong equivalence of programs, we are justified in considering these notions as they apply to the denoted CTs;

 

(iii)

Shown that many useful program equivalence laws are actually identifies for CTs.

 

We have not studied the wider relation of observation-equivalence over programs. But it turns out that, for any equivalence relation which is defined in terms of \(\xrightarrow{{\mu v}}\) and/or ∼, we can think of this also as as equivalence relation over CTs.

7. Observation equivalence and its properties

8. Some proofs about data structures

9. Translation into CCS

10. Determinancy and confluence

11. Conclusion

Backmatter