{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:49:10Z","timestamp":1762458550570},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425564"},{"type":"electronic","value":"9783540448044"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44804-7_2","type":"book-chapter","created":{"date-parts":[[2007,7,20]],"date-time":"2007-07-20T18:22:41Z","timestamp":1184955761000},"page":"23-38","source":"Crossref","is-referenced-by-count":30,"title":["Faster and Symbolic CTMC Model Checking"],"prefix":"10.1007","author":[{"given":"Joost-Pieter","family":"Katoen","sequence":"first","affiliation":[]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,30]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur and T.A. Henzinger. Reactive modules. In IEEE Symp. on Logic in Computer Science, 207\u2013218, 1996.","DOI":"10.1109\/LICS.1996.561320"},{"key":"2_CR2","series-title":"Lect Notes Comput Sci","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":"A. Aziz, K. Sanwal, V. Singhal and R. Brayton. Verifying continuous time Markov chains. In Computer-Aided Verification, LNCS 1102: 269\u2013276, 1996."},{"issue":"1","key":"2_CR3","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. ACMT rans. on Computational Logic, 1(1): 162\u2013170, 2000.","journal-title":"ACMT rans. on Computational Logic"},{"issue":"2\/3","key":"2_CR4","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"R.I. Bahar","year":"1997","unstructured":"R.I. Bahar, E.A. Frohm, C.M. Gaona, G.D. Hachtel, E. Macii, A. Pardo and F. Somenzi. Algebraic decision diagrams and their applications. Formal Methods in System Design, 10(2\/3): 171\u2013206, 1997.","journal-title":"Formal Methods in System Design"},{"key":"2_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1007\/3-540-63165-8_199","volume-title":"Automata, Languages and Programming","author":"C. Baier","year":"1997","unstructured":"C. Baier, E. Clarke, V. Hartonas-Garmhausen, M. Kwiatkowska, and M. Ryan. Symbolic model checking for probabilistic processes. In Automata, Languages and Programming, LNCS 1256: 430\u2013440, 1997."},{"key":"2_CR6","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, 2000."},{"key":"2_CR7","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, 1999."},{"issue":"3","key":"2_CR8","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C. Baier","year":"1998","unstructured":"C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching-time logic with fairness. Distr. Comp., 11(3): 125\u2013155, 1998.","journal-title":"Distr. Comp."},{"key":"2_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Found. of Softw. Techn. and Th. Comp. Sc.","author":"A. Bianco","year":"1995","unstructured":"A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Found. of Softw. Techn. and Th. Comp. Sc., LNCS 1026: 499\u2013513, 1995."},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"K. Brace, R. Rudell and R. Bryant. Efficient implementation of a BDD package. In: 27th ACM\/IEEE Design Automation Conference, 1990.","DOI":"10.1145\/123186.123222"},{"key":"2_CR11","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. ACMT rans. on Progr. Lang. and Sys., 8: 244\u2013263, 1986.","journal-title":"ACMT rans. on Progr. Lang. and Sys."},{"issue":"2\/3","key":"2_CR12","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1023\/A:1008695706493","volume":"10","author":"E. Clarke","year":"1997","unstructured":"E. Clarke, M. Fujita, P.C. McGeer and J.C-Y. Yang. Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. In Formal Methods in System Design, 10(2\/3): 149\u2013169, 1997.","journal-title":"Formal Methods in System Design"},{"key":"2_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/BFb0028174","volume-title":"A Decade of Concurrency","author":"E. Clarke","year":"1993","unstructured":"E. Clarke, O. Grumberg and D. Long. Verification tools for finite-state concurrent programs. In A Decade of Concurrency, LNCS 803: 124\u2013175, 1993."},{"key":"2_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-46419-0_27","volume-title":"Tools and Algorithms for the Analysis and Construction of Systems","author":"L. Alfaro de","year":"2000","unstructured":"L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker and R. Segala. Symbolic model checking for probabilistic processes using MTBDDs and the Kronecker representation. In Tools and Algorithms for the Analysis and Construction of Systems, LNCS 1785: 395\u2013410, 2000."},{"issue":"4","key":"2_CR15","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1145\/42404.42409","volume":"31","author":"B.L. Fox","year":"1988","unstructured":"B.L. Fox and P.W. Glynn. Computing Poisson probabilities. Comm. of the ACM, 31(4): 440\u2013445, 1988.","journal-title":"Comm. of the ACM"},{"issue":"2","key":"2_CR16","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. Oper. Res. 32(2): 343\u2013361, 1984.","journal-title":"Oper. Res."},{"issue":"5","key":"2_CR17","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H.A. Hansson","year":"1994","unstructured":"H.A. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Form. Asp. of Comp., 6(5): 512\u2013535, 1994.","journal-title":"Form. Asp. of Comp."},{"key":"2_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-48778-6_6","volume-title":"Formal Methods for Real-Time and Prob. Sys.","author":"V. Hartonas-Garmhausen","year":"1999","unstructured":"V. Hartonas-Garmhausen, S. Campos and E.M. Clarke. ProbVerus: probabilistic symbolic model checking. In Formal Methods for Real-Time and Prob. Sys., LNCS 1601: 96\u2013111, 1999."},{"key":"2_CR19","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, 2000."},{"key":"2_CR20","unstructured":"H. Hermanns, J. Meyer-Kayser and M. Siegle. Multi-terminal binary decision diagrams to represent and analyse continuous-time Markov chains. In Proc. 3rd Int. Workshop on the Num. Sol. of Markov Chains, pp. 188\u2013207, 1999."},{"issue":"9","key":"2_CR21","doi-asserted-by":"publisher","first-page":"1649","DOI":"10.1109\/49.62852","volume":"8","author":"O.C. Ibe","year":"1990","unstructured":"O.C. Ibe and K.S. Trivedi. Stochastic Petri net models of polling systems. IEEE J. on Sel. Areas in Comms., 8(9): 1649\u20131657, 1990.","journal-title":"IEEE J. on Sel. Areas in Comms."},{"key":"2_CR22","unstructured":"J. Kemeny, J. Snell and A. Knapp. Denumerable Markov Chains. Van Nostrand, 1966."},{"key":"2_CR23","first-page":"87","volume":"3","author":"A. Jensen","year":"1953","unstructured":"A. Jensen. Markov chains as an aid in the study of Markov processes. Skand. Aktuarietidskrift, 3: 87\u201391, 1953.","journal-title":"Skand. Aktuarietidskrift"},{"key":"2_CR24","unstructured":"J.K. Muppala and K.S. Trivedi. Numerical transient solution of finite Markovian queueing systems. In U. Bhat, ed, Queueing and Related Models, Oxford University Press, 1992."},{"key":"2_CR25","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. Perf. Ev., 35: 233\u2013251, 1999.","journal-title":"Perf. Ev."},{"key":"2_CR26","unstructured":"D. Parker. Implementation of symbolic model checking for probabilistic systems. Ph.D thesis, School of Computer Science, University of Birmingham, 2001 (to appear)."},{"key":"2_CR27","volume-title":"CUDD: CU decision diagram package","author":"F. Somenzi","year":"1997","unstructured":"F. Somenzi. CUDD: CU decision diagram package. Public software, Colorado University, Boulder, 1997."},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"W. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton Univ. Press, 1994.","DOI":"10.1515\/9780691223384"}],"container-title":["Lecture Notes in Computer Science","Process Algebra and Probabilistic Methods. Performance Modelling and Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44804-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T13:48:49Z","timestamp":1683985729000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44804-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425564","9783540448044"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-44804-7_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}