Pym, D;
Anderson, G;
(2017)
A substructural modal logic of utility.
Journal of Logic and Computation
, 27
(5)
pp. 1421-1464.
10.1093/logcom/exw030.
Preview |
Text
Pym_exw030.pdf - Published Version Download (524kB) | Preview |
Abstract
We introduce a substructural modal logic of utility that can be used to reason aboutoptimality with respect to properties of states. Our notion of state is quite general, and is able to represent resource allocation problems in distributed systems. The underlying logic is a variant of the modal logic of bunched implications, and based on resource semantics, which is closely related to concurrent separation logic. We consider a labelled transition semantics and establish conditions under which Hennessy—Milner soundness and completeness hold. By considering notions of cost, strategy and utility, we are able to formulate characterizations of Pareto optimality, best responses, and Nash equilibrium within resource semantics. We also show that our logic is able to serve as a logic for a fully featured process algebra and explain the interaction between utility and the structure of processes.
| Type: | Article |
|---|---|
| Title: | A substructural modal logic of utility |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1093/logcom/exw030 |
| Publisher version: | https://academic.oup.com/logcom/article/27/5/1421/... |
| Language: | English |
| Additional information: | Copyright © The Author, 2017. Published by Oxford University Press. This is an Open Access article distributed under the terms of the Creative Commons Attribution License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted reuse, distribution, and reproduction in any medium, provided the original work is properly cited. |
| Keywords: | Substructural logic, bunched logic, modal logic, process algebra, resource semantics, Hennessy—Milner logic utility, Pareto optimality, Nash equilibrium |
| 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/1537287 |
Archive Staff Only
 |
View Item |
