{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T05:04:55Z","timestamp":1737435895891,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540424970"},{"type":"electronic","value":"9783540446859"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44685-0_12","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T10:16:21Z","timestamp":1186740981000},"page":"169-183","source":"Crossref","is-referenced-by-count":11,"title":["Symbolic Computation of Maximal Probabilisti Reachability"],"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":"Jeremy","family":"Sproston","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,8,22]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, K. Cer\u016bans, B. Jonsson, and Y.-K. Tsay. General decidability theorems for infinite-state systems. In Proc. LICS\u201996, pages 313\u2013321. IEEE Computer Society Press, 1996.","key":"12_CR1","DOI":"10.1109\/LICS.1996.561359"},{"issue":"1","key":"12_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1):3\u201334, 1995.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"12_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183\u2013235, 1994.","journal-title":"Theoretical Computer Science"},{"key":"12_CR4","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. Springer, 2000."},{"issue":"3","key":"12_CR5","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C. Baier","year":"1998","unstructured":"C. Baier and M. Z. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11(3):125\u2013155, 1998.","journal-title":"Distributed Computing"},{"key":"12_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Proc. FSTTCS\u201995","author":"A. Bianco","year":"1995","unstructured":"A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Proc. FSTTCS\u201995, volume 1026 of LNCS, pages 499\u2013513. Springer, 1995."},{"doi-asserted-by":"crossref","unstructured":"J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Approximating labeled Markov processes. In Proc. LICS 2000, pages 95\u2013106. IEEE Computer Society Press, 2000.","key":"12_CR7","DOI":"10.1109\/LICS.2000.855759"},{"doi-asserted-by":"crossref","unstructured":"B. Haverkort. Performance of Computer Communication Systems: A Model-Based Approach. John Wiley and Sons, 1998.","key":"12_CR8","DOI":"10.1002\/0470841923"},{"doi-asserted-by":"crossref","unstructured":"M. R. Henzinger, T. A. Henzinger, and P. W. Kopke. Computing simulations on finite and infinite graphs. In Proc. FOCS\u201995, pages 453\u2013462. IEEE Computer Society Press, 1995.","key":"12_CR9","DOI":"10.1109\/SFCS.1995.492576"},{"key":"12_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45449-7","volume-title":"A classification of symbolic transition systems","author":"T. A. Henzinger","year":"2001","unstructured":"T. A. Henzinger, R. Majumdar, and J.-F. Raskin. A classification of symbolic transition systems, 2001. Preliminary version appeared in Proc. STACS 2000, volume 1770 of LNCS, pages 13\u201334, Springer, 2000."},{"issue":"2","key":"12_CR11","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. A. Henzinger","year":"1994","unstructured":"T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193\u2013244, 1994.","journal-title":"Information and Computation"},{"key":"12_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1007\/BFb0030633","volume-title":"Proc. TAP-SOFT\u201997","author":"P. Iyer","year":"1997","unstructured":"P. Iyer and M. Narasimha. Probabilistic lossy channel systems. In Proc. TAP-SOFT\u201997, volume 1214 of LNCS, pages 667\u2013681. Springer, 1997."},{"doi-asserted-by":"crossref","unstructured":"J. G. Kemeny, J. L. Snell, and A. W. Knapp. Denumerable Markov Chains. Graduate Texts in Mathematics. Springer, 2nd edition, 1976.","key":"12_CR13","DOI":"10.1007\/978-1-4684-9455-6"},{"key":"12_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/3-540-44618-4_11","volume-title":"Proc. CONCUR 2000","author":"M. Z. Kwiatkowska","year":"2000","unstructured":"M. Z. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Verifying quantitative properties of continuous probabilistic timed automata. In Proc. CONCUR 2000, volume 1877 of LNCS, pages 123\u2013137. Springer, 2000."},{"doi-asserted-by":"crossref","unstructured":"M. Z. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science, 2001. Special issue on ARTS\u201999. To appear.","key":"12_CR15","DOI":"10.1016\/S0304-3975(01)00046-9"},{"doi-asserted-by":"crossref","unstructured":"M. Z. Kwiatkowska, G. Norman, and J. Sproston. Symbolic computation of maximal probabilistic reachability. Technical Report CSR-01-5, School of Computer Science, University of Birmingham, 2001.","key":"12_CR16","DOI":"10.1007\/3-540-44685-0_12"},{"key":"12_CR17","first-page":"40","volume":"70","author":"P. Pettersson","year":"2000","unstructured":"P. Pettersson and K. G. Larsen. Uppaal2k. Bulletin of the European Association for Theoretical Computer Science, 70:40\u201344, 2000.","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"12_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-45352-0_5","volume-title":"Proc. FTRTFT 2000","author":"J. Sproston","year":"2000","unstructured":"J. Sproston. Decidable model checking of probabilistic hybrid automata. In Proc. FTRTFT 2000, volume 1926 of LNCS, pages 31\u201345. Springer, 2000."},{"unstructured":"J. Sproston. Model Checking of Probabilistic Timed and Hybrid Systems. PhD thesis, University of Birmingham, 2001.","key":"12_CR19"},{"key":"12_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-48778-6_4","volume-title":"Proc. ARTS\u201999","author":"M. I. A. Stoelinga","year":"1999","unstructured":"M. I. A. Stoelinga and F. Vaandrager. Root contention in IEEE1394. In Proc. ARTS\u201999, volume 1601 of LNCS, pages 53\u201374. Springer, 1999."},{"doi-asserted-by":"crossref","unstructured":"M. Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proc. FOCS\u201985, pages 327\u2013338. IEEE Computer Society Press, 1985.","key":"12_CR21","DOI":"10.1109\/SFCS.1985.12"},{"doi-asserted-by":"crossref","unstructured":"P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proc. POPL\u201986, pages 184\u2013193. ACM, 1986.","key":"12_CR22","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2001 \u2014 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44685-0_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T07:24:29Z","timestamp":1737357869000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44685-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540424970","9783540446859"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-44685-0_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}