Editing Bunched logic (section)

=== Resources and processes ===

Bunched logic has been used in connection with the (synchronous) resource-process calculus SCRP<ref name=PymTofts2>{{cite journal|last1=Pym|first1=David|last2=Tofts|first2=Chris|title=A Calculus and logic of resources and processes|journal=Formal Aspects of Computing|date=2006|volume=8|issue=4|pages=495–517|doi=10.1007/s00165-006-0018-z|s2cid=16623194|url=http://www0.cs.ucl.ac.uk/staff/D.Pym/pym-tofts-fac-preprint.pdf}}</ref><ref name=":0">{{Cite journal|title = Algebra and Logic for Resource-based Systems Modelling|last1 = Collinson|first1 = Matthew|journal = Mathematical Structures in Computer Science|doi = 10.1017/S0960129509990077|last2 = Pym|first2 = David|year = 2009|volume = 19|issue = 5|pages = 959–1027|citeseerx = 10.1.1.153.3899|s2cid = 14228156}}</ref><ref name=":1">{{Cite book|title = A Discipline of Mathematical Systems Modelling|last1 = Collinson|first1 = Matthew|publisher = College Publications|year = 2012|isbn = 978-1-904987-50-5|location = London|last2 = Monahan|first2 = Brian|last3 = Pym|first3 = David}}</ref> in order to give a (modal) logic that characterizes, in the sense of [[Matthew Hennessy|Hennessy]]–[[Robin Milner|Milner]], the compositional structure of concurrent systems.

SCRP is notable for interpreting <math> A * B </math> in terms of ''both'' parallel composition of systems and composition of their associated resources.
The semantic clause of SCRP's process logic that corresponds to separation logic's rule for concurrency asserts that a formula <math> A * B </math> is true in resource-process state <math> R </math>, <math> E </math> just in case there are decompositions of the resource <math>R = S \bullet T</math> and process 
<math>E</math> ~ <math>F \times G</math>, where ~ denotes [[bisimulation]], such that <math>A</math> is true in the resource-process state <math> S </math>, <math> F </math> and <math>B</math> is true in the resource-process state <math> T </math>, <math> G </math>; that is <math> R, E \models A </math> iff <math> S, F \models A </math> and <math> T, G \models B </math>.

The system SCRP<ref name="PymTofts2" /><ref name=":0" /><ref name=":1" /> is based directly on bunched logic's resource semantics; that is, on ordered monoids of resource elements. While direct and intuitively appealing, this choice leads to a specific technical problem: the Hennessy–Milner completeness theorem holds only for fragments of the modal logic that exclude the multiplicative implication and multiplicative modalities. This problem is solved by basing resource-process calculus on a resource semantics in which resource elements are combined using two combinators, one corresponding to concurrent composition and one corresponding to choice.<ref>{{Cite journal|title = A Calculus and Logic of Bunched Resources and Processes|last1 = Anderson|first1 = Gabrielle|date = 2015|journal = Theoretical Computer Science|volume = 614|pages = 63–96|doi = 10.1016/j.tcs.2015.11.035|last2 = Pym|first2 = David|doi-access = free}}</ref>