# 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 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).

**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.

**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.

**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.

**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.

**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:

- 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.

**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.

**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.

**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.

**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).

**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.

**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.

**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.

## Grant Period 2 (May 1, 2016 -- Apr 30, 2016)

**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.

**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.

**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.

**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).

**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.

**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.

**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

**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.

**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.

**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.

**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.

**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.

**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.

**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).

**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.

**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.

**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.

**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.

**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.

**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).

**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.

**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?

## Grant Period 3 (May 1, 2017 -- Apr 30, 2017)

**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.

**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.

**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.

**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.

**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.

**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

**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.

Reversible Computation - Extending Horizons of Computing

## Links

Memorandum of UnderstandingCOST rules and guidelines

**Contact**

**Irek Ulidowski**

Management Committee Chair

**Ivan Lanese**

Management Committee Vice Chair

**Veronica Gaspes**

STSM Coordinator

**Jovanka Pantovic**

COST Action Equality Chair

**Anna Philippou**

COST Policy Coordinator

**Ralph Stuebner**

COST Science Officer

**Michael Kirkedal Thomsen**

COST Action Website Chair