R. Bruni, F. Honsell, M. Lenisa, and M. Miculan
Modeling fresh names in pi-calculus using
abstractions
Technical Report TR-21-02, Dipartimento di Matematica e Informatica,
Università di Udine, Italy, 2002
In this paper, we model fresh names in the
pi-calculus using
abstractions w.r.t. 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.
This
is cast within a category of coalgebras over algebras with
infinitely many unary operators, in order to capitalize on
theta.
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. Finally, we improve
previous encodings of the pi-calculus in the Calculus of
Inductive Constructions.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43