{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:08:40Z","timestamp":1760202520517},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[1989,3,1]],"date-time":"1989-03-01T00:00:00Z","timestamp":604713600000},"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":[[1989,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>A number of mutual exclusion algorithms are studied by representing them as agents in the Calculus of Communicating Systems and using an automated tool embodying some of the theory of the Calculus to analyse the representations. It is determined whether or not each of the algorithms preserves mutual exclusion and is live.<\/jats:p>","DOI":"10.1007\/bf01887209","type":"journal-article","created":{"date-parts":[[2005,7,5]],"date-time":"2005-07-05T06:18:31Z","timestamp":1120544311000},"page":"273-292","source":"Crossref","is-referenced-by-count":38,"title":["Automated analysis of mutual exclusion algorithms using CCS"],"prefix":"10.1145","volume":"1","author":[{"given":"D. J.","family":"Walker","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Edinburgh, EH9 3JZ, Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Baeten J.: Procesalgebra Kluwer programmatuurkunde 1986."},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Baeten J. Bergstra J. and Klop J. W.: Decidability of Bisimulation Equivalence for Processes Generating Context-free Languages in Springer LNCS 299 1987.","DOI":"10.1007\/3-540-17945-3_5"},{"key":"e_1_2_1_2_3_2","unstructured":"Clarke E. and Emerson E. A.: Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic in Springer LNCS 131 1981."},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Clarke E. and Gr\u00fcmberg O.: Research on Automatic Verification of Finite-State Concurrent Systems. Ann. Rev. Comput. Sci. 2 1987.","DOI":"10.1146\/annurev.cs.02.060187.001413"},{"key":"e_1_2_1_2_5_2","unstructured":"Cleaveland R. Parrow J. and Steffen B.: The Concurrency Workbench to appear in [Gre89]."},{"key":"e_1_2_1_2_6_2","unstructured":"Cleaveland R. Parrow J. and Steffen B.: A Semantics based Verification Tool for Finite State Systems to appear in Proc. Ninth Int. Symp. on Protocol Specification Testing and Verification North Holland 1989."},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Dijkstra E. W.: Solution of a Problem in Concurrent Programming Control. Comm. ACM 8\/9 1965.","DOI":"10.1145\/365559.365617"},{"key":"e_1_2_1_2_8_2","unstructured":"Emerson E. A. and Lei C-L.: Modalities for Model Checking: Branching Time Strikes Back. Sci. Comput. Prog. 6 1987."},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Emerson E. A. and Srinivasan J.: Branching time temporal logic in Springer LNCS 354 1989.","DOI":"10.1007\/BFb0013022"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Francez N.: Fairness Springer 1986.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"e_1_2_1_2_11_2","unstructured":"Proceedings of Workshop on Automatic Verification Methods for Finite State Systems Grenoble 1989 to appear in Springer LNCS series."},{"key":"e_1_2_1_2_12_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_13_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/365153.365167","article-title":"Comments on a Problem in Concurrent Programming Control","volume":"9","author":"Hyman H.","year":"1966","journal-title":"Comm. ACM"},{"key":"e_1_2_1_2_14_2","unstructured":"Jonsson B. and Parrow J.: Deciding Bisimulation Equivalences for a Class of Non-Finite-State Programs in Springer LNCS 349 1989."},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Knuth D. E.: Additional Comments on a Problem in Concurrent Programming Control. Comm. ACM 9\/5 1966.","DOI":"10.1145\/355592.365595"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Kozen D.: Results on the Prepositional \u03bc -Calculus. Theoretical Computer Science 27 1983.","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Lamport L.: The Mutual Exclusion Problem Part II \u2014 Statement and Solutions. JACM 33\/2 1986.","DOI":"10.1145\/5383.5385"},{"key":"e_1_2_1_2_18_2","unstructured":"Larsen K.: Proof Systems for Hennessy-Milner Logic with Recursion to appear in Information and Computation 1989."},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pneuli A.: The Anchored Version of the Temporal Framework in Springer LNCS 354 1989.","DOI":"10.1007\/BFb0013024"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Milner R.: A Calculus of Communicating Systems Springer-Verlag 1980; available as University of Edinburgh report ECS-LFCS-87-7.","DOI":"10.1007\/3-540-10235-3"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Milner R.: Calculi for Synchrony and Asynchrony. Theoretical Computer Science 25 1983.","DOI":"10.1016\/0304-3975(83)90114-7"},{"key":"e_1_2_1_2_22_2","unstructured":"Milner R.: Communication and Concurrency Prentice-Hall 1989."},{"key":"e_1_2_1_2_23_2","unstructured":"Parrow J.: Verifying a CSMA\/CD-Protocol with CCS University of Edinburgh report ECS-LFCS-87-18 1987."},{"key":"e_1_2_1_2_24_2","unstructured":"Peterson J. L. and Silberschatz A.: Operating System Concepts 2nd ed. Addison Wesley 1985."},{"key":"e_1_2_1_2_25_2","unstructured":"Pratt V. A Decidable Mu-Calculus in Proc. 22nd ACM FOCS 1981."},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Queille J. and Sifakis J.: Specification and Verification of Concurrent Systems in CESAR in Springer LNCS 137 1981.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Stirling C.: Temporal Logics for CCS in Springer LNCS 354 1989.","DOI":"10.1007\/BFb0013039"},{"key":"e_1_2_1_2_28_2","unstructured":"Stirling C.: Modal and Temporal Logics chapter to appear in Handbook of Logic in Computer Science OUP 1989."},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Stirling C. and Walker D.: Local Model Checking in the Modal Mu-Calculus in Springer LNCS 351 1989.","DOI":"10.1007\/3-540-50939-9_144"},{"key":"e_1_2_1_2_30_2","unstructured":"Stirling C. and Walker D.: CCS Liveness and Local Model Checking in the Linear Time Mu-Calculus to appear in [Gre89]."},{"key":"e_1_2_1_2_31_2","unstructured":"Walker D.: Introduction to a Calculus of Communicating Systems University of Edinburgh report ECS-LFCS-87-22 1987."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01887209.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01887209\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01887209","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:24:29Z","timestamp":1641482669000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01887209"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989,3]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1989,3]]}},"alternative-id":["10.1007\/BF01887209"],"URL":"https:\/\/doi.org\/10.1007\/bf01887209","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1989,3]]}}}