Comparing operational models of name-passing process calculi

AbstractWe study three operational models of name-passing process calculi: coalgebras on (pre)sheaves, indexed labelled transition systems, and history dependent automata. The coalgebraic model is considered both for presheaves over the category of finite sets and injections, and for its subcategory of atomic sheaves known as the Schanuel topos. Each coalgebra induces an indexed labelled transition system. Such transition systems are characterised, relating the coalgebraic approach to an existing model of name-passing. Further, we consider internal labelled transition systems within the sheaf topos, and axiomatise a class that is in precise correspondence with the coalgebraic and the indexed labelled transition system models. By establishing and exploiting the equivalence of the Schanuel topos with a category of named-sets, these internal labelled transition systems are also related to the theory of history dependent automata