Anderson, G;
Pym, D;
(2016)
A calculus and logic of bunched resources and processes.
Theoretical Computer Science
, 614
pp. 63-96.
10.1016/j.tcs.2015.11.035.
Preview |
Text
1-s2.0-S0304397515011214-main.pdf - Published Version Download (878kB) | Preview |
Abstract
Mathematical modelling and simulation modelling are fundamental tools of engineering, science, and social sciences such as economics, and provide decision-support tools in management. Mathematical models are essentially deployed at all scales, all levels of complexity, and all levels of abstraction. Models are often required to be executable, as a simulation, on a computer. We present some contributions to the process-theoretic and logical foundations of discrete-event modelling with resources and processes. Building on previous work in resource semantics, process calculus, and modal logic, we describe a process calculus with an explicit representation of resources in which processes and resources co-evolve. The calculus is closely connected to a substructural modal logic that may be used as a specification language for properties of models. In contrast to earlier work, we formulate the resource semantics, and its relationship with process calculus, in such a way that we obtain soundness and completeness of bisimulation with respect to logical equivalence for the naturally full range of logical connectives and modalities. We give a range of examples of the use of the process combinators and logical structure to describe system structure and behaviour.
Type: | Article |
---|---|
Title: | A calculus and logic of bunched resources and processes |
Open access status: | An open access version is available from UCL Discovery |
DOI: | 10.1016/j.tcs.2015.11.035 |
Publisher version: | http://dx.doi.org/10.1016/j.tcs.2015.11.035 |
Language: | English |
Additional information: | ©2015 The Authors. Published by Elsevier B.V. This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/). |
Keywords: | Modal logic, Process algebra, Bunched logic, Resource semantics |
UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
URI: | https://discovery.ucl.ac.uk/id/eprint/1476675 |
Archive Staff Only
View Item |