Structured coalgebras and minimal HD-automata for the -calculus |
| |
Authors: | Ugo Montanari Marco Pistore |
| |
Affiliation: | aComputer Science Department, University of Pisa, Corso Italia 40, 56100 Pisa, Italy;bDepartment of Information and Comm. Technology, University of Trento, Via Sommarive 14, 38050 Povo (Trento), Italy |
| |
Abstract: | The coalgebraic framework developed for the classical process algebras, and in particular its advantages concerning minimal realizations, does not fully apply to the π-calculus, due to the constraints on the freshly generated names that appear in the bisimulation.In this paper we propose to model the transition system of the π-calculus as a coalgebra on a category of name permutation algebras and to define its abstract semantics as the final coalgebra of such a category. We show that permutations are sufficient to represent in an explicit way fresh name generation, thus allowing for the definition of minimal realizations.We also link the coalgebraic semantics with 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. HD-automata associated with agents with a bounded number of threads in their derivatives are finite and can be actually minimized. We show that the bisimulation relation in the coalgebraic context corresponds to the minimal HD-automaton. |
| |
Keywords: | Concurrency and distributed computation π -calculus Categorical models and logics Coinductive techniques Automata theory |
本文献已被 ScienceDirect 等数据库收录! |
|