Abstract
This chapter studies denotational semantics in more depth than in the introductory chapters. We discuss the nature of behavioural models and what is required of them. We see how CSP definitions of operators naturally lead to distributive operators, and discuss topics such as full abstraction and congruence with operational semantics. We look in detail at each of the traces, stable failures and failures divergences model, and understand their healthiness conditions. We are able to specify determinism formally and study its relationship with the related concept of confluence.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The special style of brackets 〚⋅〛 is commonly used in denotational semantics to separate program syntax from abstract semantics. They have no formal significance, but give a useful visual signal. In fact we will not generally use them when it comes to dealing with CSP except in places where a clear distinction between syntax and semantics is vital.
- 2.
The fact that only a single behaviour of each argument is used is closely related to the “no copying” requirement we placed on combinator operational semantics in Chap. 9. That requirement implies that no operator can use more than one behaviour of an on argument as it progresses. There is nothing of a similar nature that prevents off arguments being used multiple times; but all the standard, non-recursive, CSP operators with off arguments happen to obey the no-copy rule for them also.
- 3.
The effect of F4 is, in combination with F2, to make the failures behaviour of a process standardised in line with the assumption discussed in Sect. 7.1.1 that ✓ is a non-controllable signal. We could have achieved the same effect by (i) removing ✓ from refusal sets, and (ii) not having any failures with terminated traces. A stable failure (s,X) would then be interpreted as coming from a stable state (without τ or ✓) rather than allowing it to come from any ✓-stable state. This would represent exactly the same equivalence over LTSs and CSP processes as the representation above: see Exercise 10.7.
Stylistically, it would probably be cleaner to take the option described in the previous paragraph, but we have used the representation above for two reasons. Firstly, it is obviously desirable that the notation of \(\mathcal{F}\) should be consistent with \(\mathcal{N}\), and using this alternative approach for \(\mathcal{N}\) would require the addition of an extra component to the model that told us the terminated traces. Secondly, the version in which ✓ can be a member of refusal sets is consistent with TPC.
- 4.
There is no reason why one could not use a richer finite-behaviour model of the form we will see in Chap. 11 provided one was careful with the definition of \({\mathit{Chaos}}\/_{H}\). However, the author has never found cause to do so.
- 5.
The observant reader of this book and TPC will notice that D1 is slightly different from the version in TPC, and that we have dropped condition D3 from there. Both these changes are consequences of our decision here to drop terminated traces \(s\hat{\phantom{\cdot}}\langle\checkmark \rangle \) as possible members of D. This change makes no difference to the equivalence the model induces over processes. The modification was, in fact, suggested in an exercise in TPC.
- 6.
This is because it models what processes communicate and when they diverge but not when they refuse things stably. So the top element is the one that does no diverging and no communicating, and refuses everything instead.
- 7.
The formula \(\bigcap_{n=0}^{n}F^{n}(\mathbf{div})\) is correct whenever F is a continuous function with respect to ⊑, or the recursion is guarded, but in general the fixed point might be a proper refinement of this value.
- 8.
Each process this syntax can create has the property that if \(s\hat{\phantom{\cdot}}\langle\checkmark \rangle\) is a trace, then (for a∈Σ, \(s\hat{\phantom{\cdot}}\langle a\rangle\) is not.
- 9.
One could add \(\mathop{ \varTheta _{A}}\) into this list, but it does not preserve the property of confluence described below.
- 10.
Therefore 〈a,b,a,c,a,d〉−〈a,d,a,d〉=〈b,c,a〉, with the first two as and the only d being deleted from the first trace.
- 11.
Readers who compare this definition with that in TPC will see that this one is abstracted. The one in TPC is not in fact confluent because the nodes input data over left and up, which is prefix-choice not single prefix. Networks like that one, where communication patterns are confluent even though the unabstracted networks are not, are themselves of interest. See [127] for example.
- 12.
The proof of the \(\mathcal{N}\) result in the printed version of TPC is faulty: the reader should consult the on-line version.
References
Brookes, S.D.: A model for communicating sequential processes. Oxford University D.Phil. thesis (1983) (published as a Carnegie-Mellon University technical report)
Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984)
Brookes, S.D., Roscoe, A.W.: An improved failures model for CSP. In: Proceedings of the Pittsburgh seminar on concurrency. LNCS, vol. 197. Springer, Berlin (1985)
Brookes, S.D., Roscoe, A.W., Walker, D.J.: An operational semantics for CSP. Technical report (1988)
Dijkstra, E.W., Scholten, C.S.: A class of simple communication patterns. In: Selected Writings on Computing, EWD643. Springer, Berlin (1982)
Hoare, C.A.R.: A model for communicating sequential processes. In: McKeag, R.M., MacNaughten, A.M. (eds.) On the construction of programs. Cambridge University Press, Cambridge (1980)
Hoare, C.A.R., Brookes, S.D., Roscoe, A.W.: A theory of communicating sequential processes. Technical Monograph PRG-16, Oxford University Computing Laboratory (1981) (draft of [63])
Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Berlin (1980)
Milner, R.: Communication and Concurrency. Prentice Hall, New York (1989)
Roscoe, A.W.: A mathematical theory of communicating processes. Oxford University D.Phil. Thesis (1982)
Roscoe, A.W.: Denotational semantics for occam. In: Proceedings of the Pittsburgh Seminar on Concurrency. LNCS, vol. 197. Springer, Berlin (1985)
Roscoe, A.W.: Topology, computer science and the mathematics of convergence. In: Reed, G.M., Roscoe, A.W., Wachter, R.F. (eds.) Topology and Category Theory in Computer Science. Oxford University Press, London (1991)
Roscoe, A.W.: An alternative order for the failures model. J. Log. Comput. 2, 5 (1992)
Roscoe, A.W.: Unbounded nondeterminism in CSP. J. Log. Comput. 3, 2 (1993)
Roscoe, A.W.: The pursuit of buffer tolerance (2005). web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/106.pdf
Roscoe, A.W.: CSP is expressive enough for π. In: Jones, C.B., Roscoe, A.W., Wood, K.R. (eds.) Reflections on the Work of C.A.R. Hoare. Springer, Berlin (2010)
Walker, D.J.: An operational semantics for CSP. Oxford University M.Sc. Dissertation (1986)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2010 Springer-Verlag London Limited
About this chapter
Cite this chapter
Roscoe, A.W. (2010). Denotational Semantics and Behavioural Models. In: Understanding Concurrent Systems. Texts in Computer Science. Springer, London. https://doi.org/10.1007/978-1-84882-258-0_10
Download citation
DOI: https://doi.org/10.1007/978-1-84882-258-0_10
Publisher Name: Springer, London
Print ISBN: 978-1-84882-257-3
Online ISBN: 978-1-84882-258-0
eBook Packages: Computer ScienceComputer Science (R0)