{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:30Z","timestamp":1761611190366},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2006,12,1]],"date-time":"2006-12-01T00:00:00Z","timestamp":1164931200000},"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":[[2006,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Recent advances in logics for reasoning about resources provide a new approach to compositional reasoning in interacting systems. We present a calculus of resources and processes, based on a development of Milner\u2019s synchronous calculus of communication systems, SCCS, that uses an explicit model of resource. Our calculus models the co-evolution of resources and processes with synchronization constrained by the availability of resources. We provide a logical characterization, analogous to Hennessy\u2013Milner logic\u2019s characterization of bisimulation in CCS, of bisimulation between resource processes which is compositional in the concurrent and local structure of systems.<\/jats:p>","DOI":"10.1007\/s00165-006-0018-z","type":"journal-article","created":{"date-parts":[[2006,10,27]],"date-time":"2006-10-27T08:01:11Z","timestamp":1161936071000},"page":"495-517","source":"Crossref","is-referenced-by-count":29,"title":["A Calculus and logic of resources and processes"],"prefix":"10.1145","volume":"18","author":[{"given":"David","family":"Pym","sequence":"first","affiliation":[{"name":"Hewlett-Packard Laboratories, Filton Road, Stoke Gifford, BS34 8QZ, Bristol, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chris","family":"Tofts","sequence":"additional","affiliation":[{"name":"Hewlett-Packard Laboratories, Filton Road, Stoke Gifford, BS34 8QZ, Bristol, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00229-0"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/361454.361473"},{"key":"e_1_2_1_2_3_2","volume-title":"Operating system principles","author":"Brinch Hansen P","year":"1973"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3472-0","volume-title":"The origin of concurrent programming","author":"Brinch Hansen P","year":"2002"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Birtwistle G (1979) Demos\u2014discrete event modelling on Simula. Macmillan","DOI":"10.1007\/978-1-4899-6685-8"},{"key":"e_1_2_1_2_6_2","unstructured":"Birtwistle G (1981) Demos implementation guide and reference manual. Technical Report 81\/70\/22 University of Calgary"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Bergstra JA Klop JW (1984) The algebra of recursively defined processes and the algebra of regular processes. In: Proceedings of 11th ICALP LNCS 172","DOI":"10.1007\/3-540-13345-3_7"},{"issue":"4","key":"e_1_2_1_2_8_2","first-page":"299","article-title":"An operational semantics of process-orientated simulation languages: part I \u03c0Demos","volume":"10","author":"Birtwistle G","year":"1993","journal-title":"Trans Soc Comput Simul"},{"issue":"4","key":"e_1_2_1_2_9_2","first-page":"303","article-title":"An operational semantics of process-orientated simulation languages: part II\u00a0\u03bcDemos","volume":"11","author":"Birtwistle G","year":"1994","journal-title":"Trans Soc Comput Simul"},{"issue":"3","key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1145\/290274.290303","article-title":"A denotational semantics for a process-based simulation language","volume":"8","author":"Birtwistle G","year":"1998","journal-title":"ACM ToMaCS"},{"key":"e_1_2_1_2_11_2","first-page":"281","article-title":"Getting demos models right\u2014part I practice","volume":"3","author":"Birtwistle G","year":"2000","journal-title":"Simul Practice Theor"},{"key":"e_1_2_1_2_12_2","first-page":"281","article-title":"Getting demos models right\u2014part II ... and theory","volume":"3","author":"Birtwistle G","year":"2000","journal-title":"Simul Practice Theor"},{"issue":"2","key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/S0890-5401(03)00137-8","article-title":"A spatial logic of concurrency (part i)","volume":"186","author":"Cardelli L","year":"2003","journal-title":"Inf Comput"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Clementson AT (1965) Extended control and simulation language. Comput J 9(3)","DOI":"10.1093\/comjnl\/9.3.215"},{"key":"e_1_2_1_2_15_2","unstructured":"Dam MF (1990) Relevance logic and concurrent computation. Ph.D. thesis University of Edinburgh"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Dijkstra EW (1968) Cooperating sequential processes. In: Progamming L Academic Press Reprinted in [BH02] pp 43\u2013112 New York","DOI":"10.1007\/978-1-4757-3472-0_2"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289519"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/978-94-009-5203-4_3","volume-title":"Handbook of philosophical logic, vol III: alternatives to classical logic. number 166 in Synthese Library","author":"Dunn JM","year":"1986"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Girard J-Y (1987) Linear logic. Theoret Comput Sci pp. 1\u2013102","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503003943"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Galmiche D M\u00e9ry D Pym D (2002) Resource Tableaux. In: Proceedings of CSL 2002. vol 2471 of LNCS pp 183\u2013199","DOI":"10.1007\/3-540-45793-3_13"},{"key":"e_1_2_1_2_22_2","volume-title":"Semantics of programming languages: structures and techniques","author":"Gunter CA","year":"1992"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1972) Towards a theory of parallel programming. In: Hoare Perrot (eds) Operating systems techniques. Academic Press New York Reprinted in [BH02]","DOI":"10.1007\/978-1-4757-3472-0_6"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/355620.361161"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Ishtiaq SS O\u2019Hearn P (2001) BI as an assertion language for mutable data structures. In: 28th ACM-SIGPLAN symposium on principles of programming languages London pp 14\u201326 Association for Computing Machinery","DOI":"10.1145\/373243.375719"},{"key":"e_1_2_1_2_27_2","first-page":"83","article-title":"Semantical considerations on modal logic","volume":"16","author":"Kripke SA","year":"1963","journal-title":"Acta Philosophica Fennica"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Kripke SA (1965) Semantical analysis of intuitionistic logic I. In: Crossley JN Dummett MAE (eds) Formal systems and recursive functions North-Holland Amsterdam pp 92\u2013130","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"e_1_2_1_2_29_2","first-page":"279","article-title":"Trace theory","volume":"255","author":"Mazurkiewicz A","year":"1987","journal-title":"Lecture Notes Comput Sci"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90114-7"},{"key":"e_1_2_1_2_31_2","volume-title":"Communication and concurrency","author":"Milner R","year":"1989"},{"key":"e_1_2_1_2_32_2","volume-title":"Communication systems and the \u03c0-calculus","author":"Milner R","year":"1999"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn P (2004) Resources concurrency and local reasoning. In: Proceedings of Concur 04 London LNCS. Springer Berlin Heidelberg New York","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Pym DJ O\u2019Hearn PW Yang H (2004) Possible worlds and resources: the semantics of BI . Theoret Comput Sci 315(1):257\u2013305. Erratum: p. 285 l. \u221212: \u201c for some  \u201d should be \u201c\u201d","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Pym DJ (2002) The semantics and proof theory of the logic of the logic of bunched implications vol 26 of Applied Logic Series. Kluwer Dordrecht. Errata and Remarks [Pym04] maintained at: http:\/\/www.cs.bath.ac.uk\/~pym\/BI-monograph-errata.pdf","DOI":"10.1007\/978-94-017-0091-7"},{"key":"e_1_2_1_2_38_2","unstructured":"Pym DJ (2004) Errata and remarks for The semantics and proof theory of the logic of bunched implications implications [Pym02] . Maintained at:http:\/\/www.cs.bath.ac.uk\/~pym\/BI-monograph-errata.pdf"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS \u201902 IEEE Computer Society Press pp 55\u201374","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00649991"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.5555\/500817"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211867"},{"key":"e_1_2_1_2_43_2","volume-title":"Efficiently modelling resource in a process algebra","author":"Tofts C","year":"2003"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-006-0018-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-006-0018-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-006-0018-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:44:02Z","timestamp":1641483842000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-006-0018-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,12]]},"references-count":43,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,12]]}},"alternative-id":["10.1007\/s00165-006-0018-z"],"URL":"https:\/\/doi.org\/10.1007\/s00165-006-0018-z","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,12]]}}}