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 |