{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T01:10:42Z","timestamp":1773105042591,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540439134","type":"print"},{"value":"9783540456056","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45605-8_5","type":"book-chapter","created":{"date-parts":[[2007,5,16]],"date-time":"2007-05-16T02:15:19Z","timestamp":1179281719000},"page":"57-76","source":"Crossref","is-referenced-by-count":36,"title":["Reduction and Refinement Strategies for Probabilistic Analysis"],"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":[[2002,7,4]]},"reference":[{"key":"5_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1007\/BFb0084802","volume-title":"Proceedings of the Third Conference on Concurrency Theory CONCUR\u2019 92","author":"R. Alur","year":"1992","unstructured":"R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. Minimization of timed transition systems. In Proceedings of the Third Conference on Concurrency Theory CONCUR\u2019 92, volume 630 of LNCS, pages 340\u2013354. Springer-Verlag, 1992."},{"key":"5_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Computer Aided Verification, CAV\u201995","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 Computer Aided Verification, CAV\u201995, volume 939 of LNCS, July 1995."},{"issue":"2\/3","key":"5_CR3","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"R. Bahar","year":"1997","unstructured":"R. Bahar, E. Frohm, C. Gaona, G. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Algebraic decision diagrams and their applications. Formal Methods in System Design, 10(2\/3):171\u2013206, April 1997.","journal-title":"Formal Methods in System Design"},{"key":"5_CR4","series-title":"Lect Notes Comput Sci","volume-title":"CONCUR\u201999","author":"C. Baier","year":"1999","unstructured":"C. Baier, J.-P. Katoen, and H. Hermanns. Approximate symbolic model checking of continuous-time Markov chains. In CONCUR\u201999, volume 1664 of LNCS, 1999."},{"key":"5_CR5","unstructured":"Christel Baier. On Algorithmic Verification Methods for Probabilistic Systems. Habilitation thesis, Faculty for Mathematics and Informatics, University of Mannheim, 1998."},{"key":"5_CR6","unstructured":"M. Berkelaar. LP_Solve: Mixed integer linear program solver, ftp:\/\/ftp.ics.ele.tue.nl\/pub\/lp_solve ."},{"key":"5_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Foundations of Software Technology and Theoretical Computer Science, FSTTCS\u201995","author":"A. Bianco","year":"1995","unstructured":"A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Foundations of Software Technology and Theoretical Computer Science, FSTTCS\u201995, volume 1026 of LNCS, 1995."},{"key":"5_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028779","volume-title":"Computer Aided Verification, CAV\u201998","author":"M. Bozga","year":"1998","unstructured":"M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: A model-checking tool for real-time systems. In Computer Aided Verification, CAV\u201998, volume 1427 of LNCS, July 1998."},{"key":"5_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-44804-7_3","volume-title":"Process Algebra and Probabilistic Methods-Performance Modelling and Verification, PAPM-PROBMIV 2001","author":"P.R. D\u2019Argenio","year":"2001","unstructured":"P.R. D\u2019Argenio, B. Jeannet, H.E. Jensen, and K.G. Larsen. Reachability analysis of probabilistic systems by successive refinements. In Process Algebra and Probabilistic Methods-Performance Modelling and Verification, PAPM-PROBMIV 2001, volume 2165 of LNCS, pages 39\u201356, 2001."},{"key":"5_CR10","unstructured":"Luca de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, 1997."},{"key":"5_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Computer Aided Verification, GAV\u201996","author":"J.-C. Fernandez","year":"1996","unstructured":"J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP (C\u00e6sar \/ Ald\u00e9baran Development Package): A protocol validation and verification toolbox. In Computer Aided Verification, GAV\u201996, volume 1102 of LNCS, July 1996."},{"issue":"2\/3","key":"5_CR12","doi-asserted-by":"crossref","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":"5_CR13","unstructured":"K. Fukuda. Cddlib. ftp:\/\/ftp.ifor.math.ethz.ch\/pub\/fukuda\/cdd ."},{"key":"5_CR14","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":"5_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48778-6_6","volume-title":"AMAST Workshop on Real-Time and Probabilistic Systems, AMAST\u201999","author":"V. Hartonas-Garmhausen","year":"1999","unstructured":"V. Hartonas-Garmhausen and S. Campos. ProbVerus: Probabilistic symbolic model checking. In AMAST Workshop on Real-Time and Probabilistic Systems, AMAST\u201999, volume 1601 of LNCS, 1999."},{"key":"5_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Proc. International Workshop TYPES\u201993","author":"L. Helmink","year":"1994","unstructured":"L. Helmink, M. Sellink, and F. Vaandrager. Proof-checking a data link protocol. In Proc. International Workshop TYPES\u201993, volume 806 of LNCS, 1994."},{"key":"5_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46419-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000","author":"H. Hermanns","year":"2000","unstructured":"H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. A Markov chain model checker. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000, volume 1785 of LNCS, 2000."},{"issue":"5","key":"5_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"G. Holzmann. The model cheker spin. IEEE Transactions on Software Engineering, 23(5):279\u2013295, 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"M. Huth and M. Kwiatkowska. Quantitative analysis and model checking. In Logic in Computer Science, LICS\u201997. IEEE Computer Society Press, 1997.","DOI":"10.1109\/LICS.1997.614940"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"B. Jonsson and K.G. Larsen. Specification and refinement of probabilistic processes. In Procs. 6th Annual Symposium on Logic in Computer Science, pages 266\u2013277. IEEE Press, 1991.","DOI":"10.1109\/LICS.1991.151651"},{"key":"5_CR21","unstructured":"B. Jonsson, K.G. Larsen, and W. Yi. Probabilistic extensions in process algebras. In J.A. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebras. Elsevier, 2001."},{"key":"5_CR22","series-title":"Lect Notes Comput Sci","volume-title":"TOOLS\u20192002","author":"M. Kwiatkowska","year":"2002","unstructured":"M. Kwiatkowska, G. Norman, and D. Parker. PRISM: Probabilistic symbolic model checker. In TOOLS\u20192002, volume 2324 of LNCS, April 2002."},{"key":"5_CR23","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","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 J.P. Katoen, editor, Procs. of the 5th ARTS, volume 1601 of LNCS, pages 75\u201395. Springer, 1999."},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Kim G. Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a nutshell. Springer International Journal of Software Tools for Technology Transfer, 1(1\/2), 1997.","DOI":"10.1007\/s100090050010"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"D. Lehmann and M. Rabin. On the advantages of free choice: A symmetric fully distributed solution to the dining philosophers problem. In Proc. 8th Symposium on Principles of Programming Languages, 1981.","DOI":"10.1145\/567532.567547"},{"key":"5_CR26","unstructured":"N. Lynch, I. Saias, and R. Segala. Proving time bounds for randomized distributed algorithms. In Proc. 13th ACM Symposium on Principles of Distributed Computing, 1984."},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"K. Mehlhorn and A.K. Tsakalidis:. Data structures. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume A: Algorithms and Complexity, pages 301\u2013342. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88071-0.50011-4"},{"key":"5_CR28","unstructured":"PRISM Web Page, http:\/\/www.cs.bham.ac.uk\/~dxp\/prism\/ ."},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"M.L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley series in probability and mathematical statistics. John Wiley & Sons, 1994.","DOI":"10.1002\/9780470316887"},{"key":"5_CR30","unstructured":"R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Department of Mathematics, Massachusetts Institute of Technology, 1995."},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"D. Simons, and M. Stoelinga. Mechanical verification of the IEEE1394a root contention protocol using Uppaal2k. To appear in International Journal on Software Tools for Technlogy Transfer, 2001.","DOI":"10.1007\/s100090100059"},{"key":"5_CR32","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 5th AMAST Workshop on Real-Time and Probabilistic Systems (ARTS\u201999)","author":"M. Stoelinga","year":"1999","unstructured":"M. Stoelinga and F. Vaandrager. Root contention in IEEE 1394. In Proc. 5th AMAST Workshop on Real-Time and Probabilistic Systems (ARTS\u201999), volume 1601 of LNCS, 1999."}],"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_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T01:26:30Z","timestamp":1587518790000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45605-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439134","9783540456056"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-45605-8_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}