{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:46:32Z","timestamp":1767339992051,"version":"3.41.0"},"reference-count":23,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2008,12,1]],"date-time":"2008-12-01T00:00:00Z","timestamp":1228089600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2008,12]]},"abstract":"<jats:p>The three classical process algebras CCS, CSP and ACP present several differences in their respective technical machinery. This is due, not only to the difference in their operators, but also to the terminology and \u2018way of thinking\u2019 of the community that has been (and still is) working with them. In this paper we will first discuss these differences and try to clarify the different usage of terminology and concepts. Then, as a result of this discussion, we define a generic process algebra where each of the basic mechanisms of the three process algebras (including minimal fixpoint based unguarded recursion) is expressed by an operator, and which can be used as an underlying common language. We show an example of the advantages of adopting such a language instead of one of the three more specialised algebras: producing a complete axiomatisation for Milner's observational congruence in the presence of (unguarded) recursion and static operators. More precisely, we provide a syntactical characterisation (allowing as many terms as possible) for the equations involved in recursion operators, which guarantees that transition systems generated by the operational semantics are finite state. Conversely, we show that every process admits a specification in terms of such a restricted form of recursion. We then present an axiomatisation that is ground complete over such a restricted signature. Notably, we also show that the two standard axioms of Milner for weakly unguarded recursion can be expressed using a single axiom only.<\/jats:p>","DOI":"10.1017\/s0960129508007111","type":"journal-article","created":{"date-parts":[[2008,9,18]],"date-time":"2008-09-18T10:18:14Z","timestamp":1221733094000},"page":"1057-1089","source":"Crossref","is-referenced-by-count":11,"title":["A ground-complete axiomatisation of finite-state processes in a generic process algebra"],"prefix":"10.1017","volume":"18","author":[{"given":"JOS C. M.","family":"BAETEN","sequence":"first","affiliation":[]},{"given":"MARIO","family":"BRAVETTI","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2008,12,1]]},"reference":[{"key":"S0960129508007111_manual_ref-1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004006"},{"key":"S0960129508007111_manual_ref-5","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_21"},{"key":"S0960129508007111_manual_ref-3","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00253-8"},{"key":"S0960129508007111_manual_ref-18","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1145\/233551.233556","article-title":"Branching time and abstraction in bisimulation semantics","volume":"43","author":"van","year":"1996","journal-title":"Journal of the ACM"},{"key":"S0960129508007111_manual_ref-7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-18625-5_49"},{"key":"S0960129508007111_manual_ref-17","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00251-4"},{"key":"S0960129508007111_manual_ref-22","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0084781"},{"key":"S0960129508007111_manual_ref-15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57182-5_39"},{"key":"S0960129508007111_manual_ref-8","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80025-X"},{"key":"S0960129508007111_manual_ref-4","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54430-5_83"},{"key":"S0960129508007111_manual_ref-13","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"key":"S0960129508007111_manual_ref-12","doi-asserted-by":"publisher","DOI":"10.1145\/566385.566386"},{"key":"S0960129508007111_manual_ref-16","first-page":"188","volume-title":"Proceedings First Workshop on the Algebra of Communicating Processes, ACP94","author":"van Glabbeek","year":"1994"},{"key":"S0960129508007111_manual_ref-9","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90088-X"},{"key":"S0960129508007111_manual_ref-23","unstructured":"Vaandrager, F.W. (1986) Verification of two communication protocols by means of process algebra. Technical Report report CS-R8608, CWI Amsterdam, 1986."},{"key":"S0960129508007111_manual_ref-14","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039617"},{"key":"S0960129508007111_manual_ref-21","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90070-9"},{"key":"S0960129508007111_manual_ref-10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16444-8_1"},{"volume-title":"Communication and Concurrency","year":"1989","author":"Milner","key":"S0960129508007111_manual_ref-20"},{"key":"S0960129508007111_manual_ref-11","first-page":"21","volume-title":"Proc. Logic Colloquium'86","author":"Bergstra","year":"1988"},{"key":"S0960129508007111_manual_ref-6","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.12.077"},{"volume-title":"Process algebra (equational theories of communicating processes)","year":"2008","author":"Baeten","key":"S0960129508007111_manual_ref-2"},{"volume-title":"Communicating Sequential Processes","year":"1985","author":"Hoare","key":"S0960129508007111_manual_ref-19"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129508007111","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T06:44:50Z","timestamp":1750488290000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129508007111\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12]]},"references-count":23,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2008,2]]}},"alternative-id":["S0960129508007111"],"URL":"https:\/\/doi.org\/10.1017\/s0960129508007111","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2008,12]]}}}