|Abstract of Paper|
$\pi$-Calculus, Structured Coalgebras and Minimal HD-Automata
by Ugo Montanari and Marco Pistore
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.