{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,9]],"date-time":"2025-12-09T15:44:17Z","timestamp":1765295057873},"reference-count":39,"publisher":"Oxford University Press (OUP)","issue":"8","license":[{"start":{"date-parts":[[2020,1,19]],"date-time":"2020-01-19T00:00:00Z","timestamp":1579392000000},"content-version":"vor","delay-in-days":49,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,12,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a substructural epistemic logic, based on Boolean BI, in which the epistemic modalities are parametrized on agents\u2019 local resources. The new modalities can be seen as generalizations of the usual epistemic modalities. The logic combines Boolean BI\u2019s resource semantics\u2014we introduce BI and its resource semantics at some length\u2014with epistemic agency. We illustrate the use of the logic in systems modelling by discussing some examples about access control, including semaphores, using resource tokens. We also give a labelled tableaux calculus and establish soundness and completeness with respect to the resource semantics.<\/jats:p>","DOI":"10.1093\/logcom\/exz024","type":"journal-article","created":{"date-parts":[[2019,9,5]],"date-time":"2019-09-05T19:27:36Z","timestamp":1567711656000},"page":"1251-1287","source":"Crossref","is-referenced-by-count":4,"title":["A substructural epistemic resource logic: theory and modelling applications"],"prefix":"10.1093","volume":"29","author":[{"given":"Didier","family":"Galmiche","sequence":"first","affiliation":[{"name":"Universit\u00e9 de Lorraine, CNRS, LORIA, 54000, Nancy, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Kimmel","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Lorraine, CNRS, LORIA, 54000, Nancy, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pym","sequence":"additional","affiliation":[{"name":"University College London, London, WC1E 6BT, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2020,1,19]]},"reference":[{"key":"2020021103154254200_ref1","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/j.tcs.2015.11.035","article-title":"A calculus and logic of bunched resources and processes","volume":"614","author":"Anderson","year":"2016","journal-title":"Theoretical Computer Science"},{"key":"2020021103154254200_ref2","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","article-title":"Logic programming with focusing proofs in linear logic","volume":"2","author":"Andreoli","year":"1992","journal-title":"Journal of Logic and Computation"},{"key":"2020021103154254200_ref3","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1093\/logcom\/exm015","article-title":"Epistemic actions as resources","volume":"17","author":"Baltag","year":"2006","journal-title":"Journal of Logic and Computation"},{"key":"2020021103154254200_ref4","first-page":"453","article-title":"Parametric completeness for separation theories","volume-title":"ACM Symposium on Principles of Programming Languages, POPL 41","author":"Brotherston","year":"2014"},{"key":"2020021103154254200_ref5","volume-title":"Crimson Tide","author":"Bruckheimer (Producer)","year":"1995"},{"key":"2020021103154254200_ref6","first-page":"150","article-title":"Causality in linear logic","volume-title":"Proc. FoSSaCS 2019","author":"Castellan","year":"2019"},{"key":"2020021103154254200_ref7","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1016\/S1571-0661(05)80035-0","article-title":"Typed multiset rewriting specifications of security protocols","volume":"40","author":"Cervesato","year":"2001","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2020021103154254200_ref8","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":"2020021103154254200_ref9","volume-title":"A Discipline of Mathematical Systems Modelling","author":"Collinson","year":"2012"},{"key":"2020021103154254200_ref10","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1093\/logcom\/exv020","article-title":"Layered graph logic as an assertion language for access control policy models","volume":"27","author":"Collinson","year":"2017","journal-title":"Journal of Logic and Computation"},{"key":"2020021103154254200_ref11","doi-asserted-by":"crossref","first-page":"953","DOI":"10.1093\/logcom\/exu002","article-title":"A substructural logic for layered graphs","volume":"24","author":"Collinson","year":"2014","journal-title":"Journal of Logic and Computation"},{"key":"2020021103154254200_ref12","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1016\/j.jal.2013.07.005","article-title":"Relational semantics for full linear logic","volume":"12","author":"Coumans","year":"2014","journal-title":"Journal of Applied Logic"},{"key":"2020021103154254200_ref13","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1093\/logcom\/exv031","article-title":"A modal separation logic for resource dynamics","volume":"28","author":"Courtault","year":"2018","journal-title":"Journal of Logic and Computation"},{"key":"2020021103154254200_ref14","first-page":"156","article-title":"An epistemic separation logic","volume-title":"22nd International Workshop on Logic, Language, Information, and Computation, WoLLIC 2015","author":"Courtault","year":"2015"},{"key":"2020021103154254200_ref15","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":"2020021103154254200_ref16","volume-title":"Handbook of Epistemic Logic","author":"van Ditmarsch","year":"2015"},{"key":"2020021103154254200_ref17","first-page":"469","article-title":"Intuitionistic layered graph logic","volume-title":"Proc. IJCAR 2016","author":"Docherty","year":"2016"},{"key":"2020021103154254200_ref18","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.entcs.2018.03.018","article-title":"A stone-type duality theorem for separation logic via its underlying bunched logics","volume":"336","author":"Docherty","year":"2018","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2020021103154254200_ref19","first-page":"27:1","article-title":"A stone-type duality theorem for separation logic via its underlying bunched logics","volume":"15","author":"Docherty","year":"2019","journal-title":"Logical Methods in Computer Science"},{"key":"2020021103154254200_ref20","first-page":"106","article-title":"A substructural epistemic resource logic","volume-title":"Proc. ICLA 2017","author":"Galmiche","year":"2017"},{"key":"2020021103154254200_ref21","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":"2005","journal-title":"Mathematical Structures in Computer Science"},{"key":"2020021103154254200_ref22","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/11863908_19","article-title":"A linear logic of authorization and knowledge","volume-title":"11th European Symposium on Research in Computer Security, ESORICS 2006","author":"Garg","year":"2006"},{"key":"2020021103154254200_ref23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1986","journal-title":"Theoretical Computer Science"},{"key":"2020021103154254200_ref24","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/978-3-540-40981-6_11","article-title":"Modeling adversaries in a logic for security protocol analysis","volume-title":"Formal Aspects of Security, FASec 2002","author":"Halpern","year":"2003"},{"key":"2020021103154254200_ref25","first-page":"14","article-title":"BI as an assertion language for mutable data structures","volume-title":"28th ACM Symposium on Principles of Programming Languages (POPL)","author":"Ishtiaq","year":"2001"},{"key":"2020021103154254200_ref26","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1006\/inco.1994.1036","article-title":"Logic programming in a fragment of intuitionistic linear logic","volume":"110","author":"Hodas","year":"1994","journal-title":"Information and Computation"},{"key":"2020021103154254200_ref27","doi-asserted-by":"crossref","first-page":"605","DOI":"10.1093\/logcom\/exu031","article-title":"The formal strong completeness of partial monoidal Boolean BI","volume":"26","author":"Larchey-Wendling","year":"2014","journal-title":"Journal of Logic and Computation"},{"key":"2020021103154254200_ref28","doi-asserted-by":"crossref","first-page":"269","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":"2020021103154254200_ref29","first-page":"219","article-title":"Budget-constrained knowledge in multiagent systems","volume-title":"Proc. AAMAS 2015","author":"Naumov","year":"2015"},{"key":"2020021103154254200_ref30","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":"The Bulletin of Symbolic Logic"},{"key":"2020021103154254200_ref31","doi-asserted-by":"crossref","first-page":"747","DOI":"10.1017\/S0956796802004495","article-title":"On bunched typing","volume":"13","author":"O\u2019Hearn","year":"2003","journal-title":"Journal of Functional Programming"},{"key":"2020021103154254200_ref32","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","article-title":"Resources, concurrency and local reasoning","volume":"375","author":"O\u2019Hearn","year":"2007","journal-title":"Theoretical Computer Science"},{"key":"2020021103154254200_ref33","first-page":"591","article-title":"Knowledge and security","author":"Pucella"},{"key":"2020021103154254200_ref34","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-0091-7","volume-title":"The Semantics and Proof Theory of the Logic of Bunched Implications","author":"Pym","year":"2002"},{"key":"2020021103154254200_ref35","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1145\/3326938.3326940","article-title":"Resource semantics: logic as a modelling technology","volume":"6","author":"Pym","year":"2019","journal-title":"ACM SIGLOG News"},{"key":"2020021103154254200_ref36","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","journal-title":"Theoretical Computer Science"},{"key":"2020021103154254200_ref37","first-page":"55","article-title":"Separation logic: a logic for shared mutable data structures","volume-title":"IEEE Symposium on Logic in Computer Science, LICS 2002","author":"Reynolds","year":"2002"},{"key":"2020021103154254200_ref38","volume-title":"The Weakest Link","author":"Schneier","year":"2005"},{"key":"2020021103154254200_ref39","article-title":"A spatial-epistemic logic for reasoning about security protocols","volume-title":"8th Int. Workshop on Security Issues in Concurrency, SecCo 2010","author":"Toninho","year":"2010"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/29\/8\/1251\/32376276\/exz024.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/29\/8\/1251\/32376276\/exz024.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,18]],"date-time":"2021-01-18T15:39:00Z","timestamp":1610984340000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/29\/8\/1251\/5709592"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12]]},"references-count":39,"journal-issue":{"issue":"8","published-online":{"date-parts":[[2020,1,19]]},"published-print":{"date-parts":[[2019,12,10]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exz024","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2019,12]]},"published":{"date-parts":[[2019,12]]}}}