{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:28:47Z","timestamp":1754483327285},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1995,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Morgan [Mor90a] has described a correspondence between Back's action systems [BKS83] and the conventional\n            <jats:italic>failures-divergences<\/jats:italic>\n            model of Hoare's\n            <jats:italic>communicating sequential processes<\/jats:italic>\n            (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.\n          <\/jats:p>\n          <jats:p>\n            Fortunately there is an extended\n            <jats:italic>infinite traces<\/jats:italic>\n            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.\n          <\/jats:p>\n          <jats:p>In passing, we develop a definition of the weakest precondition under which an infinite heterogeneous trace of actions is enabled.<\/jats:p>","DOI":"10.1007\/bf01214622","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T16:30:35Z","timestamp":1109349035000},"page":"37-53","source":"Crossref","is-referenced-by-count":18,"title":["Action systems, unbounded nondeterminism, and infinite traces"],"prefix":"10.1145","volume":"7","author":[{"given":"Michael","family":"Butler","sequence":"first","affiliation":[{"name":"Oxford University Programming Research Group, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carroll","family":"Morgan","sequence":"additional","affiliation":[{"name":"Oxford University Programming Research Group, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","volume-title":"Tract 131","author":"Back R.J.R.","year":"1980"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Back R.J.R.: Refining atomicity in parallel algorithms. In PARLE'89 volume LNCS 366. Springer-Verlag 1989.","DOI":"10.1007\/3-540-51285-3_42"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/3-540-52559-9_61"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Back R.J.R.: Refinement calculus lattices and higher order logic. In Marktoberdorf International Summer School \u2014 Program Design Calculi July 1992.","DOI":"10.1007\/978-3-662-02880-3_2"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Back R.J.R. and Kurki-Suonio R.: Decentralisation of process nets with centralised control. In 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing pages 131\u2013142 1983.","DOI":"10.1145\/800221.806716"},{"key":"e_1_2_1_2_6_2","unstructured":"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."},{"key":"e_1_2_1_2_7_2","unstructured":"Butler M.J.: A CSP Approach To Action Systems . D.Phil. Thesis Programming Research Group Oxford University 1992."},{"key":"e_1_2_1_2_8_2","unstructured":"Dijkstra E.W.: A Discipline of Programming . Prentice-Hall 1976."},{"key":"e_1_2_1_2_9_2","unstructured":"He J.: Process refinement. In J. McDermid editor The Theory and Practice of Refinement . Butterworths 1989."},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Hoare C.A.R.: Communicating Sequential Processes . Prentice-Hall 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"e_1_2_1_2_11_2","unstructured":"Hitchcock P. and Park D.: Induction rules and termination proofs. In IRIA Conference on Automata Languages and Programming Theory France 1972."},{"key":"e_1_2_1_2_12_2","unstructured":"Jones G. and Goldsmith M.: Programming in occam 2 . Prentice-Hall 1988."},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01788563"},{"key":"e_1_2_1_2_14_2","unstructured":"Morgan C.C.: Parallel Programming Without Synchronisation . Ph.D. Thesis University of Sydney 1979."},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Morgan C.C.: The specification statement. ACM Trans. Prog. Lang. and Sys. 10(3) 1988. Reprinted in [MRG88].","DOI":"10.1145\/44501.44503"},{"key":"e_1_2_1_2_16_2","unstructured":"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."},{"key":"e_1_2_1_2_17_2","unstructured":"Morgan C.C.: Programming from Specifications . Prentice-Hall 1990."},{"key":"e_1_2_1_2_18_2","unstructured":"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."},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90011-6"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/69558.69559"},{"key":"e_1_2_1_2_21_2","unstructured":"Roscoe A.W. and Barrett G.: Unbounded Nondeterminism in CSP . In MFPS '89 volume LNCS 298. Springer-Verlag 1989."},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/3.2.131"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Tarski A.: A lattice-theoretic fixpoint theorem and its applications. Pacific Journal Math. 5 1955.","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Woodcock J.C.P. and Morgan C.C.: Refinement of state-based concurrent systems. In D. Bj\u00f8rner C.A.R. Hoare and H. Langmaack editors VDM '90 volume LNCS 428. Springer-Verlag 1990.","DOI":"10.1007\/3-540-52513-0_18"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01214622.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01214622\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01214622","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:21:54Z","timestamp":1641482514000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01214622"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,1]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1995,1]]}},"alternative-id":["10.1007\/BF01214622"],"URL":"https:\/\/doi.org\/10.1007\/bf01214622","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,1]]}}}