UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

A logic of separating modalities

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. Green open access

[img]
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 > Provost and Vice Provost Offices
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
Downloads since deposit
0Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item