{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:01:48Z","timestamp":1779087708372,"version":"3.51.4"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031757747","type":"print"},{"value":"9783031757754","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-75775-4_13","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T07:26:29Z","timestamp":1731396389000},"page":"293-313","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking Markov Chains as\u00a0Distribution Transformers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8770-3523","authenticated-orcid":false,"given":"Rajab","family":"Aghamov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5321-9343","authenticated-orcid":false,"given":"Christel","family":"Baier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9405-2332","authenticated-orcid":false,"given":"Toghrul","family":"Karimov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-0339-1230","authenticated-orcid":false,"given":"Joris","family":"Nieuwveld","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0031-9356","authenticated-orcid":false,"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4829-0476","authenticated-orcid":false,"given":"Jakob","family":"Piribauer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-5709-899X","authenticated-orcid":false,"given":"Mihir","family":"Vahanwala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2629417","volume":"62","author":"M Agrawal","year":"2015","unstructured":"Agrawal, M., Akshay, S., Genest, B., Thiagarajan, P.S.: Approximate verification of the symbolic dynamics of Markov chains. J. ACM (JACM) 62, 1\u201334 (2015)","journal-title":"J. ACM (JACM)"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Almagor, S., Karimov, T., Kelmendi, E., Ouaknine, J., Worrell, J.: Deciding $$\\omega $$-regular properties on linear recurrence sequences. Proc. ACM Program. Lang. 5(POPL) (2021)","DOI":"10.1145\/3434329"},{"key":"13_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-41026-0","volume-title":"Linear Algebra Done Right","author":"S Axler","year":"2023","unstructured":"Axler, S.: Linear Algebra Done Right, 4th edn. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-41026-0","edition":"4"},{"key":"13_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2000","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2000)"},{"key":"13_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in Real Algebraic Geometry","author":"S Basu","year":"2006","unstructured":"Basu, S., Pollack, R., Roy, M.-F.: Algorithms in Real Algebraic Geometry. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/3-540-33099-2"},{"key":"13_CR6","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1093\/logcom\/exl004","volume":"16","author":"D Beauquier","year":"2006","unstructured":"Beauquier, D., Rabinovich, A., Slissenko, A.: A logic of probability with decidable model checking. J. Log. Comput. 16, 461\u2013487 (2006)","journal-title":"J. Log. Comput."},{"key":"13_CR7","unstructured":"Bilu, Y., Luca, F., Nieuwveld, J., Ouaknine, J., Purser, D., Worrell, J.: Skolem meets schanuel. In: Szeider, S., Ganian, R., Silva, A. (eds.) 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 241, pp. 20:1\u201320:15, Dagstuhl, Germany. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"13_CR8","unstructured":"Bilu, Y., Luca, F., Nieuwveld, J., Ouaknine, J., Purser, D., Worrell, J.: The Skolem Tool (2022)"},{"key":"13_CR9","unstructured":"Karimov, T.: Algorithmic verification of linear dynamical systems. Ph.D. thesis, Universit\u00e4t des Saarlandes (2024)"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Karimov, T., Kelmendi, E., Nieuwveld, J., Ouaknine, J., Worrell, J.: The power of positivity. In: 2023 38th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 1\u201311 (2023)","DOI":"10.1109\/LICS56636.2023.10175758"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Karimov, T., et al.: What\u2019s decidable about linear loops? Proc. ACM Program. Lang. 6(POPL) (2022)","DOI":"10.1145\/3498727"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Korthikanti, V.A., Viswanathan, M., Agha, G., Kwon, Y.-M.: Reasoning about MDPs as transformers of probability distributions. In: QEST, pp. 199\u2013208 (2010)","DOI":"10.1109\/QEST.2010.35"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-540-30482-1_21","volume-title":"Formal Methods and Software Engineering","author":"YM Kwon","year":"2004","unstructured":"Kwon, Y.M., Agha, G.: Linear inequality LTL (iLTL): a model checker for discrete time Markov chains. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 194\u2013208. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30482-1_21"},{"key":"13_CR14","first-page":"63","volume":"349","author":"M Mignotte","year":"1984","unstructured":"Mignotte, M., Shorey, T.N., Tijdeman, R.: The distance between terms of an algebraic recurrence sequence. Journal f\u00fcr die reine und angewandte Mathematik 349, 63\u201376 (1984)","journal-title":"Journal f\u00fcr die reine und angewandte Mathematik"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-662-43951-7_27","volume-title":"Automata, Languages, and Programming","author":"J Ouaknine","year":"2014","unstructured":"Ouaknine, J., Worrell, J.: On the positivity problem for simple linear recurrence sequences. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014. LNCS, vol. 8573, pp. 318\u2013329. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43951-7_27"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: Positivity problems for low-order linear recurrence sequences. In: Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2014, Portland, Oregon, USA, 5\u20137 January 2014, pp. 366\u2013379. SIAM (2014)","DOI":"10.1137\/1.9781611973402.27"},{"key":"13_CR17","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2024.106481","volume":"186","author":"M Vahanwala","year":"2024","unstructured":"Vahanwala, M.: Skolem and positivity completeness of ergodic Markov chains. Inf. Process. Lett. 186, 106481 (2024)","journal-title":"Inf. Process. Lett."},{"key":"13_CR18","first-page":"177","volume":"38","author":"NK Vereshchagin","year":"1985","unstructured":"Vereshchagin, N.K.: The problem of appearance of a zero in a linear recurrence sequence. Matematicheskie Zametki (in Russian) 38, 177\u2013189 (1985)","journal-title":"Matematicheskie Zametki (in Russian)"}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75775-4_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T08:03:43Z","timestamp":1731398623000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75775-4_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031757747","9783031757754"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75775-4_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}}]}}