A MODEL FOR COMMUNICATING SEQUENTIAL PROCESSES

Abstract

This thesis describes the construction and mathematical properties of a model for communication sequential processes. We define a semantic model for processes based on failures, which encapsulate certain finite aspects of process behaviour and allow an elegant treatment of nondeterminism. We define a set of process operations, including nondertministic choice, conditional composition, and various forms of parallel composition. These process operations enjoy many interesting mathematical properties, which allow us to prove many process identities. The failures model is well suited to reasoning about deadlock properties of processes, and some examples are given to illustrate this.