The Topos of Labelled Trees: A Categorical Semantics for SCCS

Article type: Research Article

Authors: Kasangian, Stefano | Vigna, Sebastiano

Affiliations: Dipartimento di Scienze dell'Informazione Università Ca' Foscari di Venezia Venezia, Italy kasan@vmimat.mat.unimi.it | Dipartimento di Scienze dell'Informazione Università degli Studi di Milano Milano, Italy vigna@dsi.unimi.it

Abstract: In this paper a we give a semantics for SCCS using the constructions of the topos of labelled trees. The semantics accounts for all aspects of the original formulation of SCCS, including unbounded non-determinism. Then, a partial solution to the problem of characterizing bisimulation in terms of a class of morphisms is proposed. We define a class of morphisms of the topos of trees, called conflict preserving, such that two trees T and U are bisimilar iff there is a pair of conflict preserving morphisms f : T → U and g : U → T such that fgf = f and gfg = g. It is the first characterization which does not require the existence of a third quotient object. The results can be easily extended to more general transition systems.

Keywords: process algebras, semantics, category theory, topos theory

DOI: 10.3233/FI-1997-32102

Journal: Fundamenta Informaticae, vol. 32, no. 1, pp. 27-45, 1997