Oxford logo
[KN96b] M. Kwiatkowska and G. Norman. Metric Denotational Semantics for PEPA. In M. Ribaudo (editor), Proc. 4th Process Algebras and Performance Modelling Workshop (PAPM'96), pages 120-138, CLUT. July 1996. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (114 KB)  pdf pdf (240 KB)  bib bib
Abstract. Stochastic process algebras, which combine the features of a process calculus with stochastic analysis, were introduced to enable compositional performance analysis of systems. At the level of syntax, compositionality presents itself in terms of operators, which can be used to build more complex systems from simple components. Denotational semantics is a method for assigning to syntactic objects elements of a suitably chosen semantic domain. This is compositional in style, as operators are represented by certain functions on the domain, and often allows to gain additional insight by considering the properties of those functions. We consider Performance Evaluation Process Algebra (PEPA), a stochastic process algebra introduced by Hillston. Based on the methodology introduced by de Bakker and Zucker, we give denotational semantics to PEPA by means of a complete metric space of suitably enriched trees. We investigate continuity properties of the PEPA operators and show that our semantic domain is fully abstract with respect to strong equivalence.