Event structure semantics of (controlled) reversible CCS
File(s)
Accepted version
Author(s)
Graversen, Eva
Phillips, Iain
Yoshida, Nobuko
Type
Journal Article
Abstract
CCSK is a reversible form of CCS which is causal, meaning that actions can be reversed if and only if each action caused by them has already been reversed; there is no control on whether or when a computation reverses. We propose an event structure semantics for CCSK. For this purpose we define a category of reversible bundle event structures, and use the causal subcategory to model CCSK. We then modify CCSK to control the reversibility with a rollback primitive, which reverses a specific action and all actions caused by it. To define the event structure semantics of rollback, we change our reversible bundle event structures by making the conflict relation asymmetric rather than symmetric, and we exploit their capacity for non-causal reversibility.
Date Issued
2021-06-01
Date Acceptance
2021-04-28
Citation
Journal of Logical and Algebraic Methods in Programming, 2021, 121
ISSN
2352-2208
Publisher
Elsevier
Journal / Book Title
Journal of Logical and Algebraic Methods in Programming
Volume
121
Copyright Statement
© 2021 Elsevier Inc. All rights reserved. This manuscript is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International Licence http://creativecommons.org/licenses/by-nc-nd/4.0/
Sponsor
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Grant Number
EP/V000462/1
EP/V000462/1
ERI 025567 (EP/K034413/1)
EP/K011715/1
EP/N027833/1
EP/T006544/1
EP/T014709/1
Subjects
Science & Technology
Technology
Computer Science, Theory & Methods
Logic
Computer Science
Science & Technology - Other Topics
Reversible computations
CCS
Event structures
Static reversibility
Denotational semantics
Publication Status
Published
Article Number
ARTN 100686
Date Publish Online
2021-05-03