[12-08] Seminar: A compositional semantics for the reversible pi-calculus
Rerversible operational semantics for concurrent systems is quite intensively studied in the context of debugging or in order to realize safe transactional systems, where rollback is necessary to undo partial transactions that failed to terminate. The main difficulty is that backtracking in concurrent systems (where there is no global ordering of events) needs to be done consistently with causality. In compositional semantics (SOS style) the definition of causality becomes non trivial for calculi with extrusion mechanisms such as the pi-calculus. In this talk we present a fully compositional and reversible semantics for the (full) pi-calculus. This reversible language relies on a characterization of causality in the presence of contextual events that differ for the pre existing definitions of causality from the 90's. In particular we propose some correctness criteria to characterize "compositional" causality by means of sound over-approximation.