Free-algebra models for the pi-calculus

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The finite pi-calculus has an explicit set-theoretic functor-category 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 pi-calculus, 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 pi-calculus, 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 free-algebra models are fully abstract.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computational Structures
EditorsVladimiro Sassone
Place of PublicationBerlin
PublisherSpringer-Verlag GmbH
Pages155-169
Number of pages15
ISBN (Electronic)978-3-540-31982-5
ISBN (Print)978-3-540-25388-4
DOIs
Publication statusPublished - 2005
Event8th International Conference on Foundations of Software Science and Computation Structures - Edinburgh
Duration: 4 Apr 20058 Apr 2005

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
Volume3441
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference8th International Conference on Foundations of Software Science and Computation Structures
CityEdinburgh
Period4/04/058/04/05

Keywords

  • notations
  • computation
  • monads

Cite this