Abstract
Morgan [Mor90a] has described a correspondence between Back's action systems [BKS83] and the conventionalfailures-divergences model of Hoare'scommunicating sequential processes (CSP) formalism [Hoa85]. However, the CSP failures-divergences model does not treat unbounded nondeterminism, although unbounded nondeterminism arises quite naturally in action systems; to that extent, the correspondence between the two approaches is inadequate.
Fortunately there is an extendedinfinite traces model of CSP [RoB89] which treats unbounded nondeterminism. We extend the CSP-action system correspondence, using that model instead, to take the unbounded nondeterminism of action systems properly into account.
In passing, we develop a definition of the weakest precondition under which an infinite heterogeneous trace of actions is enabled.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Back, R.J.R.:Correctness Preserving Program Refinements: Proof Theory and Applications. Tract 131, Mathematisch Centrum, Amsterdam, 1980.
Back, R.J.R.: Refining atomicity in parallel algorithms. InPARLE'89, volume LNCS 366. Springer-Verlag, 1989.
Back, R.J.R.: Refinement calculus II: Parallel and reactive systems. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors,Stepwise Refinement of Distributed Systems, volume LNCS 430. Springer-Verlag, 1990.
Back, R.J.R.: Refinement calculus, lattices and higher order logic. InMarktoberdorf International Summer School — Program Design Calculi, July 1992.
Back, R.J.R. and Kurki-Suonio, R.: Decentralisation of process nets with centralised control. In2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pages 131–142, 1983.
Back, R.J.R. and Sere, K.: Deriving an occam implementation of action systems. In C.C. Morgan and J.C.P. Woodcock, editors,3rd BCS-FACS Refinement Workshop. Springer-Verlag, 1990.
Butler, M.J.:A CSP Approach To Action Systems. D.Phil. Thesis, Programming Research Group, Oxford University, 1992.
Dijkstra, E.W.:A Discipline of Programming. Prentice-Hall, 1976.
He, J.: Process refinement. In J. McDermid, editor,The Theory and Practice of Refinement. Butterworths, 1989.
Hoare, C.A.R.:Communicating Sequential Processes. Prentice-Hall, 1985.
Hitchcock, P. and Park, D.: Induction rules and termination proofs. InIRIA Conference on Automata Languages and Programming Theory, France, 1972.
Jones, G. and Goldsmith, M.:Programming in occam 2. Prentice-Hall, 1988.
Josephs, M.B.: A state-based approach to communicating sequential processes.Distributed Computing, 3:9–18, 1988.
Morgan, C.C.:Parallel Programming Without Synchronisation. Ph.D. Thesis, University of Sydney, 1979.
Morgan, C.C.: The specification statement.ACM Trans. Prog. Lang. and Sys., 10(3), 1988. Reprinted in [MRG88].
Morgan, C.C.: Of wp and CSP. In W.H.J. Feijen, A.J.M. van Gasteren, D. Gries, and J. Misra, editors,Beauty is our business: a birthday salute to Edsger W. Dijkstra. Springer-Verlag, 1990.
Morgan, C.C.:Programming from Specifications. Prentice-Hall, 1990.
Morgan, C.C., Robinson, K.A. and Gardiner, P.H.B.:On the Refinement Calculus. Technical Monograph PRG-70, Programming Research Group, Oxford University, October 1988.
Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus.Sci. Comp. Prog., 9(3):298–306, 1987.
Nelson, G.: A generalization of Dijkstra's calculus.ACM Trans. Prog. Lang. Sys., 11(4):517–561, 1989.
Roscoe, A.W. and Barrett, G.:Unbounded Nondeterminism in CSP. InMFPS '89, volume LNCS 298. Springer-Verlag, 1989.
Roscoe, A.W.:Unbounded Nondeterminism in CSP.J. Logic Computat., 3(2): 131–172, 1993.
Tarski, A.: A lattice-theoretic fixpoint theorem and its applications.Pacific Journal Math., 5, 1955.
Woodcock, J.C.P. and Morgan, C.C.: Refinement of state-based concurrent systems. In D. Bjørner, C.A.R. Hoare, and H. Langmaack, editors,VDM '90, volume LNCS 428. Springer-Verlag, 1990.
Author information
Authors and Affiliations
Additional information
Funded by Broadcom Éireann Research Ltd, Dublin.
Rights and permissions
About this article
Cite this article
Butler, M., Morgan, C. Action systems, unbounded nondeterminism, and infinite traces. Formal Aspects of Computing 7, 37–53 (1995). https://doi.org/10.1007/BF01214622
Received:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF01214622