×

Performance measure sensitive congruences for Markovian process algebras. (English) Zbl 1019.68065

Summary: The modeling and analysis experience with process algebras has shown the necessity of extending them with priority, probabilistic internal/external choice, and time while preserving compositionality. The purpose of this paper is to make a further step by introducing a way to express performance measures, in order to allow the modeler to capture the QoS metrics of interest. We show that the standard technique of expressing stationary and transient performance measures as weighted sums of state probabilities and transition frequencies can be imported in the process algebra framework. Technically speaking, if we denote by \(n\) \(\in N\) the number of performance measures of interest, in this paper we define a family of extended Markovian process algebras with generative master-reactive slaves synchronization mechanism called \(\text{EMPA}_{\text{gr}_{n}}\) including probabilities, priorities, exponentially distributed durations, and sequences of rewards of length \(n.\) Then we show that the Markovian bisimulation equivalence \(\sim_{MB_{n}}\) is a congruence for \(\text{EMPA}_{\text{gr}_{n}}\) which preserves the specified performance measures and we give a sound and complete axiomatization for finite \(\text{EMPA}_{\text{gr}_{n}}\) terms. Finally, we present a case study conducted with the software tool TwoTowers in which we contrast the average performance of a selection of distributed algorithms for mutual exclusion modeled with \(\text{EMPA}_{\text{gr}_{n}}\).

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

PEPA
Full Text: DOI

References:

[1] Ajmone Marsan, M.; Balbo, G.; Conte, G.; Donatelli, S.; Franceschinis, G., Modelling with Generalized Stochastic Petri Nets (1995), Wiley: Wiley New York · Zbl 0843.68080
[2] C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen, On the logical characterisation of performability properties, Proc. 27th Internat. Colloq. on Automata, Languages and Programming (ICALP ’00), Lecture Notes in Computer Science, Vol. 1853, Geneve, Switzerland, 2000, pp. 780-792.; C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen, On the logical characterisation of performability properties, Proc. 27th Internat. Colloq. on Automata, Languages and Programming (ICALP ’00), Lecture Notes in Computer Science, Vol. 1853, Geneve, Switzerland, 2000, pp. 780-792. · Zbl 0973.68014
[3] C. Baier, J.-P. Katoen, H. Hermanns, Approximate symbolic model checking of continuous time Markov chains, Proc. 10th Internat. Conf. on Concurrency Theory (CONCUR ’00), Lecture Notes in Computer Science, Vol. 1664, Eindhoven, The Netherlands, 1999, pp. 146-162.; C. Baier, J.-P. Katoen, H. Hermanns, Approximate symbolic model checking of continuous time Markov chains, Proc. 10th Internat. Conf. on Concurrency Theory (CONCUR ’00), Lecture Notes in Computer Science, Vol. 1664, Eindhoven, The Netherlands, 1999, pp. 146-162. · Zbl 0934.03044
[4] M. Bernardo, An algebra-based method to associate rewards with EMPA terms, Proc. 24th Internat. Colloq. on Automata, Languages and Programming (ICALP ’97), Lecture Notes in Computer Science, Vol. 1256, Bologna, Italy, 1997, pp. 358-368.; M. Bernardo, An algebra-based method to associate rewards with EMPA terms, Proc. 24th Internat. Colloq. on Automata, Languages and Programming (ICALP ’97), Lecture Notes in Computer Science, Vol. 1256, Bologna, Italy, 1997, pp. 358-368. · Zbl 1401.68222
[5] M. Bernardo, Theory and application of extended Markovian process algebra, Ph.D. Thesis, University of Bologna, Italy, 1999 (; M. Bernardo, Theory and application of extended Markovian process algebra, Ph.D. Thesis, University of Bologna, Italy, 1999 (
[6] M. Bernardo, W.R. Cleaveland, S.T. Sims, W.J. Stewart, TwoTowers: a tool integrating functional and performance analysis of concurrent systems, Proc. IFIP Joint Internat. Conf. on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing and Verification (FORTE/PSTV ’98), Kluwer, Paris, France, 1998, pp. 457-467.; M. Bernardo, W.R. Cleaveland, S.T. Sims, W.J. Stewart, TwoTowers: a tool integrating functional and performance analysis of concurrent systems, Proc. IFIP Joint Internat. Conf. on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing and Verification (FORTE/PSTV ’98), Kluwer, Paris, France, 1998, pp. 457-467.
[7] M. Bravetti, A. Aldini, An asynchronous calculus for generative-reactive probabilistic systems, Tech. Report UBLCS-2000-03, University of Bologna (Italy), 2000 (extended abstract in Proc. 8th Internat. Workshop on Process Algebra and Performance Modelling (PAPM ’00), Carleton Scientific, Geneva, Switzerland, 2000, pp. 591-605).; M. Bravetti, A. Aldini, An asynchronous calculus for generative-reactive probabilistic systems, Tech. Report UBLCS-2000-03, University of Bologna (Italy), 2000 (extended abstract in Proc. 8th Internat. Workshop on Process Algebra and Performance Modelling (PAPM ’00), Carleton Scientific, Geneva, Switzerland, 2000, pp. 591-605).
[8] M. Bravetti, M. Bernardo, Compositional asymmetric cooperations for process algebras with probabilities, priorities, and time, Tech. Report UBLCS-2000-01, University of Bologna, Italy, 2000 (extended abstract Proc. 1st Internat. Workshop on Models for Time Critical Systems (MTCS ’00), Electronic Notes in Theoretical Computer Science, Vol. 39(3), State College, PA, 2000).; M. Bravetti, M. Bernardo, Compositional asymmetric cooperations for process algebras with probabilities, priorities, and time, Tech. Report UBLCS-2000-01, University of Bologna, Italy, 2000 (extended abstract Proc. 1st Internat. Workshop on Models for Time Critical Systems (MTCS ’00), Electronic Notes in Theoretical Computer Science, Vol. 39(3), State College, PA, 2000). · Zbl 0970.68114
[9] Ciardo, G.; Muppala, J.; Trivedi, K. S., On the solution of GSPN reward models, Performance Evaluation, 12, 237-253 (1991) · Zbl 0754.60097
[10] G. Clark, Formalising the specification of rewards with PEPA, Proc. 4th Workshop on Process Algebras and Performance Modelling (PAPM ’96), CLUT, Torino, Italy, 1996, pp. 139-160.; G. Clark, Formalising the specification of rewards with PEPA, Proc. 4th Workshop on Process Algebras and Performance Modelling (PAPM ’96), CLUT, Torino, Italy, 1996, pp. 139-160.
[11] G. Clark, S. Gilmore, J. Hillston, Specifying performance measures for PEPA, Proc. 5th AMAST Internat. Workshop on Formal Methods for Real Time and Probabilistic Systems (ARTS ’99), Lecture Notes in Computer Science, Vol. 1601, Bamberg, Germany, 1999, pp. 211-227.; G. Clark, S. Gilmore, J. Hillston, Specifying performance measures for PEPA, Proc. 5th AMAST Internat. Workshop on Formal Methods for Real Time and Probabilistic Systems (ARTS ’99), Lecture Notes in Computer Science, Vol. 1601, Bamberg, Germany, 1999, pp. 211-227.
[12] Clarke, E. M.; Grumberg, O.; Peled, D. A., Model Checking (1999), MIT Press: MIT Press Cambridge, MA
[13] W.R. Cleaveland, G. Lüttgen, V. Natarajan, Priority in Process Algebras, Handbook of Process Algebra, Elsevier, 2001.; W.R. Cleaveland, G. Lüttgen, V. Natarajan, Priority in Process Algebras, Handbook of Process Algebra, Elsevier, 2001.
[14] W.R. Cleaveland, S. Sims, The NCSU concurrency workbench, Proc. 8th Internat. Conf. on Computer Aided Verification (CAV ’96), Lecture Notes in Computer Science, Vol. 1102, New Brunswick, NJ, 1996, pp. 394-397.; W.R. Cleaveland, S. Sims, The NCSU concurrency workbench, Proc. 8th Internat. Conf. on Computer Aided Verification (CAV ’96), Lecture Notes in Computer Science, Vol. 1102, New Brunswick, NJ, 1996, pp. 394-397.
[15] Courtois, P. J., Decomposability: Queueing and Computer System Applications (1977), Academic Press: Academic Press New York · Zbl 0368.68004
[16] De Nicola, R.; Hennessy, M. C.B., Testing equivalences for processes, Theoret. Comput. Sci., 34, 83-133 (1983) · Zbl 0985.68518
[17] van Glabbeek, R. J.; Smolka, S. A.; Steffen, B., Reactive, generative and stratified models of probabilistic processes, Inform. Comput., 121, 59-80 (1995) · Zbl 0832.68042
[18] Haverkort, B. R.; Trivedi, K. S., Specification techniques for Markov reward models, Discrete Event Dyn. Systems: Theory Appl., 3, 219-247 (1993) · Zbl 0777.68029
[19] H. Hermanns, Leistungsvorhersage von Verhaltensbeschreibungen mittels Temporale Logik, contribution to the GI/ITG Fachgespraech ’95: Formale Beschreibungstechniken fuer Verteilte Systeme, 1995.; H. Hermanns, Leistungsvorhersage von Verhaltensbeschreibungen mittels Temporale Logik, contribution to the GI/ITG Fachgespraech ’95: Formale Beschreibungstechniken fuer Verteilte Systeme, 1995.
[20] H. Hermanns, Interactive Markov chains, Ph.D. Thesis, University of Erlangen-Nürnberg, Germany, 1998.; H. Hermanns, Interactive Markov chains, Ph.D. Thesis, University of Erlangen-Nürnberg, Germany, 1998. · Zbl 0937.60065
[21] Hillston, J., A Compositional Approach to Performance Modelling (1996), Cambridge University Press: Cambridge University Press Cambridge
[22] Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0637.68007
[23] Howard, R. A., Dynamic Probabilistic Systems (1971), Wiley: Wiley New York · Zbl 0227.90031
[24] Kleinrock, L., Queueing Systems (1975), Wiley: Wiley New York · Zbl 0334.60045
[25] Larsen, K. G.; Skou, A., Bisimulation through probabilistic testing, Inform. Comput., 94, 1-28 (1991) · Zbl 0756.68035
[26] Lynch, N. A., Distributed Algorithms (1996), Morgan Kaufmann Publishers: Morgan Kaufmann Publishers Los Alamos, CA · Zbl 0877.68061
[27] Meyer, J. F., Performabilitya retrospective and some pointers to the future, Performance Evaluation, 14, 139-156 (1992) · Zbl 0749.68014
[28] Milner, R., Communication and Concurrency (1989), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[29] Qureshi, M. A.; Sanders, W. H., Reward model solution methods with impulse and rate rewardsan algorithm and numerical results, Performance Evaluation, 20, 413-436 (1994) · Zbl 0941.68518
[30] Sanders, W. H.; Meyer, J. F., A unified approach for specifying measures of performance, dependability, and performability, Dependable Comput. Fault Tolerant Systems, 4, 215-237 (1991)
[31] R. Segala, Modeling and verification of randomized distributed real-time systems, Ph.D. Thesis, MIT, Boston, MA, 1995.; R. Segala, Modeling and verification of randomized distributed real-time systems, Ph.D. Thesis, MIT, Boston, MA, 1995.
[32] Stewart, W. J., Introduction to the Numerical Solution of Markov Chains (1994), Princeton University Press: Princeton University Press Princeton · Zbl 0821.65099
[33] Tofts, C. M.N., Processes with probabilities, priority and time, Formal Aspects Comput., 6, 536-564 (1994) · Zbl 0820.68072
[34] Trivedi, K. S.; Muppala, J. K.; Woolet, S. P.; Haverkort, B. R., Composite performance and dependability analysis, Performance Evaluation, 14, 197-215 (1992) · Zbl 0757.90028
[35] Vissers, C. A.; Scollo, G.; van Sinderen, M.; Brinksma, E., Specification styles in distributed systems design and verification, Theoret. Comput. Sci., 89, 179-206 (1991) · Zbl 0772.68065
[36] Wu, S.-H.; Smolka, S. A.; Stark, E. W., Composition and behaviors of probabilistic I/O automata, Theoret. Comput. Sci., 176, 1-38 (1997) · Zbl 0903.68123
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.