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. We characterise the transition relations induced by the coalgebraic model, observing the differences between the first two models. Furthermore by imposing conditions on history dependent automata, this model is shown to become equivalent to the sheaf-theoretic coalgebraic model