Andrew Butterfield (Trinity College Dublin): Concurrency and State in UTP - Choice as Parallelism

(Joint work with Pawel Gancarski and Jim Woodcock)

Abstract: A key area of exploration in the Unifying Theories of Programming (UTP) paradigm is the unification of theories of concurrent systems like CSP or CCS with imperative systems that have explicit state change resulting from variable assignment. Much current work focusses on the Circus language, which is a fusion of Z and CSP. While the difficulties in merging concurrency with shared state are well known, this talk focusses on an less obvious interaction - that of state change coupled with external choice. We demonstrate, in our models of state-rich concurrency, that there is an string operational connection between parallelism and event-based choice.