In this paper, we model fresh names in the pi-calculus using abstractions with respect to a new binding operator theta. Both the theory and the metatheory of the pi-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 theta-automaton.
Modeling Fresh Names in pi-calculus Using Abstractions
BRUNI, ROBERTO;
2004-01-01
Abstract
In this paper, we model fresh names in the pi-calculus using abstractions with respect to a new binding operator theta. Both the theory and the metatheory of the pi-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 theta-automaton.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
