Abstract of Paper

$\pi$-Calculus, Structured Coalgebras and Minimal HD-Automata
by Ugo Montanari and Marco Pistore

Abstract:

The ordinary notion of bisimulation for $\pi$-calculus agents contains
conditions about freshly generated names which make impossible to define the
bisimilarity class of an agent ``in isolation'', but require to make
reference to another agent, or at least to its free names. As a consequence,
the coalgebraic framework, and in particular its advantages concerning
minimal realizations, does not fully apply.

We propose to model $\pi$-calculus as a coalgebra on a category of name
permutation algebras (permutations are used to characterize in a general way
the free names of $\pi$-calculus agents) and to define its abstract
semantics as the final coalgebra of such a category. In the final coalgebra,
the ``free names'' associated to agents by the permutations define the set
of names that are ``active'' in the agents. Since equivalent agents have the
same active names, this result allows for the definition of a semantically
correct mechanism of name deallocation.

We also introduce a slightly improved version of history dependent (HD)
automata, a model developed for verification purposes, where states have
local names and transitions are decorated with names and name relations. We
show that, in this improved version of HD-automata, the bisimilarity
relation corresponds to the minimal automaton.  Moreover, automata
associated to agents with a bounded number of threads are finite and can be
actually minimized.