A categorical model of the fusion calculus

Marino Miculan

Dipartimento di Matematica e Informatica
Università degli Studi di Udine

Thursday, 11 February 2010, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

Abstract: We provide a categorical presentation of the fusion calculus. Working in a suitable category of presheaves, we describe the syntax as initial algebra of a signature endofunctor, and the semantics as coalgebras of a "behaviour" endofunctor. To this end, we first give a a new, congruence-free presentation of the Fusion calculus; then, the behaviour endofunctor is constructed by adding in a systematic way a notion of "state" to the intuitive endofunctor induced by the LTS. Coalgebras can be given a concrete presentation as "stateful indexed labelled transition systems"; the bisimilarity over these systems is a congruence, and corresponds to hyperequivalence. Then, we model the labelled transition system of the fusion calculus by abstract categorical rules. As a consequence, we get a semantics for the fusion calculus which is both compositional and fully abstract: two processes have the same semantics if they are bisimilar, that is, hyperequivalent.

ERDF
Tarmo Uustalu
Last update 11 February 2010