A complete set of axioms for a theory of communicating sequential processes

In an abstract varsion of Hoare's CSP is defined and a denotational semantics based on the possible fallures of processes is given for it. This semantics induces a natural proorder on processes. We define formally this proorder and prova that it can be characterized as the smallest relation satisfying a particular set of axioms. The characterization will shed lights on problems arising from the way divergence and underspecification are handled.