Imperial College London

DrIainPhillips

Faculty of EngineeringDepartment of Computing

Senior Lecturer - Computing
 
 
 
//

Contact

 

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

 
 
//

Location

 

427Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Publication Type
Year
to

67 results found

Lanese I, Phillips I, Ulidowski I, 2024, An axiomatic theory for reversible computation, ACM Transactions on Computational Logic, ISSN: 1529-3785

Undoing computations of a concurrent system is beneficial in many situations, e.g., in reversible debugging of multi-threaded programs and in recovery from errors due to optimistic execution in parallel discrete event simulation. A number of approaches have been proposed for how to reverse formal models of concurrent computation including process calculi such as CCS, languages like Erlang, and abstract models such as prime event structures and occurrence nets. However it has not been settled what properties a reversible system should enjoy, nor how the various properties that have been suggested, such as the parabolic lemma and the causal-consistency property, are related. We contribute to a solution to these issues by using a generic labelled transition system equipped with a relation capturing whether transitions are independent to explore the implications between various reversibility properties. In particular, we show how all properties we consider are derivable from a set of axioms. Our intention is that when establishing properties of some formalism it will be easier to verify the axioms rather than proving properties such as the parabolic lemma directly. We also introduce two new properties related to causal consistent reversibility, namely causal liveness and causal safety, stating, respectively, that an action can be undone if (causal liveness) and only if (causal safety) it is independent from all the following actions. These properties come in three flavours: defined in terms of independent transitions, independent events, or via an ordering on events. Both causal liveness and causal safety are derivable from our axioms.

Journal article

Glück R, Lanese I, Mezzina CA, Miszczak JA, Phillips I, Ulidowski I, Vidal Get al., 2023, Towards a taxonomy for reversible computation approaches, 15th International Conference on Reversible Computation (RC), Publisher: Springer, Pages: 24-39

Reversible computation is a paradigm allowing computationto proceed not only in the usual, forward direction, but also backwards. Reversible computation has been studied in a variety of models, including sequential and concurrent programming languages, automata, process calculi, Turing machines, circuits, Petri nets, event structures, termrewriting, quantum computing, and others. Also, it has found applications in areas as different as low-power computing, debugging, simulation, robotics, database design, and biochemical modeling. Thus, while the broad idea of reversible computation is the same in all the areas, ithas been interpreted and adapted to fit the various settings. The existing notions of reversible computation however have never been compared and categorized in detail. This work aims at being a first stepping stone towards a taxonomy of the approaches that co-exist under the term re-versible computation. We hope that such a work will shed light on the relation among the various approaches.

Conference paper

Graversen E, Phillips I, Yoshida N, 2022, Event structures for the reversible early internal π-calculus, Journal of Logical and Algebraic Methods in Programming, Vol: 124, Pages: 1-46, ISSN: 2352-2208

The 휋-calculus is a widely used process calculus, which models communications between processes and allows the passing of communication links. Various operationalsemantics of the 휋-calculus have been proposed, which can be classified according towhether transitions are unlabelled (so-called reductions) or labelled. With labelled transitions, we can distinguish early and late semantics. The early version allows a processto receive names it already knows from the environment, while the late semantics andreduction semantics do not. All existing reversible versions of the 휋-calculus use reduction or late semantics, despite the early semantics of the (forward-only) 휋-calculusbeing more widely used than the late. We introduce two reversible forms of the internal 휋-calculus; these are the first to use early semantics. The internal 휋-calculus is asubset of the 휋-calculus where every link sent by an output is private, yielding greatersymmetry between inputs and outputs. One of the new reversible calculi uses staticreversibility, where performing an action does not change the structure of the process,and the other uses dynamic reversibility, where performing an action moves it to a separate history. We show an operational correspondence between the two calculi. Forthe static calculus we define denotational event structure semantics, which generate anevent structure inductively on the structure on the process. For the dynamic calculus wedefine operational event structure semantics, which generate an event structure basedon a labelled asynchronous transition system. We describe a correspondence betweenthe resulting event structures.

Journal article

Medic D, Mezzina CA, Phillips I, Yoshida Net al., 2021, Towards a formal account for software transactional memory, Twelfth International Conference on Reversible Computation, Publisher: Springer Verlag, Pages: 255-263, ISSN: 0302-9743

Software transactional memory (STM) is a concurrency con-trol mechanism for shared memory systems. It is opposite to the lockbased mechanism, as it allows multiple processes to access the same setof variables in a concurrent way. Then according to the used policy, theeffect of accessing to shared variables can be committed (hence, madepermanent) or undone. In this paper, we define a formal framework fordescribing STMs and show how with a minor variation of the rules it ispossible to model two common policies for STM: reader preference andwriter preference.

Conference paper

Lanese I, Phillips I, 2021, Forward-reverse observational equivalences in CCSK, 13th International Conference on Reversible Computation 2021, Publisher: Springer Verlag, Pages: 126-143, ISSN: 0302-9743

In the context of CCSK, a reversible extension of CCS, we study observational equivalences that distinguish forward moves from backward ones. We present a refinement of the notion of forward-reverse bisimilarity and show that it coincides with a notion of forward-reverse barbed congruence. We also show a set of sound axioms allowing one to reason equationally on process equivalences.

Conference paper

Graversen E, Phillips I, Yoshida N, 2021, Event structure semantics of (controlled) reversible CCS, Journal of Logical and Algebraic Methods in Programming, Vol: 121, ISSN: 2352-2208

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.

Journal article

Medic D, Mezzina CA, Phillips I, Yoshida Net al., 2020, A parametric framework for reversible pi-calculi, Information and Computation, Vol: 275, ISSN: 0890-5401

This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality inπ-calculus, which differ in the treatment of parallel extrusions of the same name. Hence, by using a parametric way of bookkeeping the order and the dependencies among extruders it is possible to map different causal semantics into the same framework. Starting from this simple observation, we present a uniform framework forreversibleπ-calculi that is parametric with respect to a data structure that stores information about the extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We prove causal-consistency for the three instances of our framework. Furthermore, we prove a causal correspondence between the appropriate instances of the framework and the Boreale-Sangiorgi semantics and an operational correspondence with the reversibleπ-calculus causal semantics.

Journal article

Graversen E, Phillips I, Yoshida N, 2020, Event structures for the reversible early internal pi-calculus, Twelfth International Conference on Reversible Computation, Publisher: Springer Verlag, Pages: 71-90, ISSN: 0302-9743

The pi-calculus is a widely used process calculus, which models com-munications between processes and allows the passing of communication links.Various operational semantics of the pi-calculus have been proposed, which canbe classified according to whether transitions are unlabelled (so-called reductions)or labelled. With labelled transitions, we can distinguish early and late semantics.The early version allows a process to receive names it already knows from the en-vironment, while the late semantics and reduction semantics do not. All existingreversible versions of the pi-calculus use reduction or late semantics, despite theearly semantics of the (forward-only) pi-calculus being more widely used than thelate. We define piIH, the first reversible early pi-calculus, and give it a denotationalsemantics in terms of reversible bundle event structures. The new calculus is a re-versible form of the internal pi-calculus, which is a subset of the pi-calculus whereevery link sent by an output is private, yielding greater symmetry between inputsand outputs.

Conference paper

Melgratti H, Mezzina CA, Phillips I, Pinna GM, Ulidowski Iet al., 2020, Reversible occurrence nets and causal reversible prime event structures, Twelfth International Conference on Reversible Computation, Publisher: Springer Verlag, Pages: 35-53, ISSN: 0302-9743

One of the well-known results in concurrency theory con-cerns the relationship between event structures and occurrence nets: anoccurrence net can be associated with a prime event structure, and viceversa. More generally, the relationships between various forms of eventstructures and suitable forms of nets have been long established. Goodexamples are the close relationship between inhibitor event structuresand inhibitor occurrence nets, or between asymmetric event structuresand asymmetric occurrence nets. Several forms of event structures suitedfor the modelling of reversible computation have recently been developed;also a method for reversing occurrence nets has been proposed. This pa-per bridges the gap between reversible event structures and reversiblenets. We introduce the notion of reversible occurrence net, which is ageneralisation of the notion of reversible unfolding. We show that re-versible occurrence nets correspond precisely to a subclass of reversibleprime event structures, the causal reversible prime event structures.

Conference paper

Aman B, Ciobanu G, Glück R, Kaarsgaard R, Kari J, Kutrib M, Lanese I, Mezzina CA, Mikulski Ł, Nagarajan R, Phillips I, Pinna GM, Prigioniero L, Ulidowski I, Vidal Get al., 2020, Foundations of reversible computation, Reversible Computation: Extending Horizons of Computing, Editors: Ulidowski, Lanese, Schultz, Ferreira, Publisher: Springer Verlag, Pages: 1-40

Reversible computation allows computation to proceed not only in the standard, forward direction, but also backward, recovering past states. While reversible computation has attracted interest for its multiple applications, covering areas as different as low-power computing, simulation, robotics and debugging, such applications need to be supported by a clear understanding of the foundations of reversible computation. We report below on many threads of research in the area of foundations of reversible computing, giving particular emphasis to the results obtained in the framework of the European COST Action IC1405, entitled “Reversible Computation - Extending Horizons of Computing”, which took place in the years 2015–2019.

Book chapter

Lanese I, Phillips I, Ulidowski I, 2020, An axiomatic approach to reversible computation, 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2020), Publisher: Springer, Pages: 442-461

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.

Conference paper

Graversen E, Phillips I, Yoshida N, 2019, Towards a categorical representation of reversible event structures, Journal of Logical and Algebraic Methods in Programming, Vol: 104, Pages: 16-59, ISSN: 2352-2208

We study categories for reversible computing, focussing on reversible forms of event structures. Event structures are a well-established model of true concurrency. There exist a number of forms of event structures, including prime event structures, asymmetric event structures, and general event structures. More recently, reversible forms of these types of event structure have been defined. We formulate corresponding categories and functors between them. We show that products and coproducts exist in many cases.We define stable reversible general event structures and stable configuration systems, and we obtain an isomorphism between the subcategory of the former in normal form and the finitely enabled subcategory of the latter. In most work on reversible computing, including reversible process calculi, a causality condition is posited, meaning that the cause of an event may not be reversed before the event itself. Since reversible event structures are not assumed to be causal in general, we also define causal subcategories of these event structures.Keywords: reversible computation, reversible event structures, category theory

Journal article

Jäschke R, Weidlich M, 2019, Preface

Book chapter

Medic D, Mezzina CA, Phillips I, Yoshida Net al., 2018, A parametric framework for reversible π-calculi, Express/SOS 2018, Publisher: Open Publishing Association, Pages: 87-103, ISSN: 2075-2180

This paper presents a study of causality in a reversible, concurrent setting. There exist various notions of causality in pi-calculus, which differ in the treatment of parallel extrusions of the same name. In this paper we present a uniform framework for reversible pi-calculi that is parametric with respect to a data structure that stores information about an extrusion of a name. Different data structures yield different approaches to the parallel extrusion problem. We map three well-known causal semantics into our framework. We show that the (parametric) reversibility induced by our framework is causally-consistent and prove a causal correspondence between an appropriate instance of the framework and Boreale and Sangiorgi's causal semantics.

Conference paper

Graversen E, Phillips I, Yoshida N, 2018, Event structure semantics of (controlled) reversible CCS, 10th International Conference on Reversible Computation, Publisher: Springer Verlag, ISSN: 0302-9743

CCSK is a reversible form of CCS which is causal, meaning that ac-tions can be reversed if and only if each action caused by them has already beenreversed; there is no control on whether or when a computation reverses. We pro-pose an event structure semantics for CCSK. For this purpose we define a cat-egory of reversible bundle event structures, and use the causal subcategory tomodel CCSK. We then modify CCSK to control the reversibility with a rollbackprimitive, which reverses a specific action and all actions caused by it. To definethe event structure semantics of rollback, we change our reversible bundle eventstructures by making the conflict relation asymmetric rather than symmetric, andwe exploit their capacity for non-causal reversibility.

Conference paper

Ulidowski I, Phillips ICC, Yuen S, 2018, Reversing event structures, New Generation Computing, Vol: 36, Pages: 281-306, ISSN: 0288-3635

Reversible computation has attracted increasing interest in recent years. In this paper, we show how to model reversibility in concurrent computation as realised abstractly in terms of event structures. Two different forms of event structures are considered, namely event structures defined by causation and prevention relations and event structures given by an enabling relation with prevention. We then show how to reverse the two kinds of event structures, and discuss causal as well as out-of-causal order reversibility.

Journal article

Graversen E, Phillips ICC, Yoshida N, 2017, Towards a categorical representation of reversible event structures, 10th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES 2017), Publisher: Open Publishing Association, Pages: 49-60, ISSN: 2075-2180

We study categories for reversible computing, focussing on reversible forms of event structures.Event structures are a well-established model of true concurrency. There exist a number of formsof event structures, including prime event structures, asymmetric event structures, and general eventstructures. More recently, reversible forms of these types of event structures have been defined.We formulate corresponding categories and functors between them. We show that products and co-products exist in many cases. In most work on reversible computing, including reversible processcalculi, a cause-respecting condition is posited, meaning that the cause of an event may not be re-versed before the event itself. Since reversible event structures are not assumed to be cause-respectingin general, we also define cause-respecting subcategories of these event structures. Our longer-termaim is to formulate event structure semantics for reversible process calculi.

Conference paper

Phillips I, Rahaman H, 2017, Preface, ISBN: 9783319599359

Book

Phillips ICC, Ulidowski I, 2015, Reversibility and asymmetric conflict in event structures, Journal of Logical and Algebraic Methods in Programming, Vol: 84, Pages: 781-805, ISSN: 2352-2208

Reversible computation has attracted increasing interest in recent years, withapplications in hardware, software and biochemistry. We introducereversibleforms of prime event structures and asymmetric event structures. In order tocontrol the manner in which events are reversed, we use asymmetric conflicton events. We prove a number of results about reachable configurations; forinstance, we show under what conditions reachable configurationswhich arefinite are reachable by purely finite means. We discuss, with examples, reversingin causal order, where an event is only reversed once all events it caused havebeen reversed, as well as forms of non-causal reversi

Journal article

Pesu T, Phillips ICC, 2015, Real-time Methods in Reversible Computation, 7th International Conference on Reversible Computation, Publisher: Springer, Pages: 45-59

Bennett has shown how to simulate arbitrary forwards-only computations by fully reversible computation. In particular he has given a space-efficient linear time simulation. After describing a different linear-time reversible simulation with improved space efficiency, we initiate the study of real-time simulations. In addition to being linear-time, these must offer continuous progress, meaning that the delay between successive forward events must be bounded by a constant.

Conference paper

Ulidowski I, Phillips I, Yuen S, 2014, Concurrency and Reversibility, REVERSIBLE COMPUTATION, RC 2014, Vol: 8507, Pages: 1-14, ISSN: 0302-9743

Journal article

Phillips ICC, Ulidowski I, 2013, Event Identifier Logic, Mathematical Structures in Computer Science, Vol: n/a, Pages: 1-51, ISSN: 1469-8072

Journal article

Phillips I, Ulidowski I, Yuen S, 2013, Modelling of bonding with processes and events, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 7948 LNCS, Pages: 141-154, ISSN: 0302-9743

We introduce two forms of modelling of systems that consist of objects that are combined together by the means of bonds. In reaction systems for bonding we define how bonds are created and dissolved via reduction-style semantics. The usefulness of reaction systems is illustrated with examples taken from software engineering and biochemistry. We also introduce reversible event structures and define the notion of configuration. We then discuss how to give semantics of reaction systems for bonding in terms of reversible event structures. © 2013 Springer-Verlag Berlin Heidelberg.

Journal article

Phillips I, Ulidowski I, Yuen S, 2013, A reversible process calculus and the modelling of the ERK signalling pathway, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 7581 LNCS, Pages: 218-232, ISSN: 0302-9743

We introduce a reversible process calculus with a new feature of execution control that allows us to change the direction and pattern of computation. This feature allows us to model a variety of modes of reverse computation, ranging from strict backtracking to reversing which respects causal ordering of events, and even reversing which violates causal ordering. The SOS rules that define the operators of the new calculus employ communication keys to handle communication correctly and key identifiers to control execution. As an application of our calculus, we model the ERK signalling pathway which delivers mitogenic and differentiation signals from the membrane of a cell to its nucleus. The proteins participating in the pathway are represented by reversible processes in such a way that the pathway's bio-chemical reactions are simply interactions between the processes. © 2013 Springer-Verlag Berlin Heidelberg.

Journal article

Phillips ICC, Ulidowski I, Yuen S, 2013, A Reversible Process Calculus and the Modelling of the ERK Signalling Pathway, Fourth International Workshop on Reversible Computation, Pages: 218-232, ISSN: 0302-9743

Conference paper

Phillips ICC, Ulidowski I, Yuen S, 2013, Modelling of Bonding with Processes and Events, 5th International Conference on Reversible Computation, Publisher: Springer, Pages: 141-154

We introduce two forms of modelling of systems that consist of objects that are combined together by the means of bonds. In reaction systems for bonding we define how bonds are created and dissolved via reduction-style semantics. The usefulness of reaction systems is illustrated with examples taken from software engineering and biochemistry. We also introduce reversible event structures and define the notion ofconfiguration. We then discuss how to give semantics of reaction systems for bonding in terms of reversible event structures.

Conference paper

Phillips ICC, Ulidowski I, 2013, Reversibility and Asymmetric Conflict in Event Structures, CONCUR 2013, 24th International Conference on Concurrency Theory, Publisher: Springer, Pages: 303-318

Conference paper

Phillips ICC, Ulidowski I, 2012, A Hierarchy of Reverse Bisimulations on Stable Configuration Structures, Mathematical Structures in Computer Science, Vol: 22, Pages: 333-372

Journal article

Phillips ICC, Ulidowski I, 2011, A Logic with Reverse Modalities for History-preserving Bisimulations, 18th International Workshop on Expressiveness of Concurrency, EXPRESS'11, Pages: 104-118

Conference paper

Phillips I, Ulidowski I, 2009, Reverse Bisimulations on Stable Configuration Structures, Structural Operational Semantics 2009

The relationships between various equivalences on configuration structures, including interleaving bisimulation (IB), step bisimulation (SB) and hereditary history-preserving (HH) bisimulation, have been investigated by van Glabbeek and Goltz (and later Fecher). Since HH bisimulation may be characterised by the use of reverse as well as forward transitions, it is of interest to investigate forms of IB and SB where both forward and reverse transitions are allowed. Bednarczyk asked whether SB with reverse steps (which we shall call reverse SB) is as strong as HH bisimulation. This question remains open. We give various characterisations of reverse SB, showing that forward steps do not add extra power. We strengthen Bednarczyk's result that, in the absence of auto-concurrency, reverse IB is as strong as HH bisimulation, by showing that we need only exclude auto-concurrent events at the same depth in the configuration.

Conference paper

This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.

Request URL: http://wlsprd.imperial.ac.uk:80/respub/WEB-INF/jsp/search-html.jsp Request URI: /respub/WEB-INF/jsp/search-html.jsp Query String: respub-action=search.html&id=00004651&limit=30&person=true