{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T15:52:22Z","timestamp":1776441142145,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":63,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540724827","type":"print"},{"value":"9783540725220","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-72522-0_6","type":"book-chapter","created":{"date-parts":[[2007,6,5]],"date-time":"2007-06-05T19:02:12Z","timestamp":1181070132000},"page":"220-270","source":"Crossref","is-referenced-by-count":346,"title":["Stochastic Model Checking"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"6_CR1","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R. Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.: Reactive modules. Formal Methods in System Design\u00a015(1), 7\u201348 (1999)","journal-title":"Formal Methods in System Design"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/978-3-540-40903-8_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S. Andova","year":"2004","unstructured":"Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol.\u00a02791, pp. 88\u2013104. Springer, Heidelberg (2004)"},{"issue":"1","key":"6_CR3","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/0196-6774(90)90021-6","volume":"15","author":"J. Aspnes","year":"1990","unstructured":"Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. Journal of Algorithms\u00a015(1), 441\u2013460 (1990)","journal-title":"Journal of Algorithms"},{"key":"6_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":"Computer Aided Verification","author":"A. Aziz","year":"1996","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 269\u2013276. Springer, Heidelberg (1996)"},{"issue":"1","key":"6_CR5","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A. Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model checking continuous time Markov chains. ACM Transactions on Computational Logic\u00a01(1), 162\u2013170 (2000)","journal-title":"ACM Transactions on Computational Logic"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-60045-0_48","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1995","unstructured":"Aziz, A., Singhal, V., Balarin, F., Brayton, R., Sangiovanni-Vincentelli, A.: It usually works: The temporal logic of stochastic systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 155\u2013165. Springer, Heidelberg (1995)"},{"issue":"2-3","key":"6_CR7","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"I. Bahar","year":"1997","unstructured":"Bahar, I., Frohm, E., Gaona, C., Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. Formal Methods in System Design\u00a010(2-3), 171\u2013206 (1997)","journal-title":"Formal Methods in System Design"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/10722167_28","volume-title":"Computer Aided Verification","author":"C. Baier","year":"2000","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model checking continuous-time Markov chains by transient analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 358\u2013372. Springer, Heidelberg (2000)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","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":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the Logical Characterisation of Performability Properties. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, pp. 780\u2013792. Springer, Heidelberg (2000)"},{"issue":"6","key":"6_CR10","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering\u00a029(6), 524\u2013541 (2003)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-45694-5_23","volume-title":"CONCUR 2002 - Concurrency Theory","author":"C. Baier","year":"2002","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H., Haverkort, B.R.: Simulation for Continuous-Time Markov Chains. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 338\u2013354. Springer, Heidelberg (2002)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR\u201999. Concurrency Theory","author":"C. Baier","year":"1999","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H.: Approximate Symbolic Model Checking of Continuous-Time Markov Chains (Extended Abstract). In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 146\u2013161. Springer, Heidelberg (1999)"},{"issue":"3","key":"6_CR13","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C. Baier","year":"1998","unstructured":"Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distributed Computing\u00a011(3), 125\u2013155 (1998)","journal-title":"Distributed Computing"},{"issue":"3","key":"6_CR14","first-page":"299","volume":"8","author":"L. Benini","year":"2000","unstructured":"Benini, L., Bogliolo, A., Paleologo, G., Micheli, G.D.: Policy optimization for dynamic power management. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a08(3), 299\u2013316 (2000)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A. Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"6_CR16","volume-title":"Probability and Measure","author":"P. Billingsley","year":"1995","unstructured":"Billingsley, P.: Probability and Measure. Wiley, Chichester (1995)"},{"key":"6_CR17","doi-asserted-by":"publisher","first-page":"59","DOI":"10.2307\/3215235","volume":"31","author":"P. Buchholz","year":"1994","unstructured":"Buchholz, P.: Exact and ordinary lumpability in finite Markov chains. Journal of Applied Probability\u00a031, 59\u201375 (1994)","journal-title":"Journal of Applied Probability"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/11795490_6","volume-title":"Principles of Distributed Systems","author":"L. Cheung","year":"2006","unstructured":"Cheung, L.: Randomized Wait-Free Consensus Using an Atomicity Assumption. In: Anderson, J.H., Prencipe, G., Wattenhofer, R. (eds.) OPODIS 2005. LNCS, vol.\u00a03974, pp. 47\u201360. Springer, Heidelberg (2006)"},{"issue":"6","key":"6_CR19","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1016\/j.peva.2005.06.001","volume":"63","author":"G. Ciardo","year":"2006","unstructured":"Ciardo, G., Jones, R., Miner, A., Siminiceanu, R.: Logic and stochastic modeling with smart. Performance Evaluation\u00a063(6), 578\u2013608 (2006)","journal-title":"Performance Evaluation"},{"issue":"2","key":"6_CR20","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. Clarke","year":"1986","unstructured":"Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logics. ACM Transactions on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2-3","key":"6_CR21","first-page":"149","volume":"10","author":"E. Clarke","year":"1997","unstructured":"Clarke, E., Fujita, M., McGeer, P., McMillan, K., Yang, J., Zhao, X.: Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. Formal Methods in System Design\u00a010(2-3), 149\u2013169 (1997)","journal-title":"Formal Methods in System Design"},{"key":"6_CR22","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1109\/SFCS.1988.21950","volume-title":"Proc. 29th Annual Symposium on Foundations of Computer Science (FOCS\u201988)","author":"C. Courcoubetis","year":"1988","unstructured":"Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite state probabilistic programs. In: Proc. 29th Annual Symposium on Foundations of Computer Science (FOCS\u201988), 1988, pp. 338\u2013345. IEEE Computer Society Press, Los Alamitos (1988)"},{"issue":"4","key":"6_CR23","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM\u00a042(4), 857\u2013907 (1995)","journal-title":"Journal of the ACM"},{"issue":"2-3","key":"6_CR24","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10009-003-0118-5","volume":"5","author":"C. Daws","year":"2004","unstructured":"Daws, C., Kwiatkowska, M., Norman, G.: Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM. Int. Journal on Software Tools for Technology Transfer\u00a05(2-3), 221\u2013236 (2004)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"issue":"6","key":"6_CR25","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1145\/3812.3818","volume":"28","author":"S. Even","year":"1985","unstructured":"Even, S., Goldreich, O., Lempel, A.: A randomized protocol for signing contracts. Communications of the ACM\u00a028(6), 637\u2013647 (1985)","journal-title":"Communications of the ACM"},{"issue":"8","key":"6_CR26","first-page":"981","volume":"12","author":"W. Fokkink","year":"2006","unstructured":"Fokkink, W., Pang, J.: Variations on itai-rodeh leader election for anonymous rings and their analysis in prism. Journal of Universal Computer Science\u00a012(8), 981\u20131006 (2006)","journal-title":"Journal of Universal Computer Science"},{"issue":"4","key":"6_CR27","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1145\/42404.42409","volume":"31","author":"B. Fox","year":"1988","unstructured":"Fox, B., Glynn, P.: Computing Poisson probabilities. Communications of the ACM\u00a031(4), 440\u2013445 (1988)","journal-title":"Communications of the ACM"},{"key":"6_CR28","volume-title":"Performance Analysis of Communication Systems: Modeling with Non-Markovian Stochastic Petri Nets","author":"R. German","year":"2000","unstructured":"German, R.: Performance Analysis of Communication Systems: Modeling with Non-Markovian Stochastic Petri Nets. John Wiley and Sons, Chichester (2000)"},{"issue":"5","key":"6_CR29","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"6_CR30","volume-title":"Performance of Computer Communication Systems: A Model-Based Approach","author":"B. Haverkort","year":"1988","unstructured":"Haverkort, B.: Performance of Computer Communication Systems: A Model-Based Approach. John Wiley & Sons, Chichester (1988)"},{"key":"6_CR31","volume-title":"Proc. Int. Conf. Dependable Systems and Networks (DSN\u201902)","author":"B. Haverkort","year":"2002","unstructured":"Haverkort, B., Cloth, L., Hermanns, H., Katoen, J.-P., Baier, C.: Model checking performability properties. In: Proc. Int. Conf. Dependable Systems and Networks (DSN\u201902), 2002, IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"6_CR32","series-title":"Lecture Notes in Bioinformatics","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/11885191_3","volume-title":"Computational Methods in Systems Biology","author":"J.K. Heath","year":"2006","unstructured":"Heath, J.K., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic Model Checking of Complex Biological Pathways. In: Priami, C. (ed.) CMSB 2006. LNCS (LNBI), vol.\u00a04210, pp. 32\u201347. Springer, Heidelberg (2006)"},{"key":"6_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-3-540-24622-0_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 73\u201384. Springer, Heidelberg (2004)"},{"key":"6_CR34","series-title":"Lecture Notes in Computer Science","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":"Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: A Markov Chain Model Checker. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol.\u00a01785, pp. 347\u2013362. Springer, Heidelberg (2000)"},{"key":"6_CR35","series-title":"Lecture Notes in Computer Science","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":"Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: Towards model checking stochastic process algebra. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol.\u00a01945, pp. 420\u2013439. Springer, Heidelberg (2000)"},{"key":"6_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A Tool for Automatic Verification of Probabilistic Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"6_CR37","unstructured":"IEEE standard for a high performance serial bus. IEEE Computer Society, IEEE Std. 1394-1995."},{"issue":"1","key":"6_CR38","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/0890-5401(90)90004-2","volume":"88","author":"A. Itai","year":"1990","unstructured":"Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Information and Computation\u00a088(1), 60\u201387 (1990)","journal-title":"Information and Computation"},{"key":"6_CR39","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1109\/QEST.2005.2","volume-title":"Proc. Second Int. Conf. Quantitative Evaluation of Systems (QEST 05)","author":"J.-P. Katoen","year":"2005","unstructured":"Katoen, J.-P., Khattri, M., Zapreev, I.: A Markov reward model checker. In: Proc. Second Int. Conf. Quantitative Evaluation of Systems (QEST 05), 2005, pp. 243\u2013244. IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"6_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-44804-7_2","volume-title":"Process Algebra and Probabilistic Methods. Performance Modelling and Verification","author":"J.-P. Katoen","year":"2001","unstructured":"Katoen, J.-P., Kwiatkowska, M., Norman, G., Parker, D.: Faster and Symbolic CTMC Model Checking. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol.\u00a02165, pp. 23\u201338. Springer, Heidelberg (2001)"},{"key":"6_CR41","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov Chains","author":"J. Kemeny","year":"1976","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains, 2nd edn. Springer, Heidelberg (1976)","edition":"2"},{"key":"6_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/3-540-45605-8_10","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Pacheco, A.: Model Checking CSL until Formulae with Random Time Bounds. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, pp. 152\u2013168. Springer, Heidelberg (2002)"},{"key":"6_CR43","unstructured":"Kwiatkowska, M., Norman, G., Pacheco, A.: Model checking expected time and expected reward formulae with random time bounds. In: Proc. 2nd Euro-Japanese Workshop on Stochastic Risk Modelling for Finance, Insurance, Production and Reliability (September 2002)"},{"issue":"2","key":"6_CR44","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/j.camwa.2005.11.016","volume":"51","author":"M. Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Pacheco, A.: Model checking expected time and expected reward formulae with random time bounds. Computers & Mathematics with Applications\u00a051(2), 305\u2013316 (2006)","journal-title":"Computers & Mathematics with Applications"},{"key":"6_CR45","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM users\u2019 guide. Available from http:\/\/www.cs.bham.ac.uk\/~dxp\/prism"},{"issue":"2","key":"6_CR46","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/s10009-004-0140-2","volume":"6","author":"M. Kwiatkowska","year":"2004","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. Int. Journal on Software Tools for Technology Transfer\u00a06(2), 128\u2013142 (2004)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"6_CR47","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"M. Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design\u00a029, 33\u201378 (2006)","journal-title":"Formal Methods in System Design"},{"key":"6_CR48","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1109\/MASCOT.2004.1348189","volume-title":"Proc. 12th Int. Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS\u201904)","author":"M. Kwiatkowska","year":"2004","unstructured":"Kwiatkowska, M., Parker, D., Zhang, Y., Mehmood, R.: Dual-processor parallelisation of symbolic probabilistic model checking. In: DeGroot, D., Harrison, P. (eds.) Proc. 12th Int. Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS\u201904), pp. 123\u2013130. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"6_CR49","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K. Larsen","year":"1991","unstructured":"Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Information and Computation\u00a094, 1\u201328 (1991)","journal-title":"Information and Computation"},{"issue":"2","key":"6_CR50","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/s00165-005-0062-0","volume":"17","author":"G. Norman","year":"2005","unstructured":"Norman, G., Parker, D., Kwiatkowska, M., Shukla, S., Gupta, R.: Using probabilistic model checking for dynamic power management. Formal Aspects of Computing\u00a017(2), 160\u2013176 (2005)","journal-title":"Formal Aspects of Computing"},{"issue":"6","key":"6_CR51","doi-asserted-by":"crossref","first-page":"561","DOI":"10.3233\/JCS-2006-14604","volume":"14","author":"G. Norman","year":"2006","unstructured":"Norman, G., Shmatikov, V.: Analysis of probabilistic contract signing. Journal of Computer Security\u00a014(6), 561\u2013589 (2006)","journal-title":"Journal of Computer Security"},{"key":"6_CR52","unstructured":"Parker, D.: Implementation of Symbolic Model Checking for Probabilistic Systems. PhD thesis, University of Birmingham (2002)"},{"key":"6_CR53","unstructured":"PRISM web site: http:\/\/www.cs.bham.ac.uk\/~dxp\/prism"},{"key":"6_CR54","doi-asserted-by":"crossref","unstructured":"Qiu, Q., Wu, Q., Pedram, M.: Stochastic modeling of a power-managed system: Construction and optimization. In: Proc. Int. Symposium on Low Power Electronics and Design (1999)","DOI":"10.1145\/313817.313923"},{"issue":"10","key":"6_CR55","doi-asserted-by":"publisher","first-page":"1200","DOI":"10.1109\/43.952737","volume":"20","author":"Q. Qiu","year":"2001","unstructured":"Qiu, Q., Wu, Q., Pedram, M.: Stochastic modeling of a power-managed system: construction and optimization. IEEE Transactions on Computer Aided Design\u00a020(10), 1200\u20131217 (2001)","journal-title":"IEEE Transactions on Computer Aided Design"},{"key":"6_CR56","series-title":"CRM Monograph Series","doi-asserted-by":"crossref","DOI":"10.1090\/crmm\/023","volume-title":"Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems","author":"J. Rutten","year":"2004","unstructured":"Rutten, J., Kwiatkowska, M., Norman, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems. CRM Monograph Series, vol.\u00a023. American Mathematical Society, New York (2004)"},{"key":"6_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/BFb0015027","volume-title":"CONCUR \u201994: Concurrency Theory","author":"R. Segala","year":"1994","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol.\u00a0836, pp. 481\u2013496. Springer, Heidelberg (1994)"},{"key":"6_CR58","unstructured":"Somenzi, F.: CUDD: Colorado University decision diagram package. Public software, Colorado Univeristy, Boulder (1997), http:\/\/vlsi.colorado.edu\/~fabio\/"},{"key":"6_CR59","doi-asserted-by":"crossref","unstructured":"Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton (1994)","DOI":"10.1515\/9780691223384"},{"key":"6_CR60","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R. Tarjan","year":"1972","unstructured":"Tarjan, R.: Depth-first search and linear graph algorithms. SIAM Journal on Computing\u00a01, 146\u2013160 (1972)","journal-title":"SIAM Journal on Computing"},{"key":"6_CR61","volume-title":"Probability and Statistics with Reliability, Queuing, and Computer Science Applications","author":"K. Trivedi","year":"2001","unstructured":"Trivedi, K.: Probability and Statistics with Reliability, Queuing, and Computer Science Applications. John Wiley & Sons, Chichester (2001)"},{"key":"6_CR62","first-page":"327","volume-title":"Proc. 26th Annual Symposium on Foundations of Computer Science (FOCS\u201985)","author":"M. Vardi","year":"1985","unstructured":"Vardi, M.: Automatic verification of probabilistic concurrent finite state programs. In: Proc. 26th Annual Symposium on Foundations of Computer Science (FOCS\u201985), 1985, pp. 327\u2013338. IEEE Computer Society Press, Los Alamitos (1985)"},{"issue":"3","key":"6_CR63","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","volume":"8","author":"H. Younes","year":"2006","unstructured":"Younes, H., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. Int. Journal on Software Tools for Technology Transfer\u00a08(3), 216\u2013228 (2006)","journal-title":"Int. Journal on Software Tools for Technology Transfer"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Performance Evaluation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72522-0_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T06:16:14Z","timestamp":1683872174000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72522-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540724827","9783540725220"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72522-0_6","relation":{},"subject":[]}}