LFCS Seminar: Tuesday 30 April-Marco Bernardo

Title: A Process Algebraic Theory of Reversible Systems

Abstract:

Reversibility is the capability of a system of undoing its own actions starting from

the last performed one, in such a way that a past consistent state is reached.

This is not trivial in the case of concurrent systems, as the last performed action may

not be uniquely identifiable. There are several approaches to address causality-consistent

reversibility, some of which include a notion of forward-reverse bisimilarity. We first

present a process calculus for reversible sequential systems on which we investigate

compositionality properties, axiomatizations, and modal logic characterizations of

forward-reverse bisimilarity as well as of its two components, i.e., forward bisimilarity

and reverse bisimilarity, both in the strong case and in the weak case. Then we add

parallel composition and develop expansion laws for the considered equivalences, with

forward bisimilarity being interleaving while reverse and forward-reverse bisimilarities

being truly concurrent.