{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T15:25:13Z","timestamp":1742397913183},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540779643"},{"type":"electronic","value":"9783540779667"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-77966-7_9","type":"book-chapter","created":{"date-parts":[[2008,2,1]],"date-time":"2008-02-01T08:59:24Z","timestamp":1201856364000},"page":"69-85","source":"Crossref","is-referenced-by-count":32,"title":["How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison"],"prefix":"10.1007","author":[{"given":"David N.","family":"Jansen","sequence":"first","affiliation":[]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]},{"given":"Marcel","family":"Oldenkamp","sequence":"additional","affiliation":[]},{"given":"Mari\u00eblle","family":"Stoelinga","sequence":"additional","affiliation":[]},{"given":"Ivan","family":"Zapreev","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"9_CR1","first-page":"213","volume":"153","author":"G. Agha","year":"2006","unstructured":"Agha, G., Meseguer, J., Sen, K.: PMaude: Rewrite-based specification language for probabilistic object systems. ENTCS\u00a0153(2), 213\u2013239 (2006)","journal-title":"ENTCS"},{"key":"9_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, Berlin (2004)"},{"key":"9_CR3","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.K.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 269\u2013276. Springer, Heidelberg (1996)"},{"issue":"4","key":"9_CR4","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/1059816.1059821","volume":"32","author":"C. Baier","year":"2005","unstructured":"Baier, C., Ciesinski, F., Gr\u00f6\u00dfer, M.: ProbMela and verification of Markov decision processes. SIGMETRICS Perform. Eval. Rev.\u00a032(4), 22\u201327 (2005)","journal-title":"SIGMETRICS Perform. Eval. Rev."},{"issue":"6","key":"9_CR5","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 Trans. on Softw. Eng.\u00a029(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. on Softw. Eng."},{"key":"9_CR6","first-page":"167","volume-title":"Quantitative Evaluation of Systems: QEST","author":"E. Bode","year":"2006","unstructured":"Bode, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R., Wimmer, R., Becker, B.: Compositional Performability Evaluation for STATEMATE. In: Quantitative Evaluation of Systems: QEST, pp. 167\u2013178. IEEE CS, Los Alamitos (2006)"},{"key":"9_CR7","unstructured":"Changuion, B., Davies, I., Nelte, M.: DaNAMiCS: A Petri net editor (2007), \n                    \n                      http:\/\/www.cs.uct.ac.za\/Research\/DNA\/microweb\/danamics\/DNAFrameH.html"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Cox, D.R.: A use of complex probabilities in the theory of stochastic processes. In: Proc. Cambridge Philosophical Society, vol.\u00a051, pp. 313\u2013319 (1955)","DOI":"10.1017\/S0305004100030231"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1007\/978-3-540-30182-0_55","volume-title":"Computer and Information Sciences - ISCIS 2004","author":"D. D\u2019Aprile","year":"2004","unstructured":"D\u2019Aprile, D., Donatelli, S., Sproston, J.: CSL model checking for the GreatSPN tool. In: Aykanat, C., Dayar, T., K\u00f6rpeo\u011flu, \u0130. (eds.) ISCIS 2004. LNCS, vol.\u00a03280, pp. 543\u2013552. Springer, Heidelberg (2004)"},{"key":"9_CR10","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF00289519","volume":"1","author":"E.W. Dijkstra","year":"1971","unstructured":"Dijkstra, E.W.: Hierarchical ordering of sequential processes. Acta Informatica\u00a01, 115\u2013138 (1971)","journal-title":"Acta Informatica"},{"issue":"6","key":"9_CR11","first-page":"53","volume":"128","author":"W. Fokkink","year":"2005","unstructured":"Fokkink, W., Pang, J.: Simplifying Itai-Rodeh leader election for anonymous rings. ENTCS\u00a0128(6), 53\u201368 (2005)","journal-title":"ENTCS"},{"issue":"1","key":"9_CR12","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/174666.174667","volume":"26","author":"R. Gupta","year":"1994","unstructured":"Gupta, R., Smolka, S.A., Bhaskar, S.: On randomization in sequential and distributed algorithms. ACM Comput. Surv.\u00a026(1), 7\u201386 (1994)","journal-title":"ACM Comput. Surv."},{"issue":"5","key":"9_CR13","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":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-48778-6_6","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"V. Hartonas-Garmhausen","year":"1999","unstructured":"Hartonas-Garmhausen, V., Campos, S., Clarke, E.M.: ProbVerus: probabilistic symbolic model checking. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, pp. 96\u2013110. Springer, Heidelberg (1999)"},{"issue":"1\u20134","key":"9_CR15","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0166-5316(99)00056-5","volume":"39","author":"H. Hermanns","year":"2000","unstructured":"Hermanns, H., Herzog, U., Klehmet, U., Mertsiotakis, V., Siegle, M.: Compositional performance modelling with the TIPPtool. Performance Evaluation\u00a039(1\u20134), 5\u201335 (2000)","journal-title":"Performance Evaluation"},{"key":"9_CR16","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":"9_CR17","unstructured":"Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi-terminal binary decision diagrams to represent and analyse continuous-time Markov chains. In: Plateau, B., Stewart, W.J., Silva, M. (eds.) Num. Sol. of Markov Chains, Zaragoza, Prensas Universitarias, pp. 188\u2013207 (1999)"},{"key":"9_CR18","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511569951","volume-title":"A Compositional Approach to Performance Modelling","author":"J. Hillston","year":"1996","unstructured":"Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, New York (1996)"},{"key":"9_CR19","volume-title":"Introduction to Mathematical Statistics","author":"R.V. Hogg","year":"1978","unstructured":"Hogg, R.V., Craig, A.T.: Introduction to Mathematical Statistics, 4th edn. Macmillan, New York (1978)","edition":"4"},{"issue":"9","key":"9_CR20","doi-asserted-by":"publisher","first-page":"1649","DOI":"10.1109\/49.62852","volume":"8","author":"O.C. Ibe","year":"1990","unstructured":"Ibe, O.C., Trivedi, K.S.: Stochastic Petri net models of polling systems. IEEE J. on Sel. Areas in Comm.\u00a08(9), 1649\u20131657 (1990)","journal-title":"IEEE J. on Sel. Areas in Comm."},{"issue":"1","key":"9_CR21","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. Inf. and Comp.\u00a088(1), 60\u201387 (1990)","journal-title":"Inf. and Comp."},{"issue":"2","key":"9_CR22","doi-asserted-by":"publisher","first-page":"489","DOI":"10.2307\/1992942","volume":"85","author":"S. Karlin","year":"1957","unstructured":"Karlin, S., McGregor, J.L.: The differential equations of birth-and-death processes, and the Stieltjes moment problem. Trans. of the AMS\u00a085(2), 489\u2013546 (1957)","journal-title":"Trans. of the AMS"},{"key":"9_CR23","first-page":"243","volume-title":"Quantitative Evaluation of Systems","author":"J.-P. Katoen","year":"2005","unstructured":"Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: Quantitative Evaluation of Systems, pp. 243\u2013244. IEEE CS, Los Alamitos (2005)"},{"key":"9_CR24","first-page":"301","volume-title":"Quantitative Evaluation of Systems: QEST","author":"J.-P. Katoen","year":"2006","unstructured":"Katoen, J.-P., Zapreev, I.S.: Safe on-the-fly steady-state detection for time-bounded reachability. In: Quantitative Evaluation of Systems: QEST, pp. 301\u2013310. IEEE CS, Los Alamitos (2006)"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., et al. (eds.) TOOLS 2002. LNCS, vol.\u00a02324, pp. 200\u2013204. Springer, Heidelberg (2002)"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) Formal methods for performance evaluation. LNCS, vol.\u00a04486, pp. 220\u2013270. Springer, Heidelberg (2007)"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45605-8_16","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"R. Lassaigne","year":"2002","unstructured":"Lassaigne, R., Peyronnet, S.: Approximate verification of probabilistic systems. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, pp. 213\u2013214. Springer, Heidelberg (2002)"},{"key":"9_CR28","unstructured":"Lecca, P., Priami, C.: Cell cycle control in eukaryotes: A BioSpi model. Technical Report DIT-03-045, Informatica e Telecommunicazioni: University of Trento (2003)"},{"issue":"3","key":"9_CR29","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/0305-0548(93)90001-Y","volume":"20","author":"S.G. Mohanty","year":"1993","unstructured":"Mohanty, S.G., Montazer-Haghighi, A., Trueblood, R.: On the transient behavior of a finite birth-death process with an application. Computers and Operations Research\u00a020(3), 239\u2013248 (1993)","journal-title":"Computers and Operations Research"},{"issue":"6","key":"9_CR30","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. J. of Computer Security\u00a014(6), 561\u2013589 (2006)","journal-title":"J. of Computer Security"},{"key":"9_CR31","unstructured":"Oldenkamp, M.: Probabilistic model checking: A comparison of tools. MSc thesis, Univ. of Twente, Netherlands (2007), \n                    \n                      http:\/\/www.cs.utwente.nl\/~oldenkampha\/"},{"issue":"4-5","key":"9_CR32","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-005-0216-7","volume":"8","author":"G.D. Penna","year":"2006","unstructured":"Penna, G.D., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Finite horizon analysis of Markov chains with the Murphi verifier. STTT\u00a08(4-5), 397\u2013409 (2006)","journal-title":"STTT"},{"issue":"1","key":"9_CR33","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A. Pnueli","year":"1986","unstructured":"Pnueli, A., Zuck, L.D.: Verification of multiprocess probabilistic protocols. Distributed Comput.\u00a01(1), 53\u201372 (1986)","journal-title":"Distributed Comput."},{"key":"9_CR34","unstructured":"PRISM: Probabilistic symbolic model checker (2006), \n                    \n                      http:\/\/www.cs.bham.ac.uk\/~dxp\/prism\/"},{"key":"9_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2004","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 202\u2013215. Springer, Heidelberg (2004)"},{"key":"9_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1007\/11513988_26","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2005","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 266\u2013280. Springer, Heidelberg (2005)"},{"key":"9_CR37","volume-title":"Regenerative Stochastic Simulation","author":"G.S. Shedler","year":"1993","unstructured":"Shedler, G.S.: Regenerative Stochastic Simulation. Academic Pr, London (1993)"},{"key":"9_CR38","unstructured":"Somenzi, F.: CUDD: CU decision diagram package. Public software (1997), \n                    \n                      http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"},{"key":"9_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/11513988_43","volume-title":"Computer Aided Verification","author":"H.L.S. Younes","year":"2005","unstructured":"Younes, H.L.S.: Ymer: A statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 429\u2013433. Springer, Heidelberg (2005)"},{"issue":"3","key":"9_CR40","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","volume":"8","author":"H.L.S. Younes","year":"2006","unstructured":"Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. STTT\u00a08(3), 216\u2013228 (2006)","journal-title":"STTT"},{"key":"9_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"H.L.S. Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 223\u2013235. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-77966-7_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:57:29Z","timestamp":1619521049000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-77966-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540779643","9783540779667"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-77966-7_9","relation":{},"subject":[]}}