Verification system for freedom from deadlock of communicating sequential processes

The communicating sequential processes (CSP) proposed by Hoare are a model for parallel computation in which the processes do not share a variable and perform the interprocess information exchange and synchronization by the communication instruction function. This paper first extends the verification system for the partial validity of CSP previously proposed by the authors and an axiomatic system is presented by implementing part of the inference rules which can deal with the deadlock‐free property of CSP. The soundness of the system is shown. The system previously proposed by the authors can provide the inferences in a concurrent way independently of the processes, without following the sequential procedure of proving a property for a process and proving a certain relation between processes. The system proposed in this paper employs a similar procedure and verification is made in parallel for the partial validity and deadlock‐free property of CSP.