Freshness and name-restriction in sets of traces with names

Abstract

We use nominal sets (sets with names and binding) to define a framework for trace semantics with dynamic allocation of resources. Using novel constructions in nominal sets, including the technical devices of positive nominal sets and maximal planes, we define notions of capture-avoiding composition and name-restriction on sets of traces with names. We conclude with an extended version of Kleene algebras which summarises in axiomatic form the relevant properties of the constructions. © 2011 Springer-Verlag.