{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:24:12Z","timestamp":1725891852984},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540472377"},{"type":"electronic","value":"9783540472384"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901914_5","type":"book-chapter","created":{"date-parts":[[2006,10,10]],"date-time":"2006-10-10T01:21:43Z","timestamp":1160443303000},"page":"24-38","source":"Crossref","is-referenced-by-count":6,"title":["Eager Markov Chains"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Noomene","family":"Ben Henda","sequence":"additional","affiliation":[]},{"given":"Richard","family":"Mayr","sequence":"additional","affiliation":[]},{"given":"Sven","family":"Sandberg","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/3-540-44618-4_24","volume-title":"CONCUR 2000 - Concurrency Theory","author":"P.A. Abdulla","year":"2000","unstructured":"Abdulla, P.A., Baier, C., Iyer, P., Jonsson, B.: Reasoning about probabilistic lossy channel systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, p. 320. Springer, Heidelberg (2000)"},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1006\/inco.1999.2843","volume":"160","author":"P.A. Abdulla","year":"2000","unstructured":"Abdulla, P.A., \u010cer\u0101ns, K., Jonsson, B., Yih-Kuen, T.: Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation\u00a0160, 109\u2013127 (2000)","journal-title":"Information and Computation"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Henda, N.B., Mayr, R.: Verifying infinite Markov chains with a finite attractor or the global coarseness property. In: Proc. LICS 2005, pp. 127\u2013136 (2005)","DOI":"10.1109\/LICS.2005.54"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Henda, N.B., Mayr, R., Sandberg, S.: Eager Markov chains. Technical Report 2006-009, Department of Information Technology, Uppsala University (2006)","DOI":"10.1007\/11901914_5"},{"key":"5_CR5","volume-title":"Proc. QEST 2006","author":"P.A. Abdulla","year":"2006","unstructured":"Abdulla, P.A., Henda, N.B., Mayr, R., Sandberg, S.: Limiting behavior of Markov chains with eager attractors. In: Proc. QEST 2006. IEEE Computer Society Press, Los Alamitos (to appear, 2006)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-36576-1_3","volume-title":"Foundations of Software Science and Computational Structures","author":"P.A. Abdulla","year":"2003","unstructured":"Abdulla, P.A., Rabinovich, A.: Verification of probabilistic systems with faulty communication. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 39\u201353. Springer, Heidelberg (2003)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1031","DOI":"10.1007\/11523468_83","volume-title":"Automata, Languages and Programming","author":"E. Asarin","year":"2005","unstructured":"Asarin, E., Collins, P.: Noisy Turing machines. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 1031\u20131042. Springer, Heidelberg (2005)"},{"issue":"1","key":"5_CR8","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A. Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Trans. on Computational Logic\u00a01(1), 162\u2013170 (2000)","journal-title":"ACM Trans. on Computational Logic"},{"issue":"2","key":"5_CR9","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1016\/j.ipl.2005.09.011","volume":"97","author":"C. Baier","year":"2006","unstructured":"Baier, C., Bertrand, N., Schnoebelen, P.: A note on the attractor-property of infinite-state Markov chains. Information Processing Letters\u00a097(2), 58\u201363 (2006)","journal-title":"Information Processing Letters"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/3-540-48778-6_3","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"C. Baier","year":"1999","unstructured":"Baier, C., Engelen, B.: Establishing qualitative properties for probabilistic lossy channel systems: An algorithmic approach. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, pp. 34\u201352. Springer, Heidelberg (1999)"},{"issue":"2","key":"5_CR11","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1145\/1059816.1059819","volume":"32","author":"C. Baier","year":"2005","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model checking meets performance evaluation. ACM Performance Evaluation Review\u00a032(2), 10\u201315 (2005)","journal-title":"ACM Performance Evaluation Review"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-45798-4_12","volume-title":"Performance Evaluation of Complex Systems: Techniques and Tools","author":"C. Baier","year":"2002","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Automated performance and dependability evaluation using model checking. In: Calzarossa, M.C., Tucci, S. (eds.) Performance 2002. LNCS, vol.\u00a02459, pp. 261\u2013289. Springer, Heidelberg (2002)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/3-540-36576-1_8","volume-title":"Foundations of Software Science and Computational Structures","author":"N. Bertrand","year":"2003","unstructured":"Bertrand, N., Schnoebelen, P.: Model checking lossy channels systems is probably decidable. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 120\u2013135. Springer, Heidelberg (2003)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/11590156_30","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"T. Br\u00e1zdil","year":"2005","unstructured":"Br\u00e1zdil, T., Ku\u010dera, A.: Computing the expected accumulated reward and gain for a subclass of infinite Markov chains. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol.\u00a03821, pp. 372\u2013383. Springer, Heidelberg (2005)"},{"key":"5_CR15","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"4","key":"5_CR16","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM\u00a042(4), 857\u2013907 (1995)","journal-title":"Journal of the ACM"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/3-540-46419-0_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Alfaro de","year":"2000","unstructured":"de Alfaro, L., Kwiatkowska, M.Z., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using mtbdds and the Kronecker representation. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol.\u00a01785, pp. 123\u2013137. Springer, Heidelberg (2000)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-30538-5_2","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J. Esparza","year":"2004","unstructured":"Esparza, J., Etessami, K.: Verifying probabilistic procedural programs. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 16\u201331. Springer, Heidelberg (2004)"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ku\u010dera, A., Mayr, R.: Model checking probabilistic pushdown automata. In: Proc. LICS 2004, pp. 12\u201321 (2004)","DOI":"10.1109\/LICS.2004.1319596"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ku\u010dera, A., Mayr, R.: Quantitative analysis of probabilistic pushdown automata: Expectations and variances. In: Proc. LICS 2005, pp. 117\u2013126 (2005)","DOI":"10.1109\/LICS.2005.39"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-31980-1_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Etessami","year":"2005","unstructured":"Etessami, K., Yannakakis, M.: Algorithmic verification of recursive probabilistic state machines. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 253\u2013270. Springer, Heidelberg (2005)"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-31856-9_28","volume-title":"STACS 2005","author":"K. Etessami","year":"2005","unstructured":"Etessami, K., Yannakakis, M.: Recursive Markov Chains, Stochastic Grammars, and Monotone Systems of Nonlinear Equations. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol.\u00a03404, pp. 340\u2013352. Springer, Heidelberg (2005)"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"891","DOI":"10.1007\/11523468_72","volume-title":"Automata, Languages and Programming","author":"K. Etessami","year":"2005","unstructured":"Etessami, K., Yannakakis, M.: Recursive Markov decision processes and recursive stochastic games. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 891\u2013903. Springer, Heidelberg (2005)"},{"key":"5_CR24","volume-title":"An Introduction to Probability Theory and Its Applications","author":"W. Feller","year":"1966","unstructured":"Feller, W.: An Introduction to Probability Theory and Its Applications, 2nd edn., vol.\u00a01. Wiley & Sons, Chichester (1966)","edition":"2"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Hart, S., Sharir, M.: Probabilistic temporal logics for finite and bounded models. In: Proc. STOC 1984, pp. 1\u201313 (1984)","DOI":"10.1145\/800057.808660"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1007\/BFb0030633","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"P. Iyer","year":"1997","unstructured":"Iyer, P., Narasimha, M.: Probabilistic lossy channel systems. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol.\u00a01214, pp. 667\u2013681. Springer, Heidelberg (1997)"},{"issue":"2","key":"5_CR27","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1145\/1059816.1059820","volume":"32","author":"M. Kwiatkowska","year":"2005","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking in practice: Case studies with PRISM. ACM Performance Evaluation Review\u00a032(2), 16\u201321 (2005)","journal-title":"ACM Performance Evaluation Review"},{"key":"5_CR28","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0019-9958(82)91022-1","volume":"53","author":"D. Lehmann","year":"1982","unstructured":"Lehmann, D., Shelah, S.: Reasoning with time and chance. Information and Control\u00a053, 165\u2013198 (1982)","journal-title":"Information and Control"},{"key":"5_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1008","DOI":"10.1007\/3-540-45061-0_78","volume-title":"Automata, Languages and Programming","author":"A. Rabinovich","year":"2003","unstructured":"Rabinovich, A.: Quantitative analysis of probabilistic lossy channel systems. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol.\u00a02719, pp. 1008\u20131021. Springer, Heidelberg (2003)"},{"key":"5_CR30","unstructured":"St\u01cenic\u01ce, P.: Good lower and upper bounds on binomial coefficients. Journal of Inequalities in Pure and Applied Mathematics\u00a02(3) (2001)"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. FOCS 1985, pp. 327\u2013338 (1985)","DOI":"10.1109\/SFCS.1985.12"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901914_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,21]],"date-time":"2019-04-21T11:23:04Z","timestamp":1555845784000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901914_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540472377","9783540472384"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/11901914_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}