{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T17:40:56Z","timestamp":1763746856668},"reference-count":49,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2009,9,4]],"date-time":"2009-09-04T00:00:00Z","timestamp":1252022400000},"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":[[2009,10]]},"abstract":"<jats:p>Mathematical modelling is one of the fundamental tools of science and engineering. Very often, models are required to be executable, as a simulation, on a computer. In this paper, we present some contributions to the process-theoretic and logical foundations of discrete-event modelling with resources and processes. We present a process calculus with an explicit representation of resources in which processes and resources co-evolve. The calculus is closely connected to a logic that may be used as a specification language for properties of models. The logic is strong enough to allow requirements that a system has a certain structure: for example, that it is a parallel composite of subsystems. This work consolidates, extends and improves upon aspects of earlier work of ours in this area. An extended example, consisting of a semantics for a simple parallel programming language, indicates a connection with separating logics for concurrency.<\/jats:p>","DOI":"10.1017\/s0960129509990077","type":"journal-article","created":{"date-parts":[[2009,9,4]],"date-time":"2009-09-04T04:21:04Z","timestamp":1252038064000},"page":"959-1027","source":"Crossref","is-referenced-by-count":41,"title":["Algebra and logic for resource-based systems modelling"],"prefix":"10.1017","volume":"19","author":[{"given":"MATTHEW","family":"COLLINSON","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"DAVID","family":"PYM","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,9,4]]},"reference":[{"key":"S0960129509990077_ref46","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211867"},{"key":"S0960129509990077_ref44","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055628"},{"key":"S0960129509990077_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0091-7"},{"key":"S0960129509990077_ref31","volume-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"S0960129509990077_ref30","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90114-7"},{"key":"S0960129509990077_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"key":"S0960129509990077_ref28","article-title":"Deriving bisimulation congruences for reactive systems. In: Proc. CONCUR 2000","volume":"1877","author":"Leifer","year":"2000","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129509990077_ref27","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"key":"S0960129509990077_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"S0960129509990077_ref39","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"S0960129509990077_ref32","volume-title":"Communicating systems and the \u03c0-calculus","author":"Milner","year":"1999"},{"key":"S0960129509990077_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80311-1"},{"key":"S0960129509990077_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_29"},{"key":"S0960129509990077_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"S0960129509990077_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0060438"},{"key":"S0960129509990077_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0047-2"},{"key":"S0960129509990077_ref11","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508007159"},{"key":"S0960129509990077_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151648"},{"key":"S0960129509990077_ref9","unstructured":"Cardelli L. and Gordon A. (1998) Mobile ambients. In Nivat M. (ed.) Foundations of Software Science and Computational Structures. Springer-Verlag Lecture Notes in Computer Science 1378 40\u2013155."},{"key":"S0960129509990077_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4899-6685-8"},{"key":"S0960129509990077_ref2","volume-title":"Principles of Concurrent and Distributed Programming","author":"Ben-Ari","year":"1990"},{"key":"S0960129509990077_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.036"},{"key":"S0960129509990077_ref22","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950700597X"},{"key":"S0960129509990077_ref48","doi-asserted-by":"crossref","unstructured":"Victor B. and Moller F. (1994) The Mobility Workbench \u2013 a tool for the \u03c0-calculus. In: Dill D. (ed.) CAV'94: Computer Aided Verification. Springer-Verlag Lecture Notes in Computer Science 818 428\u2013440.","DOI":"10.1007\/3-540-58179-0_73"},{"key":"S0960129509990077_ref41","doi-asserted-by":"crossref","unstructured":"Pym D. and Tofts C. (2007) Systems Modelling via Resources and Processes: Philosphy, Calculus, Semantics, and Logic. In: Cardelli L. , Fiore M. and Winskel G. (eds.) Computation, Meaning and Logic: articles dedicated to Gordon Plotkin. Electronic Notes in Theoretical Computer Science 172 545\u2013587. (Errata at: http:\/\/www.cs.bath.ac.uk\/~pym\/pym-tofts-fac-errata.pdf.)","DOI":"10.1016\/j.entcs.2007.02.020"},{"key":"S0960129509990077_ref17","unstructured":"Demos 2k Team (2002) Demos 2000. http:\/\/www.demos2k.org."},{"key":"S0960129509990077_ref37","first-page":"183","volume-title":"Proceedings of the 14th Symposium on Logic in Computer Science (LICS99), Trento, Italy","author":"Pym","year":"1999"},{"key":"S0960129509990077_ref49","first-page":"1","volume-title":"Handbook of Logic in Computer Science","author":"Winskel","year":"1995"},{"key":"S0960129509990077_ref8","doi-asserted-by":"crossref","unstructured":"Calcagno C. , Gardner P. and Zarfaty U. (2005) Context logic and tree update. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2005 (POPL) 271\u2013282.","DOI":"10.1145\/1040305.1040328"},{"key":"S0960129509990077_ref47","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.12.114"},{"key":"S0960129509990077_ref5","first-page":"205","article-title":"Characterising the structure of simulations using CCS","volume":"10","author":"Birtwistle","year":"1993","journal-title":"Transactions of the Simulation Society"},{"key":"S0960129509990077_ref24","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0057"},{"key":"S0960129509990077_ref36","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511983382"},{"key":"S0960129509990077_ref35","first-page":"17","article-title":"Structural operational semantics","volume":"60","author":"Plotkin","year":"2004","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"S0960129509990077_ref16","article-title":"An embedding theorem for closed categories. In: Proceedings of the Sydney Category Seminar 1972\/73","volume":"420","author":"Day","year":"1973","journal-title":"Springer-Verlag Lecture Notes in Mathematics"},{"key":"S0960129509990077_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/S0928-4869(00)00030-6"},{"key":"S0960129509990077_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"S0960129509990077_ref14","unstructured":"Dahl O.-J. , Myhrhaug B. and Nygaard K. (1970) Simula 67 Common Base Language. NCC Publication S-52, Norwegian Computing Center, Oslo."},{"key":"S0960129509990077_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0018-z"},{"key":"S0960129509990077_ref13","first-page":"1","article-title":"Static bilog: a unifying language for spatial structures","volume":"80","author":"Conforti","year":"2007","journal-title":"Fundamenta Informaticae"},{"key":"S0960129509990077_ref43","first-page":"163","article-title":"Deriving bisimulation congruences using 2-categories","volume":"10","author":"Sassone","year":"2003","journal-title":"Nordic Journal of Computing"},{"key":"S0960129509990077_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"S0960129509990077_ref42","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"S0960129509990077_ref34","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"S0960129509990077_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90093-3"},{"key":"S0960129509990077_ref25","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19630090502"},{"key":"S0960129509990077_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/S0928-4869(00)00029-X"},{"key":"S0960129509990077_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3550-5"},{"key":"S0960129509990077_ref3","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exm019"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129509990077","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T06:53:18Z","timestamp":1556607198000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129509990077\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,9,4]]},"references-count":49,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2009,10]]}},"alternative-id":["S0960129509990077"],"URL":"https:\/\/doi.org\/10.1017\/s0960129509990077","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,9,4]]}}}