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.
|Title of host publication||Computer Performance Evaluation.Modelling Techniques and Tools|
|Subtitle of host publication||11th International Conference, TOOLS 2000 Schaumburg, IL, USA, March 27–31, 2000 Proceedings|
|Editors||Boudewijn R. Haverkort, Henrik C. Bohnenkamp, Connie U. Smith|
|Number of pages||15|
|Publication status||Published - 2000|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer Berlin / Heidelberg|