{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T13:30:23Z","timestamp":1760707823017},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439134"},{"type":"electronic","value":"9783540456056"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45605-8_10","type":"book-chapter","created":{"date-parts":[[2007,5,16]],"date-time":"2007-05-16T02:15:19Z","timestamp":1179281719000},"page":"152-168","source":"Crossref","is-referenced-by-count":5,"title":["Model Checking CSL until Formulae with Random Time Bounds"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ant\u00f3nio","family":"Pacheco","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"10_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume-title":"Proc. CAV\u201996","author":"A. Aziz","year":"1996","unstructured":"A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Verifying continuous time Markov chains. In Proc. CAV\u201996, volume 1102 of LNCS, pages 269\u2013276. Springer, 1996."},{"issue":"1","key":"10_CR2","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. ACM Transactions on Computational Logic, 1(1):162\u2013170, 2000.","journal-title":"ACM Transactions on Computational Logic"},{"key":"10_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1007\/10722167_28","volume-title":"Proc. CAV 2000","author":"C. Baier","year":"2000","unstructured":"C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model checking continuous-time Markov chains by transient analysis. In Proc. CAV 2000, volume 1855 of LNCS, pages 358\u2013372, 2000."},{"key":"10_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"Proc. CONCUR\u201999","author":"C. Baier","year":"1999","unstructured":"C. Baier, J.-P. Katoen, and H. Hermanns. Approximative symbolic model checking of continuous-time Markov chains. In Proc. CONCUR\u201999, volume 1664 of LNCS, pages 146\u2013162. Springer, 1999."},{"issue":"2","key":"10_CR5","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. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"6","key":"10_CR6","doi-asserted-by":"publisher","first-page":"835","DOI":"10.1109\/90.650143","volume":"5","author":"M. Crovella","year":"1997","unstructured":"M. Crovella and A. Bestavros. Self-similarity in world wide Web traffic: evidence and possible causes. IEEE\/ACM Transactions on Networking, 5(6):835\u2013846, 1997.","journal-title":"IEEE\/ACM Transactions on Networking"},{"issue":"4","key":"10_CR7","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1145\/42404.42409","volume":"31","author":"B. Fox","year":"1988","unstructured":"B. Fox and P. Glynn. Computing Poisson probabilities. Communications of the ACM, 31(4):440\u2013445, 1988.","journal-title":"Communications of the ACM"},{"key":"10_CR8","unstructured":"R. German. Performance Analysis of Communication Systems: Modeling with Non-Markovian Stochastic Petri Nets. John Wiley and Sons, 2000."},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"J. Grandell. Mixed Poisson Processes. Chapman & Hall, 1997.","DOI":"10.1007\/978-1-4899-3117-7"},{"issue":"2","key":"10_CR10","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. Miller. The randomization technique as a modeling tool and solution procedure for transient Markov processes. Operations Research, 32(2):343\u2013361, 1984.","journal-title":"Operations Research"},{"key":"10_CR11","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 probability. Formal Aspects of Computing, 6:512\u2013535, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"A. Jensen. Markov chains as an aid in the study of Markov processes. Skandinavisk Aktuarietidsskrift, Marts, pages 87\u201391, 1953.","DOI":"10.1080\/03461238.1953.10419459"},{"key":"10_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/3-540-44804-7_2","volume-title":"Proc. PAPM-PROBMIV 2001","author":"J.-P. Katoen","year":"2001","unstructured":"J.-P. Katoen, M. Kwiatkowska, G. Norman, and D. Parker. Faster and symbolic CTMC model checking. In Proc. PAPM-PROBMIV 2001, volume 2165 of LNCS, pages 23\u201338. Springer, 2001."},{"key":"10_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/3-540-46002-0_5","volume-title":"Proc. TACAS 2002","author":"M. Kwiatkowska","year":"2002","unstructured":"M. Kwiatkowska, G. Norman, and D. Parker. Probabilistic symbolic model checking with PRISM: A hybrid approach. In Proc. TACAS 2002, volume 2280 of LNCS, pages 52\u201366. Springer, 2002."},{"key":"10_CR15","series-title":"Lect Notes Comput Sci","first-page":"57","volume-title":"Proc PAPM-PROBMIV 2001","author":"G.I. L\u00f3pes","year":"2001","unstructured":"G.I. L\u00f3pes, H. Hermanns, and J.-P. Katoen. Beyond memoryless distributions. In Proc PAPM-PROBMIV 2001, volume 2165 of LNCS, pages 57\u201370. Springer, 2001."},{"key":"10_CR16","unstructured":"S. Moln\u00e1r and I. Maricza, editors. Source characterization in broadband networks. COST 257 Mid-term seminar interim report on source characterization, 2000."},{"key":"10_CR17","unstructured":"J. Muppala and K. Trivedi. Queueing Systems, Queueing and Related Models, chapter Numerical Transient Solution of Finite Markovian Queueing Systems, pages 262\u2013284. Oxford University Press, 1992."},{"issue":"1","key":"10_CR18","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1017\/S0515036100006796","volume":"12","author":"H. Panjer","year":"1982","unstructured":"H. Panjer. Recursive evaluation of a family of compound distributions. Astin Bulletin, 12(1):22\u201326, 1982.","journal-title":"Astin Bulletin"},{"key":"10_CR19","unstructured":"PRISM web page. http:\/\/www.cs.bham.ac.uk\/~dxp\/prism\/ ."},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"W. J. Stewart. Introduction to the Numerical Solution of Markov Chains. Princeton, 1994.","DOI":"10.1515\/9780691223384"}],"container-title":["Lecture Notes in Computer Science","Process Algebra and Probabilistic Methods: Performance Modeling and Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45605-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T21:31:55Z","timestamp":1683840715000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45605-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439134","9783540456056"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-45605-8_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}