{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:20:33Z","timestamp":1779074433184,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":93,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642214547","type":"print"},{"value":"9783642214554","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21455-4_3","type":"book-chapter","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T14:00:01Z","timestamp":1307714401000},"page":"53-113","source":"Crossref","is-referenced-by-count":197,"title":["Automated Verification Techniques for Probabilistic Systems"],"prefix":"10.1007","author":[{"given":"Vojt\u011bch","family":"Forejt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"de Alfaro, L.: Formal Verification of Probabilistic Systems. Ph.D. thesis, Stanford University (1997)"},{"key":"3_CR2","series-title":"ENTCS","volume-title":"Proc. 1st Int. Workshop Probabilistic Methods in Verification (PROBMIV 1998)","author":"L. Alfaro de","year":"1998","unstructured":"de Alfaro, L.: From fairness to chance. In: Baier, C., Huth, M., Kwiatkowska, M., Ryan, M. (eds.) Proc. 1st Int. Workshop Probabilistic Methods in Verification (PROBMIV 1998). ENTCS, vol.\u00a022. Elsevier, Amsterdam (1998)"},{"key":"3_CR3","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1109\/QEST.2009.10","volume-title":"Proc. 6th Int. Conf. Quantitative Evaluation of Systems (QEST 2009)","author":"H. Aljazzar","year":"2009","unstructured":"Aljazzar, H., Leue, S.: Generation of counterexamples for model checking of Markov decision processes. In: Proc. 6th Int. Conf. Quantitative Evaluation of Systems (QEST 2009), pp. 197\u2013206. IEEE CS Press, Los Alamitos (2009)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-01702-5_15","volume-title":"Hardware and Software: Verification and Testing","author":"M. Andr\u00e9s","year":"2009","unstructured":"Andr\u00e9s, M., D\u2019Argenio, P., van Rossum, P.: Significant diagnostic counterexamples in probabilistic model checking. In: Chockler, H., Hu, A. (eds.) HVC 2008. LNCS, vol.\u00a05394, pp. 129\u2013148. Springer, Heidelberg (2009)"},{"issue":"1","key":"3_CR5","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/0196-6774(90)90021-6","volume":"15","author":"J. Aspnes","year":"1990","unstructured":"Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. Journal of Algorithms\u00a015(1), 441\u2013460 (1990)","journal-title":"Journal of Algorithms"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-60045-0_48","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1995","unstructured":"Aziz, A., Singhal, V., Balarin, F., Brayton, R., Sangiovanni-Vincentelli, A.: It usually works: The temporal logic of stochastic systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 155\u2013165. Springer, Heidelberg (1995)"},{"key":"3_CR7","unstructured":"Baier, C.: On algorithmic verification methods for probabilistic systems, habilitation thesis, Fakult\u00e4t f\u00fcr Mathematik & Informatik, Universit\u00e4t Mannheim (1998)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-04761-9_12","volume-title":"Automated Technology for Verification and Analysis","author":"C. Baier","year":"2009","unstructured":"Baier, C., Groesser, M., Ciesinski, F.: Quantitative analysis under fairness constraints. In: Liu, Z., Ravn, A. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 135\u2013150. Springer, Heidelberg (2009)"},{"key":"3_CR9","first-page":"493","volume-title":"Proc. 3rd IFIP Int. Conf. Theoretical Computer Science (TCS 2006)","author":"C. Baier","year":"2004","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: L\u00e9vy, J.J., Mayr, E., Mitchell, J. (eds.) Proc. 3rd IFIP Int. Conf. Theoretical Computer Science (TCS 2006), pp. 493\u2013506. Kluwer, Dordrecht (2004)"},{"issue":"1","key":"3_CR10","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2005.07.022","volume":"345","author":"C. Baier","year":"2005","unstructured":"Baier, C., Hermanns, H., Katoen, J.P., Haverkort, B.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theoretical Computer Science\u00a0345(1), 2\u201326 (2005)","journal-title":"Theoretical Computer Science"},{"key":"3_CR11","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"3","key":"3_CR12","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C. Baier","year":"1998","unstructured":"Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distributed Computing\u00a011(3), 125\u2013155 (1998)","journal-title":"Distributed Computing"},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1109\/QEST.2008.29","volume-title":"Proc. 5rd Int. Conf. Quantitative Evaluation of Systems (QEST 2008)","author":"J. Barnat","year":"2008","unstructured":"Barnat, J., Brim, L., Cerna, I., Ceska, M., Tumova, J.: ProbDiVinE-MC: Multi-core LTL model checker for probabilistic systems. In: Proc. 5rd Int. Conf. Quantitative Evaluation of Systems (QEST 2008), pp. 77\u201378. IEEE CS Press, Los Alamitos (2008)"},{"key":"3_CR14","volume-title":"Dynamic Programming","author":"R. Bellman","year":"1957","unstructured":"Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)"},{"issue":"3","key":"3_CR15","first-page":"299","volume":"8","author":"L. Benini","year":"2000","unstructured":"Benini, L., Bogliolo, A., Paleologo, G., De Micheli, G.: Policy optimization for dynamic power management. IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems\u00a08(3), 299\u2013316 (2000)","journal-title":"IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems"},{"key":"3_CR16","volume-title":"Dynamic Programming and Optimal Control","author":"D. Bertsekas","year":"1995","unstructured":"Bertsekas, D.: Dynamic Programming and Optimal Control, vol.\u00a01,2. Athena Scientific, Belmont (1995)"},{"issue":"3","key":"3_CR17","doi-asserted-by":"publisher","first-page":"580","DOI":"10.1287\/moor.16.3.580","volume":"16","author":"D. Bertsekas","year":"1991","unstructured":"Bertsekas, D., Tsitsiklis, J.: An analysis of stochastic shortest path problems. Mathematics of Operations Research\u00a016(3), 580\u2013595 (1991)","journal-title":"Mathematics of Operations Research"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A. Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"3_CR19","volume-title":"Probability and Measure","author":"P. Billingsley","year":"1995","unstructured":"Billingsley, P.: Probability and Measure. Wiley, Chichester (1995)"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-70583-3_13","volume-title":"Automata, Languages and Programming","author":"T. Br\u00e1zdil","year":"2008","unstructured":"Br\u00e1zdil, T., Forejt, V., Ku\u010dera, A.: Controller synthesis and verification for Markov decision processes with qualitative branching time objectives. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L., Halld\u00f3rsson, M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol.\u00a05126, pp. 148\u2013159. Springer, Heidelberg (2008)"},{"key":"3_CR21","first-page":"349","volume-title":"21th IEEE Symp. Logic in Computer Science (LICS 2006)","author":"T. Br\u00e1zdil","year":"2006","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Forejt, V., Ku\u010dera, A.: Stochastic games with branching-time winning objectives. In: 21th IEEE Symp. Logic in Computer Science (LICS 2006), pp. 349\u2013358. IEEE CS Press, Los Alamitos (2006)"},{"key":"3_CR22","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Ku\u010dera, A., Obdr\u017e\u00e1lek, J.: Qualitative reachability in stochastic BPA games. In: Albers, S., Marion, J.Y. (eds.) 26th Int. Symp. Theoretical Aspects of Computer Science (STACS 2009). LIPIcs, vol.\u00a03, pp. 207\u2013218. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2009)"},{"key":"3_CR23","unstructured":"Br\u00e1zdil, T., Forejt, V., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J., Ku\u010dera, A.: Continuous-time stochastic games with time-bounded reachability. In: Kannan, R., Kumar, K. (eds.) Proc. 29th Int. Conf. Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2009). LIPIcs, vol.\u00a04, pp. 61\u201372. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2009)"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Calinescu, R., Grunske, L., Kwiatkowska, M., Mirandola, R., Tamburrelli, G.: Dynamic QoS management and optimisation in service-based systems. IEEE Transactions on Software Engineering (2010)","DOI":"10.1109\/TSE.2010.92"},{"key":"3_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/3-540-45694-5_25","volume-title":"CONCUR 2002 - Concurrency Theory","author":"S. Cattani","year":"2002","unstructured":"Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Janar, P., Ketinsky, M., Kuera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 371\u2013385. Springer, Heidelberg (2002)"},{"issue":"1","key":"3_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1838552.1838553","volume":"12","author":"R. Chadha","year":"2010","unstructured":"Chadha, R., Viswanathan, M.: A counterexample guided abstraction-refinement framework for Markov decision processes. ACM Transactions on Computational Logic\u00a012(1), 1\u201349 (2010)","journal-title":"ACM Transactions on Computational Logic"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-69850-0_7","volume-title":"25 Years of Model Checking","author":"K. Chatterjee","year":"2008","unstructured":"Chatterjee, K., Henzinger, T.: Value iteration. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp. 107\u2013138. Springer, Heidelberg (2008)"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-642-14295-6_34","volume-title":"Computer Aided Verification","author":"K. Chatterjee","year":"2010","unstructured":"Chatterjee, K., Henzinger, T., Jobstmann, B., Singh, R.: Measuring and synthesizing systems in probabilistic environments. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 380\u2013395. Springer, Heidelberg (2010)"},{"key":"3_CR29","unstructured":"Cheung, L.: Reconciling Nondeterministic and Probabilistic Choices. Ph.D. thesis, Radboud University of Nijmegen (2006)"},{"key":"3_CR30","first-page":"131","volume-title":"Proc. 3rd Int. Conf. Quantitative Evaluation of Systems (QEST 2006)","author":"F. Ciesinski","year":"2006","unstructured":"Ciesinski, F., Baier, C.: Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: Proc. 3rd Int. Conf. Quantitative Evaluation of Systems (QEST 2006), pp. 131\u2013132. IEEE CS Press, Los Alamitos (2006)"},{"key":"3_CR31","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1109\/QEST.2008.45","volume-title":"Proc. 5th Int. Conf. Quantitative Evaluation of Systems (QEST 2008)","author":"F. Ciesinski","year":"2008","unstructured":"Ciesinski, F., Baier, C., Gr\u00f6\u00dfer, M., Parker, D.: Reduction techniques for model checking Markov decision processes. In: Proc. 5th Int. Conf. Quantitative Evaluation of Systems (QEST 2008), pp. 45\u201354. IEEE CS Press, Los Alamitos (2008)"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-24611-4_5","volume-title":"Validation of Stochastic Systems","author":"F. Ciesinski","year":"2004","unstructured":"Ciesinski, F., Gr\u00f6\u00dfer, M.: On probabilistic computation tree logic. In: Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol.\u00a02925, pp. 147\u2013188. Springer, Heidelberg (2004)"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E. Clarke","year":"1982","unstructured":"Clarke, E., Emerson, A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"3_CR34","first-page":"338","volume-title":"Proc. 29th Annual Symp. Foundations of Computer Science (FOCS 1988)","author":"C. Courcoubetis","year":"1988","unstructured":"Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite state probabilistic programs. In: Proc. 29th Annual Symp. Foundations of Computer Science (FOCS 1988), pp. 338\u2013345. IEEE CS Press, Los Alamitos (1988)"},{"issue":"10","key":"3_CR35","doi-asserted-by":"publisher","first-page":"1399","DOI":"10.1109\/9.720497","volume":"43","author":"C. Courcoubetis","year":"1998","unstructured":"Courcoubetis, C., Yannakakis, M.: Markov decision processes and regular events. IEEE Trans. Automatic Control\u00a043(10), 1399\u20131418 (1998)","journal-title":"IEEE Trans. Automatic Control"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Computer Aided Verification","author":"M. Daniele","year":"1999","unstructured":"Daniele, M., Giunchiglia, F., Vardi, M.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 249\u2013260. Springer, Heidelberg (1999)"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45605-8_5","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"P. D\u2019Argenio","year":"2002","unstructured":"D\u2019Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reduction and refinement strategies for probabilistic analysis. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, pp. 57\u201376. Springer, Heidelberg (2002)"},{"key":"3_CR38","first-page":"223","volume-title":"Proc. 10th Int. Conf. Application of Concurrency to System Design (ACSD 2010)","author":"B. Delahaye","year":"2010","unstructured":"Delahaye, B., Caillaud, B., Legay, A.: Probabilistic contracts: A compositional reasoning methodology for the design of stochastic systems. In: Proc. 10th Int. Conf. Application of Concurrency to System Design (ACSD 2010), pp. 223\u2013232. IEEE CS Press, Los Alamitos (2010)"},{"key":"3_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/11901914_4","volume-title":"Automated Technology for Verification and Analysis","author":"A. Donaldson","year":"2006","unstructured":"Donaldson, A., Miller, A.: Symmetry reduction for probabilistic model checking using generic representatives. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 9\u201323. Springer, Heidelberg (2006)"},{"issue":"4","key":"3_CR40","first-page":"1","volume":"4","author":"K. Etessami","year":"2008","unstructured":"Etessami, K., Kwiatkowska, M., Vardi, M., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Logical Methods in Computer Science\u00a04(4), 1\u201321 (2008)","journal-title":"Logical Methods in Computer Science"},{"key":"3_CR41","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., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 891\u2013903. Springer, Heidelberg (2005)"},{"key":"3_CR42","volume-title":"An Introduction to Probability Theory and its Applications","author":"W. Feller","year":"1968","unstructured":"Feller, W.: An Introduction to Probability Theory and its Applications. Wiley, Chichester (1968)"},{"key":"3_CR43","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1109\/QEST.2010.24","volume-title":"Proc. 7th Int. Conf. Quantitative Evaluation of Systems (QEST 2010)","author":"L. Feng","year":"2010","unstructured":"Feng, L., Kwiatkowska, M., Parker, D.: Compositional verification of probabilistic systems using learning. In: Proc. 7th Int. Conf. Quantitative Evaluation of Systems (QEST 2010), pp. 133\u2013142. IEEE CS Press, Los Alamitos (2010)"},{"key":"3_CR44","volume-title":"Proc. 33rd ACM\/IEEE International Conference on Software Engineering (ICSE 2011)","author":"A. Filieri","year":"2011","unstructured":"Filieri, A., Ghezzi, C., Tamburrelli, G.: Run-time efficient probabilistic model checking. In: Proc. 33rd ACM\/IEEE International Conference on Software Engineering (ICSE 2011). ACM, New York (2011)"},{"key":"3_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-19835-9_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V. Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P., Leino, K. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 112\u2013127. Springer, Heidelberg (2011)"},{"issue":"7","key":"3_CR46","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1016\/j.jlap.2010.07.003","volume":"79","author":"M. Fr\u00e4nzle","year":"2010","unstructured":"Fr\u00e4nzle, M., Teige, T., Eggers, A.: Engineering constraint solvers for automatic analysis of probabilistic hybrid automata. Journal of Logic and Algebraic Programming\u00a079(7), 436\u2013466 (2010)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"3_CR47","unstructured":"Giro, S.: On the automatic verification of distributed probabilistic automata with partial information. Ph.D. thesis, FaMAF, Universidad Nacional de C\u00f3rdoba (2010)"},{"issue":"1","key":"3_CR48","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1006\/inco.1995.1123","volume":"121","author":"R. Glabbeek van","year":"1995","unstructured":"van Glabbeek, R., Smolka, S., Steffen, B.: Reactive, generative, and stratified models of probabilistic processes. Information and Computation\u00a0121(1), 59\u201380 (1995)","journal-title":"Information and Computation"},{"key":"3_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11804192_19","volume-title":"Formal Methods for Components and Objects","author":"M. Gr\u00f6\u00dfer","year":"2006","unstructured":"Gr\u00f6\u00dfer, M., Baier, C.: Partial order reduction for Markov decision processes: A survey. In: de Boer, F., Bonsangue, M., Graf, S., de Roever, W.P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 408\u2013427. Springer, Heidelberg (2006)"},{"key":"3_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-12002-2_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Hahn","year":"2010","unstructured":"Hahn, E., Hermanns, H., Wachter, B., Zhang, L.: PASS: Abstraction refinement for infinite probabilistic models. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 353\u2013357. Springer, Heidelberg (2010)"},{"key":"3_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-02652-2_10","volume-title":"Model Checking Software","author":"E. Hahn","year":"2009","unstructured":"Hahn, E., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. In: Pasareanu, C. (ed.) Model Checking Software. LNCS, vol.\u00a05578, pp. 88\u2013106. Springer, Heidelberg (2009)"},{"key":"3_CR52","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1109\/RTSS.2008.19","volume-title":"Proc. IEEE Symp. Real-Time Systems (RTSS 2008)","author":"T. Han","year":"2008","unstructured":"Han, T., Katoen, J.P., Mereacre, A.: Approximate parameter synthesis for probabilistic time-bounded reachability. In: Proc. IEEE Symp. Real-Time Systems (RTSS 2008), pp. 173\u2013182. IEEE CS Press, Los Alamitos (2008)"},{"key":"3_CR53","volume-title":"Time and Probability in Formal Design of Distributed Systems","author":"H. Hansson","year":"1994","unstructured":"Hansson, H.: Time and Probability in Formal Design of Distributed Systems. Elsevier, Amsterdam (1994)"},{"issue":"5","key":"3_CR54","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"3_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-70545-1_16","volume-title":"Computer Aided Verification","author":"H. Hermanns","year":"2008","unstructured":"Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 162\u2013175. Springer, Heidelberg (2008)"},{"key":"3_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"3_CR57","volume-title":"Dynamic Programming and Markov Processes","author":"R. Howard","year":"1960","unstructured":"Howard, R.: Dynamic Programming and Markov Processes. MIT Press, Cambridge (1960)"},{"key":"3_CR58","unstructured":"Technical specifications of hard drive IBM Travelstar VP, http:\/\/www.storage.ibm.com\/storage\/oem\/data\/travvp.htm"},{"key":"3_CR59","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1145\/93385.93409","volume-title":"Proc. 9th Annual ACM Symp. Principles of Distributed Computing (PODC 1990)","author":"A. Israeli","year":"1990","unstructured":"Israeli, A., Jalfon, M.: Token management schemes and random walks yield self-stabilizating mutual exclusion. In: Proc. 9th Annual ACM Symp. Principles of Distributed Computing (PODC 1990), pp. 119\u2013131. ACM, New York (1990)"},{"key":"#cr-split#-3_CR60.1","unstructured":"Jeannet, B., D???Argenio, P., Larsen, K.: Rapture: A tool for verifying Markov decision processes. In: Cerna, I. (ed.) Proc. Tools Day, affiliated to 13th Int. Conf. Concurrency Theory (CONCUR 2002), pp. 84???98 (2002);"},{"key":"#cr-split#-3_CR60.2","unstructured":"Technical Report FIMU-RS-2002-05, Faculty of Informatics, Masaryk University (2002)"},{"key":"3_CR61","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1109\/QEST.2009.11","volume-title":"Proc. 6th Int. Conf. Quantitative Evaluation of Systems (QEST 2009)","author":"J.P. Katoen","year":"2009","unstructured":"Katoen, J.P., Hahn, E., Hermanns, H., Jansen, D., Zapreev, I.: The ins and outs of the probabilistic model checker MRMC. In: Proc. 6th Int. Conf. Quantitative Evaluation of Systems (QEST 2009), pp. 167\u2013176. IEEE CS Press, Los Alamitos (2009)"},{"key":"3_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-93900-9_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M. Kattenbelt","year":"2009","unstructured":"Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Abstraction refinement for probabilistic software. In: Jones, N., Muller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 182\u2013197. Springer, Heidelberg (2009)"},{"key":"3_CR63","doi-asserted-by":"crossref","unstructured":"Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Formal Methods in System Design\u00a036(3) (2010)","DOI":"10.1007\/s10703-010-0097-6"},{"key":"3_CR64","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov Chains","author":"J. Kemeny","year":"1976","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains, 2nd edn. Springer, Heidelberg (1976)","edition":"2"},{"key":"3_CR65","volume-title":"Modeling and Analysis of Stochastic Systems","author":"V. Kulkarni","year":"1995","unstructured":"Kulkarni, V.: Modeling and Analysis of Stochastic Systems. Chapman and Hall, Boca Raton (1995)"},{"key":"3_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/11817963_23","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 234\u2013248. Springer, Heidelberg (2006)"},{"key":"3_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal Methods for Performance Evaluation","author":"M. Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol.\u00a04486, pp. 220\u2013270. Springer, Heidelberg (2007)"},{"key":"3_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-642-04368-0_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M. Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. In: Ouaknine, J., Vaandrager, F. (eds.) FORMATS 2009. LNCS, vol.\u00a05813, pp. 212\u2013227. Springer, Heidelberg (2009)"},{"key":"3_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-12002-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Kwiatkowska","year":"2010","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 23\u201337. Springer, Heidelberg (2010)"},{"key":"3_CR70","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1002\/9780470611012.ch8","volume-title":"Modeling and Verification of Real-Time Systems: Formalisms and Software Tools","author":"M. Kwiatkowska","year":"2008","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Verification of Real-Time Probabilistic Systems. In: Modeling and Verification of Real-Time Systems: Formalisms and Software Tools, pp. 249\u2013288. John Wiley & Sons, Chichester (2008)"},{"key":"3_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-44585-4_17","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2001","unstructured":"Kwiatkowska, M., Norman, G., Segala, R.: Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 194\u2013206. Springer, Heidelberg (2001)"},{"key":"3_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-78800-3_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Legay","year":"2008","unstructured":"Legay, A., Murawski, A., Ouaknine, J., Worrell, J.: On automated verification of probabilistic programs. In: Ramakrishnan, C., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 173\u2013187. Springer, Heidelberg (2008)"},{"key":"3_CR73","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1109\/QEST.2010.47","volume-title":"Proc. 7th Int. Conf. Quantitative Evaluation of Systems (QEST 2010)","author":"M. Neuh\u00e4u\u00dfer","year":"2010","unstructured":"Neuh\u00e4u\u00dfer, M., Zhang, L.: Time-bounded reachability probabilities in continuous-time Markov decision processes. In: Proc. 7th Int. Conf. Quantitative Evaluation of Systems (QEST 2010), pp. 209\u2013218. IEEE CS Press, Los Alamitos (2010)"},{"issue":"2","key":"3_CR74","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/s00165-005-0062-0","volume":"17","author":"G. Norman","year":"2005","unstructured":"Norman, G., Parker, D., Kwiatkowska, M., Shukla, S., Gupta, R.: Using probabilistic model checking for dynamic power management. Formal Aspects of Computing\u00a017(2), 160\u2013176 (2005)","journal-title":"Formal Aspects of Computing"},{"key":"3_CR75","first-page":"46","volume-title":"Proc. 18th Annual Symp. Foundations of Computer Science (FOCS 1977)","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th Annual Symp. Foundations of Computer Science (FOCS 1977), pp. 46\u201357. IEEE CS Press, Los Alamitos (1977)"},{"key":"3_CR76","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"M. Puterman","year":"1994","unstructured":"Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons, Chichester (1994)"},{"key":"3_CR77","doi-asserted-by":"crossref","unstructured":"Rabe, M., Schewe, S.: Optimal time-abstract schedulers for CTMDPs and Markov games. In: Di Pierro, A., Norman, G. (eds.) Proc. 8th Workshop Quantitative Aspects of Programming Languages (QAPL 2010). EPTCS, vol.\u00a028, pp. 144\u2013158. Open Publishing Association (2010)","DOI":"10.4204\/EPTCS.28.10"},{"key":"3_CR78","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/S0019-9958(63)90290-0","volume":"6","author":"M. Rabin","year":"1963","unstructured":"Rabin, M.: Probabilistic automata. Information and Control\u00a06, 230\u2013245 (1963)","journal-title":"Information and Control"},{"key":"3_CR79","volume-title":"The theory and practice of concurrency","author":"A. Roscoe","year":"1997","unstructured":"Roscoe, A.: The theory and practice of concurrency. Prentice-Hall, Englewood Cliffs (1997)"},{"key":"3_CR80","unstructured":"Segala, R.: Modelling and Verification of Randomized Distributed Real Time Systems. Ph.D. thesis, Massachusetts Institute of Technology (1995)"},{"issue":"2","key":"3_CR81","first-page":"250","volume":"2","author":"R. Segala","year":"1995","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nordic Journal of Computing\u00a02(2), 250\u2013273 (1995)","journal-title":"Nordic Journal of Computing"},{"key":"3_CR82","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24611-4_1","volume-title":"Validation of Stochastic Systems","author":"A. Sokolova","year":"2004","unstructured":"Sokolova, A., de Vink, E.: Probabilistic automata: System types, parallel composition and comparison. In: Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol.\u00a02925, pp. 1\u201343. Springer, Heidelberg (2004)"},{"key":"3_CR83","doi-asserted-by":"crossref","unstructured":"Stewart, W.: Introduction to the Numerical Solution of Markov Chains, Princeton (1994)","DOI":"10.1515\/9780691223384"},{"key":"3_CR84","first-page":"327","volume-title":"Proc. 26th Annual Symp. Foundations of Computer Science (FOCS 1985)","author":"M. Vardi","year":"1985","unstructured":"Vardi, M.: Automatic verification of probabilistic concurrent finite state programs. In: Proc. 26th Annual Symp. Foundations of Computer Science (FOCS 1985), pp. 327\u2013338. IEEE CS Press, Los Alamitos (1985)"},{"issue":"1","key":"3_CR85","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Vardi","year":"1994","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115(1), 1\u201337 (1994)","journal-title":"Information and Computation"},{"key":"3_CR86","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-540-75596-8_16","volume-title":"Automated Technology for Verification and Analysis","author":"L. Zhang","year":"2007","unstructured":"Zhang, L., Hermanns, H.: Deciding simulations on probabilistic automata. In: Namjoshi, K., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 207\u2013222. Springer, Heidelberg (2007)"},{"key":"3_CR87","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-12002-2_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Zhang","year":"2010","unstructured":"Zhang, L., Neuh\u00e4u\u00dfer, M.: Model checking interactive Markov chains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 53\u201368. Springer, Heidelberg (2010)"},{"key":"3_CR88","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-642-14295-6_21","volume-title":"Computer Aided Verification","author":"L. Zhang","year":"2010","unstructured":"Zhang, L., She, Z., Ratschan, S., Hermanns, H., Hahn, E.: Safety verification for probabilistic hybrid systems. In: Cook, B., Jackson, P., Touili, T. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 196\u2013211. Springer, Heidelberg (2010)"},{"key":"3_CR89","unstructured":"http:\/\/www.prismmodelchecker.org\/benchmarks\/"},{"key":"3_CR90","unstructured":"http:\/\/www.prismmodelchecker.org\/casestudies\/"},{"key":"3_CR91","unstructured":"http:\/\/www.prismmodelchecker.org\/files\/sfm11\/"},{"key":"3_CR92","unstructured":"http:\/\/www.prismmodelchecker.org\/other-tools.php"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Eternal Networked Software Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21455-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,24]],"date-time":"2021-11-24T23:24:16Z","timestamp":1637796256000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21455-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214547","9783642214554"],"references-count":93,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21455-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}