Imperial College London
Alternate

DrIainPhillips

Faculty of Engineering, Department of Computing

Senior Lecturer - Computing
 
 
 
//

Contact

 

+44 (0)20 7594 8265i.phillips Website

 
 
//

Location

 

427Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Lanese:2020:10.1007/978-3-030-45231-5_23,
author = {Lanese, I and Phillips, I and Ulidowski, I},
doi = {10.1007/978-3-030-45231-5_23},
pages = {442--461},
publisher = {Springer},
title = {An axiomatic approach to reversible computation},
url = {http://dx.doi.org/10.1007/978-3-030-45231-5_23},
year = {2020}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - Undoing computations of a concurrent system is beneficial inmany situations, e.g., in reversible debugging of multi-threaded programsand in recovery from errors due to optimistic execution in parallel dis-crete event simulation. A number of approaches have been proposed forhow to reverse formal models of concurrent computation including pro-cess calculi such as CCS, languages like Erlang, prime eventstructuresand occurrence nets. However it has not been settled what properties areversible system should enjoy, nor how the various properties that havebeen suggested, such as the parabolic lemma and the causal-consistencyproperty, are related. We contribute to a solution to these issues by usinga generic labelled transition system equipped with a relationcapturingwhether transitions are independent to explore the implications betweenthese properties. In particular, we show how they are derivable from aset of axioms. Our intention is that when establishing properties of someformalism it will be easier to verify the axioms rather than proving prop-erties such as the parabolic lemma directly. We also introduce two newnotions related to causal consistent reversibility, namely causal safetyand causal liveness, and show that they are derivable from our axioms.
AU  - Lanese,I
AU  - Phillips,I
AU  - Ulidowski,I
DO  - 10.1007/978-3-030-45231-5_23
EP  - 461
PB  - Springer
PY  - 2020///
SP  - 442
TI  - An axiomatic approach to reversible computation
UR  - http://dx.doi.org/10.1007/978-3-030-45231-5_23
UR  - https://link.springer.com/chapter/10.1007%2F978-3-030-45231-5_23
UR  - http://hdl.handle.net/10044/1/77569
ER  -
Download