{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:00:13Z","timestamp":1770292813567,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540712084","type":"print"},{"value":"9783540712091","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71209-1_9","type":"book-chapter","created":{"date-parts":[[2007,7,4]],"date-time":"2007-07-04T18:56:34Z","timestamp":1183575394000},"page":"87-101","source":"Crossref","is-referenced-by-count":66,"title":["Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking"],"prefix":"10.1007","author":[{"given":"Joost-Pieter","family":"Katoen","sequence":"first","affiliation":[]},{"given":"Tim","family":"Kemna","sequence":"additional","affiliation":[]},{"given":"Ivan","family":"Zapreev","sequence":"additional","affiliation":[]},{"given":"David N.","family":"Jansen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","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)"},{"key":"9_CR2","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A. Aziz","year":"2000","unstructured":"Aziz, A., et al.: Model-checking continuous time Markov chains. ACM TOCL\u00a01, 162\u2013170 (2000)","journal-title":"ACM TOCL"},{"key":"9_CR3","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., et al.: It usually works: the temporal logic of stochastic systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 155\u2013165. Springer, Heidelberg (1995)"},{"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. Performance Evaluation Review\u00a032, 22\u201327 (2005)","journal-title":"Performance Evaluation Review"},{"key":"9_CR5","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., et al.: 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)"},{"key":"9_CR6","first-page":"524","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., et al.: Model-checking algorithms for continuous-time Markov chains. IEEE TSE\u00a029, 524\u2013541 (2003)","journal-title":"IEEE TSE"},{"key":"9_CR7","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.ic.2005.03.001","volume":"200","author":"C. Baier","year":"2005","unstructured":"Baier, C., et al.: Comparative branching-time semantics for Markov chains. Information and Computation\u00a0200, 149\u2013214 (2005)","journal-title":"Information and Computation"},{"key":"9_CR8","first-page":"189","volume-title":"QEST","author":"M. Ben Mamoun","year":"2006","unstructured":"Ben Mamoun, M., Pekergin, N., Youn\u00e8s, S.: Model checking of continuous-time Markov chains by closed-form bounding distributions. In: QEST, pp. 189\u2013198. IEEE CS, Los Alamitos (2006)"},{"key":"9_CR9","first-page":"167","volume-title":"QEST","author":"E. B\u00f6de","year":"2006","unstructured":"B\u00f6de, E., et al.: Compositional performability evaluation for Statemate. In: QEST, pp. 167\u2013178. IEEE CS, Los Alamitos (2006)"},{"key":"9_CR10","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":"9_CR11","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\u2013553. Springer, Heidelberg (2004)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-44804-7_3","volume-title":"Process Algebra and Probabilistic Methods. Performance Modelling and Verification","author":"P.R. D\u2019Argenio","year":"2001","unstructured":"D\u2019Argenio, P.R., et al.: Reachability analysis of probabilistic systems by successive refinements. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol.\u00a02165, pp. 39\u201356. Springer, Heidelberg (2001)"},{"key":"9_CR13","unstructured":"Derisavi, S.: Solution of Large Markov Models using Lumping Techniques and Symbolic Data Structures. PhD thesis, Univ. of Illinois at Urbana-Champaign (2005)"},{"key":"9_CR14","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/S0020-0190(03)00343-0","volume":"87","author":"S. Derisavi","year":"2003","unstructured":"Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal state-space lumping in Markov chains. IPL\u00a087, 309\u2013315 (2003)","journal-title":"IPL"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/11691617_5","volume-title":"Model Checking Software","author":"H. Fecher","year":"2006","unstructured":"Fecher, H., Leucker, M., Wolf, V.: Don\u2019t know in probabilistic systems. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 71\u201388. Springer, Heidelberg (2006)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/3-540-49519-3_9","volume-title":"Formal Methods in Computer-Aided Design","author":"K. Fisler","year":"1998","unstructured":"Fisler, K., Vardi, M.Y.: Bisimulation minimization in an automata-theoretic verification framework. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 115\u2013132. Springer, Heidelberg (1998)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/3-540-48153-2_29","volume-title":"Correct Hardware Design and Verification Methods","author":"K. Fisler","year":"1999","unstructured":"Fisler, K., Vardi, M.Y.: Bisimulation and model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 338\u2013342. Springer, Heidelberg (1999)"},{"key":"9_CR18","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1023\/A:1016091902809","volume":"21","author":"K. Fisler","year":"2002","unstructured":"Fisler, K., Vardi, M.Y.: Bisimulation minimization and symbolic model checking. Formal Methods in System Design\u00a021, 39\u201378 (2002)","journal-title":"Formal Methods in System Design"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11804192_19","volume-title":"Formal Methods for Components and Objects","author":"M. Groesser","year":"2006","unstructured":"Groesser, M., Baier, C.: Partial order reduction for Markov decision processes: a survey. In: de Boer, F.S., et al. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 408\u2013427. Springer, Heidelberg (2006)"},{"key":"9_CR20","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, 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"9_CR21","first-page":"103","volume-title":"DSN","author":"B. Haverkort","year":"2002","unstructured":"Haverkort, B., et al.: Model checking performability properties. In: DSN, pp. 103\u2013112. IEEE CS, Los Alamitos (2002)"},{"key":"9_CR22","first-page":"228","volume-title":"19th IEEE Symposium on Reliable Distributed Systems","author":"B.R. Haverkort","year":"2000","unstructured":"Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the use of model checking techniques for quantitative dependability evaluation. In: 19th IEEE Symposium on Reliable Distributed Systems, pp. 228\u2013237. IEEE CS, Los Alamitos (2000)"},{"key":"9_CR23","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/S1567-8326(02)00066-8","volume":"56","author":"H. Hermanns","year":"2003","unstructured":"Hermanns, H., et al.: On the use of MTBDDs for performability analysis and verification of stochastic systems. J. of Logic and Alg. Progr.\u00a056, 23\u201367 (2003)","journal-title":"J. of Logic and Alg. Progr."},{"key":"9_CR24","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, Cambridge (1996)"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/978-3-540-24611-4_12","volume-title":"Validation of Stochastic Systems","author":"M. Huth","year":"2004","unstructured":"Huth, M.: An abstraction framework for mixed non-deterministic and probabilistic systems. In: Baier, C., et al. (eds.) Validation of Stochastic Systems. LNCS, vol.\u00a02925, pp. 419\u2013444. Springer, Heidelberg (2004)"},{"key":"9_CR26","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/j.tcs.2005.08.008","volume":"346","author":"M. Huth","year":"2005","unstructured":"Huth, M.: On finite-state approximants for probabilistic computation tree logic. TCS\u00a0346, 113\u2013134 (2005)","journal-title":"TCS"},{"key":"9_CR27","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 Selected Areas in Communications\u00a08, 1649\u20131657 (1990)","journal-title":"IEEE J. on Selected Areas in Communications"},{"key":"9_CR28","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, 60\u201387 (1990)","journal-title":"Information and Computation"},{"key":"9_CR29","first-page":"243","volume-title":"QEST","author":"J.-P. Katoen","year":"2005","unstructured":"Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: QEST, pp. 243\u2013244. IEEE CS, Los Alamitos (2005)"},{"key":"9_CR30","first-page":"301","volume-title":"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: QEST, pp. 301\u2013310. IEEE CS, Los Alamitos (2006)"},{"key":"9_CR31","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. J. on STTT\u00a06, 128\u2013142 (2004)","journal-title":"Int. J. on STTT"},{"key":"9_CR32","first-page":"157","volume-title":"QEST","author":"M. Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: QEST, pp. 157\u2013166. IEEE CS, Los Alamitos (2006)"},{"key":"9_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/11817963_23","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 234\u2013248. Springer, Heidelberg (2006)"},{"key":"9_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K.G. Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation\u00a094, 1\u201328 (1991)","journal-title":"Information and Computation"},{"key":"9_CR35","first-page":"711","volume-title":"DSN","author":"M. Massink","year":"2004","unstructured":"Massink, M., Katoen, J.-P., Latella, D.: Model checking dependability attributes of wireless group communication. In: DSN, pp. 711\u2013720. IEEE CS, Los Alamitos (2004)"},{"key":"9_CR36","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/j.scico.2005.02.008","volume":"58","author":"D. Monniaux","year":"2005","unstructured":"Monniaux, D.: Abstract interpretation of programs as Markov decision processes. Science of Computer Programming\u00a058, 179\u2013205 (2005)","journal-title":"Science of Computer Programming"},{"key":"9_CR37","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A. Pnueli","year":"1986","unstructured":"Pnueli, A., Zuck, L.: Verification of multiprocess probabilistic protocols. Distributed Computing\u00a01, 53\u201372 (1986)","journal-title":"Distributed Computing"},{"key":"9_CR38","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/290163.290168","volume":"1","author":"M.K. Reiter","year":"1998","unstructured":"Reiter, M.K., Rubin, A.D.: Crowds: anonymity for web transactions. ACM Transactions on Information and System Security\u00a01, 66\u201392 (1998)","journal-title":"ACM Transactions on Information and System Security"},{"key":"9_CR39","first-page":"531","volume":"32","author":"J. Sproston","year":"2006","unstructured":"Sproston, J., Donatelli, S.: Backward bisimulation in Markov chain model checking. IEEE TSE\u00a032, 531\u2013546 (2006)","journal-title":"IEEE TSE"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71209-1_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:16:59Z","timestamp":1605745019000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71209-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540712084","9783540712091"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71209-1_9","relation":{},"subject":[]}}