Abstract
This paper describes efficient procedures for model checking Markov reward models, that allow us to evaluate, among others, the performability of computer-communication systems. We present the logic CSRL (Continuous Stochastic Reward Logic) to specify performability measures. It provides flexibility in measure specification and paves the way for the numerical evaluation of a wide variety of performability measures. The formal measure specification in CSRL also often helps in reducing the size of the Markov reward models that need to be numerically analysed. The paper presents background on Markov-reward models, as well as on the logic CSRL (syntax and semantics), before presenting an important duality result between reward and time. We discuss CSRL model-checking algorithms, and present five numerical algorithms and their computational complexity for verifying time- and reward-bounded until-properties, one of the key operators in CSRL. The versatility of our approach is illustrated through a performability case study.
Similar content being viewed by others
References
Ajmone Marsan M, Balbo G, Conte G, Donatelli S, Franceschinis G (1995) Modeling with generalised stochastic Petri nets. Wiley, New York
Andova S, Hermanns H, Katoen J-P (2003) Discrete-time rewards model-checked. In: Proceedings of the international workshop on formal modeling and analysis of timed systems (FORMATS’03). Lecture notes in computer science, vol 2791. Springer, Berlin, pp 88–104
Arns M, Buchholz P, Panchenko A (2008) On the numerical analysis of inhomogeneous continuous-time Markov chains. Technical report, University of Dortmund
Aziz A, Sanwal K, Singhal V, Brayton R (1996) Verifying continuous-time Markov chains. In: Proceedings of the 8th international conference on computer aided verification (CAV’96). Lecture notes in computer science, vol 1102. Springer, Berlin, pp 269–276
Aziz A, Sanwal K, Singhal V, Brayton R (2000) Model-checking continuous-time Markov chains. ACM Trans Comput Logic 1(1):162–170
Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge
Baier C, Katoen J-P, Hermanns H (1999) Approximate symbolic model checking of continuous-time Markov chains. In: Proceedings of the 10th international conference on concurrency theory (CONCUR’99). Lecture notes in computer science, vol 1664. Springer, Berlin, pp 146–161
Baier C, Haverkort BR, Hermanns H, Katoen J-P (2000) Model checking continuous-time Markov chains by transient analysis. In: Proceedings of the 12th international conference on computer aided verification (CAV’00). Lecture notes in computer science, vol 1855. Springer, Berlin, pp 358–372
Baier C, Haverkort BR, Hermanns H, Katoen J-P (2000) On the logical characterisation of performability properties. In: Proceedings of the 27th international colloquium on automata, languages and programming (ICALP’00). Lecture notes in computer science, vol 1853. Springer, Berlin, pp 780–792
Baier C, Haverkort BR, Hermanns H, Katoen J-P (2003) Model-checking algorithms for continuous-time Markov chains. IEEE Trans Softw Eng 29(6):524–541
Baier C, Cloth L, Haverkort BR, Kuntz M, Siegle M (2007) Model checking Markov chains with actions and state labels. IEEE Trans Softw Eng 33(4):209–224
Beaudry MD (1978) Performance-related reliability measures for computing systems. IEEE Trans Comput 27(6):540–547
Bobbio A, Roberti L (1992) Distribution of the minimal completion time of parallel tasks in multi-reward semi-Markov models. Perform Eval 14:239–256
Bobbio A, Telek M (1995) Markov regenerative SPN with non-overlapping activity cycles. In: Proceedings of the international IEEE performance and dependability symposium (PDS’95), pp 124–133
Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge
Cloth L (2006) Model checking algorithms for Markov reward models. PhD thesis, University of Twente
Cloth L, Haverkort BR (2006) Five performability algorithms: A comparison. In: Proceedings of the Markov anniversary meeting (MAM’06). Boson Books, Raleigh, pp 39–54
Cloth L, Katoen J-P, Khattri M, Pulungan R (2005) Model checking Markov reward models with impulse rewards. In: International conference on dependable systems and networks (DSN’05). IEEE Press, New York, pp 722–731
Cloth L, Jongerden MR, Haverkort BR (2007) Computing battery lifetime distributions. In: Proceedings of the international conference on dependable systems and networks (DSN’07), pp 780–789
Conway A, Georganas N (1989) Queueing networks: exact computational analysis. MIT Press, Cambridge
Diniz MC, de Souza e Silva E, Gail HR (2002) Calculating the distribution of a linear combination of uniform order statistics. INFORMS J Comput 14(2):124–131
Edwards S, Lavagno L, Lee E, Sangiovanni-Vincentelli A (1997) Design of embedded systems: formal models, validation and synthesis. Proc IEEE 85(3):366–390
Emerson E, Clarke E (1982) Using branching time temporal logic to synthesize synchronization skeletons. Sci Comput Program 2:241–266
Etessam K, Kwiatkowska M, Vardi MY, Yannakakis M (2008) Multi-objective model checking of Markov decision processes. Log Methods Comput Sci 4(4)
Fox BL, Glynn PW (1988) Computing Poisson probabilities. Commun ACM 31(4):440–445
German R (2000) Performance analysis of communication systems: modeling with non-Markovian stochastic Petri nets. Wiley, New York
Goyal A, Tantawi A (1988) A measure of guaranteed availability and its numerical evaluation. IEEE Trans Comput 37:25–32
Grassmann WK (1991) Finding transient solutions in Markovian event systems through randomization. In: Stewart W (ed) Numerical solution of Markov chains. Dekker, New York, pp 357–371
Gross D, Miller DR (1984) The randomization technique as a modeling tool and solution procedure for transient Markov processes. Oper Res 32(2):343–361
Größer M, Norman G, Baier C, Ciesinski F, Kwiatkowska MZ, Parker D (2006) On reduction criteria for probabilistic reward models. In: Foundations of software technology and theoretical computer science (FSTTCS). Lecture notes in computer science, vol 4337. Springer, Berlin, pp 309–320
Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Form Asp Comput 6:512–535
Haverkort BR (1993) Approximate performability and dependability analysis using generalized stochastic Petri nets. Perform Eval 18(1):61–78
Haverkort BR, Hermanns H, Katoen J-P (2000) On the use of model checking techniques for dependability evaluation. In: Proceedings of the 19th IEEE symposium on reliable distributed systems (SRDS’00). IEEE Press, New York, pp 228–237
Haverkort BR, Hermanns H, Katoen J-P, Baier C (2001) Model checking CSRL-specified performability properties. In: Proceedings of the 5th international workshop on performability modeling of computer and communications systems (PMCCS’01), pp 105–109
Haverkort BR, Marie R, Rubino G, Trivedi KS (eds) (2001) Performability modelling. Wiley, New York
Haverkort BR, Cloth L, Hermanns H, Katoen J-P, Baier C (2002) Model checking performability properties. In: Proceedings of the international conference on dependable systems and networks (DSN’02). IEEE Press, New York, pp 102–112
Hermanns H, Herzog U, Katoen J-P (2002) Process algebra for performance evaluation. Theor Comput Sci 274(1–2):43–87
Hillston J (1996) A compositional approach to performance modeling. Cambridge University Press, Cambridge
Horton G, Kulkarni VG, Nicol DM, Trivedi KS (1998) Fluid stochastic Petri nets: Theory, applications, and solution techniques. Eur J Oper Res 105:184–201
Horvath A, Gribaudo M (2002) Matrix geometric solution of fluid stochastic Petri nets. In: Proceedings of the 4th international conference on matrix analytic methods in stochastic models. World Scientific, Singapore
Huth M, Ryan M (2004) Logic in computer science, 2nd edn. Cambridge University Press, Cambridge
Katoen J-P, Khattri M, Zapreev IS (2005) A Markov reward model checker. In: Proceedings of the 2nd international conference on the quantitative evaluation of systems (QEST’05). IEEE Press, New York, pp 243–244
Katoen J-P, Kemna T, Zapreev I, Jansen DN (2007) Bisimulation minimisation mostly speeds up probabilistic model checking. In: Tools and algorithms for the construction and analysis of systems (TACAS). Lecture notes in computer science, vol 4424. Springer, Berlin, pp 87–101
Kwiatkowska M, Norman G, Parker D (2007) Stochastic model checking. In: Formal methods for performance evaluation. Lecture notes in computer science, vol 4486. Springer, Berlin, pp 220–270
Lam VV, Buchholz P, Sanders WH (2004) A structured path-based approach for computing transient rewards of large ctmcs. In: Quantitative evaluation of systems (QEST). IEEE Comput Soc, Los Alamitos, pp 136–145
Matsunawa T (1985) The exact and approximate distributions of linear combinations of selected order statistics from uniform distributions. Ann Inst Stat Math 37:1–16
Mereacre A, Katoen J-P (2008) Model checking HML on piecewise-constant inhomogeneous Markov chains. In: Formal modeling and analysis of timed systems (FORMATS). Lecture notes in computer science, vol 5215. Springer, Berlin, pp 203–218
Meyer JF (1980) On evaluating the performability of degradable computing systems. IEEE Trans Comput 29(8):720–731
Meyer JF (1982) Closed-form solutions of performability. IEEE Trans Comput 31(7):648–657
Meyer JF (1992) Performability: a retrospective and some pointers to the future. Perform Eval 14(3):139–156
Meyer JF, Sanders WH (2001) Specification and construction of performability models. In: Performability modelling. Wiley, New York
Neuts MF (1994) Matrix-geometric solutions in stochastic models. An algorithmic approach. Dover, New York
Norman G, Parker D, Kwiatkowska MZ, Shukla SK, Gupta R (2005) Using probabilistic model checking for dynamic power management. Form Asp Comput 17(2):160–176
Obal WD II, Sanders WH (1999) State-space support for path-based reward variables. Perform Eval 35(3–4):233–251
Pattipati KR, Mallubhatla R, Gopalakrishna V, Viswanatham N (2001) Markov-reward models and hyperbolic systems. In: Performability modelling. Wiley, New York, pp 83–106
Qureshi MA (1992) Reward model solution methods with impulse and rate rewards: An algorithm and numerical results. Master’s thesis, University of Arizona
Qureshi MA, Sanders WH (1994) Reward model solution methods with impulse and rate rewards: an algorithm and numerical results. Perform Eval 20(4):413–436
Remke A, Haverkort BR, Cloth L (2005) Model checking infinite-state Markov chains. In: Proceedings of the 11th international conference on tools and algorithms for the construction and analysis of systems (TACAS’05). Lecture notes in computer science, vol 2440. Springer, Berlin, pp 237–252
Remke A, Cloth L, Haverkort BR (2006) Uniformization with representatives—comprehensive transient analysis of infinite-state QBDs. In: First international conference on performance evaluation methodologies and tools. ACM, New York, pp 7–16
Sanders WH, Meyer JF (1991) Reduced base model construction methods for stochastic activity networks. IEEE J Sel Areas Commun 9(1):25–36
Sericola B (2000) Occupation times in Markov processes. Commun Stat Stochastic Models 16(5):479–510
Smith R, Trivedi KS, Ramesh A (1988) Performability analysis: Measures, an algorithm and a case study. IEEE Trans Comput 37(4):406–417
Sokolsky O, Philippou A, Lee I, Christou K (2003) Modeling and analysis of power-aware systems. In: Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of systems (TACAS’03). Lecture notes in computer science, vol 2619. Springer, Berlin, pp 409–425
Stewart WJ (1994) Introduction to the numerical solution of Markov chains. Princeton University Press, Princeton
Tijms H, Veldman R (2000) A fast algorithm for the transient reward distribution in continuous-time Markov chains. Oper Res Lett 26:155–158
Weisberg H (1971) The distribution of linear combinations of order statistics from the uniform distribution. Ann Inst Stat 42(2):704–709
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Baier, C., Cloth, L., Haverkort, B.R. et al. Performability assessment by model checking of Markov reward models. Form Methods Syst Des 36, 1–36 (2010). https://doi.org/10.1007/s10703-009-0088-7
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-009-0088-7