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.