Of wlp and CSP
Steve E. Dunne · Electronic Notes in Theoretical Computer Science · 2009
We extend Morgan's well-known derivation of the Failures-Divergences semantics of an action system endowed with a wp sequential semantics, by showing how various other CSP semantics can be extracted from an action system endowed with an appropriate sequential semantics. In doing so we expose the close but hitherto largely overlooked correspondence between the various CSP semantic models and their sequential correctness counterparts.