{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T23:34:05Z","timestamp":1725838445525},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662488980"},{"type":"electronic","value":"9783662488997"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_12","type":"book-chapter","created":{"date-parts":[[2015,11,20]],"date-time":"2015-11-20T22:59:28Z","timestamp":1448060368000},"page":"162-177","source":"Crossref","is-referenced-by-count":2,"title":["Controller Synthesis for MDPs and Frequency LTL $$_{\\setminus \\mathbf{G}\\mathbf U}$$"],"prefix":"10.1007","author":[{"given":"Vojt\u011bch","family":"Forejt","sequence":"first","affiliation":[]},{"given":"Jan","family":"Kr\u010d\u00e1l","sequence":"additional","affiliation":[]},{"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-642-54862-8_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Almagor","year":"2014","unstructured":"Almagor, S., Boker, U., Kupferman, O.: Discounting in LTL. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 424\u2013439. Springer, Heidelberg (2014)"},{"key":"12_CR2","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)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Baier, C., Klein, J., Kl\u00fcppelholz, S., Wunderlich, S.: Weight monitoring with linear temporal logic: complexity and decidability. In: CSL-LICS. ACM (2014)","DOI":"10.1145\/2603088.2603162"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02658-4_14","volume-title":"Computer Aided Verification","author":"R Bloem","year":"2009","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140\u2013156. Springer, Heidelberg (2009)"},{"issue":"3","key":"12_CR5","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values In: LICS. IEEE (2011)","DOI":"10.1109\/LICS.2011.33"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Bollig, B., Decker, N., Leucker, M.: Frequency linear-time temporal logic. In: TASE. IEEE, Beijing, July 2012","DOI":"10.1109\/TASE.2012.43"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1007\/978-3-662-44584-6_19","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"P Bouyer","year":"2014","unstructured":"Bouyer, P., Markey, N., Matteplackel, R.M.: Averaging in LTL. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 266\u2013280. Springer, Heidelberg (2014)"},{"issue":"4","key":"12_CR9","first-page":"1","volume":"10","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Chatterjee, K., Forejt, V., Ku\u010dera, A.: Markov decision processes with multiple long-run average objectives. LMCS 10(4), 1\u201329 (2014)","journal-title":"LMCS"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Forejt, V., Ku\u010dera, A.: Trading performance for stability in Markov decision processes. In: LICS. IEEE (2013)","DOI":"10.1109\/LICS.2013.39"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-642-22993-0_21","volume-title":"Mathematical Foundations of Computer Science 2011","author":"K Chatterjee","year":"2011","unstructured":"Chatterjee, K., Doyen, L.: Energy and mean-payoff parity markov decision processes. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 206\u2013218. Springer, Heidelberg (2011)"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1007\/978-3-642-39799-8_37","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2013","unstructured":"Chatterjee, K., Gaiser, A., K\u0159et\u00ednsk\u00fd, J.: Automata with generalized rabin pairs for probabilistic model checking and LTL synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 559\u2013575. Springer, Heidelberg (2013)"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Kom\u00e1rkov\u00e1, Z., K\u0159et\u00ednsk\u00fd, J.: Unifying two views on multiple mean-payoff objectives in Markov decision processes. In: LICS (2015)","DOI":"10.1109\/LICS.2015.32"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Clemente, L., Raskin, J.-F.: Multidimensional beyond worst-case and almost-sure problems for mean-payoff objectives. In: LICS (2015, To appear)","DOI":"10.1109\/LICS.2015.33"},{"issue":"4","key":"12_CR15","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-642-38536-0_36","volume-title":"Computer Science \u2013 Theory and Applications","author":"M Droste","year":"2013","unstructured":"Droste, M., Perevoshchikov, V.: Multi-weighted automata and MSO logic. In: Bulatov, A.A., Shur, A.M. (eds.) CSR 2013. LNCS, vol. 7913, pp. 418\u2013430. Springer, Heidelberg (2013)"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1007\/978-3-319-08867-9_13","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2014","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J.: From LTL to deterministic automata: a safraless compositional approach. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 192\u2013208. Springer, Heidelberg (2014)"},{"issue":"4","key":"12_CR18","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 4(4), 1\u201321 (2008)","journal-title":"LMCS"},{"key":"12_CR19","unstructured":"Forejt, V., Kr\u010d\u00e1l, J.: On frequency LTL in probabilistic systems. In: CONCUR, LIPIcs, vol. 42. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2015)"},{"key":"12_CR20","unstructured":"Forejt, V., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J.: Controller synthesis for MDPS and frequency LTL\n                    \n                      \n                    \n                    $$_{\\setminus \\text{ GU }}$$\n                   (2015). CoRR, abs\/1509.04116"},{"key":"12_CR21","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":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"628","DOI":"10.1007\/978-3-662-46681-0_57","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kini","year":"2015","unstructured":"Kini, D., Viswanathan, M.: Limit deterministic and probabilistic automata for LTL\n                    \n                      \n                    \n                    $$_{\\setminus \\text{ GU }}$$\n                  . In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 628\u2013642. Springer, Heidelberg (2015)"},{"issue":"2","key":"12_CR23","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/j.tcs.2006.07.022","volume":"363","author":"J Klein","year":"2006","unstructured":"Klein, J., Baier, C.: Experiments with deterministic \n                    \n                      \n                    \n                    $$\\omega $$\n                  -automata for formulas of linear temporal logic. Theor. Comput. Sci. 363(2), 182\u2013195 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/978-3-319-11936-6_17","volume-title":"Automated Technology for Verification and Analysis","author":"Z Kom\u00e1rkov\u00e1","year":"2014","unstructured":"Kom\u00e1rkov\u00e1, Z., K\u0159et\u00ednsk\u00fd, J.: Rabinizer 3: Safraless translation of LTL to small deterministic automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 235\u2013241. Springer, Heidelberg (2014)"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"K\u0159et\u00ednsk\u00fd, J., Ledesma-Garza, R.: Rabinizer 2: small deterministic automata for LTL\n                    \n                      \n                    \n                    $$\\setminus $$\n                  GU. In: ATVA (2013)","DOI":"10.1007\/978-3-319-02444-8_32"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-642-31424-7_7","volume-title":"Computer Aided Verification","author":"J K\u0159et\u00ednsk\u00fd","year":"2012","unstructured":"K\u0159et\u00ednsk\u00fd, J., Esparza, J.: Deterministic automata for the (F,G)-fragment of LTL. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 7\u201322. Springer, Heidelberg (2012)"},{"key":"12_CR27","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. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"12_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-319-21690-4_8","volume-title":"Computer Aided Verification","author":"M Randour","year":"2015","unstructured":"Randour, M., Raskin, J.-F., Sankur, O.: Percentile queries in multi-dimensional Markov decision processes. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 123\u2013139. Springer, Heidelberg (2015)"},{"key":"12_CR29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59126-6_7","volume-title":"Languages, Automata, and Logic","author":"W Thomas","year":"1997","unstructured":"Thomas, W.: Languages, Automata, and Logic. Springer, New York (1997)"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Tomita, T., Hagihara, S., Yonezaki, N.: A probabilistic temporal logic with frequency operators and its model checking. In: INFINITY (2011)","DOI":"10.4204\/EPTCS.73.9"},{"key":"12_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-34281-3_19","volume-title":"Formal Methods and Software Engineering","author":"T Tomita","year":"2012","unstructured":"Tomita, T., Hiura, S., Hagihara, S., Yonezaki, N.: A temporal logic with mean-payoff constraints. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 249\u2013265. Springer, Heidelberg (2012)"},{"key":"12_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency: Structure versus Automata","author":"MY Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency: Structure versus Automata. LNCS, vol. 1043. Springer, Heidelberg (1996)"},{"key":"12_CR33","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS. IEEE (1986)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T15:31:52Z","timestamp":1559316712000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}