Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
P. G. Harrison and N. M. Patel. Performance Modelling of Communication Networks and Computer Architectures. International Computer Science Series. Addison-Wesley, 1993.
M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis. Modelling with Generalized Stochastic Petri Nets. John Wiley, 1995.
J.F. Meyer, A. Movaghar, and W.H. Sanders. Stochastic activity networks: Structure, behavior and application. In Proc of Int. Workshop on Timed Petri Nets, pages 106–115, Torino, Italy, 1985. IEEE Computer Society Press.
J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.
N. Götz, U. Herzog, and M. Rettelbach. Multiprocessor and Distributed System Design: The Integration of Functional Specification and Performance Analysis using Stochastic Process Algebras. In Performance’93, 1993.
M. Bernardo and R. Gorrieri. A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time. Theoretical Computer Science, 201:1–54, July 1998.
R. A. Howard. Dynamic Probabilistic Systems, volume II: Semi-Markov and Decision Processes, chapter 13, pages 851–915. John Wiley & Sons, New York, 1971.
J. Bryans, H. Bowman, and J. Derrick. Analysis of a Multimedia Stream using Stochastic Process Algebra. In C. Priami, editor, Proc. of 6th Int. Workshop on Process Algebras and Performance Modelling, pages 51–69, Nice, France, September 1998.
H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512–535, 1994.
M. Huth and M. Kwiatkowska. Quantitative analysis and model checking. In Proceedings, Twelth Annual IEEE Symposium on Logic in Computer Science, pages 111–122, Warsaw, Poland, 29 June–2 July 1997. IEEE Computer Society Press.
V. Hartonas-Garmhausen. Probabilistic Symbolic Model Checking with Engineering Models and Applications. PhD thesis, Carnegie Mellon University, 1998.
L. de Alfaro. How to specify and verify the long-run average behavior of probabilistic systems. In LICS: IEEE Symposium on Logic in Computer Science, 1998.
S. Gilmore and J. Hillston. The PEPA Workbench: A Tool to Support a Process Algebra-based Approach to Performance Modelling. In G. Haring and G. Kotsis, editors, Proc. of 7th Conf. on Mod. Techniques and Tools for Computer Perf. Eval., volume 794 of LNCS, pages 353–368, 1994.
G. Clark. Formalising the Specification of Rewards with PEPA. In Proc. of 4th Process Algebras and Performance Modelling Workshop, pages 139–160, July 1996.
G. Clark, S. Gilmore, and J. Hillston. Specifying performance measures for PEPA. In J.P. Katoen, editor, Proc. of 5th Int. AMAST Workshop on Real-Time and Probabilistic Systems, volume 1601 of LNCS, pages 211–227, Bamberg, Germany, 1999. Springer-Verlag.
S. Gilmore, J. Hillston, and M. Ribaudo. An efficient algorithm for aggregating PEPA models. To appear in IEEE Transactions on Software Engineering, 2000.
G. Clark, S. Gilmore, J. Hillston, and N. Thomas. Experiences with the PEPA Performance Modelling Tools. IEE Proceedings—Software, 146(1):11–19, February 1999. Special issue of papers from 14th UK Performance Engineering Workshop.
K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1–28, September 1991.
M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137–161, January 1985.
G. Clark. Techniques for the Construction and Analysis of Algebraic Performance Models. PhD thesis, The University of Edinburgh, 2000.
M. Bernardo. An Algebra-Based Method to Associate Rewards with EMPA Terms. In P. Degano, R. Gorrieri, and A. Marchetti Spaccamela, editors, 24th Int. Colloquium on Automata, Languages and Programming, volume 1256 of LNCS, pages 358–368, Bologna, Italy, July 1997. Springer-Verlag.
C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous time Markov chains. In Proceedings of CONCUR’99, volume 1664 of LNCS, pages 146–162, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Clark, G., Gilmore, S., Hillston, J., Ribaudo, M. (2000). Exploiting Modal Logic to Express Performance Measures. In: Haverkort, B.R., Bohnenkamp, H.C., Smith, C.U. (eds) Computer Performance Evaluation.Modelling Techniques and Tools. TOOLS 2000. Lecture Notes in Computer Science, vol 1786. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46429-8_18
Download citation
DOI: https://doi.org/10.1007/3-540-46429-8_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67260-9
Online ISBN: 978-3-540-46429-7
eBook Packages: Springer Book Archive