{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T09:21:03Z","timestamp":1775208063013,"version":"3.50.1"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T00:00:00Z","timestamp":1775174400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T00:00:00Z","timestamp":1775174400000},"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":["Math.Comput.Sci."],"published-print":{"date-parts":[[2026,12]]},"DOI":"10.1007\/s11786-025-00624-2","type":"journal-article","created":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T08:29:04Z","timestamp":1775204944000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On the Theory of Order Over Real Numbers"],"prefix":"10.1007","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-4721-3824","authenticated-orcid":false,"given":"Bernard","family":"Boigelot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4700-6031","authenticated-orcid":false,"given":"Pascal","family":"Fontaine","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-5545-4579","authenticated-orcid":false,"given":"Baptiste","family":"Vergain","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,3]]},"reference":[{"key":"624_CR1","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of International Congress on Logic, Methodology and Philosophy of Science, pp. 1\u201312 (1962)"},{"key":"624_CR2","volume-title":"The Monadic Second-order Theory of All Countable Ordinals. Decidable theories","author":"JR B\u00fcchi","year":"1973","unstructured":"B\u00fcchi, J.R.: The Monadic Second-order Theory of All Countable Ordinals. Decidable theories, vol. 2. Springer, Berlin (1973)"},{"issue":"2","key":"624_CR3","doi-asserted-by":"publisher","first-page":"387","DOI":"10.2307\/2273556","volume":"48","author":"Y Gurevich","year":"1983","unstructured":"Gurevich, Y., Magidor, M., Shelah, S.: The monadic theory of $$\\omega _2$$. J. Symbol. Logic 48(2), 387\u2013398 (1983)","journal-title":"J. Symbol. Logic"},{"issue":"3","key":"624_CR4","first-page":"268","volume":"6","author":"A Ehrenfeucht","year":"1959","unstructured":"Ehrenfeucht, A.: Decidability of the theory of linear ordering relation. Not. Am. Math. Soc. 6(3), 268\u2013269 (1959)","journal-title":"Not. Am. Math. Soc."},{"issue":"1","key":"624_CR5","doi-asserted-by":"publisher","first-page":"109","DOI":"10.4064\/fm-59-1-109-116","volume":"59","author":"H L\u00e4uchli","year":"1966","unstructured":"L\u00e4uchli, H., Leonard, J.: On the elementary theory of linear order. Fundam. Math. 59(1), 109\u2013116 (1966)","journal-title":"Fundam. Math."},{"issue":"4","key":"624_CR6","doi-asserted-by":"publisher","first-page":"363","DOI":"10.24033\/asens.1027","volume":"71","author":"R Fra\u00efss\u00e9","year":"1954","unstructured":"Fra\u00efss\u00e9, R.: Sur l\u2019extension aux relations de quelques propri\u00e9t\u00e9s des ordres. Ann. Sci. de l\u2019\u00c9cole Normale Sup\u00e9rieure 71(4), 363\u2013388 (1954)","journal-title":"Ann. Sci. de l\u2019\u00c9cole Normale Sup\u00e9rieure"},{"issue":"2","key":"624_CR7","doi-asserted-by":"publisher","first-page":"129","DOI":"10.4064\/fm-49-2-129-141","volume":"49","author":"A Ehrenfeucht","year":"1961","unstructured":"Ehrenfeucht, A.: An application of games to the completeness problem for formalized theories. Fundam. Math. 49(2), 129\u2013141 (1961)","journal-title":"Fundam. Math."},{"key":"624_CR8","doi-asserted-by":"crossref","unstructured":"L\u00e4uchli, H.: A decision procedure for the weak second-order theory of linear order. In: Contributions to Mathematical Logic. Studies in Logic and the Foundations of Mathematics, vol. 50, pp. 189\u2013197. Elsevier, Amsterdam (1968)","DOI":"10.1016\/S0049-237X(08)70525-1"},{"issue":"3","key":"624_CR9","doi-asserted-by":"publisher","first-page":"379","DOI":"10.2307\/1971037","volume":"102","author":"S Shelah","year":"1975","unstructured":"Shelah, S.: The monadic theory of order. Ann. Math. 102(3), 379\u2013419 (1975)","journal-title":"Ann. Math."},{"key":"624_CR10","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Ehrenfeucht games, the composition method, and the monadic theory of ordinal words. In: Structures in Logic and Computer Science: A Selection of Essays in Honor of A. Ehrenfeucht. Lecture Notes in Computer Science, pp. 118\u2013143 (1997)","DOI":"10.1007\/3-540-63246-8_8"},{"key":"624_CR11","first-page":"1","volume":"141","author":"MO Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1\u201335 (1969)","journal-title":"Trans. Am. Math. Soc."},{"key":"624_CR12","unstructured":"Kamp, H.: Tense logic and the theory of linear order. Ph.D. thesis, University of California at Los Angeles (1968)"},{"key":"624_CR13","doi-asserted-by":"crossref","unstructured":"Rabinovich, A.: A proof of Kamp\u2019s theorem. Logical Methods in Computer Science 10(1) (2014)","DOI":"10.2168\/LMCS-10(1:14)2014"},{"key":"624_CR14","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of 7th ACM Symposium on Principles of Programming Languages (POPL), pp. 163\u2013170. ACM Press, New-York (1980)","DOI":"10.1145\/567446.567462"},{"key":"624_CR15","first-page":"115","volume":"26","author":"JP Burgess","year":"1985","unstructured":"Burgess, J.P., Gurevich, Y.: The decision problem for linear temporal logic. Notre Dame J. Form. Logic 26, 115\u2013128 (1985)","journal-title":"Notre Dame J. Form. Logic"},{"issue":"2","key":"624_CR16","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1016\/S0022-0000(03)00005-9","volume":"66","author":"M Reynolds","year":"2003","unstructured":"Reynolds, M.: The complexity of the temporal logic with \u201cuntil\u2019\u2019 over general linear time. J. Comput. Syst. Sci. 66(2), 393\u2013426 (2003)","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"624_CR17","first-page":"19","volume":"3","author":"M Reynolds","year":"2010","unstructured":"Reynolds, M.: The complexity of decision problems for linear temporal logics. J. Stud. Log 3(1), 19\u201350 (2010)","journal-title":"J. Stud. Log"},{"issue":"8","key":"624_CR18","doi-asserted-by":"publisher","first-page":"1063","DOI":"10.1016\/j.apal.2010.01.002","volume":"161","author":"M Reynolds","year":"2010","unstructured":"Reynolds, M.: The complexity of temporal logic over the reals. Ann. Pure Appl. Logic 161(8), 1063\u20131096 (2010)","journal-title":"Ann. Pure Appl. Logic"},{"key":"624_CR19","doi-asserted-by":"crossref","unstructured":"Rabinovich, A.: Temporal logics over linear time domains are in PSPACE. Inf. Comput. 210, 40\u201367 (2012)","DOI":"10.1016\/j.ic.2011.11.002"},{"key":"624_CR20","unstructured":"Barrett, C., Kroening, D., Melham, T.: Problem solving for the 21st century: Efficient solvers for satisfiability modulo theories. Technical Report\u00a03, London Mathematical Society and Smith Institute for Industrial Mathematics and System Engineering (2014)"},{"key":"624_CR21","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825\u2013885. IOS Press, Amsterdam (2009). Chap. 26"},{"key":"624_CR22","doi-asserted-by":"crossref","unstructured":"Habermehl, P., Hecko, M., Havlena, V., Hol\u00edk, L., Leng\u00e1l, O.: Algebraic reasoning meets automata in solving linear integer arithmetic. In: Proc. Intl. Conf. on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 14681, pp. 42\u201367. Springer, Berlin, Heidelberg (2024)","DOI":"10.1007\/978-3-031-65627-9_3"},{"key":"624_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03182-7","volume-title":"Finite Model Theory","author":"H-D Ebbinghaus","year":"1995","unstructured":"Ebbinghaus, H.-D., Flum, J.: Finite Model Theory. Springer, Berlin (1995)"},{"key":"624_CR24","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1112\/plms\/s2-30.1.264","volume":"30","author":"FP Ramsey","year":"1930","unstructured":"Ramsey, F.P.: On a problem of formal logic. Proc. Lond. Math. Soc. 30, 264\u2013286 (1930)","journal-title":"Proc. Lond. Math. Soc."},{"issue":"1","key":"624_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jcss.2006.10.009","volume":"73","author":"V Bruy\u00e8re","year":"2007","unstructured":"Bruy\u00e8re, V., Carton, O.: Automata on linear orderings. J. Comput. Syst. Sci. 73(1), 1\u201324 (2007)","journal-title":"J. Comput. Syst. Sci."},{"key":"624_CR26","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Fontaine, P., Vergain, B.: Non-emptiness test for automata over words indexed by the reals and rationals. In: Fazekas, S.Z. (ed.) Proceedings of International Conference on Implementation and Application of Automata (CIAA). Lecture Notes in Computer Science, vol. 15015, pp. 94\u2013108. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-71112-1_7"},{"key":"624_CR27","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Fontaine, P., Vergain, B.: Universal first-order quantification over automata. In: Nagy, B. (ed.) Proceedings of International Conference on Implementation and Application of Automata (CIAA). Lecture Notes in Computer Science, vol. 14151, pp. 91\u2013102. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-40247-0_6"}],"container-title":["Mathematics in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-025-00624-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11786-025-00624-2","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-025-00624-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T08:29:07Z","timestamp":1775204947000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11786-025-00624-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4,3]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,12]]}},"alternative-id":["624"],"URL":"https:\/\/doi.org\/10.1007\/s11786-025-00624-2","relation":{},"ISSN":["1661-8270","1661-8289"],"issn-type":[{"value":"1661-8270","type":"print"},{"value":"1661-8289","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,4,3]]},"assertion":[{"value":"17 April 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 January 2025","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 January 2025","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 April 2026","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of Interest"}}],"article-number":"5"}}