CMCS 2004 Preliminary Version Modeling Fresh Names in the ss-calculus using Abstractions?

Abstract In this paper, we model fresh names in the ss-calculus using abstractions with respect to a new binding operator `. Both the theory and the metatheory of the ss-calculus benefit from this simple extension. The operational semantics of this new calculus is finitely branching. Bisimulation can be given without mentioning any constraint on names, thus allowing for a straightforward definition of a coalgebraic semantics, within a category of coalgebras over permutation algebras. Following previous work by Montanari and Pistore, we present also a finite representation for finitary processes and a finite state verification procedure for bisimilarity, based on the new notion of `-automaton