{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,19]],"date-time":"2024-11-19T16:22:40Z","timestamp":1732033360659},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540253334"},{"type":"electronic","value":"9783540319801"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31980-1_16","type":"book-chapter","created":{"date-parts":[[2010,7,11]],"date-time":"2010-07-11T22:44:59Z","timestamp":1278888299000},"page":"237-252","source":"Crossref","is-referenced-by-count":7,"title":["Model Checking Infinite-State Markov Chains"],"prefix":"10.1007","author":[{"given":"Anne","family":"Remke","sequence":"first","affiliation":[]},{"given":"Boudewijn R.","family":"Haverkort","sequence":"additional","affiliation":[]},{"given":"Lucia","family":"Cloth","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-28644-8_3","volume-title":"CONCUR 2004 - Concurrency Theory","author":"P. Abdulla","year":"2004","unstructured":"Abdulla, P., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 35\u201348. Springer, Heidelberg (2004)"},{"issue":"1","key":"16_CR2","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A. Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., 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":"16_CR3","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":"7","key":"16_CR4","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.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering\u00a029(7), 524\u2013541 (2003)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"16_CR5","unstructured":"Bell, A.: Distributed evaluation of stochasic Petri nets. PhD thesis, Dept. of Computer Science, RWTH Aachen (2004)"},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1145\/302405.302672","volume-title":"Proc. 21st Int. Conf. on Software Engineering","author":"M.B. Dwyer","year":"1999","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specification for finite-state verification. In: Proc. 21st Int. Conf. on Software Engineering, pp. 411\u2013420. IEEE CS Press, Los Alamitos (1999)"},{"key":"16_CR7","unstructured":"El-Rayes, A., Kwiatkowska, M., Norman, G.: Solving infinite stochastic process algebra models through matrix-geometric methods. In: Proc. 7th Process Algebras and Performance Modelling Workshop (PAPM 1999), pp. 41\u201362. University of Zaragoza (1999)"},{"issue":"2","key":"16_CR8","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1287\/opre.32.2.343","volume":"32","author":"D. Gross","year":"1984","unstructured":"Gross, D., Miller, D.R.: The randomization technique as a modeling tool and solution procedure for transient Markov processes. Operations Research\u00a032(2), 343\u2013361 (1984)","journal-title":"Operations Research"},{"key":"16_CR9","doi-asserted-by":"publisher","DOI":"10.1002\/0470841923","volume-title":"Performance of Computer Communication Systems","author":"B.R. Haverkort","year":"1998","unstructured":"Haverkort, B.R.: Performance of Computer Communication Systems. John Wiley & Sons, Chichester (1998)"},{"key":"16_CR10","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1109\/RELDI.2000.885410","volume-title":"Proc. 19th IEEE Symposium on Reliable Distributed Systems (SRDS 2000)","author":"B.R. Haverkort","year":"2000","unstructured":"Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the use of model checking techniques for dependability evaluation. In: Proc. 19th IEEE Symposium on Reliable Distributed Systems (SRDS 2000), pp. 228\u2013237. IEEE CS Press, Los Alamitos (2000)"},{"issue":"2","key":"16_CR11","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/s100090100072","volume":"4","author":"H. Hermanns","year":"2003","unstructured":"Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: A tool for model-checking Markov chains. International Journal on Software Tools for Technology Transfer\u00a04(2), 153\u2013172 (2003)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"16_CR12","unstructured":"Katoen, J.-P.: Concepts, Algorithms, and Tools for Model Checking. In: Arbeitsberichte des IMMD, vol.\u00a032(1), Friedrich-Alexander Universit\u00e4t Erlangen N\u00fcrnberg (June 1999)"},{"issue":"2","key":"16_CR13","doi-asserted-by":"publisher","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. International Journal on Software Tools for Technology Transfer\u00a06(2), 128\u2013142 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"16_CR14","doi-asserted-by":"publisher","first-page":"650","DOI":"10.2307\/3214773","volume":"30","author":"G. Latouche","year":"1993","unstructured":"Latouche, G., Ramaswami, V.: A logarithmic reduction algorithm for quasi birth and death processes. Journal of Applied Probability\u00a030, 650\u2013674 (1993)","journal-title":"Journal of Applied Probability"},{"key":"16_CR15","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/978-3-642-79917-4_6","volume-title":"Quantitative Models in Parallel Systems","author":"I. Mitrani","year":"1995","unstructured":"Mitrani, I., Ost, A., Rettelbach, M.: TIPP and the spectral expansion method. In: Baccelli, F., Jean-Marie, A., Mitrani, I. (eds.) Quantitative Models in Parallel Systems, pp. 99\u2013113. Springer, Heidelberg (1995)"},{"key":"16_CR16","volume-title":"Matrix Geometric Solutions in Stochastic Models: An Algorithmic Approach","author":"M.F. Neuts","year":"1981","unstructured":"Neuts, M.F.: Matrix Geometric Solutions in Stochastic Models: An Algorithmic Approach. Johns Hopkins University Press, Baltimore (1981)"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Ost, A.: Performance of Communication Systems. A Model-Based Approach with Matrix-Geometric Methods. PhD thesis, Dept. of Computer Science, RWTH Aachen (2001)","DOI":"10.1007\/978-3-662-04421-6"},{"key":"16_CR18","unstructured":"Remke, A.: Model Checking Quasi Birth Death Processes. Master\u2019s thesis, Dept. of Computer Science, RWTH Aachen (2004), http:\/\/www.cs.utwente.nl\/~anne\/pub\/modelchecking.pdf"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/978-3-540-24611-4_13","volume-title":"Validation of Stochastic Systems","author":"P.. Schnoebelen","year":"2004","unstructured":"Schnoebelen, P.: The verification of probabilistic lossy channel systems. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol.\u00a02925, pp. 445\u2013465. Springer, Heidelberg (2004)"},{"issue":"3","key":"16_CR20","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1080\/15326348908807119","volume":"5","author":"J. Zhang","year":"1989","unstructured":"Zhang, J., Coyle, E.J.: Transient analysis of quasi-birth-death processes. Stochastic Models\u00a05(3), 459\u2013496 (1989)","journal-title":"Stochastic Models"}],"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\/978-3-540-31980-1_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:32:42Z","timestamp":1605760362000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31980-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540253334","9783540319801"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31980-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}