{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:20:30Z","timestamp":1779074430947,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540672821","type":"print"},{"value":"9783540464198","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46419-0_24","type":"book-chapter","created":{"date-parts":[[2007,8,8]],"date-time":"2007-08-08T19:17:25Z","timestamp":1186600645000},"page":"347-362","source":"Crossref","is-referenced-by-count":47,"title":["A Markov Chain Model Checker"],"prefix":"10.1007","author":[{"given":"Holger","family":"Hermanns","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joachim","family":"Meyer-Kayser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Siegle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"issue":"2","key":"24_CR1","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/190.191","volume":"2","author":"M. A. Marsan","year":"1984","unstructured":"M. Ajmone Marsan, G. Conte, and G. Balbo. A class of generalised stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Tr. on Comp. Sys., 2(2): 93\u2013122, 1984. 348, 358","journal-title":"ACM Tr. on Comp. Sys."},{"key":"24_CR2","series-title":"Lect Notes Comput Sci","volume-title":"TACAS","author":"L. Alfaro de","year":"2000","unstructured":"L. de Alfaro, M.Z. Kwiatkowska, G. Norman, D. Parker and R. Segala. Symbolic model checking for probabilistic processes using MTBDDs and the Kronecker representation. In TACAS, LNCS (this volume), 2000. 349"},{"key":"24_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-60045-0_48","volume-title":"CAV","author":"A. Aziz","year":"1995","unstructured":"A. Aziz, V. Singhal, F. Balarin, R. Brayton and A. Sangiovanni-Vincentelli. It usually works: the temporal logic of stochastic systems. In CAV, LNCS 939: 155\u2013165, 1995. 347"},{"key":"24_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume-title":"CAV","author":"A. Aziz","year":"1996","unstructured":"A. Aziz, K. Sanwal, V. Singhal and R. Brayton. Verifying continuous time Markov chains. In CAV, LNCS 1102: 269\u2013276, 1996. 347, 348"},{"key":"24_CR5","unstructured":"C. Baier. On algorithmic verification methods for probabilistic systems. Habilitation thesis, Univ. of Mannheim, 1999. 347, 352"},{"key":"24_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1007\/3-540-63165-8_199","volume-title":"ICALP","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 ICALP, LNCS 1256: 430\u2013440, 1997. 347"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"C. Baier, B.R. Haverkort, H. Hermanns and J.-P. Katoen. Model checking continuous-time Markov chains by transient analysis. 2000 (submitted). 360","DOI":"10.1007\/10722167_28"},{"key":"24_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR","author":"C. Baier","year":"1999","unstructured":"C. Baier, J.-P. Katoen and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In CONCUR, LNCS 1664: 146\u2013162, 1999. 347, 348, 349, 350, 351, 352, 360"},{"issue":"2","key":"24_CR9","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. Inf. Proc. Letters, 66(2): 71\u201379, 1998. 350, 353","journal-title":"Inf. Proc. Letters"},{"key":"24_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/3-540-56287-7_117","volume-title":"FSTTCS","author":"I. Christoff","year":"1992","unstructured":"I. Christoff and L. Christoff. Reasoning about safety and liveness properties for probabilistic systems. In FSTTCS, LNCS 652: 342\u2013355, 1992. 347"},{"issue":"2","key":"24_CR11","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Tr. on Progr. Lang. and Sys., 8(2): 244\u2013263, 1986. 350, 351","journal-title":"ACM Tr. on Progr. Lang. and Sys."},{"key":"24_CR12","unstructured":"A.E. Conway and N.D. Georganas. Queueing Networks \u2014 Exact Computational Algorithms. MIT Press, 1989. 348, 355"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. In Proc. IEEE Symp. on Found. of Comp. Sci., pp. 338\u2013345, 1988. 347, 352","DOI":"10.1109\/SFCS.1988.21950"},{"key":"24_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/BFb0022197","volume-title":"Comp. Perf. Ev.","author":"D.D. Deavours","year":"1997","unstructured":"D.D. Deavours and W.H. Sanders. An efficient disk-based tool for solving very large Markov models. In Comp. Perf. Ev., LNCS 1245: 58\u201371, 1997. 352"},{"key":"24_CR15","unstructured":"L. Fredlund. The timing and probability workbench: a tool for analysing timed processes. Tech. Rep. No. 49, Uppsala Univ., 1994. 348"},{"issue":"12","key":"24_CR16","doi-asserted-by":"publisher","first-page":"1479","DOI":"10.1109\/43.552081","volume":"15","author":"G. Hachtel","year":"1996","unstructured":"G. Hachtel, E. Macii, A. Padro and F. Somenzi. Markovian analysis of large finite-state machines. IEEE Tr. on CAD of Integr. Circ. and Sys., 15(12): 1479\u20131493, 1996. 360","journal-title":"IEEE Tr. on CAD of Integr. Circ. and Sys."},{"issue":"5","key":"24_CR17","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Form. Asp. of Comp., 6(5): 512\u2013535, 1994. 347, 348, 352, 353, 360","journal-title":"Form. Asp. of Comp."},{"key":"24_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/3-540-48778-6_6","volume-title":"ARTS","author":"V. Hartonas-Garmhausen","year":"1999","unstructured":"V. Hartonas-Garmhausen, S. Campos and E.M. Clarke. ProbVerus: probabilistic symbolic model checking. In ARTS, LNCS 1601: 96\u2013111, 1999. 348"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"B.R. Haverkort. Performance of Computer Communication Systems: A Model-Based Approach. John Wiley & Sons, 1998. 351","DOI":"10.1002\/0470841923"},{"key":"24_CR20","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.G. Niemegeers. Performability modelling tools and techniques. Perf. Ev., 25: 17\u201340, 1996. 350","journal-title":"Perf. Ev."},{"key":"24_CR21","unstructured":"H. Hermanns, U. Herzog and J.-P. Katoen. Process algebra for performance evaluation. Th. Comp. Sci., 2000 (to appear). 348"},{"issue":"1\u20134","key":"24_CR22","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. Perf. Ev., 39(1\u20134): 5\u201335, 2000. 351, 359","journal-title":"Perf. Ev."},{"key":"24_CR23","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. 355, 356, 360"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996. 348","DOI":"10.1017\/CBO9780511569951"},{"issue":"9","key":"24_CR25","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. 358","journal-title":"IEEE J. on Sel. Areas in Comms."},{"issue":"10","key":"24_CR26","doi-asserted-by":"publisher","first-page":"1093","DOI":"10.1109\/32.99196","volume":"17","author":"B. Plateau","year":"1991","unstructured":"B. Plateau and K. Atif, Stochastic automata networks for modeling parallel systems. IEEE Tr. on Softw. Eng., 17(10): 1093\u20131108, 1991. 348","journal-title":"IEEE Tr. on Softw. Eng."},{"key":"24_CR27","unstructured":"W. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton Univ. Press, 1994. 348, 349, 350, 351, 355"},{"key":"24_CR28","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R.E. Tarjan","year":"1972","unstructured":"R.E. Tarjan. Depth-first search and linear graph algorithms. SIAM J. of Comp., 1: 146\u2013160, 1972. 351","journal-title":"SIAM J. of Comp."},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi. Automatic verification of probabilistic concurrent finite state programs. In Proc. IEEE Symp. on Found. of Comp. Sci., pp. 327\u2013338, 1985. 347","DOI":"10.1109\/SFCS.1985.12"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46419-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T17:07:03Z","timestamp":1556730423000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46419-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672821","9783540464198"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-46419-0_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2000]]}}}