{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,2]],"date-time":"2026-05-02T23:49:19Z","timestamp":1777765759736,"version":"3.51.4"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031974380","type":"print"},{"value":"9783031974397","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-031-97439-7_9","type":"book-chapter","created":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T11:04:00Z","timestamp":1756551840000},"page":"197-206","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["PCTL Satisfiability for\u00a0Infinite Binary Trees"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6602-8028","authenticated-orcid":false,"given":"Anton\u00edn","family":"Ku\u010dera","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,30]]},"reference":[{"key":"9_CR1","unstructured":"Baier, C.: On Algorithmic Verification Methods for Probabilistic Systems. Habilitation thesis, University of Mannheim (1998)"},{"key":"9_CR2","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"issue":"3","key":"9_CR3","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. Distrib. Comput. 11(3), 125\u2013155 (1998)","journal-title":"Distrib. Comput."},{"key":"9_CR4","unstructured":"Bertrand, N., Fearnley, J., Schewe, S.: Bounded satisfiability for PCTL. In: Proceedings of CSL 2012. Leibniz International Proceedings in Informatics, vol.\u00a016, pp. 92\u2013106. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2012)"},{"key":"9_CR5","unstructured":"Billingsley, P.: Probability and Measure. Wiley, Hoboken (1995)"},{"key":"9_CR6","doi-asserted-by":"crossref","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 Computer Society Press (2006)","DOI":"10.1109\/LICS.2006.48"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Forejt, V., K\u0159et\u00ednsk\u00fd, J., Ku\u010dera, A.: The satisfiability problem for probabilistic CTL. In: Proceedings of LICS 2008, pp. 391\u2013402. IEEE Computer Society Press (2008)","DOI":"10.1109\/LICS.2008.21"},{"key":"9_CR8","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). https:\/\/doi.org\/10.1007\/978-3-540-70583-3_13"},{"key":"9_CR9","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). https:\/\/doi.org\/10.1007\/978-3-540-31856-9_12"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Katoen, J.: On the satisfiability of some simple probabilistic logics. In: Proceedings of LICS 2016, pp. 56\u201365 (2016)","DOI":"10.1145\/2933575.2934526"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Chodil, M., Ku\u010dera, A.: The finite satisfiability problem for PCTL is undecidable. In: Proceedings of LICS 2024, Article No.\u00a022, pages 1\u201314. ACM Press (2024)","DOI":"10.1145\/3661814.3662145"},{"key":"9_CR12","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2023.103478","volume":"139","author":"M Chodil","year":"2024","unstructured":"Chodil, M., Ku\u010dera, A.: The satisfiability problem for a quantitative fragment of PCTL. J. Comput. Syst. Sci. 139, 103478 (2024)","journal-title":"J. Comput. Syst. Sci."},{"key":"9_CR13","unstructured":"Chodil, M., Ku\u010dera, A.: The satisfiability and validity problems for probabilistic computational tree logic are highly undecidable. In: Proceedings of ICALP 2025. Leibniz International Proceedings in Informatics, vol.\u00a0334. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2025)"},{"key":"9_CR14","volume-title":"Model Checking","author":"E Clark","year":"1999","unstructured":"Clark, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Emerson, E.: Temporal and modal logic. Handb. Theor. Comput. Sci. B, 995\u20131072 (1991)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6, 512\u2013535 (1994)","DOI":"10.1007\/BF01211866"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Harel, D.: Effective transformations on infinite trees with applications to high undecidability dominoes, and fairness. J. Assoc. Comput. Mach. 33(1) (1986)","DOI":"10.1145\/4904.4993"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Hart, S., Sharir, M.: Probabilistic temporal logic for finite and bounded models. In: Proceedings of POPL\u201984, pp. 1\u201313. ACM Press (1984)","DOI":"10.1145\/800057.808660"},{"key":"9_CR19","unstructured":"Kraus, S., Lehmann, D.: Decision procedures for time and chance (extended abstract). In: Proceedings of FOCS\u201983, pp. 202\u2013209. IEEE Computer Society Press (1983)"},{"key":"9_CR20","unstructured":"K\u0159et\u00ednsk\u00fd, J., Rotar, A.: The satisfiability problem for unbounded fragments of probabilistic CTL. In: Proceedings of CONCUR 2018. Leibniz International Proceedings in Informatics, vol.\u00a0118, pp. 32:1\u201332:16. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2018)"},{"key":"9_CR21","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0019-9958(82)91022-1","volume":"53","author":"D Lehmann","year":"1982","unstructured":"Lehmann, D., Shelah, S.: Reasoning with time and chance. Inf. Control 53, 165\u2013198 (1982)","journal-title":"Inf. Control"},{"key":"9_CR22","unstructured":"Minsky, M.: Computation: Finite and Infinite Machines. Prentice-Hall, Upper Saddle River (1967)"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-030-99253-8_23","volume-title":"Foundations of Software Science and Computation Structures","author":"T Winkler","year":"2022","unstructured":"Winkler, T., Gehnen, C., Katoen, J.-P.: Model checking temporal properties of recursive probabilistic programs. In: FoSSaCS 2022. LNCS, vol. 13242, pp. 449\u2013469. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99253-8_23"}],"container-title":["Lecture Notes in Computer Science","Principles of Formal Quantitative Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-97439-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T15:29:22Z","timestamp":1777476562000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-97439-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,30]]},"ISBN":["9783031974380","9783031974397"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-97439-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,30]]},"assertion":[{"value":"30 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}