{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,4]],"date-time":"2025-09-04T14:28:39Z","timestamp":1756996119876},"publisher-location":"Cham","reference-count":49,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319024431"},{"type":"electronic","value":"9783319024448"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"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":[[2013]]},"DOI":"10.1007\/978-3-319-02444-8_2","type":"book-chapter","created":{"date-parts":[[2013,8,29]],"date-time":"2013-08-29T05:11:21Z","timestamp":1377753081000},"page":"5-22","source":"Crossref","is-referenced-by-count":37,"title":["Automated Verification and Strategy Synthesis for Probabilistic Systems"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"Abdeddaim, Y., Kerbaa, A., Maler, O.: Task graph scheduling using timed automata. In: Proc. IPDPS 2003 (2003)"},{"key":"2_CR2","unstructured":"de Alfaro, L.: Formal Verification of Probabilistic Systems. Ph.D. thesis, Stanford University (1997)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-78499-9_21","volume-title":"Foundations of Software Science and Computational Structures","author":"C. Baier","year":"2008","unstructured":"Baier, C., Bertrand, N., Gr\u00f6\u00dfer, M.: On decision problems for probabilistic b\u00fcchi automata. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962, pp. 287\u2013301. Springer, Heidelberg (2008)"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: Proc. TCS 2006, pp. 493\u20135062. Kluwer (2004)","DOI":"10.1007\/1-4020-8141-3_38"},{"key":"2_CR5","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"2_CR6","unstructured":"Bellman, R.: Dynamic Programming. Princeton University Press (1957)"},{"issue":"3","key":"2_CR7","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. CADICS\u00a08(3), 299\u2013316 (2000)","journal-title":"IEEE Trans. CADICS"},{"key":"2_CR8","unstructured":"Bertsekas, D.: Dynamic Programming and Optimal Control, vol. 1&2. Athena Scientific (1995)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-04468-7_15","volume-title":"Computer Safety, Reliability, and Security","author":"M. Bozzano","year":"2009","unstructured":"Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V.Y., Noll, T., Roveri, M.: The COMPASS approach: Correctness, modelling and performability of aerospace systems. In: Buth, B., Rabe, G., Seyfarth, T. (eds.) SAFECOMP 2009. LNCS, vol.\u00a05775, pp. 173\u2013186. Springer, Heidelberg (2009)"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Forejt, V., Ku\u010dera, A.: Stochastic games with branching-time winning objectives. In: Proc. LICS 2006, pp. 349\u2013358. IEEE CS Press (2006)","DOI":"10.1007\/11817949_24"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-22110-1_20","volume-title":"Computer Aided Verification","author":"P. \u010cern\u00fd","year":"2011","unstructured":"\u010cern\u00fd, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative synthesis for concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 243\u2013259. Springer, Heidelberg (2011)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/11672142_42","volume-title":"STACS 2006","author":"K. Chatterjee","year":"2006","unstructured":"Chatterjee, K., Henzinger, T.A.: Strategy improvement and randomized subexponential algorithms for stochastic parity games. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol.\u00a03884, pp. 512\u2013523. Springer, Heidelberg (2006)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/11817949_25","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"K. Chatterjee","year":"2006","unstructured":"Chatterjee, K., Henzinger, T.A.: Strategy improvement for stochastic rabin and streett games. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol.\u00a04137, pp. 375\u2013389. Springer, Heidelberg (2006)"},{"issue":"1","key":"2_CR14","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10703-013-0183-7","volume":"43","author":"T. Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Methods in System Design\u00a043(1), 61\u201392 (2013)","journal-title":"Formal Methods in System Design"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-642-36742-7_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: PRISM-games: A model checker for stochastic multi-player games. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 185\u2013191. Springer, Heidelberg (2013)"},{"issue":"2","key":"2_CR16","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0890-5401(92)90048-K","volume":"96","author":"A. Condon","year":"1992","unstructured":"Condon, A.: The complexity of stochastic games. Information and Computation\u00a096(2), 203\u2013224 (1992)","journal-title":"Information and Computation"},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1090\/dimacs\/013\/04","volume":"13","author":"A. Condon","year":"1993","unstructured":"Condon, A.: On algorithms for simple stochastic games. DIMACS Series in Discrete Mathematics and Theoretical Computer Science\u00a013, 51\u201373 (1993)","journal-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science"},{"key":"2_CR18","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.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 249\u2013260. Springer, Heidelberg (1999)"},{"issue":"6","key":"2_CR19","doi-asserted-by":"publisher","first-page":"621","DOI":"10.1007\/s10009-006-0014-x","volume":"8","author":"M. Duflot","year":"2006","unstructured":"Duflot, M., Kwiatkowska, M., Norman, G., Parker, D.: A formal analysis of Bluetooth device discovery. STTT\u00a08(6), 621\u2013632 (2006)","journal-title":"STTT"},{"issue":"4","key":"2_CR20","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. LMCS\u00a04(4), 1\u201321 (2008)","journal-title":"LMCS"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"V. Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol.\u00a06659, pp. 53\u2013113. Springer, Heidelberg (2011)"},{"key":"2_CR22","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.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 112\u2013127. Springer, Heidelberg (2011)"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-33386-6_25","volume-title":"Automated Technology for Verification and Analysis","author":"V. Forejt","year":"2012","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 317\u2013332. Springer, Heidelberg (2012)"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-642-33386-6_26","volume-title":"Automated Technology for Verification and Analysis","author":"S. Giro","year":"2012","unstructured":"Giro, S., Rabe, M.N.: Verification of partial-information probabilistic systems using counterexample-guided refinements. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 333\u2013348. Springer, Heidelberg (2012)"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"Interactive Markov Chains and the Quest for Quantified Quality","year":"2002","unstructured":"Hermanns, H. (ed.): Interactive Markov Chains and the Quest for Quantified Quality. LNCS, vol.\u00a02428. Springer, Heidelberg (2002)"},{"key":"2_CR26","unstructured":"Howard, R.: Dynamic Programming and Markov Processes. The MIT Press (1960)"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Katoen, J.P., Hahn, E., Hermanns, H., Jansen, D., Zapreev, I.: The ins and outs of the probabilistic model checker MRMC. In: Proc. QEST 2009. IEEE CS Press (2009)","DOI":"10.1109\/QEST.2009.11"},{"key":"2_CR28","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-1-4684-9455-6_4","volume-title":"Denumerable Markov Chains","author":"John G. Kemeny","year":"1976","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains, 2nd edn. Springer (1976)"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"2_CR30","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-319-02444-8_2","volume-title":"Automated Technology for Verification and Analysis","author":"Marta Kwiatkowska","year":"2013","unstructured":"Kwiatkowska, M., Parker, D.: Automated verification and strategy synthesis for probabilistic systems (extended version) (2013), available from [49]"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Lahijanian, M., Wasniewski, J., Andersson, S., Belta, C.: Motion planning and control from temporal logic specifications with probabilistic satisfaction guarantees. In: Proc. ICRA 2010, pp. 3227\u20133232 (2010)","DOI":"10.1109\/ROBOT.2010.5509686"},{"issue":"72","key":"2_CR32","doi-asserted-by":"publisher","first-page":"1470","DOI":"10.1098\/rsif.2011.0800","volume":"9","author":"M. Lakin","year":"2012","unstructured":"Lakin, M., Parker, D., Cardelli, L., Kwiatkowska, M., Phillips, A.: Design and analysis of DNA strand displacement devices using probabilistic model checking. Journal of the Royal Society Interface\u00a09(72), 1470\u20131485 (2012)","journal-title":"Journal of the Royal Society Interface"},{"issue":"1-2","key":"2_CR33","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. Larsen","year":"1997","unstructured":"Larsen, K., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1997)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Masuam, Kolobov, A.: Planning with Markov Decision Processes: An AI Perspective. Morgan & Claypool (2012)","DOI":"10.2200\/S00426ED1V01Y201206AIM017"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Formal Methods in System Design (2012) (to appear)","DOI":"10.1007\/s10703-012-0177-x"},{"key":"2_CR36","unstructured":"Poupart, P.: Exploiting Structure to Efficiently Solve Large Scale Partially Observable Markov Decision Processes. Ph.D. thesis, University of Toronto (2005)"},{"key":"2_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-642-39799-8_35","volume-title":"Computer Aided Verification","author":"A. Puggelli","year":"2013","unstructured":"Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 527\u2013542. Springer, Heidelberg (2013)"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons (1994)","DOI":"10.1002\/9780470316887"},{"key":"2_CR39","doi-asserted-by":"publisher","first-page":"728","DOI":"10.1287\/opre.21.3.728","volume":"21","author":"J. Satia","year":"1970","unstructured":"Satia, J., Lave Jr., R.: Markovian decision processes with uncertain transition probabilities. Oper. Res.\u00a021, 728\u2013740 (1970)","journal-title":"Oper. Res."},{"key":"2_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/11691372_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Sen","year":"2006","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Model-checking Markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 394\u2013410. Springer, Heidelberg (2006)"},{"issue":"1-2","key":"2_CR41","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/j.tcs.2006.08.042","volume":"367","author":"G. Steel","year":"2006","unstructured":"Steel, G.: Formal analysis of PIN block attacks. Theoretical Computer Science\u00a0367(1-2), 257\u2013270 (2006)","journal-title":"Theoretical Computer Science"},{"key":"2_CR42","doi-asserted-by":"crossref","unstructured":"Sutton, R., Barto, A.: Reinforcement Learning: An Introduction. MIT Press (1998)","DOI":"10.1109\/TNN.1998.712192"},{"key":"2_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-32940-1_26","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"M. Timmer","year":"2012","unstructured":"Timmer, M., Katoen, J.-P., van de Pol, J., Stoelinga, M.I.A.: Efficient modelling and generation of markov automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol.\u00a07454, pp. 364\u2013379. Springer, Heidelberg (2012)"},{"key":"2_CR44","doi-asserted-by":"crossref","unstructured":"Tkachev, I., Abate, A.: Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems. In: Proc. HSCC 2013, pp. 283\u2013292 (2013)","DOI":"10.1145\/2461328.2461372"},{"issue":"1","key":"2_CR45","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":"2_CR46","doi-asserted-by":"crossref","unstructured":"Wolff, E., Topcu, U., Murray, R.: Robust control of uncertain Markov decision processes with temporal logic specifications. In: Proc. CDC 2012, pp. 3372\u20133379 (2012)","DOI":"10.1109\/CDC.2012.6426174"},{"issue":"11","key":"2_CR47","doi-asserted-by":"publisher","first-page":"2817","DOI":"10.1109\/TAC.2012.2195811","volume":"57","author":"T. Wongpiromsarn","year":"2012","unstructured":"Wongpiromsarn, T., Topcu, U., Murray, R.: Receding horizon temporal logic planning. IEEE Trans. Automat. Contr.\u00a057(11), 2817\u20132830 (2012)","journal-title":"IEEE Trans. Automat. Contr."},{"issue":"6","key":"2_CR48","doi-asserted-by":"publisher","first-page":"572","DOI":"10.3166\/EJC.18.572-587","volume":"18","author":"L. Zhang","year":"2012","unstructured":"Zhang, L., She, Z., Ratschan, S., Hermanns, H., Hahn, E.M.: Safety verification for probabilistic hybrid systems. Eur. J. Control\u00a018(6), 572\u2013587 (2012)","journal-title":"Eur. J. Control"},{"key":"2_CR49","unstructured":"http:\/\/www.prismmodelchecker.org\/files\/stratsynth\/"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-02444-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,5]],"date-time":"2022-03-05T02:27:05Z","timestamp":1646447225000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-02444-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319024431","9783319024448"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-02444-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}