 Abstract:

The finite picalculus has an explicit settheoretic functorcategory model that is known to be fully abstract for strong late bisimulation congruence. We characterize this as the initial free algebra for an appropriate set of operations and equations in the enriched Lawvere theories of Plotkin and Power. Thus we obtain a novel algebraic description for models of the picalculus, and validate an existing construction as the universal such model.
The algebraic operations are intuitive, covering name creation, communication of names over channels, and nondeterminism; the equations then combine these features in a modular fashion. We work in an enriched setting, over a "possible worlds" category of sets indexed by available names. This expands significantly on the classical notion of algebraic theories, and in particular allows us to use nonstandard arities that vary as processes evolve.
Based on our algebraic theory we describe a category of models for the picalculus, and show that they all preserve bisimulation congruence. We develop a direct construction of free models in this category; and generalise previous results to prove that all freealgebra models are fully abstract.
 Copyright:
 SpringerVerlag Berlin Heidelberg 2005
 Links To Paper
 Page by author
 Page by publisher
 Bibtex format
 @InProceedings{EDIINFRR0757,
 author = {
Ian Stark
},
 title = {FreeAlgebra Models for the PiCalculus},
 book title = {Proceedings of FoSSaCS 2005 (Foundations of Software Science and Computation Structure)},
 publisher = {Springer},
 year = 2005,
 month = {Apr},
 volume = {3441},
 pages = {155169},
 doi = {10.1007/b106850},
 url = {http://www.inf.ed.ac.uk/~stark/freamp.html},
 }
