Short-Term Scientific Missions
Short-term scientific missions (STSM) are exchange visits between researchers involved in our COST Action, allowing scientists to visit an institution or laboratory in another COST country. They are aimed at fostering collaboration, sharing new techniques and infrastructure that may not be available in other participants' institutions or laboratories. STSM are intended especially for young researchers.
In this page, we list the STMSs which are currently conducted or have been condcucted within this COST Action.
> Grant Period 1
> Grant Period 2
> Grant Period 3
> Grant Period 4
Grant Period 1 (Jul 1, 2015 -- Apr 30, 2016)
Theories of operational semantics for reversible computation
Duration: Jul 13 - Jul 20, 2015
Location: Swansea University (UK)
Involved Reseachers: Peter D. Moses, Irek Ulidowski, Mohammad Reza Mousavi
Providing a rigorous mathematical semantics is the first step towards developing rigorous analysis techniques for models of computations. The goal of this STSM is to investigate and generic theories of operational semantics. More specifically, we seek generic translations from forward-only transition system specification to reversible specifications in the style of Chemical Abstract Machines developed by Gerard Berry and Gerard Boudol and vice versa. The translations are then furnished with generic meta-theorems in order to relate the semantic properties of the induced forward-only and the reversible transitions systems. The subject matter of this STSM is at the core of the challenges mentioned in the Memorandum of Understanding for IC1405 under the description of Working Group 1 (Foundations).
Duration: Jul 13 - Jul 20, 2015
Location: Swansea University (UK)
Involved Reseachers: Peter D. Moses, Irek Ulidowski, Mohammad Reza Mousavi
Providing a rigorous mathematical semantics is the first step towards developing rigorous analysis techniques for models of computations. The goal of this STSM is to investigate and generic theories of operational semantics. More specifically, we seek generic translations from forward-only transition system specification to reversible specifications in the style of Chemical Abstract Machines developed by Gerard Berry and Gerard Boudol and vice versa. The translations are then furnished with generic meta-theorems in order to relate the semantic properties of the induced forward-only and the reversible transitions systems. The subject matter of this STSM is at the core of the challenges mentioned in the Memorandum of Understanding for IC1405 under the description of Working Group 1 (Foundations).
DD-based design of Reversible Circuits
Duration: Aug 11 - Aug 15, 2015
Location: University of Nis (Serbia)
Involved Reseachers: Radomir Stankovic, Milena Stankovic, and Dr. Suzana Stojkovic (Serbia); Claudio Moraga (Germany)
The work started by analyzing and discussing possible improvements on our recent publication using Functional Decision Diagrams for the design of reversible circuits. As in any DD-based system, reordering the nodes may lead to better realizations, but the problem is known to be NP-complete. Graph dependencies however may support partial improvements. Furthermore we proved that for many benchmarks, the FDD-based realizations are better than the BBDD-based realizations. We also discussed on the possibility of using WDDs for synthesis of reversible circuits using Hadamard (instead of Toffoli) gates. After the STSM, Dr. Stojkovic continued working on the subject, obtaining positive results with local reorderings of the Decision Diagrams.
Duration: Aug 11 - Aug 15, 2015
Location: University of Nis (Serbia)
Involved Reseachers: Radomir Stankovic, Milena Stankovic, and Dr. Suzana Stojkovic (Serbia); Claudio Moraga (Germany)
The work started by analyzing and discussing possible improvements on our recent publication using Functional Decision Diagrams for the design of reversible circuits. As in any DD-based system, reordering the nodes may lead to better realizations, but the problem is known to be NP-complete. Graph dependencies however may support partial improvements. Furthermore we proved that for many benchmarks, the FDD-based realizations are better than the BBDD-based realizations. We also discussed on the possibility of using WDDs for synthesis of reversible circuits using Hadamard (instead of Toffoli) gates. After the STSM, Dr. Stojkovic continued working on the subject, obtaining positive results with local reorderings of the Decision Diagrams.
Behavioural Equivalences for Reversible Calculi
Duration: Sep 7 - Sep 11, 2015
Location: Trinity College Dublin (Ireland)
Involved Reseachers: Vasileios Koutavas, Claudio Antares Mezzina, Matthew Hennessy
Communicating transactions differ from the classical transactions (enjoying ACID properties) in the way they drop the "Isolation". This implies that they may communicate with other processes or transactions in their environment. When a transaction communicates with its environment and subsequently fails, both the transaction and its environment will be rolled back to a consistent state. Reversibility can be used to implement an improved version of communicating transactions: indeed the causality tracking mechanism implied by reversibility improves the original semantics of communicating transactions by avoiding some spurious aborting action. Starting from results on behavioural theory for communicating transactions, the goal of this STSM was to explore what is a good notion of may testing for a reversible calculus with controlled reversibility and explicit commit.
Duration: Sep 7 - Sep 11, 2015
Location: Trinity College Dublin (Ireland)
Involved Reseachers: Vasileios Koutavas, Claudio Antares Mezzina, Matthew Hennessy
Communicating transactions differ from the classical transactions (enjoying ACID properties) in the way they drop the "Isolation". This implies that they may communicate with other processes or transactions in their environment. When a transaction communicates with its environment and subsequently fails, both the transaction and its environment will be rolled back to a consistent state. Reversibility can be used to implement an improved version of communicating transactions: indeed the causality tracking mechanism implied by reversibility improves the original semantics of communicating transactions by avoiding some spurious aborting action. Starting from results on behavioural theory for communicating transactions, the goal of this STSM was to explore what is a good notion of may testing for a reversible calculus with controlled reversibility and explicit commit.
On Reversible Architecture and Memory Hierarchy
Duration: Oct 25 - Nov 4, 2015
Location: University of Cyprus (Cyprus)
Involved Reseachers: Michael Kirkedal Thomsen, Pedro Trancoso, Anna Philippou, Georgia Kapitsaki, Chryssis Georgiou
The goal of the STSM was to find the common ground between my earlier theoretical work on reversible computing architectures and modern day approaches. We had in advance identified two areas that could be interesting to look at. (1) Parallel architectures: If reversibility should work with current days CMOS we would need to work the circuits at a low frequency, which would mean that parallel architectures are essential to avoid great performance loss. (2) Memory hierarchy: The memory hierarchy is interesting because this is where most information is transferred and, thus, Landauers principle might have most benefit.
Duration: Oct 25 - Nov 4, 2015
Location: University of Cyprus (Cyprus)
Involved Reseachers: Michael Kirkedal Thomsen, Pedro Trancoso, Anna Philippou, Georgia Kapitsaki, Chryssis Georgiou
The goal of the STSM was to find the common ground between my earlier theoretical work on reversible computing architectures and modern day approaches. We had in advance identified two areas that could be interesting to look at. (1) Parallel architectures: If reversibility should work with current days CMOS we would need to work the circuits at a low frequency, which would mean that parallel architectures are essential to avoid great performance loss. (2) Memory hierarchy: The memory hierarchy is interesting because this is where most information is transferred and, thus, Landauers principle might have most benefit.
Reversible Automata Models with Limited Resources
Duration: Oct 26 to Nov 20, 2015,
Location: Justus-Liebig Universität Giessen (Germany)
Involved Reseachers: Holger Bock Axelsen (Denmark); Markus Holzer, Andreas Malcher, Martin Kutrib, Matthias Wendlandt (Germany)
The purpose of this STSM was to investigate various limited reversible automata models, with a particular view to understanding which modalities drive the separation (or unification) of reversible and deteministic computations.
To this end we studied reversible two-pushdown automata, showing a separation between reversibility and determinism, as well as a number of non-semi-decidability results. We also studied the properties of reversible transducers of various kinds, and of reversible finite state transducer-preprocessed computations of reversible pushdown automata. The relatively weak step of preprocessing an input with a reversible finite state transducer is enough to allow a reversible pushdown automaton to accept certain languages that it cannot accept without this step.
Finally, we studied the properties of a novel notion of degree of irreversibility for finite state automata: the number occurrences of a certain pattern in the state diagram for the minimal automaton accepting a given language. We showed that the problem of deciding whether a regular expression generates a reversibly regular language is PSPACE-complete (equivalently, whether a nondeterministic finite state automaton (NFA) recognizes a reversibly regular language.) We also studied how the degree of irreversibility in a DFA behaves under some usual language and automata operations, showing a number of tight and asymptotic bounds.
Duration: Oct 26 to Nov 20, 2015,
Location: Justus-Liebig Universität Giessen (Germany)
Involved Reseachers: Holger Bock Axelsen (Denmark); Markus Holzer, Andreas Malcher, Martin Kutrib, Matthias Wendlandt (Germany)
The purpose of this STSM was to investigate various limited reversible automata models, with a particular view to understanding which modalities drive the separation (or unification) of reversible and deteministic computations.
To this end we studied reversible two-pushdown automata, showing a separation between reversibility and determinism, as well as a number of non-semi-decidability results. We also studied the properties of reversible transducers of various kinds, and of reversible finite state transducer-preprocessed computations of reversible pushdown automata. The relatively weak step of preprocessing an input with a reversible finite state transducer is enough to allow a reversible pushdown automaton to accept certain languages that it cannot accept without this step.
Finally, we studied the properties of a novel notion of degree of irreversibility for finite state automata: the number occurrences of a certain pattern in the state diagram for the minimal automaton accepting a given language. We showed that the problem of deciding whether a regular expression generates a reversibly regular language is PSPACE-complete (equivalently, whether a nondeterministic finite state automaton (NFA) recognizes a reversibly regular language.) We also studied how the degree of irreversibility in a DFA behaves under some usual language and automata operations, showing a number of tight and asymptotic bounds.
Reversibility in Petri Nets
Duration: Jan 30 - Feb 08, 2016
Location: Nicolaus Copernicus University, Torun (Poland)
Involved Reseachers: Maciej Koutny, Lukasz Mikulski, Kamila Barylska, Marcin Piatkowski
Petri nets are a long established model of concurrent computation. One of its strengths is the ability to capture both the actions and (local/global) states within a single formalism. In particular, it supports the notion of locality and distributed state which has been taken advantage of in, e.g., the development of efficient verification algorithms. Moreover, Petri nets (in the form of Signal Transition Graphs - STGs - are a de facto standard in the design, analysis and synthesis of asynchronous VLSI circuits. The literature relating to Petri nets already contains some contributions which have the potential of being directly relevant to the aims and objectives of the COST Action IC1405 on Reversible Computation, e.g., the problem of the existence of home states in a given Petri nets. During the STMS the following list of topics was discussed:
Duration: Jan 30 - Feb 08, 2016
Location: Nicolaus Copernicus University, Torun (Poland)
Involved Reseachers: Maciej Koutny, Lukasz Mikulski, Kamila Barylska, Marcin Piatkowski
Petri nets are a long established model of concurrent computation. One of its strengths is the ability to capture both the actions and (local/global) states within a single formalism. In particular, it supports the notion of locality and distributed state which has been taken advantage of in, e.g., the development of efficient verification algorithms. Moreover, Petri nets (in the form of Signal Transition Graphs - STGs - are a de facto standard in the design, analysis and synthesis of asynchronous VLSI circuits. The literature relating to Petri nets already contains some contributions which have the potential of being directly relevant to the aims and objectives of the COST Action IC1405 on Reversible Computation, e.g., the problem of the existence of home states in a given Petri nets. During the STMS the following list of topics was discussed:
- What are possible ways of expressing reversibility in Petri nets ?
- To what extend is reversibility related to the classical Petri nets problems, for example, home states or reachability ?
- How one can identify Petri net markings for which reversibility is possible ?
- How to control Petri net behaviour to prevent it entering non-reversible markings ?
- How to synthesise a reversible Petri net from a behavioural specification given in terms of a transition system ?
Should Testing Equivalences for Reversible Calculi
Duration: Jan 31 - Feb 14, 2016
Location: Trinity College Dublin, Dublin (UK)
Involved Reseachers: Vasileios Koutavas, Claudio Antares Mezzina, Matthew Hennessy
Our preliminary results, on a (causally) reversible CCS with controlled reversibility, show that the canonical notion of may testing does not enjoy basic equivalence property, e.g. may test is not preserved by the action prefix operator. To this end we have started studying the theory of safety and liveness in a reversible calculus where reductions are totally ordered and rollback moves return systems to past states. Liveness and safety respectively correspond to the should-testing and inverse may-testing preorders. We have developed fully abstract models for these preorders in terms of forward transitions in a labelled transition system, and give sufficient conditions for these models to apply to other calculi. Avoiding rollback transitions in the characterisations simplifies reasoning. We show that with respect to safety, total reversibility is a conservative extension to CCS. With respect to liveness, however, adding total reversibility to CCS distinguishes more systems.
Duration: Jan 31 - Feb 14, 2016
Location: Trinity College Dublin, Dublin (UK)
Involved Reseachers: Vasileios Koutavas, Claudio Antares Mezzina, Matthew Hennessy
Our preliminary results, on a (causally) reversible CCS with controlled reversibility, show that the canonical notion of may testing does not enjoy basic equivalence property, e.g. may test is not preserved by the action prefix operator. To this end we have started studying the theory of safety and liveness in a reversible calculus where reductions are totally ordered and rollback moves return systems to past states. Liveness and safety respectively correspond to the should-testing and inverse may-testing preorders. We have developed fully abstract models for these preorders in terms of forward transitions in a labelled transition system, and give sufficient conditions for these models to apply to other calculi. Avoiding rollback transitions in the characterisations simplifies reasoning. We show that with respect to safety, total reversibility is a conservative extension to CCS. With respect to liveness, however, adding total reversibility to CCS distinguishes more systems.
Reversibility and testing
Duration: Apr 10 - Apr 21, 2016
Location: University of Halmstad (Sweden)
Involved Reseachers: Michael Kirkedal Thomsen, Mohammad Reza Mousavi
This STSM started an investigation into reversibility in software and systems and in these show potential of increasing reliability and safety. In this we specifically was interested in testing. As there are little existing work in the area of reversibility and testing, and as Mohammad and I come with different approaches, the purpose of the STSM was also to find a common ground from which to continue the work. During the stay we have defined the reversible finite state machine (rFSM) as FSMs that is both forward and backward deterministic, following the tradition of Lecerf and Bennett. It will be obvious now to think of a reversible FSM as a FSM that takes some input and generates a unique output, as is true for reversible Turing machines and programs. This is, however, not true for FSM. Turing machines programs have one specific entry point (and generally also exit point), while we in FSMs often want to reason about the behaviour from some unknown state. For FSMs it is important to include the initial and final states is input and output respectively.
Duration: Apr 10 - Apr 21, 2016
Location: University of Halmstad (Sweden)
Involved Reseachers: Michael Kirkedal Thomsen, Mohammad Reza Mousavi
This STSM started an investigation into reversibility in software and systems and in these show potential of increasing reliability and safety. In this we specifically was interested in testing. As there are little existing work in the area of reversibility and testing, and as Mohammad and I come with different approaches, the purpose of the STSM was also to find a common ground from which to continue the work. During the stay we have defined the reversible finite state machine (rFSM) as FSMs that is both forward and backward deterministic, following the tradition of Lecerf and Bennett. It will be obvious now to think of a reversible FSM as a FSM that takes some input and generates a unique output, as is true for reversible Turing machines and programs. This is, however, not true for FSM. Turing machines programs have one specific entry point (and generally also exit point), while we in FSMs often want to reason about the behaviour from some unknown state. For FSMs it is important to include the initial and final states is input and output respectively.
Reversible reduction and message-passing concurrency
Duration: Apr 11 - Apr 21, 2016
Location: Nagoya (Japan)
Involved Reseachers: Adrian Palacios and German Vidal, Spain; Naoki Nishida, Japan
During the STSM, we have formalised a framework for modelling reversible computation in the context of an asynchronous concurrent language based on message passing. For this purpose, we have introduced a reversible semantics for a subset of Core Erlang, together with the associated inverse semantics. Both semantics are specified by transition relations, whose union models the evolution of a concurrent system where some processes run forwards while others undo their actions, in an asynchronous manner.
We consider that our results are useful to understand the concept of reversibility in the context of Erlang, and to clarify the implications of the different design choices. Furthermore, we find it a promising first step towards defining safe sessions for Erlang, where the actions of a session can be undone if all the actions in this session cannot be completed.
Duration: Apr 11 - Apr 21, 2016
Location: Nagoya (Japan)
Involved Reseachers: Adrian Palacios and German Vidal, Spain; Naoki Nishida, Japan
During the STSM, we have formalised a framework for modelling reversible computation in the context of an asynchronous concurrent language based on message passing. For this purpose, we have introduced a reversible semantics for a subset of Core Erlang, together with the associated inverse semantics. Both semantics are specified by transition relations, whose union models the evolution of a concurrent system where some processes run forwards while others undo their actions, in an asynchronous manner.
We consider that our results are useful to understand the concept of reversibility in the context of Erlang, and to clarify the implications of the different design choices. Furthermore, we find it a promising first step towards defining safe sessions for Erlang, where the actions of a session can be undone if all the actions in this session cannot be completed.
Classification aspects of reversible functions
Duration: Apr 11 - Apr 16, 2016
Location: University of Nis (Serbia)
Involved Reseachers: Radomir Stankovic (Serbia); Claudio Moraga (Germany); Pawel Kerntopf, Krzysztof Podlaski (Poland)
In the case of irreversible Boolean functions, the classification is based on some relevant property of the function (dual, bent, threshold, unate, etc.). A straight forward extension to reversible functions would require that all n component functions should have a common characterizing property. This seemed to be a possibly too strong constraint. Within this STSM (also) reversible functions have been considered where all the component functions must be balanced and might have well defined but possibly different properties.
Duration: Apr 11 - Apr 16, 2016
Location: University of Nis (Serbia)
Involved Reseachers: Radomir Stankovic (Serbia); Claudio Moraga (Germany); Pawel Kerntopf, Krzysztof Podlaski (Poland)
In the case of irreversible Boolean functions, the classification is based on some relevant property of the function (dual, bent, threshold, unate, etc.). A straight forward extension to reversible functions would require that all n component functions should have a common characterizing property. This seemed to be a possibly too strong constraint. Within this STSM (also) reversible functions have been considered where all the component functions must be balanced and might have well defined but possibly different properties.
Reversible Computations in Petri Nets
Duration: Apr 17 - Apr 24, 2016
Location: Carl von Ossietzky Universität Oldenburg (Germany)
Involved Reseachers: Kamila Barylska, Lukasz Mikulski, Marcin Piatkowski (Poland); Evgeny Erofeev, Valentin Spreckels, Uli Schlachter, Eike Best (Germany)
The topic of the visit was Reversible computations in Petri nets. The aim was to investigate reversible computations in bounded Petri nets from the perspective of labelled transition systems which correspond to them. We concentrated on transitions which may be reversed only just after their executions. The synthesis tool APT was supplemented by new modules allowing to add reverses of arbitrary transitions and the synthesis based on the newly created lts. Some unwanted behavior of systems modeled by lts’s with reverses has been diagnosed and called infeasibility for reversing (when a reverse is executed more frequently than its origin). For a given lts and a single transition the problem of deciding whether this action is infeasible may be reduced to computing single source shortest paths in a directed weighted graph. The implementation of infeasibility testing is being implemented (as another module of APT).
Duration: Apr 17 - Apr 24, 2016
Location: Carl von Ossietzky Universität Oldenburg (Germany)
Involved Reseachers: Kamila Barylska, Lukasz Mikulski, Marcin Piatkowski (Poland); Evgeny Erofeev, Valentin Spreckels, Uli Schlachter, Eike Best (Germany)
The topic of the visit was Reversible computations in Petri nets. The aim was to investigate reversible computations in bounded Petri nets from the perspective of labelled transition systems which correspond to them. We concentrated on transitions which may be reversed only just after their executions. The synthesis tool APT was supplemented by new modules allowing to add reverses of arbitrary transitions and the synthesis based on the newly created lts. Some unwanted behavior of systems modeled by lts’s with reverses has been diagnosed and called infeasibility for reversing (when a reverse is executed more frequently than its origin). For a given lts and a single transition the problem of deciding whether this action is infeasible may be reduced to computing single source shortest paths in a directed weighted graph. The implementation of infeasibility testing is being implemented (as another module of APT).
Reversible cellular automata and the modelling of reversible delay insensitive networks
Duration: Apr 19 - Apr 28, 2016
Location: AGH Technical University, Krakow, Poland
Involved Reseachers: Jaroslaw Was, Jakub Porzycki (Poland), Irek Ulidowski (UK)
Implementations of reversible Delay Insensitive (DI) networks in Self-Timed Cellular Automata, a special type of asynchronous cellular automata, were discussed initially, followed by further cellular automata realisations of DI networks. Moreover, a process calculus-like framework for DI networks was researched, and an operational model was defined for representing DI modules, the environment, and communication lines that connect modules with modules, and modules with the environment. The model allows us to prove that networks of modules implement a module. This, in turn, allows us to prove that a set of three pairs of DI modules, where each pair consists of a module and its inverse, namely (RT, IRT), (Fork, Join), and (ATS, ATSinverse), is universal for all DI modules. We have discussed also a couple of ways that some of the techniques from reversible computation could be used to improve or enrich simulation theories and software tools for crowd control and pedestrian movement modelling. They might be able to help to speed up simulations which are used in decision making in crowd management, or to allow detailed investigation of rare incidents in crowd simulation.
Duration: Apr 19 - Apr 28, 2016
Location: AGH Technical University, Krakow, Poland
Involved Reseachers: Jaroslaw Was, Jakub Porzycki (Poland), Irek Ulidowski (UK)
Implementations of reversible Delay Insensitive (DI) networks in Self-Timed Cellular Automata, a special type of asynchronous cellular automata, were discussed initially, followed by further cellular automata realisations of DI networks. Moreover, a process calculus-like framework for DI networks was researched, and an operational model was defined for representing DI modules, the environment, and communication lines that connect modules with modules, and modules with the environment. The model allows us to prove that networks of modules implement a module. This, in turn, allows us to prove that a set of three pairs of DI modules, where each pair consists of a module and its inverse, namely (RT, IRT), (Fork, Join), and (ATS, ATSinverse), is universal for all DI modules. We have discussed also a couple of ways that some of the techniques from reversible computation could be used to improve or enrich simulation theories and software tools for crowd control and pedestrian movement modelling. They might be able to help to speed up simulations which are used in decision making in crowd management, or to allow detailed investigation of rare incidents in crowd simulation.
Reversibility on Session-based Communications in the Pi-Calculus and Erlang
Duration: Apr 22 - April 30, 2016
Location:University of Camerino (Italy)
Involved Reseachers: Francesco Tiezzi, Emanuela Merelli, Stefano Mancini, Polini Andrea, Barbara Re, Mostarda Leonardo, Nobuko Yoshida, Rumyana Neykova
We discussed how to build the MPST calculus for full reversible computations extending from our JLAMP paper and how to systematically analyse how the ways to reverse sessions or shared name interactions affect the complexity. However we found out that this would be a similar extension from our existing journal paper for binary session types. Hence we decided to leave this topic until we receive the feedback from the audience of RC'2016 on our paper. The main result we shall investigate in future is a new reversible calculus and session types for multiple participants with commitment and roll back primitives. This model leads to several interesting applications and usecases for a real use of reversible computing such as in Erlang. We discussed the initial idea, models and typing systems. We discussed applications and reversible commuting with several staff who are working in Complex systems and Software Engineering in Univeristy of Camerino (listed above) We gave a department talk and discuss how actor models and Erlang recovery mechanism can be extended to reversible computing framework.
Duration: Apr 22 - April 30, 2016
Location:University of Camerino (Italy)
Involved Reseachers: Francesco Tiezzi, Emanuela Merelli, Stefano Mancini, Polini Andrea, Barbara Re, Mostarda Leonardo, Nobuko Yoshida, Rumyana Neykova
We discussed how to build the MPST calculus for full reversible computations extending from our JLAMP paper and how to systematically analyse how the ways to reverse sessions or shared name interactions affect the complexity. However we found out that this would be a similar extension from our existing journal paper for binary session types. Hence we decided to leave this topic until we receive the feedback from the audience of RC'2016 on our paper. The main result we shall investigate in future is a new reversible calculus and session types for multiple participants with commitment and roll back primitives. This model leads to several interesting applications and usecases for a real use of reversible computing such as in Erlang. We discussed the initial idea, models and typing systems. We discussed applications and reversible commuting with several staff who are working in Complex systems and Software Engineering in Univeristy of Camerino (listed above) We gave a department talk and discuss how actor models and Erlang recovery mechanism can be extended to reversible computing framework.
Revisiting Reversibility in Session-based Communication
Duration: Apr 25 - Apr 29, 2016
Location: University of Groningen (Netherlands)
Involved Reseachers: Claudio Antares Mezzina, Jorge A. Perez
The purpose of this STSM was to study reversible models of structured communications. Framed within concurrency theory and process calculi approaches, we are interested in developing rich models of concurrent computation in which communicating processes follow structured interaction protocols (as described by session types), and whose underlying operational semantics admits the possibility of reversing their actions. This integration of structured communication and reversibility is expected to inform the design of sound programming abstractions for resilient communicating programs governed by casual consistent semantics. The key observation that underlies this STSM is that the design of casually consistent operational semantics for concurrent processes can take advantage of the structured protocols that typically govern their behavior. As session types abstract sequences of communication actions (protocols), they appear as a natural choice for recording the forward and backward actions of interacting processes.
Duration: Apr 25 - Apr 29, 2016
Location: University of Groningen (Netherlands)
Involved Reseachers: Claudio Antares Mezzina, Jorge A. Perez
The purpose of this STSM was to study reversible models of structured communications. Framed within concurrency theory and process calculi approaches, we are interested in developing rich models of concurrent computation in which communicating processes follow structured interaction protocols (as described by session types), and whose underlying operational semantics admits the possibility of reversing their actions. This integration of structured communication and reversibility is expected to inform the design of sound programming abstractions for resilient communicating programs governed by casual consistent semantics. The key observation that underlies this STSM is that the design of casually consistent operational semantics for concurrent processes can take advantage of the structured protocols that typically govern their behavior. As session types abstract sequences of communication actions (protocols), they appear as a natural choice for recording the forward and backward actions of interacting processes.
Grant Period 2 (May 1, 2016 -- Apr 30, 2017)
Process calculi for reversible event structures
Duration: Jun 3 - Jun 16, 2016
Location: Nagoya University (Japan)
Involved Reseachers: Irek Ulidowski (UK), Shoji Yuen, Naoki Nishida, Masahiko Sakai (Japan)
The aim of this STSM was develop a base process calculus for representing event structures, including Prime Event Structures. We formulated general principles for the operational semantics, both forward and reverse. We worked on event structures defined with pure enabling rules as opposed to event structures definable with impure rules. The operational semantics for both types of event structures were formulated. It became also clear that defining a multi-step transition relation for the calculus is more challenging than previously thought. The work on this definition is still ongoing.
Duration: Jun 3 - Jun 16, 2016
Location: Nagoya University (Japan)
Involved Reseachers: Irek Ulidowski (UK), Shoji Yuen, Naoki Nishida, Masahiko Sakai (Japan)
The aim of this STSM was develop a base process calculus for representing event structures, including Prime Event Structures. We formulated general principles for the operational semantics, both forward and reverse. We worked on event structures defined with pure enabling rules as opposed to event structures definable with impure rules. The operational semantics for both types of event structures were formulated. It became also clear that defining a multi-step transition relation for the calculus is more challenging than previously thought. The work on this definition is still ongoing.
Parallel algorithms for invertible finite state machines
Duration: Jun 16 - Jun 30, 2016
Location: Halmstad University (Sweden)
Involved Reseachers: Uraz Cengiz Turker, Mohammad Reza Mousavi
During the visit we first investigate the known results related to invertible sequences. As optimization problems are important when scalability is of interest, we first check the optimization problems related to invertible sequences. However we observed that except the formal definitions of invertible sequences, there was not a formal definition of an optimization problem related to the derivation of invertible sequences. Therefore we first introduce some problems. Afterwards we investigated and set their computational complexities.
Duration: Jun 16 - Jun 30, 2016
Location: Halmstad University (Sweden)
Involved Reseachers: Uraz Cengiz Turker, Mohammad Reza Mousavi
During the visit we first investigate the known results related to invertible sequences. As optimization problems are important when scalability is of interest, we first check the optimization problems related to invertible sequences. However we observed that except the formal definitions of invertible sequences, there was not a formal definition of an optimization problem related to the derivation of invertible sequences. Therefore we first introduce some problems. Afterwards we investigated and set their computational complexities.
Session-based Functional Programming for Reversible Communications
Duration: Jul 23 - Aug 2, 2016
Location: Nagoya University (Japan)
Involved Reseachers: Shoji Yuen, Keigo Imai, Naoki Nishida, Nobuko Yoshida
In this visit, we studied a basic notion of concurrent functional reversible computation in a session-based concurrent Ocaml instead of Concurrent Haskell. I also studied Erlang (which is a distributed functional programming) recovery mechanism. First we encoded the session-based communications into in Concurrent Ocaml (using the indexed monads) in order to statically validate linearity of communications efficiently. Secondly we also discussed how to implement permutations in asynchronous FIFO queues. In addition, I discussed a recovery mechanism of Erlang against rewriting techniques done by Professor Nishida and our session based approaches.
Duration: Jul 23 - Aug 2, 2016
Location: Nagoya University (Japan)
Involved Reseachers: Shoji Yuen, Keigo Imai, Naoki Nishida, Nobuko Yoshida
In this visit, we studied a basic notion of concurrent functional reversible computation in a session-based concurrent Ocaml instead of Concurrent Haskell. I also studied Erlang (which is a distributed functional programming) recovery mechanism. First we encoded the session-based communications into in Concurrent Ocaml (using the indexed monads) in order to statically validate linearity of communications efficiently. Secondly we also discussed how to implement permutations in asynchronous FIFO queues. In addition, I discussed a recovery mechanism of Erlang against rewriting techniques done by Professor Nishida and our session based approaches.
The efficiency of DD-based tools for reversible computation
Duration: Sep 18 - Sep 26, 2016
Location: Johannes Kepler University Linz (Austria)
Involved Reseachers: Robert Wille, Robert Meolic
Decision diagrams (DD) based methods have already been proven as a viable alternative for the design of reversible circuits. Among different types of DDs, binary decision diagrams (BDDs) are the best supported by existing tools. However, the popular general BDD packages (e.g. CUDD) are not optimized for reversible computation and they also lack support for interesting extensions, e.g. functional decision diagrams. At the University of Maribor and at the research group in Linz, various DD-based tools are used, developed, or maintained. The focus of this STSM was on the extensions of classic BDDs. This includes Quantum Multiple-valued Decision Diagrams (QMDDs), suppressed decision diagrams, and functional decision diagrams (FDDs).
Duration: Sep 18 - Sep 26, 2016
Location: Johannes Kepler University Linz (Austria)
Involved Reseachers: Robert Wille, Robert Meolic
Decision diagrams (DD) based methods have already been proven as a viable alternative for the design of reversible circuits. Among different types of DDs, binary decision diagrams (BDDs) are the best supported by existing tools. However, the popular general BDD packages (e.g. CUDD) are not optimized for reversible computation and they also lack support for interesting extensions, e.g. functional decision diagrams. At the University of Maribor and at the research group in Linz, various DD-based tools are used, developed, or maintained. The focus of this STSM was on the extensions of classic BDDs. This includes Quantum Multiple-valued Decision Diagrams (QMDDs), suppressed decision diagrams, and functional decision diagrams (FDDs).
Causal consistency of reversed computations in Petri Nets
Duration: Sep 18 - Sep 26, 2016
Location: University of Bologna (Italy)
Involved Reseachers: Ivan Lanese, Lukasz Mikulski
During the STSM the unbounded case was studied. Existence of the set of reverses (for a given transition) reduces to the existence of so called b-problematic pairs of states. It is decidable (but as complex as Reachability Problem) whether a pair of markings is b-problematic or not. Hence, in further investigation one can concentrate on a finite set of minimal b-problematic pairs of markings. The solution for bounded case adds in such situation fresh places. It is not always possible in unbounded case. There exists a net with a pair of b-problematic markings which remains b-problematic no matter how the set of places is transformed. Some partial results concerning b-problematic pairs were obtained. Several properties based on runs leading to b-problematic pairs of markings were proposed. Some of them guarantee the possibility of transformation which preserves (potentially infinite) reachability graph and construct the set of inverses. Other state that such a transformation is impossible. The set of reversible (in Petri net sense) nets is proven to be free of problematic pairs of markings. Hence, similar to bounded case, one can always transform such a net in order to provide sets of reverses for every transition.
Duration: Sep 18 - Sep 26, 2016
Location: University of Bologna (Italy)
Involved Reseachers: Ivan Lanese, Lukasz Mikulski
During the STSM the unbounded case was studied. Existence of the set of reverses (for a given transition) reduces to the existence of so called b-problematic pairs of states. It is decidable (but as complex as Reachability Problem) whether a pair of markings is b-problematic or not. Hence, in further investigation one can concentrate on a finite set of minimal b-problematic pairs of markings. The solution for bounded case adds in such situation fresh places. It is not always possible in unbounded case. There exists a net with a pair of b-problematic markings which remains b-problematic no matter how the set of places is transformed. Some partial results concerning b-problematic pairs were obtained. Several properties based on runs leading to b-problematic pairs of markings were proposed. Some of them guarantee the possibility of transformation which preserves (potentially infinite) reachability graph and construct the set of inverses. Other state that such a transformation is impossible. The set of reversible (in Petri net sense) nets is proven to be free of problematic pairs of markings. Hence, similar to bounded case, one can always transform such a net in order to provide sets of reverses for every transition.
Control Logic for Reversible Languages
Duration: Sep 18 - Sep 26, 2016
Location: University of Bremen (Germany)
Involved Reseachers: Oliver Keszocze, Michael Kirkedal Thomsen, Robert Glück, Torben Mogensen
For designing reversible programs and circuits, the Janus and SyReC languages have been designed, respectively (the latter is based on the former). Even though reversible operations only are used by these languages, control structure such as an if statement can still lead to programs/circuits that can not be computed in the reverse direction. To overcome this, so-called fi-conditions need to be specified that decide on the branch of the control flow when executing the program/circuit in reverse direction. The main result of this STSM is a lemma stating that for if constructs, given some constraints, the if- and fi-conditions are equivalent. This lemma allows to implement an easy check for full reversibility of the control construct, easily derive the fi-condition for the programmer if the requirements are met, and simplify the code by only using the condition that is less complex (if both were specified). Currently, these points are being incorporated into the SyReC compiler. We expect this to improve the convenience of using SyReC in general and allow for easier debugging of programs in particular. Similar work is done on the Janus language. Another research topic, that came up during the course of this STSM, was how a new iteration construct could be implemented in the language. The forward direction is straight-forward but for the reverse direction, again, an exit criterion needs to be found.
Duration: Sep 18 - Sep 26, 2016
Location: University of Bremen (Germany)
Involved Reseachers: Oliver Keszocze, Michael Kirkedal Thomsen, Robert Glück, Torben Mogensen
For designing reversible programs and circuits, the Janus and SyReC languages have been designed, respectively (the latter is based on the former). Even though reversible operations only are used by these languages, control structure such as an if statement can still lead to programs/circuits that can not be computed in the reverse direction. To overcome this, so-called fi-conditions need to be specified that decide on the branch of the control flow when executing the program/circuit in reverse direction. The main result of this STSM is a lemma stating that for if constructs, given some constraints, the if- and fi-conditions are equivalent. This lemma allows to implement an easy check for full reversibility of the control construct, easily derive the fi-condition for the programmer if the requirements are met, and simplify the code by only using the condition that is less complex (if both were specified). Currently, these points are being incorporated into the SyReC compiler. We expect this to improve the convenience of using SyReC in general and allow for easier debugging of programs in particular. Similar work is done on the Janus language. Another research topic, that came up during the course of this STSM, was how a new iteration construct could be implemented in the language. The forward direction is straight-forward but for the reverse direction, again, an exit criterion needs to be found.
Different themes on Reversibility
Duration: Sep 28 - Oct 9, 2016
Location: Leicester University (UK)
Involved Reseachers: Claudio Antares Mezzina, Emilio Tuosto, Irek Ulidowski
The STSM was structured into two sub-goals: 1) Automatic generation of correct rollback-able processes: The research goal is to explore how to exploit the top-down approach typical of choreographies in order to algorithmically derive reversible computations. The basic idea is to use the global views of choreographies (formalised eg as global graphs) to identify retractable actions and scope of for reversible computations. Enriching existing algorithms for projecting global view to local views (e.g., communicating) machines) one can automatically obtain local views that encompass reversible computations. 2) Reversibility and testing equivalences: The research goal is to see how reversibility can affects testing equivalences and whether an equivalence derived by it can be placed into the linear time-branching spectrum. We started by taking a simple tree based CCS and devised a class of tests that can command to undo an action. We realised that our new testing equivalence has the same discriminating power of the ready-trace simulation semantics (RTS). We have then established a correspondence between our semantics, called undo trace semantics (UT) show- ing that indeed they coincide
Duration: Sep 28 - Oct 9, 2016
Location: Leicester University (UK)
Involved Reseachers: Claudio Antares Mezzina, Emilio Tuosto, Irek Ulidowski
The STSM was structured into two sub-goals: 1) Automatic generation of correct rollback-able processes: The research goal is to explore how to exploit the top-down approach typical of choreographies in order to algorithmically derive reversible computations. The basic idea is to use the global views of choreographies (formalised eg as global graphs) to identify retractable actions and scope of for reversible computations. Enriching existing algorithms for projecting global view to local views (e.g., communicating) machines) one can automatically obtain local views that encompass reversible computations. 2) Reversibility and testing equivalences: The research goal is to see how reversibility can affects testing equivalences and whether an equivalence derived by it can be placed into the linear time-branching spectrum. We started by taking a simple tree based CCS and devised a class of tests that can command to undo an action. We realised that our new testing equivalence has the same discriminating power of the ready-trace simulation semantics (RTS). We have then established a correspondence between our semantics, called undo trace semantics (UT) show- ing that indeed they coincide
Reversible monads and reversible effects
Duration: Oct 24 - Nov 11, 2016
Location: DIKU (Denmark)
Involved Reseachers: Martti Karvonen, Robin Kaarsgaard
The aim of the STSM was to develop a theory of reversible effects, allowing reversible functional programming languages to work with effectful programs, most notably input and output. The proposed approach for this was to use monads, as they are amongst the most successful ways of incorporating effects into functional programming languages. More precisely, the plan was to extend and develop earlier work on dagger mon- ads to inverse categories, which are a natural setting for semantics of reversible programming. Alas, the first approach did not work exactly as planned. However, we discovered that so-called arrows, which generalize monads, can be modified to the reversible setting, and capture several reversible effects. For instance, both reversible computing with a state and a reversible version of the \writer monad" are covered by this framework. Moreover, the reversible arrows also have a theoretically satisfying model behind them. We're now in the process of writing the results up and submitting the work to a suitable venue.
Duration: Oct 24 - Nov 11, 2016
Location: DIKU (Denmark)
Involved Reseachers: Martti Karvonen, Robin Kaarsgaard
The aim of the STSM was to develop a theory of reversible effects, allowing reversible functional programming languages to work with effectful programs, most notably input and output. The proposed approach for this was to use monads, as they are amongst the most successful ways of incorporating effects into functional programming languages. More precisely, the plan was to extend and develop earlier work on dagger mon- ads to inverse categories, which are a natural setting for semantics of reversible programming. Alas, the first approach did not work exactly as planned. However, we discovered that so-called arrows, which generalize monads, can be modified to the reversible setting, and capture several reversible effects. For instance, both reversible computing with a state and a reversible version of the \writer monad" are covered by this framework. Moreover, the reversible arrows also have a theoretically satisfying model behind them. We're now in the process of writing the results up and submitting the work to a suitable venue.
Cellular Automata Sequential Updating by Reversible Block Rules
Duration: Nov 20 - Nov 25, 2016
Location: Karlsruhe Institute of Technology (Germany)
Involved Reseachers: Ville Salo (Finland), Thomas Worsch, Simon Wacker (Germany)
The overall topic of the STSM was reversible asynchronous cellular automata. The emphasis was on the one-dimensional full shift, but several results generalize to subshifts and CA on general groups. We concentrated on fully asynchronous cellular automata (CA) where in each step exactly one cell is updated. In general this results in a multitude of different possible computations. We therefore first restricted the updating to sequential sweeps from left to right (or right to left) by a reversible block rule. We can show that a reversible cellular automaton has a left-to-right update rule if and only if its global average movement slants to the right. The case when any order of updates (not only strict left-to-right or right-to-left) has to lead to the same result has also been considered. We can show that for cellular automata with such implementations, surjectivity implies injectivity of the global rule (which is not the case for synchronous CA in general). We in fact believe this class is very small, but we do not know a characterization until now. During the STSM we invented several technical notions that may have further use in CA theory, in particular the notion of a homotopy between two cellular automata, which has most of the good properties of classical homotopies in algebraic topology, and is naturally connected to asynchronicity.
Duration: Nov 20 - Nov 25, 2016
Location: Karlsruhe Institute of Technology (Germany)
Involved Reseachers: Ville Salo (Finland), Thomas Worsch, Simon Wacker (Germany)
The overall topic of the STSM was reversible asynchronous cellular automata. The emphasis was on the one-dimensional full shift, but several results generalize to subshifts and CA on general groups. We concentrated on fully asynchronous cellular automata (CA) where in each step exactly one cell is updated. In general this results in a multitude of different possible computations. We therefore first restricted the updating to sequential sweeps from left to right (or right to left) by a reversible block rule. We can show that a reversible cellular automaton has a left-to-right update rule if and only if its global average movement slants to the right. The case when any order of updates (not only strict left-to-right or right-to-left) has to lead to the same result has also been considered. We can show that for cellular automata with such implementations, surjectivity implies injectivity of the global rule (which is not the case for synchronous CA in general). We in fact believe this class is very small, but we do not know a characterization until now. During the STSM we invented several technical notions that may have further use in CA theory, in particular the notion of a homotopy between two cellular automata, which has most of the good properties of classical homotopies in algebraic topology, and is naturally connected to asynchronicity.
Reversibility and Synthesis of Multiparty Session Types
Duration: Nov 27 - Dec 3, 2016
Location: Universite Paris Diderot (UK)
Involved Reseachers: Julien Lange, Bernardo Toninho, Jean Krivine
During this STSM, we have investigated a theory where the implementation of roles of a multiparty session adopt a reversible semantics. In such a case, the communication between participants always eventually succeeds, thus providing a generalised notion of projection that is a total function from global and local types, preserving good semantic properties, and enabling us to represent more sophisticated protocols as well-formed global types, e.g., 2-phase commit protocol.
Duration: Nov 27 - Dec 3, 2016
Location: Universite Paris Diderot (UK)
Involved Reseachers: Julien Lange, Bernardo Toninho, Jean Krivine
During this STSM, we have investigated a theory where the implementation of roles of a multiparty session adopt a reversible semantics. In such a case, the communication between participants always eventually succeeds, thus providing a generalised notion of projection that is a total function from global and local types, preserving good semantic properties, and enabling us to represent more sophisticated protocols as well-formed global types, e.g., 2-phase commit protocol.
Reversing CSP Computations
Duration: 2016
Location: Nagoya University (Japan)
Involved Reseachers: Naoki Nishida, Josep Silva
We have defined a so-called Landauer's embedding for the CSP concurrent language. In particular, we introduce a form of reversibility in the context of a process calculi based on the synchronized parallelism model. Although there are some previous approaches that consider concurrency and reversibility for process calculi, this is the first work that considers the definition of a reversible semantics of CSP that directly operates on the Landauer's embedding (the semantics does not need the specification). Moreover, this is the first implementation of such technology for CSP. In our proposal, we start by redefining CSP tracks to conveniently store the history of a CSP computation. Thus, in our proposal, we use a form of track to reproduce a computation (forwards). Furthermore, we have defined a set of semantic rules that operate on a track to also reproduce the computation backwards. This track-based reversible semantics has been defined in two independent ways, allowing (i) deterministic reversibility, and (ii) causal consistent reversibility.
Duration: 2016
Location: Nagoya University (Japan)
Involved Reseachers: Naoki Nishida, Josep Silva
We have defined a so-called Landauer's embedding for the CSP concurrent language. In particular, we introduce a form of reversibility in the context of a process calculi based on the synchronized parallelism model. Although there are some previous approaches that consider concurrency and reversibility for process calculi, this is the first work that considers the definition of a reversible semantics of CSP that directly operates on the Landauer's embedding (the semantics does not need the specification). Moreover, this is the first implementation of such technology for CSP. In our proposal, we start by redefining CSP tracks to conveniently store the history of a CSP computation. Thus, in our proposal, we use a form of track to reproduce a computation (forwards). Furthermore, we have defined a set of semantic rules that operate on a track to also reproduce the computation backwards. This track-based reversible semantics has been defined in two independent ways, allowing (i) deterministic reversibility, and (ii) causal consistent reversibility.
Gradual reversibility of finite-state machines
Duration: Jan 1 - Jan 7, 2017
Location: Porto (Portugal)
Involved Reseachers: Rogerio Reis, Nelma Moreira, Matthias Wendlandt
We investigated the number of minimal reversible acyclic DFA's for a given language. It comes out that there are exponential many of those, which is interesting for equivalence test reasons. We also find an algorithm that minimizes a given acyclic reversible automaton in linear time which we can combine to an algorithm that computes a reversible automaton out of an acyclic irreversible DFA. We further investigate statistics on reversible DFA's. It comes out that only a very small amount of DFA's are reversible and that the most of them are acyclic. We have done this with statistics on randomly generated automata with FAdo. Moreover we discussed a definition of weakly reversible DFA's and found a way to reconstruct a language with little changes to a language accepted by a reversible finite automaton.
Duration: Jan 1 - Jan 7, 2017
Location: Porto (Portugal)
Involved Reseachers: Rogerio Reis, Nelma Moreira, Matthias Wendlandt
We investigated the number of minimal reversible acyclic DFA's for a given language. It comes out that there are exponential many of those, which is interesting for equivalence test reasons. We also find an algorithm that minimizes a given acyclic reversible automaton in linear time which we can combine to an algorithm that computes a reversible automaton out of an acyclic irreversible DFA. We further investigate statistics on reversible DFA's. It comes out that only a very small amount of DFA's are reversible and that the most of them are acyclic. We have done this with statistics on randomly generated automata with FAdo. Moreover we discussed a definition of weakly reversible DFA's and found a way to reconstruct a language with little changes to a language accepted by a reversible finite automaton.
Reversing transitions in unbounded Petri Nets
Duration: Jan 27 - Feb 2, 2017
Location: Newcastle University (UK)
Involved Reseachers: Lukasz Mikulski, Maciej Koutny
We propose a new procedure based on region theory which allows to minimize the number of effect reverses by direct adaptation of synthesis algorithm. Similar adaptation allows to minimize the number of places in the resulting net. The interplay between minimizing according to those two parameters at once still needs further investigation. Hence, the problem of finding a net with minimal number of effect reverses as well as the problem of finding a net with minimal number of places which allows to implement reverses are decidable. We obtain new results concerning strict reverses. All transitions of a solvable, labeled and finite transition system with home state can be reversed in a strict sense if and only if reverted transition system (with initial state in one of home states) is solvable. Moreover, in every labeled finite transition system with 1-safe (or elementary) solution all transitions can be reversed in a strict sense. We started investigations on reversing in systems with step (and multistep) semantics. The preliminary results shows that strict requirements (like insisting that a reverse of a step need to be a step composed of reverses) implicates many negative results even in bounded case but might be relaxed. We have shown that most of the positive results hold if we allow to reverse a step (or even multistep) by a single transition.
Duration: Jan 27 - Feb 2, 2017
Location: Newcastle University (UK)
Involved Reseachers: Lukasz Mikulski, Maciej Koutny
We propose a new procedure based on region theory which allows to minimize the number of effect reverses by direct adaptation of synthesis algorithm. Similar adaptation allows to minimize the number of places in the resulting net. The interplay between minimizing according to those two parameters at once still needs further investigation. Hence, the problem of finding a net with minimal number of effect reverses as well as the problem of finding a net with minimal number of places which allows to implement reverses are decidable. We obtain new results concerning strict reverses. All transitions of a solvable, labeled and finite transition system with home state can be reversed in a strict sense if and only if reverted transition system (with initial state in one of home states) is solvable. Moreover, in every labeled finite transition system with 1-safe (or elementary) solution all transitions can be reversed in a strict sense. We started investigations on reversing in systems with step (and multistep) semantics. The preliminary results shows that strict requirements (like insisting that a reverse of a step need to be a step composed of reverses) implicates many negative results even in bounded case but might be relaxed. We have shown that most of the positive results hold if we allow to reverse a step (or even multistep) by a single transition.
Distributed reversibility, choreographically
Duration: Feb 11 - Feb 21, 2017
Location: IMT School for Advanced Studies Lucca (Italy)
Involved Reseachers: Emilio Tuosto and Claudio Antares Mezzina
The goal of the visit was to develop and study a reversible choreographic framework. We aimed to design specification primitives of global views of choreographies that could instrument reversibility in their local views. We first defined a variant of global graphs, a models of global views of choreographies. Then we harnessed the semantics of communicating-finite state machines (CFSMs), our model of local views of choreographies, with information to handle reversible computations. Once the framework was defined, we solved one of the challenges we had identified, namely we found the conditions for sound reversible computations in our choreographic context. Then such conditions have been used to define proper projection functions to take into account reversibility while preserving well-behaviour of interactions (e.g. deadlock-freedom).
Duration: Feb 11 - Feb 21, 2017
Location: IMT School for Advanced Studies Lucca (Italy)
Involved Reseachers: Emilio Tuosto and Claudio Antares Mezzina
The goal of the visit was to develop and study a reversible choreographic framework. We aimed to design specification primitives of global views of choreographies that could instrument reversibility in their local views. We first defined a variant of global graphs, a models of global views of choreographies. Then we harnessed the semantics of communicating-finite state machines (CFSMs), our model of local views of choreographies, with information to handle reversible computations. Once the framework was defined, we solved one of the challenges we had identified, namely we found the conditions for sound reversible computations in our choreographic context. Then such conditions have been used to define proper projection functions to take into account reversibility while preserving well-behaviour of interactions (e.g. deadlock-freedom).
Adding control to Erlang's reversible semantics
Duration: Feb 12 - Feb 18, 2017
Location: University of Bologna (Italy)
Involved Reseachers: Ivan Lanese, Adrian Palacios, German Vidal
Erlang is a functional and concurrent programming language that is becoming increasingly popular for developing massively concurrent, highly available and fault-tolerant reliable systems. We have recently introduced a reversible semantics for a subset of (Core) Erlang. During the STSM, we have introduced an uncontrolled reversible semantics and have proved its main properties. In particular, we have formally proved the causal consistency of the reversible semantics. A rollback semantics has also been defined on top of the uncontrolled semantics, which can be used as a basis for defining new debugging techniques and/or novel methods to improve fault-tolerance and recovery in Erlang.
Duration: Feb 12 - Feb 18, 2017
Location: University of Bologna (Italy)
Involved Reseachers: Ivan Lanese, Adrian Palacios, German Vidal
Erlang is a functional and concurrent programming language that is becoming increasingly popular for developing massively concurrent, highly available and fault-tolerant reliable systems. We have recently introduced a reversible semantics for a subset of (Core) Erlang. During the STSM, we have introduced an uncontrolled reversible semantics and have proved its main properties. In particular, we have formally proved the causal consistency of the reversible semantics. A rollback semantics has also been defined on top of the uncontrolled semantics, which can be used as a basis for defining new debugging techniques and/or novel methods to improve fault-tolerance and recovery in Erlang.
Reversibility on Session-based Communications (in Erlang)
Duration: Feb 18 - Feb 25, 2017
Location: University of Camerino (Italy)
Involved Reseachers: Nobuko Yoshida, Rumyana Neykova, Francesco Tiezzi
In this visit, we study the effect of session types for reversible computation. We focus on two approaches towards reversibility. The first one is a top-down approach, where a global specification, written in Scribble is annotated with reversible actions and safety of the system is guaranteed via coherent checkpoints on a global type. Then checkpoints and rollback actions are generated at runtime. The second one is a bottom-up approach, where processes are extended with rollback and commit primitives, and we define semantics for backward and forward computation. This extension requires to study a compliance relation for configurations of multiple participants. Rollback and commit are explicitly specified in the process syntax. We discussed potential use cases as to examine and compare the performance implications when performing reversible computation (with visible reversible actions) and recovery computation (where processes have local memories and recover from a previous state). We plan to implement both approaches in Erlang, following the ideas outlined above.
Duration: Feb 18 - Feb 25, 2017
Location: University of Camerino (Italy)
Involved Reseachers: Nobuko Yoshida, Rumyana Neykova, Francesco Tiezzi
In this visit, we study the effect of session types for reversible computation. We focus on two approaches towards reversibility. The first one is a top-down approach, where a global specification, written in Scribble is annotated with reversible actions and safety of the system is guaranteed via coherent checkpoints on a global type. Then checkpoints and rollback actions are generated at runtime. The second one is a bottom-up approach, where processes are extended with rollback and commit primitives, and we define semantics for backward and forward computation. This extension requires to study a compliance relation for configurations of multiple participants. Rollback and commit are explicitly specified in the process syntax. We discussed potential use cases as to examine and compare the performance implications when performing reversible computation (with visible reversible actions) and recovery computation (where processes have local memories and recover from a previous state). We plan to implement both approaches in Erlang, following the ideas outlined above.
Application of Reversibility to speculative computation
Duration: Feb 18 - Mar 19, 2017
Location: Lawrence Livermore National Laboratory (USA)
Involved Reseachers: Michael Kirkedal Thomsen, Markus Schordan
In this STSM at Lawrence Livermore National Laboratory I worked with Markus Schordan to combine two ways of approaching reversibility. Markus' work resulted in the tool Backstroke that can instrument C++ programs with incremental checkpointing; this add the possibility of reversing a computation that has already been executed. My work in reversible programming languages have resulted in a tool that can take a Janus program and translate it into a C++ programs; this makes it possible to execute programs both forward and backward from a given state. In optimistic execution, reversing a performed execution is an essential feature. The two above methods shows different trade-offs with respect to execution speed and memory usage. This STSM started the work to combining the two approaches into one tool, giving the users the possibility to choose which to use. Over time this can leas to automatic methods that analyses C++ code and decide in which cases either of the two methods will be most beneficial.
Duration: Feb 18 - Mar 19, 2017
Location: Lawrence Livermore National Laboratory (USA)
Involved Reseachers: Michael Kirkedal Thomsen, Markus Schordan
In this STSM at Lawrence Livermore National Laboratory I worked with Markus Schordan to combine two ways of approaching reversibility. Markus' work resulted in the tool Backstroke that can instrument C++ programs with incremental checkpointing; this add the possibility of reversing a computation that has already been executed. My work in reversible programming languages have resulted in a tool that can take a Janus program and translate it into a C++ programs; this makes it possible to execute programs both forward and backward from a given state. In optimistic execution, reversing a performed execution is an essential feature. The two above methods shows different trade-offs with respect to execution speed and memory usage. This STSM started the work to combining the two approaches into one tool, giving the users the possibility to choose which to use. Over time this can leas to automatic methods that analyses C++ code and decide in which cases either of the two methods will be most beneficial.
Reversible Global Types with Checkpoints
Duration: Feb 19 - Mar 3, 2017
Location: INRIA - Sophia Antipolis
Involved Reseachers: Paola Giannini, Ilaria Castellani
During the STMS mission the participants worked on a calculus for reversible interaction characterized by the presence of user defined checkpoints to which participants may roll back. In doing so, a novel definition of global types, which permits participants to perform conversations that do not follow a single thread, was explored. The restriction that if a participant wants to act differently on some branch of the choice, it must be aware of which branch it is on, is anyway retained. The global type specifies were rollback can be done, by using two kinds of labels for messages: one that can be traversed only forward and another that may also trigger a rollback. Moreover, global types contain a parallel and a sequential operator; the latter acts as a join, and produces some constraints on the participants that may follow a recursive operator. This produces a very expressive interaction language.
Duration: Feb 19 - Mar 3, 2017
Location: INRIA - Sophia Antipolis
Involved Reseachers: Paola Giannini, Ilaria Castellani
During the STMS mission the participants worked on a calculus for reversible interaction characterized by the presence of user defined checkpoints to which participants may roll back. In doing so, a novel definition of global types, which permits participants to perform conversations that do not follow a single thread, was explored. The restriction that if a participant wants to act differently on some branch of the choice, it must be aware of which branch it is on, is anyway retained. The global type specifies were rollback can be done, by using two kinds of labels for messages: one that can be traversed only forward and another that may also trigger a rollback. Moreover, global types contain a parallel and a sequential operator; the latter acts as a join, and produces some constraints on the participants that may follow a recursive operator. This produces a very expressive interaction language.
Rollback Recovery on Session-based Communications
Duration: Mar 06 - Mar 12, 2017
Location: Imperial College London (UK)
Involved Reseachers: Francesco Tiezzi, Nobuko Yoshida
One aim of this STSM is is to continue the existing collaboration on reversible sessions between Francesco Tiezzi at the University of Camerino (IT) and Nobuko Yoshida at Imperial College London (UK). The main topic of the work carried out in the STSM concerned a variant of the reversible session-based pi-calculus with commit and rollback primitives. Another aim of the STSM is to disseminate the achieved results on this topic in industrial contexts, in particular we visited the UK branch of Cognizant.
Duration: Mar 06 - Mar 12, 2017
Location: Imperial College London (UK)
Involved Reseachers: Francesco Tiezzi, Nobuko Yoshida
One aim of this STSM is is to continue the existing collaboration on reversible sessions between Francesco Tiezzi at the University of Camerino (IT) and Nobuko Yoshida at Imperial College London (UK). The main topic of the work carried out in the STSM concerned a variant of the reversible session-based pi-calculus with commit and rollback primitives. Another aim of the STSM is to disseminate the achieved results on this topic in industrial contexts, in particular we visited the UK branch of Cognizant.
Improving reversible term rewriting through reachability analysis
Duration: Mar 17 - Mar 25, 2017
Location: Nagoya University (Japan)
Involved Reseachers: Naoki Nishida, German Vidal
During this STSM, we have studied different ways to improve our previous framework for reversible term rewriting. In particular, we have extended our original approach by introducing the use of a reachability analysis for conditional systems so that, when the right-hand sides of two functions do not have common reachable terms, they can be considered injective and no additional instrumentation is required. We have also considered a formalisation of dynamic updates, which is an essential feature of some functional languages like Erlang. Finally, we have also worked on the formal proofs of the uncontrolled reversible semantics for Erlang, a joint work with Ivan Lanese (University of Bologna, Italy) and Adrian Palacios (Universitat Politecnica de Valencia, Spain).
Duration: Mar 17 - Mar 25, 2017
Location: Nagoya University (Japan)
Involved Reseachers: Naoki Nishida, German Vidal
During this STSM, we have studied different ways to improve our previous framework for reversible term rewriting. In particular, we have extended our original approach by introducing the use of a reachability analysis for conditional systems so that, when the right-hand sides of two functions do not have common reachable terms, they can be considered injective and no additional instrumentation is required. We have also considered a formalisation of dynamic updates, which is an essential feature of some functional languages like Erlang. Finally, we have also worked on the formal proofs of the uncontrolled reversible semantics for Erlang, a joint work with Ivan Lanese (University of Bologna, Italy) and Adrian Palacios (Universitat Politecnica de Valencia, Spain).
Parallel algorithms for invertible finite state machines
Duration: March 16 - 1 April, 2017
Location: Halmstad University (Sweden)
Involved Reseachers: Uraz Cengiz Turker, Mohammad Reza Mousavi
In the literature, it has been reported that invertible sequences can drastically reduce the time of constructing state identification sequences. However to our knowledge the problem of generating invertible sequences has not been investigated in the literature. We investigated and proposed four algorithms that can construct invertible sequences. Besides, we introduced an educated seed selection algorithm for constructing UIO sequences which is currently evaluated.
Duration: March 16 - 1 April, 2017
Location: Halmstad University (Sweden)
Involved Reseachers: Uraz Cengiz Turker, Mohammad Reza Mousavi
In the literature, it has been reported that invertible sequences can drastically reduce the time of constructing state identification sequences. However to our knowledge the problem of generating invertible sequences has not been investigated in the literature. We investigated and proposed four algorithms that can construct invertible sequences. Besides, we introduced an educated seed selection algorithm for constructing UIO sequences which is currently evaluated.
Direct translation between universal reversible gate sets
Duration: Apr 6 - Apr 13 2017
Location: Horia Hulubei National Institute of Physics and Nuclear Engineering, Bucuresti (Romania)
Involved Reseachers: Alexandru Paler, Radu Ionicioiu
Universal quantum gate sets are investigated from at least two perspectives: their application to fault-tolerant large scale circuits (Clifford+T) and their relation to reversible Boolean functions (Toffoli + H). The problem of translating between quantum universal gate sets, such as Toffoli+H and Clifford+T, can be reformulated as the problem of "investigating the implementation of quantum gate sets on boson samplers". The problems have an equivalent formulation. The quest of building large scale quantum computers requires an efficient mapping of the algorithms to the hardware: use as few hardware as possible. Therefore, can boson samplers be used to implement any quantum algorithm?
Duration: Apr 6 - Apr 13 2017
Location: Horia Hulubei National Institute of Physics and Nuclear Engineering, Bucuresti (Romania)
Involved Reseachers: Alexandru Paler, Radu Ionicioiu
Universal quantum gate sets are investigated from at least two perspectives: their application to fault-tolerant large scale circuits (Clifford+T) and their relation to reversible Boolean functions (Toffoli + H). The problem of translating between quantum universal gate sets, such as Toffoli+H and Clifford+T, can be reformulated as the problem of "investigating the implementation of quantum gate sets on boson samplers". The problems have an equivalent formulation. The quest of building large scale quantum computers requires an efficient mapping of the algorithms to the hardware: use as few hardware as possible. Therefore, can boson samplers be used to implement any quantum algorithm?
Grant Period 3 (May 1, 2017 -- Apr 30, 2018)
Quantum Machine Learning and Topological Quantum Computation
Duration: Sep 23 - Sep 30 2017
Location: University of Verona (Italy)
Involved Reseachers: Rajagopal Nagarajan (applicant, UK), David Windridge (applicant, UK), Alessandra di Pierro (Verona), Riccardo Mengoni (Verona)
The aim of this STSM was to further develop joint work on Topological Quantum Computation and Machine Learning. In recent work, we presented a novel technique for the calculation of Hamming Distance of two binary strings via Topological Quantum Computation. In particular, we translated an encoding of the Hamming distance into a link invariant problem, which enables topological quantum computation to be applied. This was a first step towards the study of topological quantum algorithmic techniques for kernel based methods in Machine Learning. This visit has helped consolidate this work and will lead to further development. In particular, we were able to investigate ideas for possible generalisations of our techniques to string/graph edit distance and their associated kernels. We also did further research towards using quantum machine learning techniques for error correcting output codes, which aim to solve multi-class classification problems based on combining binary classifiers.
Duration: Sep 23 - Sep 30 2017
Location: University of Verona (Italy)
Involved Reseachers: Rajagopal Nagarajan (applicant, UK), David Windridge (applicant, UK), Alessandra di Pierro (Verona), Riccardo Mengoni (Verona)
The aim of this STSM was to further develop joint work on Topological Quantum Computation and Machine Learning. In recent work, we presented a novel technique for the calculation of Hamming Distance of two binary strings via Topological Quantum Computation. In particular, we translated an encoding of the Hamming distance into a link invariant problem, which enables topological quantum computation to be applied. This was a first step towards the study of topological quantum algorithmic techniques for kernel based methods in Machine Learning. This visit has helped consolidate this work and will lead to further development. In particular, we were able to investigate ideas for possible generalisations of our techniques to string/graph edit distance and their associated kernels. We also did further research towards using quantum machine learning techniques for error correcting output codes, which aim to solve multi-class classification problems based on combining binary classifiers.
Reversibility in Petri Nets with Step Sequence Semantics
Duration: Oct 7 - Oct 15 2017
Location: Universidad Complutense de Madrid (Spain)
Involved Reseachers: David de Frutos Escrig (host, Spain), Maciej Koutny (UK), Łukasz Mikulski (applicant, Poland)
Studying in depth the relation between the existence of pure solution of a transition system and possibility of reversing all its transitions leads to very interesting outcomes. We first concentrated on acyclic transition systems with a single sink, where possibility of introducing strict reverses for all action turns out to be equivalent with the solvability of reversed transition system. Considering a special case of binary systems without conflicts (see Barylska et al., On Binary Words Being Petri Net Solvable) we obtained a complete characterization of all such systems which might be reversed (without splitting). It turned out that the completely new technique have been invented. For the efficient synthesis of nets corresponding to binary sequences the only existing efficient technique was to check whether a given word contains one of the forbidden factors (see Erofeev at al., On Binary Words Being Petri Net Solvable and Best at al., Characterising Petri Net Solvable Binary Words) with quadratic solutions as the best of existing results. In contrast, the new technique utilizes our structural characterization and allows to check directly whether a word is synthesizable in linear time complexity.
Duration: Oct 7 - Oct 15 2017
Location: Universidad Complutense de Madrid (Spain)
Involved Reseachers: David de Frutos Escrig (host, Spain), Maciej Koutny (UK), Łukasz Mikulski (applicant, Poland)
Studying in depth the relation between the existence of pure solution of a transition system and possibility of reversing all its transitions leads to very interesting outcomes. We first concentrated on acyclic transition systems with a single sink, where possibility of introducing strict reverses for all action turns out to be equivalent with the solvability of reversed transition system. Considering a special case of binary systems without conflicts (see Barylska et al., On Binary Words Being Petri Net Solvable) we obtained a complete characterization of all such systems which might be reversed (without splitting). It turned out that the completely new technique have been invented. For the efficient synthesis of nets corresponding to binary sequences the only existing efficient technique was to check whether a given word contains one of the forbidden factors (see Erofeev at al., On Binary Words Being Petri Net Solvable and Best at al., Characterising Petri Net Solvable Binary Words) with quadratic solutions as the best of existing results. In contrast, the new technique utilizes our structural characterization and allows to check directly whether a word is synthesizable in linear time complexity.
Reliability and Fault-Tolerance by Choreographic Design
Duration: Oct 22 - Oct 28 2017
Location: IMT Lucca, Lucca, Italy
Involved Reseachers: Ian Cassar (applicant), Claudio Antares Mezzina
Distributed programs are hard to get right because they are required to be open, scalable, long-running, and tolerant to faults. In particular, the recent approaches to distributed software based on (micro-)services where different services are developed independently by disparate teams exacerbate the problem. In fact, services are meant to be composed together and run in open context where unpredictable behaviours can emerge. This makes it necessary to adopt suitable strategies for monitoring the execution and incorporate recovery and adaptation mechanisms so to make distributed programs more flexible and robust. The typical approach that is currently adopted is to embed such mechanisms in the program logic, which makes it hard to extract, compare and debug. We propose an approach that employs formal abstractions for specifying failure recovery and adaptation strategies. Although implementation agnostic, these abstractions would be amenable to algorithmic synthesis of code, monitoring and tests. We consider message-passing programs (a la Erlang, Go, or MPI) that are gaining momentum both in academia and industry. Our research agenda consists of (1) the definition of formal behavioural models encompassing failures, (2) the specification of the relevant properties of adaptation and recovery strategy, (3) the automatic generation of monitoring, recovery, and adaptation logic in target languages of interest.
Duration: Oct 22 - Oct 28 2017
Location: IMT Lucca, Lucca, Italy
Involved Reseachers: Ian Cassar (applicant), Claudio Antares Mezzina
Distributed programs are hard to get right because they are required to be open, scalable, long-running, and tolerant to faults. In particular, the recent approaches to distributed software based on (micro-)services where different services are developed independently by disparate teams exacerbate the problem. In fact, services are meant to be composed together and run in open context where unpredictable behaviours can emerge. This makes it necessary to adopt suitable strategies for monitoring the execution and incorporate recovery and adaptation mechanisms so to make distributed programs more flexible and robust. The typical approach that is currently adopted is to embed such mechanisms in the program logic, which makes it hard to extract, compare and debug. We propose an approach that employs formal abstractions for specifying failure recovery and adaptation strategies. Although implementation agnostic, these abstractions would be amenable to algorithmic synthesis of code, monitoring and tests. We consider message-passing programs (a la Erlang, Go, or MPI) that are gaining momentum both in academia and industry. Our research agenda consists of (1) the definition of formal behavioural models encompassing failures, (2) the specification of the relevant properties of adaptation and recovery strategy, (3) the automatic generation of monitoring, recovery, and adaptation logic in target languages of interest.
Left-to-right sweeping reversible block rules for cellular automata
Duration: Nov 12 - Nov 18 2017
Location: University of Turku, Turku (Finland)
Involved Reseachers: Jarkko Kari, Ville Salo, Thomas Worsch (applicant)
During the STSM we continued the work begun during Ville Salo's STSM at Karlsruhe last November considering sequential updating of one-dimensional CA by full left-to-right (or right-to-left) sweep with a reversible block rule. The global CA functions which can be realized in this way are now precisely characterized using the concept of left-closing (right-closing) CA and a divisibility condition. This also includes some CA which are not reversible.
The hierarchies resulting from composing alternately LR and RL sweeping rules and from composing alternately left-closing and right-closing CA are not known to be proper. But we could prove that the numbers of levels in the two hierarchies differ by at most 1.
We also had look at a concept of homotopies for cellular automata which was conceived during the STSM in 2016. An interesting byproduct of one of the basic constructions involved seems to be the description of a ``Nakamura-like'' transfer from synchronous to (general) asynchronous CA which requires only a linear increase of the number of states (instead of a quadratic blowup) if some reversibility is involved.
Duration: Nov 12 - Nov 18 2017
Location: University of Turku, Turku (Finland)
Involved Reseachers: Jarkko Kari, Ville Salo, Thomas Worsch (applicant)
During the STSM we continued the work begun during Ville Salo's STSM at Karlsruhe last November considering sequential updating of one-dimensional CA by full left-to-right (or right-to-left) sweep with a reversible block rule. The global CA functions which can be realized in this way are now precisely characterized using the concept of left-closing (right-closing) CA and a divisibility condition. This also includes some CA which are not reversible.
The hierarchies resulting from composing alternately LR and RL sweeping rules and from composing alternately left-closing and right-closing CA are not known to be proper. But we could prove that the numbers of levels in the two hierarchies differ by at most 1.
We also had look at a concept of homotopies for cellular automata which was conceived during the STSM in 2016. An interesting byproduct of one of the basic constructions involved seems to be the description of a ``Nakamura-like'' transfer from synchronous to (general) asynchronous CA which requires only a linear increase of the number of states (instead of a quadratic blowup) if some reversibility is involved.
Reversible Computation in Petri Nets
Duration: Nov 19 - Dec 2 2017
Location: Nicolaus Copernicus University, Torun (Poland)
Involved Reseachers: Anna Philippou, Kyriaki Psara (applicant), Lukasz Mikulski
The purpose of this STSM was to couple reversible computation with modelling languages that can potentially be useful in the formal layout and analysis of systems outside Computer Science. During the course of the STSM, we worked on formulating a structural translation of the model of Reversible Petri nets (RPNs) to the general model of Coloured Petri Nets (CPNs) that embeds reversible computation. As future work we plan on implementing an algorithmic translation that transforms RPNs to CPNs in an automated manner using the transformation techniques discussed during the course of the STSM. A challenging future work is to formally prove the equivalence between the RPNs and the resulting CPNs by investigating the expressiveness relationship between them and their associated trade-offs in terms of memory, expressiveness and usability. We aim to prove the soundness of our translation and demonstrate by example how the implementation of this model can be used to analyse systems from biochemistry that also embed cycles.
Duration: Nov 19 - Dec 2 2017
Location: Nicolaus Copernicus University, Torun (Poland)
Involved Reseachers: Anna Philippou, Kyriaki Psara (applicant), Lukasz Mikulski
The purpose of this STSM was to couple reversible computation with modelling languages that can potentially be useful in the formal layout and analysis of systems outside Computer Science. During the course of the STSM, we worked on formulating a structural translation of the model of Reversible Petri nets (RPNs) to the general model of Coloured Petri Nets (CPNs) that embeds reversible computation. As future work we plan on implementing an algorithmic translation that transforms RPNs to CPNs in an automated manner using the transformation techniques discussed during the course of the STSM. A challenging future work is to formally prove the equivalence between the RPNs and the resulting CPNs by investigating the expressiveness relationship between them and their associated trade-offs in terms of memory, expressiveness and usability. We aim to prove the soundness of our translation and demonstrate by example how the implementation of this model can be used to analyse systems from biochemistry that also embed cycles.
Expressivity and reasoning techniques for reversible concurrency
Duration: Nov 26 - Dec 2 2017
Location: University of Groningen, Groningen (The Netherlands)
Involved Reseachers: Claudio Antares Mezzina (applicant), Jorge A. Pérez
In recent works [1,2] we have proposed the monitor as memory approach to enable reversibility in communication-centric software systems. In communication-centric software systems, protocols specify the intended communication structures among interacting components. Our idea is to use monitors (e.g.,run-time entities that enact protocol actions) as the memories needed to record and undo communication steps. There is a monitor for each protocol participant; the monitor includes a session type that describes the intended protocol. As shown by [1] modalities can be added to type information in order to control reversibility. We have improved the results of [1] by adding parallel composition to global types, and by extending [1] with modalities [2]. Our goal is to compare the obtained framework with [3].
[1] Claudio Antares Mezzina, Jorge A. Pérez: Reversibility in session-based concurrency: A fresh look. J. Log. Algebr. Meth. Program. 90: 2-30 (2017)
[2] Claudio Antares Mezzina and Jorge A. Pérez. Causally consistent reversible choreographies. In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming PPDP. ACM, 2017.
[3] Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini: Concurrent Reversible Sessions: 28th International Conference on Concurrency
Duration: Nov 26 - Dec 2 2017
Location: University of Groningen, Groningen (The Netherlands)
Involved Reseachers: Claudio Antares Mezzina (applicant), Jorge A. Pérez
In recent works [1,2] we have proposed the monitor as memory approach to enable reversibility in communication-centric software systems. In communication-centric software systems, protocols specify the intended communication structures among interacting components. Our idea is to use monitors (e.g.,run-time entities that enact protocol actions) as the memories needed to record and undo communication steps. There is a monitor for each protocol participant; the monitor includes a session type that describes the intended protocol. As shown by [1] modalities can be added to type information in order to control reversibility. We have improved the results of [1] by adding parallel composition to global types, and by extending [1] with modalities [2]. Our goal is to compare the obtained framework with [3].
[1] Claudio Antares Mezzina, Jorge A. Pérez: Reversibility in session-based concurrency: A fresh look. J. Log. Algebr. Meth. Program. 90: 2-30 (2017)
[2] Claudio Antares Mezzina and Jorge A. Pérez. Causally consistent reversible choreographies. In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming PPDP. ACM, 2017.
[3] Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini: Concurrent Reversible Sessions: 28th International Conference on Concurrency
Reversibility on Session-based Communications
Duration: Dev 5 - Dec 12 2017
Location: Affiliation, Country: University of Camerino, (Italy)
Involved Reseachers: Nobuko Yoshida (applicant), Rumyana Neykova (applicant), Francesco Tiezzi
The purpose of this STSM was to study an extension of session types as to specify and verify reversible communication. For the binary session types, we modelled a new reversible calculus and session types for multiple participants with commitment and roll back primitives. Rollbacks and commits are explicitly specified in the process syntax. We define semantics for backward and forward computation. We study an extension of the concept of duality since the usual duality is too strong. For the global level, we follow the standard top-down approach in MPST. The extension is straightforward once the binary framework is completed. We also gave a department talk, presenting our recent work on reversible inference for Go programs which is an extension of the work presented in POPL’17. We discussed the framework and how it can be extended to apply model checking approaches and the program analysis. We obtained useful feedback and questions from the audience.
Duration: Dev 5 - Dec 12 2017
Location: Affiliation, Country: University of Camerino, (Italy)
Involved Reseachers: Nobuko Yoshida (applicant), Rumyana Neykova (applicant), Francesco Tiezzi
The purpose of this STSM was to study an extension of session types as to specify and verify reversible communication. For the binary session types, we modelled a new reversible calculus and session types for multiple participants with commitment and roll back primitives. Rollbacks and commits are explicitly specified in the process syntax. We define semantics for backward and forward computation. We study an extension of the concept of duality since the usual duality is too strong. For the global level, we follow the standard top-down approach in MPST. The extension is straightforward once the binary framework is completed. We also gave a department talk, presenting our recent work on reversible inference for Go programs which is an extension of the work presented in POPL’17. We discussed the framework and how it can be extended to apply model checking approaches and the program analysis. We obtained useful feedback and questions from the audience.
Weakly irreversible automata models
Duration: Dec 10 - Dec 23 2017
Location: Justus-Liebig Universität Giessen (Germany)
Involved Reseachers: Bruno Guillon (applicant), Martin Kutrib, Andreas Malcher, Giovanni Pighizzini, Luca Prigioniero
Weakly irreversible devices can reverse their computation, at any point, by having bounded local access to the input. During this STSM we studied:
Duration: Dec 10 - Dec 23 2017
Location: Justus-Liebig Universität Giessen (Germany)
Involved Reseachers: Bruno Guillon (applicant), Martin Kutrib, Andreas Malcher, Giovanni Pighizzini, Luca Prigioniero
Weakly irreversible devices can reverse their computation, at any point, by having bounded local access to the input. During this STSM we studied:
- Closure properties of the class of weakly irreversible languages: we obtained the non-closure of the class under most of the natural operations, with the exception of intersection, and, if allowing several initial states, union and reversal.
- Finite union of weakly irreversible languages: we obtained non-closure of the class for most of the natural operations.
- Reversible (length-preserving) pushdown transducers (realtime, synchronous, or asynchronous variants), that extend transducers by adding a pushdown store.
- Symmetric pushdown automata: symmetry is a notion close to reversibility, that asks for a model to admit history backward transitions. We developed a symmetrizing procedure that, given an input device, produces a symmetric device by adding a minimal amount of transitions. In some case, this procedure preserves acceptance.
Reversibility Applications of Reversible Computations in Petri Nets
Duration: Jan 14 - Jan 20 2018
Location: Newcastle University (UK)
Involved Reseachers: Maciej Koutny (host), Łukasz Mikulski (applicant), David de Frutos Escrig
During the STSM we have investigated Petri net solutions of binary linear transition systems and possibility of their reversing. We have prepared a complete scientific article and submitted it to the conference ATPN’18. We have also discussed the multiset semantics in Petri nets from the viewpoint of reversibility.
We have obtained an algebraic characterization of studied reversible systems (RS), which except from a specified collection of special cases, is equal to parts of cyclic solvable systems. In addition, we obtained similar algebraic characterizations of the following classes of binary linear transitions systems: cyclic solvable (CS), parts of cyclic solvable (PCS), and solvable (S). We have proposed linear algorithms for deciding membership problem in all of those classes and concluded that CS Ì PCS Ì RS Ì S (with all those inclusions strict). The new algorithms improves previously obtained solutions (which were at least quadratic).
Duration: Jan 14 - Jan 20 2018
Location: Newcastle University (UK)
Involved Reseachers: Maciej Koutny (host), Łukasz Mikulski (applicant), David de Frutos Escrig
During the STSM we have investigated Petri net solutions of binary linear transition systems and possibility of their reversing. We have prepared a complete scientific article and submitted it to the conference ATPN’18. We have also discussed the multiset semantics in Petri nets from the viewpoint of reversibility.
We have obtained an algebraic characterization of studied reversible systems (RS), which except from a specified collection of special cases, is equal to parts of cyclic solvable systems. In addition, we obtained similar algebraic characterizations of the following classes of binary linear transitions systems: cyclic solvable (CS), parts of cyclic solvable (PCS), and solvable (S). We have proposed linear algorithms for deciding membership problem in all of those classes and concluded that CS Ì PCS Ì RS Ì S (with all those inclusions strict). The new algorithms improves previously obtained solutions (which were at least quadratic).
Reversible event structures defined by a general enabling relation
Duration: Feb 2 - Feb 25 2018
Location: Nagoya University (Japan)
Involved Reseachers: Irek Ulidowski (applicant) and Shoji Yuen (host)
We studied extensions of two forms of event structures with reversibility. The first were the asymmetric event structures. They are defined by the causality and precedence relations. The second were the event structures defined a general enabling relation. The reversible versions of these two event structures were studied, namely the RAESs (reversible asymmetric event structures) and the RESs (reversible event structures). We also explored their expressiveness in representing different forms of reversibility, namely backtracking, causal reversibility and out-of-causal reversibility.
A topic of reversing imperative programming languages with the interleaving parallel composition operator was also discussed. The aim was to consider which useful constructs to include, for example local variables and procedures.
Duration: Feb 2 - Feb 25 2018
Location: Nagoya University (Japan)
Involved Reseachers: Irek Ulidowski (applicant) and Shoji Yuen (host)
We studied extensions of two forms of event structures with reversibility. The first were the asymmetric event structures. They are defined by the causality and precedence relations. The second were the event structures defined a general enabling relation. The reversible versions of these two event structures were studied, namely the RAESs (reversible asymmetric event structures) and the RESs (reversible event structures). We also explored their expressiveness in representing different forms of reversibility, namely backtracking, causal reversibility and out-of-causal reversibility.
A topic of reversing imperative programming languages with the interleaving parallel composition operator was also discussed. The aim was to consider which useful constructs to include, for example local variables and procedures.
A Distributed Reversible Semantics for Erlang
Duration: Feb 4 - Feb 10 2018
Location: Universitat Politècnica de València (Spain)
Involved Reseachers: Ivan Lanese (applicant), Adrian Palacios, German Vidal
A distributed reversible semantics for Erlang was discussed, with the aim of improving the reversible debugger for Erlang presented in [1]. Other improvements were discussed as well: the possibility of instrumenting an Erlang program so to produce a trace allowing one to reproduce the faulty behavior in the debugger; the possibility of executing forward by selecting which action to perform first (including all its causes); the possibility of using more abstract and lightweight histories.
[1] Ivan Lanese, Naoki Nishida, Adrian Palacios and German Vidal. CauDEr: A Causal-Consistent Reversible Debugger for Erlang. In Fourteenth International Symposium on Functional and Logic Programming (FLOPS 2018).
Duration: Feb 4 - Feb 10 2018
Location: Universitat Politècnica de València (Spain)
Involved Reseachers: Ivan Lanese (applicant), Adrian Palacios, German Vidal
A distributed reversible semantics for Erlang was discussed, with the aim of improving the reversible debugger for Erlang presented in [1]. Other improvements were discussed as well: the possibility of instrumenting an Erlang program so to produce a trace allowing one to reproduce the faulty behavior in the debugger; the possibility of executing forward by selecting which action to perform first (including all its causes); the possibility of using more abstract and lightweight histories.
[1] Ivan Lanese, Naoki Nishida, Adrian Palacios and German Vidal. CauDEr: A Causal-Consistent Reversible Debugger for Erlang. In Fourteenth International Symposium on Functional and Logic Programming (FLOPS 2018).
Applying spectral techniques to logic synthesis for quantum computing
Duration: Feb 11 - Feb 20 2018
Location: CIIT Lab of Faculty of Electronic Engineering, University of Nis (Serbia)
Involved Reseachers: Giulia Meuli (applicant), Prof. Radomir S. Stanković, Prof. Milena Stanković, Dr. Suzana Stojković, Prof. Pawel Kerntopf, Prof. Kryzsztof Podolski
Together with all the participants many research subjects of common interest have been discussed in details. In particular: synthesis of reversible circuits exploiting the Walsh Hadamard domain, shared functional decision diagrams, hierarchical techniques, ESOP, PPRM; Walsh spectrum properties and invariant operations; rewriting of reversible circuits for quantum application (reduction of the quantum cost). These discussions opened to new directions of research, concerning the problem of applying spectral techniques to logic synthesis of reversible circuits for quantum and in particular to the synthesis framework lhrs in revkit. The following very promising applications have been found: use of an extended set of spectral invariant operation for equivalence classification, function costing using spectrum, use of Spectral Transform Decision Diagram. These topics show immediate applicability and promise very good results. Other topics have been discussed that require longer study as the application of the Haar spectrum and the use of universal circuits.
Duration: Feb 11 - Feb 20 2018
Location: CIIT Lab of Faculty of Electronic Engineering, University of Nis (Serbia)
Involved Reseachers: Giulia Meuli (applicant), Prof. Radomir S. Stanković, Prof. Milena Stanković, Dr. Suzana Stojković, Prof. Pawel Kerntopf, Prof. Kryzsztof Podolski
Together with all the participants many research subjects of common interest have been discussed in details. In particular: synthesis of reversible circuits exploiting the Walsh Hadamard domain, shared functional decision diagrams, hierarchical techniques, ESOP, PPRM; Walsh spectrum properties and invariant operations; rewriting of reversible circuits for quantum application (reduction of the quantum cost). These discussions opened to new directions of research, concerning the problem of applying spectral techniques to logic synthesis of reversible circuits for quantum and in particular to the synthesis framework lhrs in revkit. The following very promising applications have been found: use of an extended set of spectral invariant operation for equivalence classification, function costing using spectrum, use of Spectral Transform Decision Diagram. These topics show immediate applicability and promise very good results. Other topics have been discussed that require longer study as the application of the Haar spectrum and the use of universal circuits.
Using decision diagrams and spectral approaches for constructing classifications of reversible functions
Duration: Feb 11 - Feb 17 2018
Location: Dept. Computer Science, Faculty of Electronic Engineering, University of Nis, Nis (Serbia)
Involved Reseachers: Pawel Kerntopf (applicant), Krzysztof Podlaski (applicant), Radomir Stankovic, Milena Stankovic, Suzana Stojkovic, Meuili Guilia
Reed-Muller and Walsh spectra for selected balanced functions were generated. On that basis some properties of the Walsh spectrum for balanced Boolean functions of any number of variables have been derived. For example, we had described what values of spectral coefficients can appear in the above mentioned spectra for balanced Boolean functions and what values must not appear. This can lead to discovering similar properties of spectra for reversible functions since all component functions of reversible functions are balanced. On the other hand, the spectrum invariant operations that were discussed for selected functions can also lead to new classifications for balanced and reversible functions. The relationships between arithmetic/Walsh spectra and decision diagrams were also discussed. For some exemplary functions the decision diagrams were derived. The decision diagram for a given reversible function is built from decision diagrams of each of its component functions. We have shown that using arithmetic spectra and decision diagram for representation of reversible functions we obtain smaller number of nodes comparing to previously developed methods. This can lead to better synthesis methods.
Duration: Feb 11 - Feb 17 2018
Location: Dept. Computer Science, Faculty of Electronic Engineering, University of Nis, Nis (Serbia)
Involved Reseachers: Pawel Kerntopf (applicant), Krzysztof Podlaski (applicant), Radomir Stankovic, Milena Stankovic, Suzana Stojkovic, Meuili Guilia
Reed-Muller and Walsh spectra for selected balanced functions were generated. On that basis some properties of the Walsh spectrum for balanced Boolean functions of any number of variables have been derived. For example, we had described what values of spectral coefficients can appear in the above mentioned spectra for balanced Boolean functions and what values must not appear. This can lead to discovering similar properties of spectra for reversible functions since all component functions of reversible functions are balanced. On the other hand, the spectrum invariant operations that were discussed for selected functions can also lead to new classifications for balanced and reversible functions. The relationships between arithmetic/Walsh spectra and decision diagrams were also discussed. For some exemplary functions the decision diagrams were derived. The decision diagram for a given reversible function is built from decision diagrams of each of its component functions. We have shown that using arithmetic spectra and decision diagram for representation of reversible functions we obtain smaller number of nodes comparing to previously developed methods. This can lead to better synthesis methods.
Reversibility and delegation in multiparty session types
Duration: Feb 18 - Mar 03 2018
Location: INRIA, Sophia Antipolis (France)
Involved Reseachers: Ilaria Castellani, Paola Giannini (applicant)
During the STSM we worked on defining reversible global types that would allow the description of interaction protocols in which some of the participants may join the interaction only in some branches of a conversation. Standard global types do not allow such flexibility, and for describing these protocols multiple global types are needed. We defined a calculus in which in addition to “simple communications”, which are expected to happen (in some interaction), we also have “connecting communications” that instead may not happen. Our calculus and type system reflect this distinction. The main novelties of our calculus and type system are (1) Integration of reversibility constructs and connecting communications; (2) Proof of the properties of Session Fidelity and Forward and Backward Progress for well-typed networks. In future collaborations we plan to use connecting communications to integrate delegation with reversibility.
Duration: Feb 18 - Mar 03 2018
Location: INRIA, Sophia Antipolis (France)
Involved Reseachers: Ilaria Castellani, Paola Giannini (applicant)
During the STSM we worked on defining reversible global types that would allow the description of interaction protocols in which some of the participants may join the interaction only in some branches of a conversation. Standard global types do not allow such flexibility, and for describing these protocols multiple global types are needed. We defined a calculus in which in addition to “simple communications”, which are expected to happen (in some interaction), we also have “connecting communications” that instead may not happen. Our calculus and type system reflect this distinction. The main novelties of our calculus and type system are (1) Integration of reversibility constructs and connecting communications; (2) Proof of the properties of Session Fidelity and Forward and Backward Progress for well-typed networks. In future collaborations we plan to use connecting communications to integrate delegation with reversibility.
Different themes on Reversibility
Duration: Mar 04 - Mar 10 2018
Location: Leicester University (UK)
Involved Reseachers: Claudio Antares Mezzina (applicant), Irek Ulidoski, Emilio Tuosto
The STSM was structured into two sub-goals:
1. Choreographies for Automatic Recovery
With reversible choreographies it is possible to express, from a global point of view, the condition when the system should revert a computation. Starting from this idea, we have realised an Erlang compiler, compiling global graph directly into Erlang code. The idea of the code generation is to generate, for each participant of the choreography, an actor implementing its forward behaviour and a monitor which is in charge of implementing its reverse behaviour. In this way we can separate the application logic from the recovery logic of the system of the system, more importantly we rend the forward semantics independent from the backward.
2. Reversibility and testing equivalences
We have started investigating reverse testing equivalences in the setting of event structures. The first question we have started tackling is whether to allow for testing/reversing an event and letting the system to reach a possible conflicting future of the configuration or not. Another question we have started investigating is the possibility to reverse with a single step a single event, or a set of them (given they are independent). Naturally each of these possibilities will give rise to a different equivalence. We want to systematically investigate different reversible testing equivalences for stable configuration, trying to define the spectrum of all the possible testing equivalences for reversible systems.
Duration: Mar 04 - Mar 10 2018
Location: Leicester University (UK)
Involved Reseachers: Claudio Antares Mezzina (applicant), Irek Ulidoski, Emilio Tuosto
The STSM was structured into two sub-goals:
1. Choreographies for Automatic Recovery
With reversible choreographies it is possible to express, from a global point of view, the condition when the system should revert a computation. Starting from this idea, we have realised an Erlang compiler, compiling global graph directly into Erlang code. The idea of the code generation is to generate, for each participant of the choreography, an actor implementing its forward behaviour and a monitor which is in charge of implementing its reverse behaviour. In this way we can separate the application logic from the recovery logic of the system of the system, more importantly we rend the forward semantics independent from the backward.
2. Reversibility and testing equivalences
We have started investigating reverse testing equivalences in the setting of event structures. The first question we have started tackling is whether to allow for testing/reversing an event and letting the system to reach a possible conflicting future of the configuration or not. Another question we have started investigating is the possibility to reverse with a single step a single event, or a set of them (given they are independent). Naturally each of these possibilities will give rise to a different equivalence. We want to systematically investigate different reversible testing equivalences for stable configuration, trying to define the spectrum of all the possible testing equivalences for reversible systems.
Grant Period 4 (May 1, 2018 -- Apr 30, 2019)
Reversing Computations Modelled by Reversing Petri Nets
Duration: Sep 23 - Oct 6 2018
Location: University of Cyprus (Cyprus)
Involved Reseachers: Anna Gogolińska (applicant), Łukasz Mikulski (applicant), Anna Phillipou (host), Kyriaki Psara
One of the main results of the STMS are Low Level RPNs. In LLRPNs only three types of transitions are allowed:
For LLRPNs we prepared a few working examples of their transformation to CPNs. We also prepared a formal translation to CPNs. To properly translate LLRPNs to CPNs a few, new concepts were developed. In particular, we introduced idle tokens which allow to resign from sets of molecules as a color.
Duration: Sep 23 - Oct 6 2018
Location: University of Cyprus (Cyprus)
Involved Reseachers: Anna Gogolińska (applicant), Łukasz Mikulski (applicant), Anna Phillipou (host), Kyriaki Psara
One of the main results of the STMS are Low Level RPNs. In LLRPNs only three types of transitions are allowed:
- Transporting transition with one input and one output place;
- Bond creating transition with two input places and one output place;
- Bond creating transition with one input and one output place.
For LLRPNs we prepared a few working examples of their transformation to CPNs. We also prepared a formal translation to CPNs. To properly translate LLRPNs to CPNs a few, new concepts were developed. In particular, we introduced idle tokens which allow to resign from sets of molecules as a color.
Hardware for Acoustic Time Reversal using Reversible Circuits
Duration: Oct 29 - Nov 09 2018
Location: Institut Langevin, ESPCI, Paris (France)
Involved Reseachers: Harun Siljak (applicant, Trinity College Dublin), Mathias Fink (Institut Langevin, ESPCI) and Julien de Rosny (Institut Langevin, ESPCI)
This work comprises a part of the WG4 case study on reversibility in wireless communications. We investigated the challenges of a reversible circuit implementation of hardware in wave time reversal. The goal of this STSM was to develop a detailed reversible solution for an inherently reversible signal processing technique and offer a practical application of reversible computation. While we selected underwater acoustic communications as our use case, the concepts developed during the STSM apply to the general case of wave time reversal, different waves, different media and different uses the technique may have. We have analysed different ways of performing time reversal and developed reversible hardware solutions for each of the alternatives while analysing the information conservation properties of these approaches.
Duration: Oct 29 - Nov 09 2018
Location: Institut Langevin, ESPCI, Paris (France)
Involved Reseachers: Harun Siljak (applicant, Trinity College Dublin), Mathias Fink (Institut Langevin, ESPCI) and Julien de Rosny (Institut Langevin, ESPCI)
This work comprises a part of the WG4 case study on reversibility in wireless communications. We investigated the challenges of a reversible circuit implementation of hardware in wave time reversal. The goal of this STSM was to develop a detailed reversible solution for an inherently reversible signal processing technique and offer a practical application of reversible computation. While we selected underwater acoustic communications as our use case, the concepts developed during the STSM apply to the general case of wave time reversal, different waves, different media and different uses the technique may have. We have analysed different ways of performing time reversal and developed reversible hardware solutions for each of the alternatives while analysing the information conservation properties of these approaches.
Genetic Algorithms for Reversible Quantum Circuit Design
Duration: Feb 17 - Feb 24, 2019
Location: Nottingham Trent University (UK)
Involved Reseachers: Michael Mc Gettrick (applicant), Colin Wilmott
This research STSM was to continue and solidify the software developed by Richard Cant at Nottingham Trent University (who unfortunately passed away in 2018): This software (written in C++) uses genetic algorithms to construct (optimal) quantum circuits. Given as input an overall matrix that operates on the qubits, it constructs a circuit from elementary gates (Hadamard, Rotation, Control gates) that gives the same result. We developed a suite of test input files, and established that the software works correctly rewriting permutation operations on qubits in terms of elementary control-NOT gates. One interesting circuit the software produced was to re-write a cyclic permutation of three qubits not using a sequence of two SWAP gates.
We produced some basic documentation on the operation of the code, as it comes at the moment without any user interface. Some circuits built by the program raised another interesting question we are now examining as further collaboration: For permutations of qubits, in how many different ways can we sequence the elementary gates produced (by the program)?
Duration: Feb 17 - Feb 24, 2019
Location: Nottingham Trent University (UK)
Involved Reseachers: Michael Mc Gettrick (applicant), Colin Wilmott
This research STSM was to continue and solidify the software developed by Richard Cant at Nottingham Trent University (who unfortunately passed away in 2018): This software (written in C++) uses genetic algorithms to construct (optimal) quantum circuits. Given as input an overall matrix that operates on the qubits, it constructs a circuit from elementary gates (Hadamard, Rotation, Control gates) that gives the same result. We developed a suite of test input files, and established that the software works correctly rewriting permutation operations on qubits in terms of elementary control-NOT gates. One interesting circuit the software produced was to re-write a cyclic permutation of three qubits not using a sequence of two SWAP gates.
We produced some basic documentation on the operation of the code, as it comes at the moment without any user interface. Some circuits built by the program raised another interesting question we are now examining as further collaboration: For permutations of qubits, in how many different ways can we sequence the elementary gates produced (by the program)?
Reversible Computation - Extending Horizons of Computing
Links
Memorandum of UnderstandingCOST rules and guidelines
Contact
Irek Ulidowski
Management Committee Chair
Email
Ivan Lanese
Management Committee Vice Chair
Email
Veronica Gaspes
STSM Coordinator
Email
Jovanka Pantovic
ITC Conference Grant Coordinator
Email
Anna Philippou
COST Action Equality Chair
Email
Ralph Stuebner
COST Science Officer
Email
Michael Kirkedal Thomsen
COST Action Website Chair
Email
Irek Ulidowski
Management Committee Chair
Ivan Lanese
Management Committee Vice Chair
Veronica Gaspes
STSM Coordinator
Jovanka Pantovic
ITC Conference Grant Coordinator
Anna Philippou
COST Action Equality Chair
Ralph Stuebner
COST Science Officer
Michael Kirkedal Thomsen
COST Action Website Chair