Exploiting Modal Logic to Express Performance Measures

Graham Clark, Stephen Gilmore, Jane Hillston, Marina Ribaudo

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


Stochastic process algebras such as PEPA provide ample support for the component-based construction of models. Tools compute the numerical solution of these models; however, the stochastic process algebra methodology has lacked support for the specification and calculation of complex performance measures. In this paper we present a stochastic modal logic which can aid the construction of a reward structure over the model. We discuss its relationship to the underlying theory of PEPA. We also present a performance specification language which supports high level reasoning about PEPA models, and allows queries about their equilibrium behaviour. The meaning of the specification language has its foundations in the stochastic modal logic. We describe the implementation of the logic within the PEPA Workbench and a case study is presented to illustrate the approach.
Original languageEnglish
Title of host publicationComputer Performance Evaluation.Modelling Techniques and Tools
Subtitle of host publication11th International Conference, TOOLS 2000 Schaumburg, IL, USA, March 27–31, 2000 Proceedings
EditorsBoudewijn R. Haverkort, Henrik C. Bohnenkamp, Connie U. Smith
PublisherSpringer-Verlag GmbH
Number of pages15
ISBN (Electronic)978-3-540-46429-7
ISBN (Print)978-3-540-67260-9
Publication statusPublished - 2000

Publication series

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


Dive into the research topics of 'Exploiting Modal Logic to Express Performance Measures'. Together they form a unique fingerprint.

Cite this