{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T11:37:45Z","timestamp":1770982665180,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540705826","type":"print"},{"value":"9783540705833","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70583-3_13","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"148-159","source":"Crossref","is-referenced-by-count":18,"title":["Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives"],"prefix":"10.1007","author":[{"given":"Tom\u00e1\u0161","family":"Br\u00e1zdil","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vojt\u011bch","family":"Forejt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anton\u00edn","family":"Ku\u010dera","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","first-page":"493","volume-title":"Proceedings of IFIP TCS 2004","author":"C. Baier","year":"2004","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: Proceedings of IFIP TCS 2004, pp. 493\u2013506. Kluwer, Dordrecht (2004)"},{"key":"13_CR2","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Forejt, V.: Branching-time model-checking of probabilistic pushdown automata. In: Proceedings of INFINITY 2007, pp. 24\u201333 (2007)"},{"key":"13_CR3","first-page":"349","volume-title":"Proceedings of 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: Proceedings of LICS 2006, pp. 349\u2013358. IEEE, Los Alamitos (2006)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-540-74407-8_29","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"T. Br\u00e1zdil","year":"2007","unstructured":"Br\u00e1zdil, T., Forejt, V.: Strategy synthesis for Markov decision processes and branching-time logics. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR. LNCS, vol.\u00a04703, pp. 428\u2013444. Springer, Heidelberg (2007)"},{"key":"13_CR5","unstructured":"Br\u00e1zdil, T., Forejt, V., Ku\u010dera, A.: Controller synthesis and verification for Markov decision processes with qualitative branching time objectives. Technical report FIMU-RS-2008-05, Faculty of Informatics, Masaryk University (2008)"},{"key":"13_CR6","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1109\/QEST.2004.1348035","volume-title":"Proceedings of 2nd Int. Conf. on Quantitative Evaluation of Systems (QEST 2004)","author":"K. Chatterjee","year":"2004","unstructured":"Chatterjee, K., de Alfaro, L., Henzinger, T.: Trading memory for randomness. In: Proceedings of 2nd Int. Conf. on Quantitative Evaluation of Systems (QEST 2004), pp. 206\u2013217. IEEE, Los Alamitos (2004)"},{"key":"13_CR7","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":"13_CR8","series-title":"Lecture Notes in Computer Science","first-page":"102","volume-title":"CONCUR 2003 - Concurrency Theory","author":"L. Alfaro de","year":"2003","unstructured":"de Alfaro, L.: Quantitative verification and control via the mu-calculus. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol.\u00a02761, pp. 102\u2013126. Springer, Heidelberg (2003)"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic. Handbook of TCS B, 995\u20131072 (1991)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-540-71209-1_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Etessami","year":"2007","unstructured":"Etessami, K., Kwiatkowska, M., Vardi, M., Yannakakis, M.: Multi-objective model checking of Markov decision processes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 50\u201365. Springer, Heidelberg (2007)"},{"key":"13_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4054-9","volume-title":"Competitive Markov Decision Processes","author":"J. Filar","year":"1996","unstructured":"Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, Heidelberg (1996)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1007\/978-3-540-24749-4_2","volume-title":"STACS 2004","author":"E. Gr\u00e4del","year":"2004","unstructured":"Gr\u00e4del, E.: Positional determinacy of infinite games. In: Diekert, V., Habib, M. (eds.) STACS 2004. LNCS, vol.\u00a02996, pp. 4\u201318. Springer, Heidelberg (2004)"},{"key":"13_CR13","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, 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"13_CR14","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J.E. Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1007\/11590156_44","volume-title":"Proceedings of FST&TCS 2005","author":"A. Ku\u010dera","year":"2005","unstructured":"Ku\u010dera, A., Stra\u017eovsk\u00fd, O.: On the controller synthesis for finite-state Markov decision processes. In: Proceedings of FST&TCS 2005. LNCS, vol.\u00a03821, pp. 541\u2013552. Springer, Heidelberg (2005)"},{"key":"13_CR16","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes","author":"M.L. Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes. Wiley, Chichester (1994)"},{"key":"13_CR17","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1093\/oso\/9780198537618.003.0005","volume":"2","author":"C. Stirling","year":"1992","unstructured":"Stirling, C.: Modal and temporal logics. Handbook of Logic in Comp. Sci.\u00a02, 477\u2013563 (1992)","journal-title":"Handbook of Logic in Comp. Sci."},{"key":"13_CR18","first-page":"327","volume-title":"Proceedings of FOCS 1985","author":"M. Vardi","year":"1985","unstructured":"Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of FOCS 1985, pp. 327\u2013338. IEEE, Los Alamitos (1985)"},{"key":"13_CR19","first-page":"356","volume-title":"Proceedings of LICS 2004","author":"I. Walukiewicz","year":"2004","unstructured":"Walukiewicz, I.: A landscape with games in the background. In: Proceedings of LICS 2004, pp. 356\u2013366. IEEE, Los Alamitos (2004)"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70583-3_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,29]],"date-time":"2024-02-29T06:30:51Z","timestamp":1709188251000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70583-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705826","9783540705833"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70583-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}