{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:42:00Z","timestamp":1778298120006,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540425564","type":"print"},{"value":"9783540448044","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44804-7_3","type":"book-chapter","created":{"date-parts":[[2007,7,20]],"date-time":"2007-07-20T18:22:41Z","timestamp":1184955761000},"page":"39-56","source":"Crossref","is-referenced-by-count":73,"title":["Reachability Analysis of Probabilistic Systems by Successive Refinements"],"prefix":"10.1007","author":[{"given":"Pedro R.","family":"D\u2019Argenio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bertrand","family":"Jeannet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henrik E.","family":"Jensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,8,30]]},"reference":[{"key":"3_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1007\/BFb0084802","volume-title":"Procs. of CONCUR 92, Stony Brook, NY","author":"R. Alur","year":"1992","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, and H. Wong-Toi. Minimization of timed transition systems. In R. Cleaveland, ed., Procs. of CONCUR 92, Stony Brook, NY, LNCS 630, pp. 340\u2013354. Springer, 1992."},{"key":"3_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-60045-0_48","volume-title":"Procs. of the 7th CAV, Li\u00e8ge","author":"A. Aziz","year":"1995","unstructured":"A. Aziz, V. Singhal, F. Balarin, R.K. Bryton, and A.L. Sangiovanni-Vincentelli. It usually works:the temporal logics of stochastic systems. In P. Wolper, ed., Procs. of the 7th CAV, Li\u00e8ge, LNCS 939, pp. 155\u2013165. Springer, 1995."},{"issue":"2\/3","key":"3_CR3","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"R.I. Bahar","year":"1997","unstructured":"R.I. Bahar, E.A. Frohm, C.M. Gaona, G.D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic decision diagrams and their applications. Formal Methods in System Design, 10(2\/3):171\u2013206, 1997.","journal-title":"Formal Methods in System Design"},{"key":"3_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"Procs. of CONCUR 99, Eindhoven","author":"C. Baier","year":"1999","unstructured":"C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In J.C.M. Baeten and S. Mauw, eds., Procs. of CONCUR 99, Eindhoven, LNCS 1664, pp. 146\u2013161. Springer, 1999."},{"key":"3_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Procs. 15th FSTTCS, Pune","author":"A. Bianco","year":"1995","unstructured":"A. Bianco and L. de Alfaro. Model checking of probabilistic and non-deterministic systems. In Procs. 15 th FSTTCS, Pune, LNCS 1026, pp. 499\u2013513. Springer, 1995."},{"key":"3_CR6","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1016\/0167-6423(92)90018-7","volume":"18","author":"A. Bouajjani","year":"1992","unstructured":"A. Bouajjani, J. C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel. Minimal state graph generation. Science of Computer Programming, 18:247\u2013269, 1992.","journal-title":"Science of Computer Programming"},{"key":"3_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"416","DOI":"10.1007\/BFb0035403","volume-title":"Procs. of the 3rd TACAS, Enschede","author":"P.R. D\u2019Argenio","year":"1997","unstructured":"P.R. D\u2019Argenio, J.-P. Katoen, T.C. Ruys, and J. Tretmans. The bounded retransmission protocol must be on time! In E. Brinksma, ed., Procs. of the 3rd TACAS, Enschede, LNCS 1217, pp. 416\u2013431. Springer, 1997."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"P.R. D\u2019Argenio, B. Jeannet, H.E. Jensen, and K.G. Larsen. Reachability Analysis of Probabilistic Systems by Successive Refinements. CTIT Technical Report, 2001. To appear.","DOI":"10.1007\/3-540-44804-7_3"},{"key":"3_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Procs. of the 6th Workshop TACAS, Berlin","author":"L. Alfaro de","year":"2000","unstructured":"L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, and R. Segala. Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation. In Graf and Schwartzbach [11]."},{"issue":"2\/3","key":"3_CR10","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1023\/A:1008647823331","volume":"10","author":"M. Fujita","year":"1997","unstructured":"M. Fujita, P.C. McGeer, and J.C.-Y. Yang. Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. Formal Methods in System Design, 10(2\/3):149\u2013169, April 1997.","journal-title":"Formal Methods in System Design"},{"key":"3_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-46419-0","volume-title":"Procs. of the 6th Workshop TACAS, Berlin","author":"S. Graf","year":"2000","unstructured":"S. Graf and M. Schwartzbach, eds. Procs. of the 6th Workshop TACAS, Berlin, LNCS 1785. Springer, 2000."},{"key":"3_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Procs. of the 5th AMAST Conference, Munich","author":"J.F. Groote","year":"1996","unstructured":"J.F. Groote and J. van de Pol. A bounded retransmission protocol for large data packets \u2014 A case study in computer checked algebraic verification. In M. Wirsing and M. Nivat, eds., Procs. of the 5 th AMAST Conference, Munich, LNCS 1101. Springer, 1996."},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H.A. Hansson","year":"1994","unstructured":"H.A. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6:512\u2013535, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"3_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/3-540-48778-6_6","volume-title":"Procs of the 5th ARTS, Bamberg","author":"V. Hartonas-Garmhausen","year":"1999","unstructured":"V. Hartonas-Garmhausen and S. Campos. ProbVerus: Probabilistic symbolic model mhecking. In In Katoen [24], pp. 96\u2013110."},{"key":"3_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/3-540-58085-9_75","volume-title":"Procs. International Workshop TYPES\u201993, Nijmegen","author":"L. Helmink","year":"1994","unstructured":"L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-checking a data link protocol. In H. Barendregt and T. Nipkow, eds., Procs. International Workshop TYPES\u201993, Nijmegen, LNCS 806, pp. 127\u2013165. Springer, 1994."},{"key":"3_CR16","unstructured":"H. Hermanns. Personal communication, 2001."},{"key":"3_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/3-540-46419-0_24","volume-title":"A Markov chain model checker","author":"H. Hermanns","year":"2000","unstructured":"H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. A Markov chain model checker. In Graf and Schwartzbach [11], p. 347\u2013362."},{"key":"3_CR18","unstructured":"H. Hermanns, J. Meyer-Kayser, and M. Siegle. Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In B. Plateau, W.J. Stewart, and M. Silva, eds., 3rd Int. Workshop on the Numerical Solution of Markov Chains, pp. 188\u2013207. Prensas Universitarias de Zaragoza, 1999."},{"key":"3_CR19","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, 1985."},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"M. Huth and M. Kwiatkowska. Quantitative analysis and model checking. In Procs. 12 th Annual Symposium on Logic in Computer Science, Warsaw. IEEE Press, 1997.","DOI":"10.1109\/LICS.1997.614940"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"B. Jeannet. Dynamic partitioning in linear relation analysis. Application to the verification of reactive systems. Formal Methods in System Design, 2001. To appear.","DOI":"10.7146\/brics.v7i38.20204"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"B. Jonsson and K.G. Larsen. Specification and refinement of probailistic processes. In Procs. 6 th Annual Symposium on Logic in Computer Science, Amsterdam, pp. 266\u2013277. IEEE Press, 1991.","DOI":"10.1109\/LICS.1991.151651"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"B. Jonsson, K.G. Larsen, and W. Yi. Probabilistic extensions in process algebras. In J.A. Bergstra, A. Ponse, and S. Smolka, eds., Handbook of Process Algebras, pp. 685\u2013710. Elsevier, 2001.","DOI":"10.1016\/B978-044482830-9\/50029-1"},{"key":"3_CR24","series-title":"Lect Notes Comput Sci","volume-title":"Procs of the 5th ARTS, Bamberg","year":"1999","unstructured":"J.-P. Katoen, ed. Procs of the 5th ARTS, Bamberg, LNCS 1601. Springer, 1999."},{"key":"3_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/3-540-48778-6_5","volume-title":"Procs of the 5th ARTS, Bamberg","author":"M. Kwiatkowska","year":"1999","unstructured":"M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston. Automatic verification of real-time systems with probability distributions. In Katoen [24], pp. 75\u201395."},{"key":"3_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K.G. Larsen","year":"1991","unstructured":"K.G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94:1\u201328, 1991.","journal-title":"Information and Computation"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"M.L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, 1994.","DOI":"10.1002\/9780470316887"},{"key":"3_CR28","unstructured":"R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology, 1995."},{"key":"3_CR29","series-title":"Lect Notes Comput Sci","volume-title":"Procs. of the 8th CAV, New Brunswick, New Jersey","author":"H. Sipma","year":"1996","unstructured":"H. Sipma, T.E. Uribe, and Z. Manna. Deductive model checking. In R. Alur and T.A. Henzinger, eds. Procs. of the 8th CAV, New Brunswick, New Jersey, LNCS 1102. Springer, 1996."},{"key":"3_CR30","unstructured":"F. Somenzi. Cudd: Colorado University Decision Diagram Package. ftp:\/\/vlsi.colorado.edu\/pub ."},{"key":"3_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/BFb0055344","volume-title":"Procs. of the 5th FTRTFT, Lyngby","author":"R. F. L. Spelberg","year":"1998","unstructured":"R. F. Lutje Spelberg, W. J. Toetenel, and M. Ammerlaan. Partition refinement in real-time model checking. In A.P. Ravn and H. Rischel, eds., Procs. of the 5th FTRTFT, Lyngby, LNCS 1486, pp. 143\u2013157. Springer, 1998."}],"container-title":["Lecture Notes in Computer Science","Process Algebra and Probabilistic Methods. Performance Modelling and Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44804-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T20:46:36Z","timestamp":1737319596000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44804-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425564","9783540448044"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-44804-7_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}