On the expressiveness of CSP
Andrew William Roscoe · 2008
Abstract. We show that Hoare’s CSP, with the addition of the exception-throwing operator P ΘA Q in which any occurrence of an event a ∈ A within P hands control to Q, can simulate any operator that has a “CSP-like ” operational semantics. Thus any language, all of whose operators are CSP-like, has a semantics over each of the behavioural models of CSP and a natural theory of refinement. This demonstrates that CSP+ is a natural language to compile other notations into. We explore the range of possibilities for CSP-like languages, which include the π-calculus.