Lectures on a calculus for communicating systems. (English) Zbl 0609.68020

Milner, Robin

Concurrency, Semin. Pittsburgh/Pa. 1984, Lect. Notes Comput. Sci. 197, 197-220 (1985).

[For the entire collection see Zbl 0562.00011.]
Some new aspects and approaches to the CCS calculus are presented. A motivation example and the definition of the basic calculus with its evaluation rules form the first part - new is the possibility of infinite summation. In the next part observational equivalence and congruence are defined by means of bisimulation (original notions were defined without use of bisimulation). Their properties are studied and some nice advantages of this approach are discussed. The third lecture presents equational axioms; their completeness for all finite behaviors is proved (axioms are sound for all behaviors). An alternative characterization of observational equivalence in the modal logic framework is given. The final part shows how value manipulations, derived combinators and delta- terminations can be encoded into the basic calculus and the derived calculus is presented. Some practical implications of the presence of infinite summation (esp. a representation) of dynamically varying configurations) are discussed as well.

Reviewer: M.Křetínský

MSC:

68N25	Theory of operating systems
68Q60	Specification and verification (program logics, model checking, etc.)
68Q55	Semantics in the theory of computing

Keywords:

concurrent computation; semantics; CCS calculus; observational equivalence; modal logic

Citations:

Zbl 0562.00011