{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:59:00Z","timestamp":1781027940005,"version":"3.54.1"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We consider linear dynamical systems under floating-point rounding. In these systems, a matrix is repeatedly applied to a vector, but the numbers are rounded into floating-point representation after each step (i.e., stored as a fixed-precision mantissa and an exponent). The approach more faithfully models realistic implementations of linear loops, compared to the exact arbitrary-precision setting often employed in the study of linear dynamical systems.<\/jats:p>\n                  <jats:p>\n                    Our results are twofold: We show that for non-negative matrices there is a special structure to the sequence of vectors generated by the system: the mantissas are periodic and the exponents grow linearly. We leverage this to show decidability of\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\omega $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>\u03c9<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -regular temporal model checking against semialgebraic predicates. This contrasts with the unrounded setting, where even the non-negative case encompasses the long-standing open Skolem and Positivity problems.\n                  <\/jats:p>\n                  <jats:p>On the other hand, when negative numbers are allowed in the matrix, we show that the reachability problem is undecidable by encoding a two-counter machine. Again, this is in contrast with the unrounded setting where point-to-point reachability is known to be decidable in polynomial time.<\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_3","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T16:19:12Z","timestamp":1682093952000},"page":"47-65","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Model Checking Linear Dynamical Systems under Floating-point Rounding"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0875-300X","authenticated-orcid":false,"given":"Engel","family":"Lefaucheux","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0031-9356","authenticated-orcid":false,"given":"Jo\u00ebl","family":"Ouaknine","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0394-1634","authenticated-orcid":false,"given":"David","family":"Purser","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1987-9487","authenticated-orcid":false,"given":"Mohammadamin","family":"Sharifi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","unstructured":"Abbasi, R., Schiffl, J., Darulova, E., Ulbrich, M., Ahrendt, W.: Deductive verification of floating-point java programs in key. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Part of ETAPS 2021. Part II. Lecture Notes in Computer Science, vol. 12652, pp. 242\u2013261. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_13","DOI":"10.1007\/978-3-030-72013-1_13"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Akshay, S., Antonopoulos, T., Ouaknine, J., Worrell, J.: Reachability problems for Markov chains. Inf. Process. Lett. 115(2), 155\u2013158 (2015). https:\/\/doi.org\/10.1016\/j.ipl.2014.08.013","DOI":"10.1016\/j.ipl.2014.08.013"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Akshay, S., Bazille, H., Genest, B., Vahanwala, M.: On robustness for the Skolem and Positivity problems. In: Berenbrink, P., Monmege, B. (eds.) 39th International Symposium on Theoretical Aspects of Computer Science, STACS 2022. LIPIcs, vol.\u00a0219, pp. 5:1\u20135:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2022.5","DOI":"10.4230\/LIPIcs.STACS.2022.5"},{"key":"3_CR4","doi-asserted-by":"publisher","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), 1\u201324 (2021). https:\/\/doi.org\/10.1145\/3434329","DOI":"10.1145\/3434329"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Baier, C., Funke, F., Jantsch, S., Karimov, T., Lefaucheux, E., Ouaknine, J., Pouly, A., Purser, D., Whiteland, M.A.: Reachability in dynamical systems with rounding. In: 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2020. LIPIcs, vol.\u00a0182, pp. 36:1\u201336:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2020.36","DOI":"10.4230\/LIPIcs.FSTTCS.2020.36"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Baier, C., Funke, F., Jantsch, S., Karimov, T., Lefaucheux, E., Ouaknine, J., Purser, D., Whiteland, M.A., Worrell, J.: Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications. In: Klin, B., Lasota, S., Muscholl, A. (eds.) 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0243, pp. 10:1\u201310:16. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2022.10","DOI":"10.4230\/LIPIcs.CONCUR.2022.10"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Becker, H., Panchekha, P., Darulova, E., Tatlock, Z.: Combining tools for optimization and analysis of floating-point computations. In: Havelund, K., Peleska, J., Roscoe, B., de\u00a0Vink, E.P. (eds.) Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018. Lecture Notes in Computer Science, vol. 10951, pp. 355\u2013363. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_21","DOI":"10.1007\/978-3-319-95582-7_21"},{"key":"3_CR8","doi-asserted-by":"publisher","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. LIPIcs, vol.\u00a0241, pp. 20:1\u201320:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2022.20","DOI":"10.4230\/LIPIcs.MFCS.2022.20"},{"key":"3_CR9","unstructured":"Boyle, M.: Notes on the Perron-Frobenius theory of nonnegative matrices (2005)"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Braverman, M.: Termination of integer linear programs. In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification, 18th International Conference, CAV 2006 Proceedings. Lecture Notes in Computer Science, vol.\u00a04144, pp. 372\u2013385. Springer (2006). https:\/\/doi.org\/10.1007\/11817963_34","DOI":"10.1007\/11817963_34"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: The collected works of J. Richard B\u00fcchi, pp. 425\u2013435. Springer (1990)","DOI":"10.1007\/978-1-4613-8928-6_23"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Chonev, V., Ouaknine, J., Worrell, J.: On the complexity of the orbit problem. J. ACM 63(3), 23:1\u201323:18 (2016). https:\/\/doi.org\/10.1145\/2857050","DOI":"10.1145\/2857050"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"D\u2019Costa, J., Karimov, T., Majumdar, R., Ouaknine, J., Salamati, M., Soudjani, S., Worrell, J.: The pseudo-Skolem problem is decidable. In: Bonchi, F., Puglisi, S.J. (eds.) 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021. LIPIcs, vol.\u00a0202, pp. 34:1\u201334:21. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2021.34","DOI":"10.4230\/LIPIcs.MFCS.2021.34"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"D\u2019Costa, J., Karimov, T., Majumdar, R., Ouaknine, J., Salamati, M., Worrell, J.: The pseudo-reachability problem for diagonalisable linear dynamical systems. In: Szeider, S., Ganian, R., Silva, A. (eds.) 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022. LIPIcs, vol.\u00a0241, pp. 40:1\u201340:13. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2022.40","DOI":"10.4230\/LIPIcs.MFCS.2022.40"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Haase, C.: A survival guide to Presburger arithmetic. ACM SIGLOG News 5(3), 67\u201382 (2018). https:\/\/doi.org\/10.1145\/3242953.3242964","DOI":"10.1145\/3242953.3242964"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Kannan, R., Lipton, R.J.: Polynomial-time algorithm for the orbit problem. J. ACM 33(4), 808\u2013821 (1986). https:\/\/doi.org\/10.1145\/6490.6496","DOI":"10.1145\/6490.6496"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Karimov, T., Kelmendi, E., Ouaknine, J., Worrell, J.: What\u2019s decidable about discrete linear dynamical systems? In: Raskin, J., Chatterjee, K., Doyen, L., Majumdar, R. (eds.) Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 13660, pp. 21\u201338. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-22337-2_2","DOI":"10.1007\/978-3-031-22337-2_2"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Karimov, T., Lefaucheux, E., Ouaknine, J., Purser, D., Varonka, A., Whiteland, M.A., Worrell, J.: What\u2019s decidable about linear loops? Proc. ACM Program. Lang. 6(POPL), 1\u201325 (2022). https:\/\/doi.org\/10.1145\/3498727","DOI":"10.1145\/3498727"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Lefaucheux, E., Ouaknine, J., Purser, D., Sharifi, M.: Model checking linear dynamical systems under floating-point rounding. CoRR abs\/2211.04301 (2022). https:\/\/doi.org\/10.48550\/arXiv.2211.04301","DOI":"10.48550\/arXiv.2211.04301"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Lohar, D., Jeangoudoux, C., Sobel, J., Darulova, E., Christakis, M.: A two-phase approach for conditional floating-point verification. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Part of ETAPS 2021. Part II. Lecture Notes in Computer Science, vol. 12652, pp. 43\u201363. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_3","DOI":"10.1007\/978-3-030-72013-1_3"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"Luca, F., Ouaknine, J., Worrell, J.: Algebraic model checking for discrete linear dynamical systems. In: Bogomolov, S., Parker, D. (eds.) Formal Modeling and Analysis of Timed Systems - 20th International Conference, FORMATS 2022. Lecture Notes in Computer Science, vol. 13465, pp. 3\u201315. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-15839-1_1","DOI":"10.1007\/978-3-031-15839-1_1"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Maurica, F., Mesnard, F., Payet, E.: Optimal approximation for efficient termination analysis of floating-point loops. In: 2017 1st International Conference on Next Generation Computing Applications (NextComp). pp. 17\u201322. IEEE (2017)","DOI":"10.1109\/NEXTCOMP.2017.8016170"},{"key":"3_CR23","unstructured":"Minsky, M.L.: Computation. Prentice-Hall Englewood Cliffs (1967)"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Ouaknine, J., Worrell, J.: Positivity problems for low-order linear recurrence sequences. In: Chekuri, C. (ed.) Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2014. pp. 366\u2013379. SIAM (2014). https:\/\/doi.org\/10.1137\/1.9781611973402.27","DOI":"10.1137\/1.9781611973402.27"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Schneider, H.: Wielandt\u2019s proof of the exponent inequality for primitive nonnegative matrices. Linear Algebra and its Applications 353(1), 5\u201310 (2002)","DOI":"10.1016\/S0024-3795(02)00414-7"},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) Computer Aided Verification, 16th International Conference, CAV 2004 Proceedings. Lecture Notes in Computer Science, vol.\u00a03114, pp. 70\u201382. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_6","DOI":"10.1007\/978-3-540-27813-9_6"},{"key":"3_CR27","doi-asserted-by":"publisher","unstructured":"Xia, B., Yang, L., Zhan, N., Zhang, Z.: Symbolic decision procedure for termination of linear programs. Formal Aspects Comput. 23(2), 171\u2013190 (2011). https:\/\/doi.org\/10.1007\/s00165-009-0144-5","DOI":"10.1007\/s00165-009-0144-5"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:06:09Z","timestamp":1781024769000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}