In his categorical framework, Stark defines a domain-theoretic model for the π-calculus based on functor categories. Despite being a sound abstract model, a more concrete semantics is required if it is to be used as a basis for proving properties about mobile systems. In this paper, we concretize Stark’s denotational model for the π-calculus and provide a full definition of the semantic domains involved. We also include an example of how the model may be approximated in an abstract interpretation analysis.
Author and article information
School of Computer Applications
Dublin City University
Dublin 9, Ireland