{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T06:51:20Z","timestamp":1767163880370,"version":"build-2238731810"},"reference-count":30,"publisher":"Oxford University Press (OUP)","issue":"5","license":[{"start":{"date-parts":[[2020,3,3]],"date-time":"2020-03-03T00:00:00Z","timestamp":1583193600000},"content-version":"vor","delay-in-days":1120,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,7,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We introduce a substructural modal logic of utility that can be used to reason aboutoptimality with respect to properties of states. Our notion of state is quite general, and is able to represent resource allocation problems in distributed systems. The underlying logic is a variant of the modal logic of bunched implications, and based on resource semantics, which is closely related to concurrent separation logic. We consider a labelled transition semantics and establish conditions under which Hennessy\u2014Milner soundness and completeness hold. By considering notions of cost, strategy and utility, we are able to formulate characterizations of Pareto optimality, best responses, and Nash equilibrium within resource semantics. We also show that our logic is able to serve as a logic for a fully featured process algebra and explain the interaction between utility and the structure of processes.<\/jats:p>","DOI":"10.1093\/logcom\/exw030","type":"journal-article","created":{"date-parts":[[2016,12,2]],"date-time":"2016-12-02T07:05:39Z","timestamp":1480662339000},"page":"1421-1464","source":"Crossref","is-referenced-by-count":4,"title":["A Substructural Modal Logic of Utility"],"prefix":"10.1093","volume":"27","author":[{"given":"Gabrielle","family":"Anderson","sequence":"first","affiliation":[{"name":"University College London, Department of Computer Science, London WC1E 6BT, UK."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pym","sequence":"first","affiliation":[{"name":"University College London, Department of Computer Science, London WC1E 6BT, UK."}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2017,2,7]]},"reference":[{"key":"2020030308581582000_B1","article-title":"Hennessy-Milner completeness in transition systems with synchronous concurrent composition","author":"Anderson","journal-title":"Technical report, RN\/15\/05, University College London, 2015"},{"key":"2020030308581582000_B2","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/j.tcs.2015.11.035","article-title":"A calculus and logic of bunched resource processes","volume":"614","author":"Anderson","year":"2016","journal-title":"Theoretical Computer Science"},{"key":"2020030308581582000_B3","first-page":"118","article-title":"Decision support for systems security investment","author":"Beres","year":"2010","journal-title":"Proceedings of the 5th Workshops on Network Operations and Management Symposium"},{"key":"2020030308581582000_B4","first-page":"118","article-title":"Decision support for systems security investment","author":"Beresnevichiene","year":"2010","journal-title":"Network Operations and Management Symposium Workshops"},{"key":"2020030308581582000_B5","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1109\/MSP.2015.97","article-title":"Improving security policy decisions with models","volume":"13","author":"Caulfield","year":"2015","journal-title":"IEEE Security and Privacy"},{"key":"2020030308581582000_B6","first-page":"9","article-title":"Modelling and simulating systems security policy","volume-title":"Proceedings of the 8th Conference on Simulation Tools and Techniques","author":"Caulfield","year":"2015"},{"key":"2020030308581582000_B7","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/978-3-319-07620-1_21","article-title":"Compositional security modelling: structure, economics, and behaviour","volume":"8533","author":"Caulfield","year":"2014","journal-title":"Lecture Notes in Computer Science"},{"key":"2020030308581582000_B8","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511621192","volume-title":"Modal Logic: An Introduction","author":"Chellas.","year":"1980"},{"key":"2020030308581582000_B9","doi-asserted-by":"crossref","first-page":"1207","DOI":"10.1093\/logcom\/exp021","article-title":"A logical and computational theory of located resource","volume":"19","author":"Collinson","year":"2009","journal-title":"Journal of Logic and Computation"},{"issue":"10","key":"2020030308581582000_B10","first-page":"1","article-title":"Semantics for structured systems modelling and simulation","volume":"34","author":"Collinson","year":"2010","journal-title":"Proceedings of the 3rd Conference on Simulation Tools and Techniques"},{"key":"2020030308581582000_B11","volume-title":"A Discipline of Mathematical Systems Modelling","author":"Collinson","year":"2012"},{"key":"2020030308581582000_B12","doi-asserted-by":"crossref","first-page":"959","DOI":"10.1017\/S0960129509990077","article-title":"Algebra and logic for resource-based systems modelling","volume":"19","author":"Collinson","year":"2009","journal-title":"Mathematical Structures in Computer Science"},{"key":"2020030308581582000_B13","author":"Coulouris","year":"2000","journal-title":"Distributed systems: concepts and design"},{"key":"2020030308581582000_B14","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1016\/j.tcs.2016.04.040","article-title":"A logic of separating modalities","volume":"637","author":"Courtault","year":"2016","journal-title":"Theoretical Computer Science"},{"key":"2020030308581582000_B15","doi-asserted-by":"crossref","first-page":"2537","DOI":"10.1016\/j.scico.2013.02.009","article-title":"Compositional reasoning for weighted markov decision processes","volume":"78","author":"Deng","year":"2013","journal-title":"Science of Computer Programming"},{"key":"2020030308581582000_B16","doi-asserted-by":"crossref","first-page":"1033","DOI":"10.1017\/S0960129505004858","article-title":"The semantics of BI and resource tableaux","volume":"15","author":"Galmiche","year":"2015","journal-title":"Mathematical Structures in Computer Science"},{"key":"2020030308581582000_B17","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/3-540-10003-2_79","article-title":"On observing nondeterminism and concurrency","volume":"Vol. 85","author":"Hennessy","year":"1980","journal-title":"Lecture Notes in Computer Science"},{"key":"2020030308581582000_B18","first-page":"14","article-title":"BI as an assertion language for mutable data structures","volume-title":"Proceedings of the 28th Symposium on Principles of Programming Languages","author":"Ishtiaq","year":"2001"},{"key":"2020030308581582000_B19","first-page":"697","article-title":"A temporal logic for markov chains","volume-title":"Proceedings of the 7th Conference on Autonomous Agents and Multiagent Systems","author":"Jamroga.","year":"2008"},{"key":"2020030308581582000_B20","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/978-3-642-37036-6_4","article-title":"Language constructs for non-well-founded computation","volume":"Vol. 7792","author":"Jeannin","year":"2013","journal-title":"Lecture Notes in Computer Science"},{"key":"2020030308581582000_B21","article-title":"Towards a science of risk analysis","author":"Hewlett-Packard Laboratories"},{"key":"2020030308581582000_B22","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1017\/S0960129509007567","article-title":"Exploring the relation between intuitionistic BI and Boolean BI: an unexpected embedding","volume":"19","author":"Larchey-Wendling","year":"2009","journal-title":"Mathematical Structures in Computer Science"},{"key":"2020030308581582000_B23","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","article-title":"Calculi for synchrony and asynchrony","volume":"25","author":"Milner.","year":"1983","journal-title":"Theoretical Computer Science"},{"key":"2020030308581582000_B24","author":"Milner.","year":"1989","journal-title":"Communication and Concurrency"},{"key":"2020030308581582000_B25","doi-asserted-by":"crossref","first-page":"215","DOI":"10.2307\/421090","article-title":"The logic of bunched implications","volume":"5","author":"O\u2019Hearn","year":"1999","journal-title":"Bulletin of Symbolic Logic"},{"key":"2020030308581582000_B26","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/j.tcs.2003.11.020","article-title":"Possible worlds and resources: the semantics of BI","volume":"315","author":"Pym","year":"2003","journal-title":"Theoretical Computer Science"},{"key":"2020030308581582000_B27","author":"Read.","year":"1989","journal-title":"Relevant Logic: A Philosophical Examination of Inference"},{"key":"2020030308581582000_B28","first-page":"55","article-title":"Separation logic: A logic for shared mutable data structures","author":"Reynolds.","year":"2002","journal-title":"Proceedings of the 17th Conference on Logic in Computer Science"},{"key":"2020030308581582000_B29","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511811654","volume-title":"Multiagent Systems: Algorithmic, Game-Theoretic, and Logical Foundations","author":"Shoham","year":"2008"},{"key":"2020030308581582000_B30","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-24611-4_1","article-title":"Probabilistic automata: system types, parallel composition and comparison","volume":"Vol. 2925","author":"Sokolova","year":"2004","journal-title":"Lecture Notes in Computer Science"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/27\/5\/1421\/32761612\/exw030.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/27\/5\/1421\/32761612\/exw030.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,3]],"date-time":"2020-03-03T08:58:30Z","timestamp":1583225910000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/27\/5\/1421\/5775560"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,7]]},"references-count":30,"aliases":["10.1093\/logcom\/exw032"],"journal-issue":{"issue":"5","published-online":{"date-parts":[[2017,2,7]]},"published-print":{"date-parts":[[2017,7,1]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exw030","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2017,7]]},"published":{"date-parts":[[2017,2,7]]}}}