Deriving Weak Bisimulation Congruences from Reduction Systems

The focus of process calculi is interaction rather than computation, and for this very reason: (i) their operational semantics is conveniently expressed by labelled transition systems (LTSs) whose labels model the possible interacth the environment; (ii) their abstract semantics is conveniently expressed by observational congruences. However, many current-day process calculi are more easily equipped with reduction semantics, where the notion of observable action is missing. Recent techniques attempted to bridge this gap by synthesising LTSs whose labels are process contexts that enable reactions and for which bisimulation is a congruence. Starting from Sewell’s set-theoretic construction, category-theoretic techniques were defined and based on Leifer and Milner’s relative pushouts, later refined by Sassone and the fourth author to deal with structural congruences given as groupoidal 2-categories. Building on recent works concerning observational equivalences for tile logic, the p...

• Type: Conference
• Year: 2005
• Where: CONCUR
• Authors: Roberto Bruni, Fabio Gadducci, Ugo Montanari, Pawel Sobocinski
• Keywords: CONCUR 2005, Current-day Process Calculi, Observational Congruence, Process Calculi