Local names, memory and symmetry in operational semantics

In this talk we discuss a basic notion of memory and symmetry for labelled transition systems extended with local names and permutation groups over them. In particular, the issue of keeping these models finite in the presence of name allocation is considered. Symmetry arises in the obtained structures, due to locality of names.

Labelled transition systems provide a model for the operational semantics of programming languages. The semantic equivalence of the model is very often bisimilarity. However, when the language features a notion of resource and allocation (e.g. the "new" construct in object-oriented programming or the scope extrusion of the pi-calculus), ad-hoc notions of bisimilarity are needed.

These notions are recovered as standard constructions by resorting to coalgebras in a presheaf category or in nominal sets. By doing this, one gets a fully abstract semantics. However, a coalgebra can be infinite due to resource allocation. Finite models can be recovered in many cases by resorting to an equivalent categorical presentation, namely history-dependent automata, which are coalgebras in a free coproduct completion.

We will look at the computational interpretation of history-dependent automata, from the point of view that they are an enrichment of classical labelled transition systems with local names, name
generation and garbage collection of unused names. Surprisingly, when names are made local, an explicit notion of symmetry (expressed in terms of groups of isomorphisms of names) arises in the base category. We will see how the final coalgebra provides a notion of behavioural symmetry of a system.