Abstract
There are two dimensions to study when we try to understand what behavioural models for CSP exist: what finitely observable things to record and what infinitely observable things to add to these. In this chapter we study what finite observation models exist. We examine the long-understood acceptances or ready-sets and refusal testing models. We discover two newer models: the acceptance-traces model of all finite linear observations, which is the finest possible model in this category, and the revivals model which sits above traces and stable failures, and below all other models. The structural result that proves this last fact puts ideas such as full abstraction in a completely new light. For each model we see what sorts of specification are best cast in terms of it.
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.
It was in helping with this work that the author first recognised the importance of allowing actions to occur after no refusal and suggested the • alternative.
- 2.
This does not happen for the final event seen in a revival because that event is always possible from the same state as the refusal. The revivals of \( P\backslash X \) only arise from those states that refuse the whole of X.
- 3.
This is important, because tests that require more cannot be decided in the class of finite-behaviour models. By “finitely observable properties”, we mean ones that the process’s representation in \(\mathcal{FL}\) can answer. We should notice that the class of divergence-strict models provides no competition because such models can never decide non-trivial finitely observable properties: if P satisfies some such property and Q does not, then the same is respectively true of \( P\,\sqcap \,{\rm div} \) and \( Q\,\sqcap \,{\rm div} \). But these last two processes are identified in any divergence-strict model.
References
Brookes, S.D., Rounds, W.C.: Possible futures, acceptances, refusals, and communicating processes. In: Foundations of Computer Science, 1981, SFCS’81 (1981)
Fournet, C., Hoare, C.A.R., Rajamani, S.K., Rehof, J.: Stuck-free conformance. In: CAV (2004)
Mukkaram, A.: A refusal testing model for CSP. Oxford University D.Phil. Thesis (1993)
Olderog, E.R., Hoare, C.A.R.: Specification-oriented semantics for communicating processes. Acta Inform. 23, 9–66 (1986)
Phillips, I.: Refusal testing. Theor. Comput. Sci. 50, 241–284 (1987)
Reed, J.N., Roscoe, A.W., Sinclair, J.E.: Responsiveness and stable revivals. Form. Asp. Comput. 19, 3 (2007)
Roscoe, A.W.: Revivals, stuckness and the hierarchy of CSP models. J. Log. Algebr. Program. 78, 3 (2009)
van Glabbeek, R.J.: The linear time—branching time spectrum I. In: The Handbook of Process Algebra. Elsevier, Amsterdam (2001)
van Glabbeek, R.J.: The linear time—branching time spectrum II. In: CONCUR (1999)
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). Finite Observation Models. In: Understanding Concurrent Systems. Texts in Computer Science. Springer, London. https://doi.org/10.1007/978-1-84882-258-0_11
Download citation
DOI: https://doi.org/10.1007/978-1-84882-258-0_11
Publisher Name: Springer, London
Print ISBN: 978-1-84882-257-3
Online ISBN: 978-1-84882-258-0
eBook Packages: Computer ScienceComputer Science (R0)