{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T13:51:49Z","timestamp":1742392309148,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":59,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540442523"},{"type":"electronic","value":"9783540457985"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45798-4_12","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T01:42:40Z","timestamp":1183426960000},"page":"261-289","source":"Crossref","is-referenced-by-count":12,"title":["Automated Performance and Dependability Evaluation Using Model Checking"],"prefix":"10.1007","author":[{"given":"Christel","family":"Baier","sequence":"first","affiliation":[]},{"given":"Boudewijn","family":"Haverkort","sequence":"additional","affiliation":[]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,5]]},"reference":[{"issue":"1","key":"12_CR1","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A. Aziz","year":"2000","unstructured":"A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Model checking continuous time Markov chains. ACM Transactions on Computational Logic, 1(1): 162\u2013170, 2000.","journal-title":"ACM Transactions on Computational Logic"},{"key":"12_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"Concurrency Theory","author":"C. Baier","year":"1999","unstructured":"C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In Concurrency Theory, LNCS 1664: 146\u2013162, Springer-Verlag, 1999."},{"key":"12_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/10722167_28","volume-title":"Computer Aided Verification","author":"C. Baier","year":"2000","unstructured":"C. Baier, B.R. Haverkort, H. Hermanns, and J.-P. Katoen. Model checking continuous-time Markov chains by transient analysis. In Computer Aided Verification, LNCS 1855: 358\u2013372, Springer-Verlag, 2000."},{"key":"12_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"780","DOI":"10.1007\/3-540-45022-X_65","volume-title":"Automata, Languages, and Programming","author":"C. Baier","year":"2000","unstructured":"C. Baier, B.R. Haverkort, H. Hermanns, and J.-P. Katoen. On the logical characterisation of performability properties. In Automata, Languages, and Programming, LNCS 1853: 780\u2013792, Springer-Verlag, 2000."},{"key":"12_CR5","unstructured":"C. Baier, B.R. Haverkort, H. Hermanns, and J.-P. Katoen. Model checking algorithms for continuous-time Markov chains. Technical report TR-CTIT-02-10. Centre for Telematics and Information Technology, University of Twente. 2001."},{"issue":"2","key":"12_CR6","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0020-0190(98)00038-6","volume":"66","author":"C. Baier","year":"1998","unstructured":"C. Baier and M. Kwiatkowska. On the verification of qualitative properties of probabilistic processes under fairness constraints. Information Processing Letters, 66(2): 71\u201379, 1998.","journal-title":"Information Processing Letters"},{"key":"12_CR7","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1109\/TC.1978.1675145","volume":"C-27","author":"M. D. Beaudry","year":"1978","unstructured":"M. D. Beaudry. Performance-related reliability measures for computing systems. IEEE Transactions on Computers, C-27: 540\u2013547, 1978.","journal-title":"IEEE Transactions on Computers"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"B. B\u00e9rard, M. Bidoit, A. Finkel, F. Laroussine, A. Petit, L. Petrucci, and Ph. Schnoebelen. Systems and Software Verification. Springer-Verlag, 2001.","DOI":"10.1007\/978-3-662-04558-9"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"A. Bobbio and M. Telek. Markov regenerative SPN with non-overlapping activity cycles. In Proc. Int\u2019l IEEE Performance and Dependability Symposium: 124\u2013133, 1995.","DOI":"10.1109\/IPDS.1995.395811"},{"key":"12_CR10","doi-asserted-by":"publisher","first-page":"59","DOI":"10.2307\/3215235","volume":"31","author":"P. Buchholz","year":"1994","unstructured":"P. Buchholz. Exact and ordinary lumpability in finite Markov chains. Journal of Applied Probability, 31: 59\u201375, 1994.","journal-title":"Journal of Applied Probability"},{"key":"12_CR11","unstructured":"P. Buchholz, J.-P. Katoen, P. Kemper, and C. Tepper. Model checking large structured Markov chains. Journal of Logic and Algebraic Programming, to appear, 2001."},{"issue":"1\u20132","key":"12_CR12","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0166-5316(95)00008-L","volume":"24","author":"G. Chiola","year":"1995","unstructured":"G. Chiola, G. Franceschinis, R. Gaeta, and M. Ribaudo. GreatSPN 1.7: graphical editor and analyzer for timed and stochastic Petri nets. Performance Evaluation, 24(1\u20132):47\u201368, 1995.","journal-title":"Performance Evaluation"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"G. Ciardo, J.K. Muppala, and K.S. Trivedi. SPNP: stochastic Petri net package. In Proc. 3rd Int. Workshop on Petri Nets and Performance Models, pp. 142\u2013151, IEEE CS Press, 1989.","DOI":"10.1109\/PNPM.1989.68548"},{"key":"12_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/3-540-48778-6_13","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"G. Clark","year":"1999","unstructured":"G. Clark, S. Gilmore, and J. Hillston. Specifying performance measures for PEPA. In Formal Methods for Real-Time and Probabilistic Systems, LNCS 1601: 211\u2013227, Springer-Verlag, 1999."},{"key":"12_CR15","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"E. Clarke, E. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8: 244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"12_CR16","unstructured":"E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"issue":"6","key":"12_CR17","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/6.499951","volume":"33","author":"E. Clarke","year":"1996","unstructured":"E. Clarke and R. Kurshan. Computer-aided verification. IEEE Spectrum, 33(6): 61\u201367, 1996.","journal-title":"IEEE Spectrum"},{"key":"12_CR18","unstructured":"J. Desharnais and P. Panangaden. Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes. Journal of Logic and Algebraic Programming, to appear, 2001."},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"S. Derisavi, H. Hermanns, and W.H. Sanders. Optimal state space lumping in Markov models. 2002. submitted for publication.","DOI":"10.1016\/S0020-0190(03)00343-0"},{"key":"12_CR20","unstructured":"W. Feller. An Introduction to Probability Theory and its Applications. John Wiley & Sons, 1968."},{"key":"12_CR21","unstructured":"R. German. Performance Analysis of Communication Systems: Modeling with Non-Markovian Stochastic Petri Nets. John Wiley & Sons, 2000."},{"key":"12_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/3-540-58021-2_20","volume-title":"Computer Performance Evaluation, Modeling Techniques and Tools","author":"S. Gilmore","year":"1994","unstructured":"S. Gilmore and J. Hillston. The PEPA workbench: a tool to support a process algebra-based approach to performance modelling. In Computer Performance Evaluation, Modeling Techniques and Tools, LNCS 794: 353\u2013368, Springer-Verlag, 1994."},{"key":"12_CR23","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1109\/12.75148","volume":"37","author":"A. Goyal","year":"1988","unstructured":"A. Goyal and A.N. Tantawi. A measure of guaranteed availability and its numerical evaluation. IEEE Transactions on Computers, 37: 25\u201332, 1988.","journal-title":"IEEE Transactions on Computers"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"W.K. Grassmann. Finding transient solutions in Markovian event systems through randomization. In Numerical Solution of Markov Chains, pp. 357\u2013371, Marcel Dekker Inc, 1991.","DOI":"10.1201\/9781003210160-18"},{"issue":"2","key":"12_CR25","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1287\/opre.32.2.343","volume":"32","author":"D. Gross","year":"1984","unstructured":"D. Gross and D.R. Miller. The randomization technique as a modeling tool and solution procedure for transient Markov chains. Operations Research 32(2): 343\u2013361, 1984.","journal-title":"Operations Research"},{"key":"12_CR26","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"D. Harel. Statecharts: a visual formalism for complex systems. Science of Computer Programming, 8: 231\u2013274, 1987.","journal-title":"Science of Computer Programming"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"B.R. Haverkort. Performance of Computer Communication Systems: A Model-Based Approach. John Wiley & Sons, 1998.","DOI":"10.1002\/0470841923"},{"key":"12_CR28","unstructured":"B.R. Haverkort, R. Marie, G. Rubino, and K.S. Trivedi (editors). Performability Modelling: Techniques and Tools. John Wiley & Sons, 2001."},{"key":"12_CR29","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/0166-5316(94)00038-7","volume":"25","author":"B.R. Haverkort","year":"1996","unstructured":"B.R. Haverkort and I. Niemegeers. Performability modelling tools and techniques. Performance Evaluation, 25: 17\u201340, 1996.","journal-title":"Performance Evaluation"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"B.R. Haverkort, H. Hermanns, and J.-P. Katoen. The use of model checking techniques for quantitative dependability evaluation. In IEEE Symposium on Reliable Distributed Systems., pp. 228\u2013238. IEEE CS Press, 2000.","DOI":"10.1109\/RELDI.2000.885410"},{"key":"12_CR31","unstructured":"B.R. Haverkort, L. Cloth, H. Hermanns, J.-P. Katoen, and C. Baier. Model checking CSRL-specified performability properties. In 5th Int. Workshop on Performability Modeling of Computer and Communication Systems, Erlangen, Arbeitsberichte des IMMD, 34 (13), 2001. 2001."},{"key":"12_CR32","doi-asserted-by":"crossref","unstructured":"B.R. Haverkort, L. Cloth, H. Hermanns, J.-P. Katoen, and C. Baier. Model checking performability properties. In Proc. IEEE Int\u2019l Conference on Dependable Systems and Networks, IEEE CS press, 2002.","DOI":"10.1109\/DSN.2002.1028891"},{"key":"12_CR33","first-page":"135","volume":"74","author":"H. Hermanns","year":"2001","unstructured":"H. Hermanns. Construction and verfication of performance and reliability models. Bulletin of the EATCS, 74:135\u2013154, 2001.","journal-title":"Bulletin of the EATCS"},{"issue":"1\u20132","key":"12_CR34","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/S0304-3975(00)00305-4","volume":"274","author":"H. Hermanns","year":"2002","unstructured":"H. Hermanns, U. Herzog, and J.-P. Katoen. Process algebra for performance evaluation. Theoretical Computer Science, 274(1\u20132):43\u201387, 2002.","journal-title":"Theoretical Computer Science"},{"issue":"1\u20134","key":"12_CR35","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0166-5316(99)00056-5","volume":"39","author":"H. Hermanns","year":"2000","unstructured":"H. Hermanns, U. Herzog, U. Klehmet, V. Mertsiotakis, and M. Siegle. Compositional performance modelling with the TIPPtool. Performance Evaluation, 39(1\u20134): 5\u201335, 2000.","journal-title":"Performance Evaluation"},{"key":"12_CR36","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-46419-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Hermanns","year":"2000","unstructured":"H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. A Markov chain model checker. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1785: 347\u2013362, Springer-Verlag, 2000."},{"key":"12_CR37","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-40911-4_24","volume-title":"Integrated Formal Methods","author":"H. Hermanns","year":"2000","unstructured":"H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. Towards model checking stochastic process algebra. In Integrated Formal Methods, LNCS 1945: 420\u2013439, Springer-Verlag, 2000."},{"key":"12_CR38","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/3-540-48778-6_15","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"H. Hermanns","year":"1999","unstructured":"H. Hermanns and M. Siegle. Bisimulation algorithms for stochastic process algebras and their BDD-based implementation. In Formal Methods for Real-Time and Probabilistic Systems, LNCS 1601: 244\u2013265, Springer-Verlag, 1999."},{"key":"12_CR39","doi-asserted-by":"crossref","unstructured":"J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511569951"},{"issue":"5","key":"12_CR40","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"G.J. Holzmann. The model checker Spin. IEEE Transactions on Software Engineering, 23(5): 279\u2013295, 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"12_CR41","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1016\/S0377-2217(97)00028-3","volume":"105","author":"G. Horton","year":"1998","unstructured":"G. Horton, V. Kulkarni, D. Nicol, K. Trivedi. Fluid stochastic Petri nets: Theory, application and solution techniques. Eur. J. Oper. Res., 105(1): 184\u2013201,1998.","journal-title":"Eur. J. Oper. Res."},{"key":"12_CR42","unstructured":"R.A. Howard. Dynamic Probabilistic Systems; Volume 1: Markov Models. John Wiley & Sons, 1971."},{"key":"12_CR43","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/3-540-44804-7_4","volume-title":"Process Algebra and Probabilistic Methods","author":"G.G. Infante-Lopez","year":"2001","unstructured":"G.G. Infante-Lopez, H. Hermanns, and J.-P. Katoen. Beyond memoryless distributions: Model checking semi-Markov chains. In Process Algebra and Probabilistic Methods, LNCS 2165: 57\u201370, Springer-Verlag, 2001."},{"key":"12_CR44","first-page":"87","volume":"36","author":"A. Jensen","year":"1953","unstructured":"A. Jensen. Markov chains as an aid in the study of Markov processes. Skandinavisk Aktuarietidskrift 36: 87\u201391, 1953.","journal-title":"Skandinavisk Aktuarietidskrift"},{"key":"12_CR45","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/3-540-44804-7_2","volume-title":"Process Algebra and Probabilistic Methods","author":"J.-P. Katoen","year":"2001","unstructured":"J.-P. Katoen, M.Z. Kwiatkowska, G. Norman, and D. Parker. Faster and symbolic CTMC model checking. In Process Algebra and Probabilistic Methods, LNCS 2165: 23\u201338, Springer-Verlag, 2001."},{"key":"12_CR46","unstructured":"J.G. Kemeny and J.L. Snell. Finite Markov Chains. Van Nostrand, 1960."},{"key":"12_CR47","unstructured":"V.G. Kulkarni. Modeling and Analysis of Stochastic Systems. Chapman & Hall, 1995."},{"key":"12_CR48","series-title":"Lect Notes Comput Sci","volume-title":"Process Algebra and Probabilistic Methods","author":"M.Z. Kwiatkowska","year":"2002","unstructured":"M.Z. Kwiatkowska, G. Norman, and A. Pacheco. Model checking CSL until formulae with random time bounds. In Process Algebra and Probabilistic Methods, LNCS 2399, Springer-Verlag, 2002."},{"key":"12_CR49","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"8","key":"12_CR50","doi-asserted-by":"publisher","first-page":"720","DOI":"10.1109\/TC.1980.1675654","volume":"29","author":"J.F. Meyer","year":"1980","unstructured":"J.F. Meyer. On evaluating the performability of degradable computing systems. IEEE Transactions on Computers, 29(8): 720\u2013731, 1980.","journal-title":"IEEE Transactions on Computers"},{"issue":"7","key":"12_CR51","doi-asserted-by":"publisher","first-page":"648","DOI":"10.1109\/TC.1982.1676062","volume":"31","author":"J.F. Meyer","year":"1982","unstructured":"J.F. Meyer. Closed-form solutions of performability, IEEE Transactions on Computers, 31(7): 648\u2013657, 1982.","journal-title":"IEEE Transactions on Computers"},{"issue":"3\u20134","key":"12_CR52","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/0166-5316(92)90002-X","volume":"14","author":"J.F. Meyer","year":"1992","unstructured":"J.F. Meyer. Performability: a retrospective and some pointers to the future. Performance Evaluation, 14(3\u20134): 139\u2013156, 1992.","journal-title":"Performance Evaluation"},{"key":"12_CR53","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/S0166-5316(99)00010-3","volume":"35","author":"W.D. Obal II","year":"1999","unstructured":"W.D. Obal II and W.H. Sanders. State-space support for path-based reward variables. Performance Evaluation, 35: 233\u2013251, 1999.","journal-title":"Performance Evaluation"},{"key":"12_CR54","doi-asserted-by":"crossref","unstructured":"D. Peled. Software Reliability Methods. Springer-Verlag, 2001.","DOI":"10.1007\/978-1-4757-3540-6"},{"key":"12_CR55","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/0166-5316(95)00012-M","volume":"24","author":"W.H. Sanders","year":"1995","unstructured":"W.H. Sanders, W.D. Obal II, M.A. Qureshi, and F.K. Widnajarko. The UltraSAN modeling environment. Performance Evaluation, 24: 89\u2013115, 1995.","journal-title":"Performance Evaluation"},{"issue":"5","key":"12_CR56","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1080\/15326340008807601","volume":"16","author":"B. Sericola","year":"2000","unstructured":"B. Sericola. Occupation times in Markov processes. Stochastic Models, 16(5): 339\u2013351, 2000.","journal-title":"Stochastic Models"},{"key":"12_CR57","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/0166-5316(92)90003-Y","volume":"14","author":"E. Souza e Silva de","year":"1992","unstructured":"E. de Souza e Silva and H.R. Gail. Performability analysis of computer systems: from model specification to solution. Perf. Ev., 14: 157\u2013196, 1992.","journal-title":"Perf. Ev."},{"key":"12_CR58","doi-asserted-by":"crossref","unstructured":"W.J. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton University Press, 1994.","DOI":"10.1515\/9780691223384"},{"key":"12_CR59","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/S0167-6377(00)00023-7","volume":"26","author":"H.C. Tijms","year":"2000","unstructured":"H.C. Tijms, R. Veldman. A fast algorithm for the transient reward distribution in continuous-time Markov chains, Operation Research Letters, 26: 155\u2013158, 2000.","journal-title":"Operation Research Letters"}],"container-title":["Lecture Notes in Computer Science","Performance Evaluation of Complex Systems: Techniques and Tools"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45798-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T03:32:56Z","timestamp":1737171176000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45798-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540442523","9783540457985"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/3-540-45798-4_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}