Courtault, J-R;
Galmiche, D;
Pym, D;
(2016)
A logic of separating modalities.
Theoretical Computer Science
, 637
pp. 30-58.
10.1016/j.tcs.2016.04.040.
Preview |
Text
1-s2.0-S030439751630113X-main.pdf - Published Version Download (879kB) | Preview |
Abstract
We present a logic of separating modalities, LSM, that is based on Boolean BI. LSM's modalities, which generalize those of S4, combine, within a quite general relational semantics, BI's resource semantics with modal accessibility. We provide a range of examples illustrating their use for modelling. We give a proof system based on a labelled tableaux calculus with countermodel extraction, establishing its soundness and completeness with respect to the semantics.
| Type: | Article |
|---|---|
| Title: | A logic of separating modalities |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1016/j.tcs.2016.04.040 |
| Publisher version: | http://dx.doi.org/10.1016/j.tcs.2016.04.040 |
| Language: | English |
| Additional information: | © 2016 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: | Science & Technology, Technology, Computer Science, Theory & Methods, Computer Science, Bunched logic, Separation logic, Modal logic, Resource semantics, Tableaux, Concurrency, RESOURCE TABLEAUX, LINEAR LOGIC, PETRI NETS, SEMANTICS, BI |
| 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/1496576 |
Archive Staff Only
 |
View Item |
