{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T12:07:25Z","timestamp":1774958845870,"version":"3.50.1"},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T00:00:00Z","timestamp":1774915200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T00:00:00Z","timestamp":1774915200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2026,6]]},"abstract":"Abstract<\/jats:title>\n \n Automata operating on representations of ultimately periodic words were introduced as an alternative way of capturing acceptance of regular\n \n \n $$\\omega $$<\/jats:tex-math>\n \n \u03c9<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -languages. Families of DFAs and lasso automata (which use pairs of words to represent ultimately periodic words) followed, and gave rise to minimisation algorithms, a Myhill-Nerode theorem and language learning algorithms. Yet Kleene theorems for such a well-established class are still missing, and lasso languages have not been studied algebraically. We are filling this gap by introducing rational lasso languages, expressions and a theory of lasso languages. We show a Kleene theorem for lasso languages and explore the connection between rational lasso and\n \n \n $$\\omega $$<\/jats:tex-math>\n \n \u03c9<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -expressions, which yields a Kleene theorem for\n \n \n $$\\omega $$<\/jats:tex-math>\n \n \u03c9<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -languages with respect to saturated lasso automata. For one direction of the Kleene theorems, we also provide a Brzozowski construction for lasso automata from rational lasso expressions. Our results offer a method to construct saturated lasso automata from rational\n \n \n $$\\omega $$<\/jats:tex-math>\n \n \u03c9<\/mml:mi>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -expressions.\n <\/jats:p>","DOI":"10.1007\/s00224-025-10231-0","type":"journal-article","created":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T11:28:45Z","timestamp":1774956525000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Kleene Theorems for Lasso Languages and $$\\omega $$-Languages"],"prefix":"10.1007","volume":"70","author":[{"given":"Mike","family":"Cruchten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,3,31]]},"reference":[{"key":"10231_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"554","DOI":"10.1007\/3-540-58027-1_27","volume-title":"Mathematical Foundations of Programming Semantics, 9th International Conference, New Orleans, LA, USA, April 7\u201310, 1993, Proceedings","author":"H Calbrix","year":"1993","unstructured":"Calbrix, H., Nivat, M., Podelski, A.: Ultimately periodic words of rational $$\\omega $$-languages. In: Brookes, S.D., Main, M.G., Melton, A., Mislove, M.W., Schmidt, D.A. (eds.) Mathematical Foundations of Programming Semantics, 9th International Conference, New Orleans, LA, USA, April 7\u201310, 1993, Proceedings. Lecture Notes in Computer Science, vol. 802, pp. 554\u2013566. Springer, Berlin, Heidelberg (1993)"},{"issue":"4","key":"10231_CR2","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model checker. Int. J. Softw. Tools Technol. Transf. 2(4), 410\u2013425 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10231_CR3","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-48119-2_16","volume-title":"FM\u201999 - Formal Methods","author":"J-M Couvreur","year":"1999","unstructured":"Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM\u201999 - Formal Methods, pp. 253\u2013271. Springer, Berlin, Heidelberg (1999)"},{"key":"10231_CR4","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"Computer Aided Verification","author":"RH Hardin","year":"1996","unstructured":"Hardin, R.H., Har\u2019El, Z., Kurshan, R.P.: Cospan. In: Alur, R., Henzinger, T.A. (eds.) Computer Aided Verification, pp. 423\u2013427. Springer, Berlin, Heidelberg (1996)"},{"key":"10231_CR5","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: In: Dembi\u0144ski, P., \u015aredniawa, M. (eds.) Simple On-the-fly automatic verification of linear temporal logic, pp. 3\u201318. Springer, Boston, MA (1996)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"10231_CR6","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: In: Manna, Z., Peled, D.A. (eds.) An Automata-Theoretic Approach to Infinite-State Systems, pp. 202\u2013259. Springer, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-13754-9_11"},{"issue":"5","key":"10231_CR7","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Trans. Software Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"10231_CR8","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/j.tcs.2016.07.031","volume":"650","author":"D Angluin","year":"2016","unstructured":"Angluin, D., Fisman, D.: Learning regular omega languages. Theor. Comput. Sci. 650, 57\u201372 (2016)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"10231_CR9","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0304-3975(96)00312-X","volume":"183","author":"O Maler","year":"1997","unstructured":"Maler, O., Staiger, L.: On syntactic congruences for omega-languages. Theor. Comput. Sci. 183(1), 93\u2013112 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"10231_CR10","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"11","volume-title":"41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)","author":"D Angluin","year":"2016","unstructured":"Angluin, D., Boker, U., Fisman, D.: Families of DFAs as Acceptors of omega-Regular Languages. In: Faliszewski, P., Muscholl, A., Niedermeier, R. (eds.) 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol. 58, pp. 11\u201311114. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2016)"},{"key":"10231_CR11","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"5","volume-title":"8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)","author":"V Ciancia","year":"2019","unstructured":"Ciancia, V., Venema, Y.: Omega-Automata: A Coalgebraic Perspective on Regular omega-Languages. In: Roggenbach, M., Sokolova, A. (eds.) 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), vol. 139, pp. 5\u20131518. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2019)"},{"key":"10231_CR12","unstructured":"Cruchten, M.: Topics in $$\\Omega $$-automata \u2013 A journey through lassos, algebra, coalgebra and expressions. Master\u2019s thesis, The University of Amsterdam (2022)"},{"key":"10231_CR13","unstructured":"Terese: Term Rewriting Systems. Cambridge tracts in theoretical computer science, vol. 55. Cambridge University Press, Cambridge, UK (2003)"},{"issue":"2","key":"10231_CR14","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D Kozen","year":"1994","unstructured":"Kozen, D.: A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events. Inf. Comput. 110(2), 366\u2013390 (1994)","journal-title":"Inf. Comput."},{"issue":"7","key":"10231_CR15","first-page":"337","volume":"12","author":"KW Wagner","year":"1976","unstructured":"Wagner, K.W.: Eine Axiomatisierung der Theorie der regul\u00e4ren Folgenmengen. J. Inf. Process. Cybern. 12(7), 337\u2013354 (1976)","journal-title":"J. Inf. Process. Cybern."},{"issue":"4","key":"10231_CR16","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"JA Brzozowski","year":"1964","unstructured":"Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481\u2013494 (1964)","journal-title":"J. ACM"},{"issue":"3","key":"10231_CR17","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1142\/S0129054105003157","volume":"16","author":"B Krawetz","year":"2005","unstructured":"Krawetz, B., Lawrence, J., Shallit, J.O.: State complexity and the monoid of transformations of a finite set. Int. J. Found. Comput. Sci. 16(3), 547\u2013563 (2005)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"10231_CR18","doi-asserted-by":"crossref","unstructured":"Kapp\u00e9, T., Brunet, P., Silva, A., Zanasi, F.: Concurrent Kleene algebra: Free model and completeness. In: Ahmed, A. (ed.) Proceedings of the 27th European symposium on programming, ESOP 2018. Lecture Notes in Computer Science, vol. 10801, pp. 856\u2013882. Springer, Cham (2018)","DOI":"10.1007\/978-3-319-89884-1_30"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-025-10231-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00224-025-10231-0","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-025-10231-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T11:28:46Z","timestamp":1774956526000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00224-025-10231-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,31]]},"references-count":18,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,6]]}},"alternative-id":["10231"],"URL":"https:\/\/doi.org\/10.1007\/s00224-025-10231-0","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,31]]},"assertion":[{"value":"30 June 2025","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 March 2026","order":2,"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 no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"19"}}