Sanderson, Michael Thomas

2019-02-15T14:19:57Z

2019-02-15T14:19:57Z

1983

Proofs of observational equivalence of behaviour expressions in Milner's Calculus of Communicating Systems can be quite lengthy, and as larger and more practical systems of agents are considered the need for shorter proof techniques becomes more important. In this thesis a number of results about the calculus are proved which give rise to give more natural techniques. Three principal areas of research are presented:

(i) A study of strong confluence and determinacy is made, extending Hilner's work to the whole calculus - the appropriate modifications to take value-passing into account are motivated and defined, and a strong confluence theorem is proved. It is shown that a useful subcalculus of CCS is strongly confluent.

(ii) An investigation into criteria for uniqueness of solution of equations pf the form b = Fib] is performed. To do this a concept of derivations of an agent A "causing" derivations of FlAl is defined; using this, conditions are imposed on F which imply uniqueness, and a study follows of how these conditions relate to the structure of F.

(iii) By using an alternative, stronger, definition of observational equivalence as a maximal fixed point it is found that equivalences can be demonstrated by constructing bisimulations between agents, and results leading to an algorithm for such constructions are presented. Also, using this alternative definition a weaker form of confluence can be defined very easily, and this is investigated.

The theoretical material in this thesis is supplemented by examples demonstrating how the results proved can be applied to give proof techniques for use within the calculus.

http://hdl.handle.net/1842/33815

The University of Edinburgh

Annexe Thesis Digitisation Project 2019 Block 22

Proof techniques for CCS

Thesis or Dissertation

Doctoral

PhD Doctor of Philosophy