{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,23]],"date-time":"2026-01-23T11:08:01Z","timestamp":1769166481968,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642198342","type":"print"},{"value":"9783642198359","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-19835-9_11","type":"book-chapter","created":{"date-parts":[[2011,3,14]],"date-time":"2011-03-14T11:03:16Z","timestamp":1300100596000},"page":"112-127","source":"Crossref","is-referenced-by-count":76,"title":["Quantitative Multi-objective Verification for Probabilistic Systems"],"prefix":"10.1007","author":[{"given":"Vojt\u011bch","family":"Forejt","sequence":"first","affiliation":[]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]},{"given":"Hongyang","family":"Qu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","unstructured":"de Alfaro, L.: Formal Verification of Probabilistic Systems. Ph.D. thesis, Stanford University (1997)"},{"key":"11_CR2","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., Gr\u00f6\u00dfer, M., Ciesinski, F.: Quantitative analysis under fairness constraints. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 135\u2013150. Springer, Heidelberg (2009)"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: Proc. IFIP TCS 2004, pp. 493\u2013506 (2004)","DOI":"10.1007\/1-4020-8141-3_38"},{"issue":"3","key":"11_CR4","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"},{"issue":"3","key":"11_CR5","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 Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a08(3), 299\u2013316 (2000)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"11_CR6","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.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"11_CR7","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.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol.\u00a05126, pp. 148\u2013159. Springer, Heidelberg (2008)"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Caillaud, B., Delahaye, B., Larsen, K., Legay, A., Pedersen, M., Wasowski, A.: Compositional design methodology with constraint Markov chains. In: QEST (2010)","DOI":"10.1109\/QEST.2010.23"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-540-77050-3_39","volume-title":"FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science","author":"K. Chatterjee","year":"2007","unstructured":"Chatterjee, K.: Markov decision processes with multiple long-run average objectives. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol.\u00a04855, pp. 473\u2013484. Springer, Heidelberg (2007)"},{"key":"11_CR10","unstructured":"Chatterjee, K., de Alfaro, L., Faella, M., Henzinger, T., Majumdar, R., Stoelinga, M.: Compositional quantitative reasoning. In: Proc. QEST 2006 (2006)"},{"key":"11_CR11","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":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/11672142_26","volume-title":"STACS 2006","author":"K. Chatterjee","year":"2006","unstructured":"Chatterjee, K., Majumdar, R., Henzinger, T.: Markov decision processes with multiple objectives. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol.\u00a03884, pp. 325\u2013336. Springer, Heidelberg (2006)"},{"key":"11_CR13","volume-title":"Multicriteria Analysis","year":"1997","unstructured":"Cl\u00edmaco, J. (ed.): Multicriteria Analysis. Springer, Heidelberg (1997)"},{"issue":"10","key":"11_CR14","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 Transactions on Automatic Control\u00a043(10), 1399\u20131418 (1998)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Delahaye, B., Caillaud, B., Legay, A.: Probabilistic contracts: A compositional reasoning methodology for the design of stochastic systems. In: ACSD 2010 (2010)","DOI":"10.1109\/ACSD.2010.13"},{"issue":"4","key":"11_CR16","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":"11_CR17","first-page":"133","volume-title":"Proc. QEST 2010","author":"L. Feng","year":"2010","unstructured":"Feng, L., Kwiatkowska, M., Parker, D.: Compositional verification of probabilistic systems using learning. In: Proc. QEST 2010, pp. 133\u2013142. IEEE, Los Alamitos (2010)"},{"key":"11_CR18","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. Tech. Rep. RR-10-26, Oxford University Computing Laboratory (2010)"},{"key":"11_CR19","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. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"11_CR20","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":"11_CR21","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":"11_CR22","doi-asserted-by":"crossref","unstructured":"Norman, G., Parker, D., Kwiatkowska, M., Shukla, S., Gupta, R.: Using probabilistic model checking for dynamic power management. FAC\u00a017(2) (2005)","DOI":"10.1007\/s00165-005-0062-0"},{"key":"11_CR23","unstructured":"Segala, R.: Modelling and Verification of Randomized Distributed Real Time Systems. Ph.D. thesis, Massachusetts Institute of Technology (1995)"},{"key":"11_CR24","unstructured":"http:\/\/www.prismmodelchecker.org\/files\/tacas11\/"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19835-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T07:38:16Z","timestamp":1558424296000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19835-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198342","9783642198359"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19835-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}