{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T21:27:57Z","timestamp":1743024477829,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319669014"},{"type":"electronic","value":"9783319669021"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66902-1_11","type":"book-chapter","created":{"date-parts":[[2017,8,29]],"date-time":"2017-08-29T11:34:20Z","timestamp":1504006460000},"page":"175-192","source":"Crossref","is-referenced-by-count":1,"title":["Tableaux for Policy Synthesis for MDPs with PCTL* Constraints"],"prefix":"10.1007","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[]},{"given":"Sylvie","family":"Thi\u00e9baux","sequence":"additional","affiliation":[]},{"given":"Felipe","family":"Trevizan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,30]]},"reference":[{"key":"11_CR1","volume-title":"Constrained Markov Decision Processes","author":"E Altman","year":"1999","unstructured":"Altman, E.: Constrained Markov Decision Processes, vol. 7. CRC Press, Boca Raton (1999)"},{"key":"11_CR2","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: TCS 2004 (2004)"},{"key":"11_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Thi\u00e9baux, S., Trevizan, F.: Tableaux for policy synthesis for MDPS with PCTL* constraints. CoRR, abs\/1706.10102 (2017)","DOI":"10.1007\/978-3-319-66902-1_11"},{"key":"11_CR5","unstructured":"Br\u00e1zdil, T., Brozek, V., Forejt, V., Kucera, A.: Stochastic games with branching-time winning objectives. In: 21th IEEE Symposium on Logic in Computer Science LICS (2006)"},{"key":"11_CR6","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 2007. LNCS, vol. 4703, pp. 428\u2013444. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74407-8_29"},{"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. LNCS, vol. 5126, pp. 148\u2013159. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-70583-3_13"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-540-31856-9_12","volume-title":"STACS 2005","author":"T Br\u00e1zdil","year":"2005","unstructured":"Br\u00e1zdil, T., Ku\u010dera, A., Stra\u017eovsk\u00fd, O.: On the decidability of temporal properties of probabilistic pushdown automata. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol. 3404, pp. 145\u2013157. Springer, Heidelberg (2005). doi: 10.1007\/978-3-540-31856-9_12"},{"issue":"4","key":"11_CR9","doi-asserted-by":"crossref","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":"11_CR10","doi-asserted-by":"crossref","unstructured":"Ding, X.C., Pinto, A., Surana, A.: Strategic planning under uncertainties via constrained Markov decision processes. In: IEEE International Conference on Robotics and Automation ICRA (2013)","DOI":"10.1109\/ICRA.2013.6631226"},{"issue":"5","key":"11_CR11","doi-asserted-by":"crossref","first-page":"1244","DOI":"10.1109\/TAC.2014.2298143","volume":"59","author":"XC Ding","year":"2014","unstructured":"Ding, X.C., Smith, S., Belta, C., Rus, D.: Optimal control of Markov decision processes with linear temporal logic constraints. IEEE Trans. Automat. Contr. 59(5), 1244\u20131257 (2014)","journal-title":"IEEE Trans. Automat. Contr."},{"key":"11_CR12","unstructured":"Dolgov, D., Durfee, E.: Stationary deterministic policies for constrained MDPs with multiple rewards, costs, and discount factors. In: IJCAI (2005)"},{"key":"11_CR13","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. 6659, pp. 53\u2013113. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-21455-4_3"},{"key":"11_CR14","volume-title":"Denumerable Markov Chains: With a Chapter of Markov Random Fields by David Griffeath","author":"J Kemeny","year":"2012","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains: With a Chapter of Markov Random Fields by David Griffeath, vol. 40. Springer, Heidelberg (2012)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/11590156_44","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","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: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 541\u2013552. Springer, Heidelberg (2005). doi: 10.1007\/11590156_44"},{"key":"11_CR16","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. 4486, pp. 220\u2013270. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-72522-0_6"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","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":"M Kwiatkowska","year":"2013","unstructured":"Kwiatkowska, M., Parker, D.: Automated verification and strategy synthesis for probabilistic systems. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 5\u201322. Springer, Cham (2013). doi: 10.1007\/978-3-319-02444-8_2"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Reynolds, M.: A new rule for LTL tableaux. In: GandALF (2016)","DOI":"10.4204\/EPTCS.226.20"},{"key":"11_CR19","unstructured":"Reynolds, M.: A traditional tree-style tableau for LTL. CoRR, abs\/1604.03962 (2016)"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Sprauel, J., Kolobov, A., Teichteil-K\u00f6nigsbuch, F.: Saturated path-constrained MDP: planning under uncertainty and deterministic model-checking constraints. In: AAAI (2014)","DOI":"10.1609\/aaai.v28i1.9041"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Svorenov\u00e1, M., Cerna, I., Belta, C.: Optimal control of MDPs with temporal logic constraints. In: CDC (2013)","DOI":"10.1109\/CDC.2013.6760491"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Trevizan, F., Thi\u00e9baux, S., Santana, P., Williams, B.: Heuristic search in dual space for constrained stochastic shortest path problems. In: ICAPS (2016)","DOI":"10.1609\/icaps.v26i1.13768"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66902-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,25]],"date-time":"2023-08-25T08:51:59Z","timestamp":1692953519000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66902-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319669014","9783319669021"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66902-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}