{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T10:40:02Z","timestamp":1790851202701,"version":"4.1.0"},"reference-count":66,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,2,1]],"date-time":"2010-02-01T00:00:00Z","timestamp":1264982400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2010,2]]},"DOI":"10.1007\/s10703-009-0088-7","type":"journal-article","created":{"date-parts":[[2010,3,17]],"date-time":"2010-03-17T12:21:35Z","timestamp":1268828495000},"page":"1-36","source":"Crossref","is-referenced-by-count":21,"title":["Performability assessment by model checking of Markov reward models"],"prefix":"10.1007","volume":"36","author":[{"given":"Christel","family":"Baier","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lucia","family":"Cloth","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Boudewijn R.","family":"Haverkort","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2010,3,18]]},"reference":[{"key":"88_CR1","volume-title":"Modeling with generalised stochastic Petri nets","author":"M Ajmone Marsan","year":"1995","unstructured":"Ajmone Marsan M, Balbo G, Conte G, Donatelli S, Franceschinis G (1995) Modeling with generalised stochastic Petri nets. Wiley, New York"},{"key":"88_CR2","series-title":"Lecture notes in computer science","first-page":"88","volume-title":"Proceedings of the international workshop on formal modeling and analysis of timed systems (FORMATS\u201903)","author":"S Andova","year":"2003","unstructured":"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\u201903). Lecture notes in computer science, vol\u00a02791. Springer, Berlin, pp\u00a088\u2013104"},{"key":"88_CR3","unstructured":"Arns M, Buchholz P, Panchenko A (2008) On the numerical analysis of inhomogeneous continuous-time Markov chains. Technical report, University of Dortmund"},{"key":"88_CR4","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume-title":"Proceedings of the 8th international conference on computer aided verification (CAV\u201996)","author":"A Aziz","year":"1996","unstructured":"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\u201996). Lecture notes in computer science, vol\u00a01102. Springer, Berlin, pp\u00a0269\u2013276"},{"issue":"1","key":"88_CR5","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A Aziz","year":"2000","unstructured":"Aziz A, Sanwal K, Singhal V, Brayton R (2000) Model-checking continuous-time Markov chains. ACM Trans Comput Logic 1(1):162\u2013170","journal-title":"ACM Trans Comput Logic"},{"key":"88_CR6","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J-P (2008) Principles of model checking. MIT Press, Cambridge"},{"key":"88_CR7","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"Proceedings of the 10th international conference on concurrency theory (CONCUR\u201999)","author":"C Baier","year":"1999","unstructured":"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\u201999). Lecture notes in computer science, vol\u00a01664. Springer, Berlin, pp\u00a0146\u2013161"},{"key":"88_CR8","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1007\/10722167_28","volume-title":"Proceedings of the 12th international conference on computer aided verification (CAV\u201900)","author":"C Baier","year":"2000","unstructured":"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\u201900). Lecture notes in computer science, vol\u00a01855. Springer, Berlin, pp\u00a0358\u2013372"},{"key":"88_CR9","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"780","DOI":"10.1007\/3-540-45022-X_65","volume-title":"Proceedings of the 27th international colloquium on automata, languages and programming (ICALP\u201900)","author":"C Baier","year":"2000","unstructured":"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\u201900). Lecture notes in computer science, vol\u00a01853. Springer, Berlin, pp\u00a0780\u2013792"},{"issue":"6","key":"88_CR10","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C Baier","year":"2003","unstructured":"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\u2013541","journal-title":"IEEE Trans Softw Eng"},{"issue":"4","key":"88_CR11","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1109\/TSE.2007.36","volume":"33","author":"C Baier","year":"2007","unstructured":"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\u2013224","journal-title":"IEEE Trans Softw Eng"},{"issue":"6","key":"88_CR12","doi-asserted-by":"crossref","first-page":"540","DOI":"10.1109\/TC.1978.1675145","volume":"27","author":"MD Beaudry","year":"1978","unstructured":"Beaudry MD (1978) Performance-related reliability measures for computing systems. IEEE Trans Comput 27(6):540\u2013547","journal-title":"IEEE Trans Comput"},{"key":"88_CR13","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0166-5316(92)90007-4","volume":"14","author":"A Bobbio","year":"1992","unstructured":"Bobbio A, Roberti L (1992) Distribution of the minimal completion time of parallel tasks in multi-reward semi-Markov models. Perform Eval 14:239\u2013256","journal-title":"Perform Eval"},{"key":"88_CR14","doi-asserted-by":"crossref","unstructured":"Bobbio A, Telek M (1995) Markov regenerative SPN with non-overlapping activity cycles. In: Proceedings of the international IEEE performance and dependability symposium (PDS\u201995), pp\u00a0124\u2013133","DOI":"10.1109\/IPDS.1995.395811"},{"key":"88_CR15","volume-title":"Model checking","author":"E Clarke","year":"1999","unstructured":"Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge"},{"key":"88_CR16","unstructured":"Cloth L (2006) Model checking algorithms for Markov reward models. PhD thesis, University of Twente"},{"key":"88_CR17","first-page":"39","volume-title":"Proceedings of the Markov anniversary meeting (MAM\u201906)","author":"L Cloth","year":"2006","unstructured":"Cloth L, Haverkort BR (2006) Five performability algorithms: A\u00a0comparison. In: Proceedings of the Markov anniversary meeting (MAM\u201906). Boson Books, Raleigh, pp\u00a039\u201354"},{"key":"88_CR18","first-page":"722","volume-title":"International conference on dependable systems and networks (DSN\u201905)","author":"L Cloth","year":"2005","unstructured":"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\u201905). IEEE Press, New York, pp\u00a0722\u2013731"},{"key":"88_CR19","doi-asserted-by":"crossref","unstructured":"Cloth L, Jongerden MR, Haverkort BR (2007) Computing battery lifetime distributions. In: Proceedings of the international conference on dependable systems and networks (DSN\u201907), pp\u00a0780\u2013789","DOI":"10.1109\/DSN.2007.26"},{"key":"88_CR20","volume-title":"Queueing networks: exact computational analysis","author":"A Conway","year":"1989","unstructured":"Conway A, Georganas N (1989) Queueing networks: exact computational analysis. MIT Press, Cambridge"},{"issue":"2","key":"88_CR21","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1287\/ijoc.14.2.124.121","volume":"14","author":"MC Diniz","year":"2002","unstructured":"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\u2013131","journal-title":"INFORMS J Comput"},{"issue":"3","key":"88_CR22","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1109\/5.558710","volume":"85","author":"S Edwards","year":"1997","unstructured":"Edwards S, Lavagno L, Lee E, Sangiovanni-Vincentelli A (1997) Design of embedded systems: formal models, validation and synthesis. Proc IEEE 85(3):366\u2013390","journal-title":"Proc IEEE"},{"key":"88_CR23","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E Emerson","year":"1982","unstructured":"Emerson E, Clarke E (1982) Using branching time temporal logic to synthesize synchronization skeletons. Sci Comput Program 2:241\u2013266","journal-title":"Sci Comput Program"},{"key":"88_CR24","doi-asserted-by":"crossref","unstructured":"Etessam K, Kwiatkowska M, Vardi MY, Yannakakis M (2008) Multi-objective model checking of Markov decision processes. Log Methods Comput Sci 4(4)","DOI":"10.2168\/LMCS-4(4:8)2008"},{"issue":"4","key":"88_CR25","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1145\/42404.42409","volume":"31","author":"BL Fox","year":"1988","unstructured":"Fox BL, Glynn PW (1988) Computing Poisson probabilities. Commun ACM 31(4):440\u2013445","journal-title":"Commun ACM"},{"key":"88_CR26","volume-title":"Performance analysis of communication systems: modeling with non-Markovian stochastic Petri nets","author":"R German","year":"2000","unstructured":"German R (2000) Performance analysis of communication systems: modeling with non-Markovian stochastic Petri nets. Wiley, New York"},{"key":"88_CR27","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/12.75148","volume":"37","author":"A Goyal","year":"1988","unstructured":"Goyal A, Tantawi A (1988) A measure of guaranteed availability and its numerical evaluation. IEEE Trans Comput 37:25\u201332","journal-title":"IEEE Trans Comput"},{"key":"88_CR28","first-page":"357","volume-title":"Numerical solution of Markov chains","author":"WK Grassmann","year":"1991","unstructured":"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\u00a0357\u2013371"},{"issue":"2","key":"88_CR29","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1287\/opre.32.2.343","volume":"32","author":"D Gross","year":"1984","unstructured":"Gross D, Miller DR (1984) The randomization technique as a modeling tool and solution procedure for transient Markov processes. Oper Res 32(2):343\u2013361","journal-title":"Oper Res"},{"key":"88_CR30","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/11944836_29","volume-title":"Foundations of software technology and theoretical computer science (FSTTCS)","author":"M Gr\u00f6\u00dfer","year":"2006","unstructured":"Gr\u00f6\u00dfer 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\u00a04337. Springer, Berlin, pp\u00a0309\u2013320"},{"key":"88_CR31","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson H, Jonsson B (1994) A logic for reasoning about time and reliability. Form Asp Comput 6:512\u2013535","journal-title":"Form Asp Comput"},{"issue":"1","key":"88_CR32","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/0166-5316(93)90027-R","volume":"18","author":"BR Haverkort","year":"1993","unstructured":"Haverkort BR (1993) Approximate performability and dependability analysis using generalized stochastic Petri nets. Perform Eval 18(1):61\u201378","journal-title":"Perform Eval"},{"key":"88_CR33","first-page":"228","volume-title":"Proceedings of the 19th IEEE symposium on reliable distributed systems (SRDS\u201900)","author":"BR Haverkort","year":"2000","unstructured":"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\u201900). IEEE Press, New York, pp\u00a0228\u2013237"},{"key":"88_CR34","unstructured":"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\u201901), pp\u00a0105\u2013109"},{"key":"88_CR35","volume-title":"Performability modelling","year":"2001","unstructured":"Haverkort BR, Marie R, Rubino G, Trivedi KS (eds) (2001) Performability modelling. Wiley, New York"},{"key":"88_CR36","first-page":"102","volume-title":"Proceedings of the international conference on dependable systems and networks (DSN\u201902)","author":"BR Haverkort","year":"2002","unstructured":"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\u201902). IEEE Press, New York, pp\u00a0102\u2013112"},{"issue":"1\u20132","key":"88_CR37","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/S0304-3975(00)00305-4","volume":"274","author":"H Hermanns","year":"2002","unstructured":"Hermanns H, Herzog U, Katoen J-P (2002) Process algebra for performance evaluation. Theor Comput Sci 274(1\u20132):43\u201387","journal-title":"Theor Comput Sci"},{"key":"88_CR38","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511569951","volume-title":"A compositional approach to performance modeling","author":"J Hillston","year":"1996","unstructured":"Hillston J (1996) A compositional approach to performance modeling. Cambridge University Press, Cambridge"},{"key":"88_CR39","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1016\/S0377-2217(97)00028-3","volume":"105","author":"G Horton","year":"1998","unstructured":"Horton G, Kulkarni VG, Nicol DM, Trivedi KS (1998) Fluid stochastic Petri nets: Theory, applications, and solution techniques. Eur J Oper Res 105:184\u2013201","journal-title":"Eur J Oper Res"},{"key":"88_CR40","volume-title":"Proceedings of the 4th international conference on matrix analytic methods in stochastic models","author":"A Horvath","year":"2002","unstructured":"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"},{"key":"88_CR41","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in computer science","author":"M Huth","year":"2004","unstructured":"Huth M, Ryan M (2004) Logic in computer science, 2nd\u00a0edn. Cambridge University Press, Cambridge","edition":"2"},{"key":"88_CR42","first-page":"243","volume-title":"Proceedings of the 2nd international conference on the quantitative evaluation of systems (QEST\u201905)","author":"J-P Katoen","year":"2005","unstructured":"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\u201905). IEEE Press, New York, pp\u00a0243\u2013244"},{"key":"88_CR43","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/978-3-540-71209-1_9","volume-title":"Tools and algorithms for the construction and analysis of systems (TACAS)","author":"J-P Katoen","year":"2007","unstructured":"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\u00a04424. Springer, Berlin, pp\u00a087\u2013101"},{"key":"88_CR44","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal methods for performance evaluation","author":"M Kwiatkowska","year":"2007","unstructured":"Kwiatkowska M, Norman G, Parker D (2007) Stochastic model checking. In: Formal methods for performance evaluation. Lecture notes in computer science, vol\u00a04486. Springer, Berlin, pp\u00a0220\u2013270"},{"key":"88_CR45","first-page":"136","volume-title":"Quantitative evaluation of systems (QEST)","author":"VV Lam","year":"2004","unstructured":"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\u00a0136\u2013145"},{"key":"88_CR46","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF02481076","volume":"37","author":"T Matsunawa","year":"1985","unstructured":"Matsunawa T (1985) The exact and approximate distributions of linear combinations of selected order statistics from uniform distributions. Ann Inst Stat Math 37:1\u201316","journal-title":"Ann Inst Stat Math"},{"key":"88_CR47","series-title":"Lecture notes in computer science","first-page":"203","volume-title":"Formal modeling and analysis of timed systems (FORMATS)","author":"A Mereacre","year":"2008","unstructured":"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\u00a05215. Springer, Berlin, pp\u00a0203\u2013218"},{"issue":"8","key":"88_CR48","doi-asserted-by":"crossref","first-page":"720","DOI":"10.1109\/TC.1980.1675654","volume":"29","author":"JF Meyer","year":"1980","unstructured":"Meyer JF (1980) On evaluating the performability of degradable computing systems. IEEE Trans Comput 29(8):720\u2013731","journal-title":"IEEE Trans Comput"},{"issue":"7","key":"88_CR49","doi-asserted-by":"crossref","first-page":"648","DOI":"10.1109\/TC.1982.1676062","volume":"31","author":"JF Meyer","year":"1982","unstructured":"Meyer JF (1982) Closed-form solutions of performability. IEEE Trans Comput 31(7):648\u2013657","journal-title":"IEEE Trans Comput"},{"issue":"3","key":"88_CR50","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1016\/0166-5316(92)90002-X","volume":"14","author":"JF Meyer","year":"1992","unstructured":"Meyer JF (1992) Performability: a retrospective and some pointers to the future. Perform Eval 14(3):139\u2013156","journal-title":"Perform Eval"},{"key":"88_CR51","volume-title":"Performability modelling","author":"JF Meyer","year":"2001","unstructured":"Meyer JF, Sanders WH (2001) Specification and construction of performability models. In: Performability modelling. Wiley, New York"},{"key":"88_CR52","volume-title":"Matrix-geometric solutions in stochastic models. An algorithmic approach","author":"MF Neuts","year":"1994","unstructured":"Neuts MF (1994) Matrix-geometric solutions in stochastic models. An algorithmic approach. Dover, New York"},{"issue":"2","key":"88_CR53","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/s00165-005-0062-0","volume":"17","author":"G Norman","year":"2005","unstructured":"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\u2013176","journal-title":"Form Asp Comput"},{"issue":"3\u20134","key":"88_CR54","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1016\/S0166-5316(99)00010-3","volume":"35","author":"WD Obal II","year":"1999","unstructured":"Obal WD II, Sanders WH (1999) State-space support for path-based reward variables. Perform Eval 35(3\u20134):233\u2013251","journal-title":"Perform Eval"},{"key":"88_CR55","first-page":"83","volume-title":"Performability modelling","author":"KR Pattipati","year":"2001","unstructured":"Pattipati KR, Mallubhatla R, Gopalakrishna V, Viswanatham N (2001) Markov-reward models and hyperbolic systems. In: Performability modelling. Wiley, New York, pp\u00a083\u2013106"},{"key":"88_CR56","unstructured":"Qureshi MA (1992) Reward model solution methods with impulse and rate rewards: An algorithm and numerical results. Master\u2019s thesis, University of Arizona"},{"issue":"4","key":"88_CR57","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1016\/0166-5316(94)90061-2","volume":"20","author":"MA Qureshi","year":"1994","unstructured":"Qureshi MA, Sanders WH (1994) Reward model solution methods with impulse and rate rewards: an algorithm and numerical results. Perform Eval 20(4):413\u2013436","journal-title":"Perform Eval"},{"key":"88_CR58","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/978-3-540-31980-1_16","volume-title":"Proceedings of the 11th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201905)","author":"A Remke","year":"2005","unstructured":"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\u201905). Lecture notes in computer science, vol\u00a02440. Springer, Berlin, pp\u00a0237\u2013252"},{"key":"88_CR59","first-page":"7","volume-title":"First international conference on performance evaluation methodologies and tools","author":"A Remke","year":"2006","unstructured":"Remke A, Cloth L, Haverkort BR (2006) Uniformization with representatives\u2014comprehensive transient analysis of infinite-state QBDs. In: First international conference on performance evaluation methodologies and tools. ACM, New York, pp\u00a07\u201316"},{"issue":"1","key":"88_CR60","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/49.64901","volume":"9","author":"WH Sanders","year":"1991","unstructured":"Sanders WH, Meyer JF (1991) Reduced base model construction methods for stochastic activity networks. IEEE J Sel Areas Commun 9(1):25\u201336","journal-title":"IEEE J Sel Areas Commun"},{"issue":"5","key":"88_CR61","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1080\/15326340008807601","volume":"16","author":"B Sericola","year":"2000","unstructured":"Sericola B (2000) Occupation times in Markov processes. Commun Stat Stochastic Models 16(5):479\u2013510","journal-title":"Commun Stat Stochastic Models"},{"issue":"4","key":"88_CR62","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1109\/12.2184","volume":"37","author":"R Smith","year":"1988","unstructured":"Smith R, Trivedi KS, Ramesh A (1988) Performability analysis: Measures, an algorithm and a case study. IEEE Trans Comput 37(4):406\u2013417","journal-title":"IEEE Trans Comput"},{"key":"88_CR63","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-36577-X_29","volume-title":"Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201903)","author":"O Sokolsky","year":"2003","unstructured":"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\u201903). Lecture notes in computer science, vol\u00a02619. Springer, Berlin, pp\u00a0409\u2013425"},{"key":"88_CR64","volume-title":"Introduction to the numerical solution of Markov chains","author":"WJ Stewart","year":"1994","unstructured":"Stewart WJ (1994) Introduction to the numerical solution of Markov chains. Princeton University Press, Princeton"},{"key":"88_CR65","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/S0167-6377(00)00023-7","volume":"26","author":"H Tijms","year":"2000","unstructured":"Tijms H, Veldman R (2000) A fast algorithm for the transient reward distribution in continuous-time Markov chains. Oper Res Lett 26:155\u2013158","journal-title":"Oper Res Lett"},{"issue":"2","key":"88_CR66","doi-asserted-by":"crossref","first-page":"704","DOI":"10.1214\/aoms\/1177693419","volume":"42","author":"H Weisberg","year":"1971","unstructured":"Weisberg H (1971) The distribution of linear combinations of order statistics from the uniform distribution. Ann Inst Stat 42(2):704\u2013709","journal-title":"Ann Inst Stat"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0088-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-009-0088-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0088-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:05:51Z","timestamp":1559253951000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-009-0088-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,2]]},"references-count":66,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,2]]}},"alternative-id":["88"],"URL":"https:\/\/doi.org\/10.1007\/s10703-009-0088-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,2]]}}}