Undecidability results for deterministic communicating sequential processes

A study is presented of the subset of the communicating sequential processes (CSP) formalism in which processes are described in terms of recursive equations using only constant processes, deterministic choice, parallel composition, and sequential composition. Even with this limited version, the formalism is powerful enough to model a Turing machine so that a number of important problems such as boundedness, deadlock, and reachability are undecidable. The subset of the CSP formalism that is used is described. A number of analysis problems that are common to discrete-event systems are discussed. The Turing machine is outlined. Well-known properties of Turing machines are used to derive the undecidability results. The results are compared to properties of other models