Forward-Reverse Observational Equivalences in CCSK

Ivan Lanese (1) , Iain Phillips (2)

1 FOCUS - Foundations of Component-based Ubiquitous Systems
2 Department of Computing [Imperial College London]

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

Mots clés: CCSK; Forward-reverse bisimilarity; Forward-reverse barbed congruence; Axiomatization

Domaines: Langage de programmation [cs.PL]; Théorie et langage formel [cs.FL]

Ivan Lanese, Iain Phillips. Forward-Reverse Observational Equivalences in CCSK. RC 2021 - 13th Conference on Reversible Computation, Jul 2021, Nagoya, Japan. pp.126 - 143, ⟨10.1007/978-3-030-79837-6_8⟩. ⟨hal-03338669⟩