{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T00:05:18Z","timestamp":1759017918576,"version":"3.44.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032060846","type":"print"},{"value":"9783032060853","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"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":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\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>-regular languages are a natural extension of the regular languages to the setting of infinite words. Likewise, they are recognised by a host of automata models, one of the most important being Alternating Parity Automata (APAs), a generalisation of B\u00fcchi automata that symmetrises both the transitions (with universal as well as existential branching) and the acceptance condition (by a parity condition).<\/jats:p>\n          <jats:p>In this work, we develop a cyclic proof system manipulating APAs, represented by an algebraic notation of Right Linear Lattice expressions. This syntax dualises that of previously introduced Right Linear Algebras, which comprised a notation for non-deterministic finite automata. Our main result is the soundness and completeness of our system for <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>-language inclusion, heavily exploiting game-theoretic techniques from the theory of <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>-regular languages.<\/jats:p>","DOI":"10.1007\/978-3-032-06085-3_24","type":"book-chapter","created":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:18Z","timestamp":1758969918000},"page":"453-472","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Cyclic System for\u00a0an\u00a0Algebraic Theory of\u00a0Alternating Parity Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0142-3676","authenticated-orcid":false,"given":"Anupam","family":"Das","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-0402-0391","authenticated-orcid":false,"given":"Abhishek","family":"De","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"24_CR1","doi-asserted-by":"publisher","unstructured":"Andr\u00e9ka, H., Mikul\u00e1s, S., N\u00e9meti, I.: The equational theory of Kleene lattices. Theoret. Comput. Sci. 412(52), 7099\u20137108 (2011). https:\/\/doi.org\/10.1016\/j.tcs.2011.09.024. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397511008000","DOI":"10.1016\/j.tcs.2011.09.024"},{"issue":"4","key":"24_CR2","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1051\/ita\/1990240404191","volume":"24","author":"M Boffa","year":"1990","unstructured":"Boffa, M.: Une remarque sur les syst\u00e8mes complets d\u2019identit\u00e9s rationnelles. Theor. Inform. Appl. 24(4), 419\u2013423 (1990)","journal-title":"Theor. Inform. Appl."},{"issue":"6","key":"24_CR3","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1051\/ita\/1995290605151","volume":"29","author":"M Boffa","year":"1995","unstructured":"Boffa, M.: Une condition impliquant toutes les identit\u00e9s rationnelles. Theor. Inform. Appl. 29(6), 515\u2013518 (1995)","journal-title":"Theor. Inform. Appl."},{"key":"24_CR4","unstructured":"Boja\u0144czyk, M.: Automata, logic and games (2023), lecture course at University of Warsaw. https:\/\/www.mimuw.edu.pl\/~bojan\/2022-2023\/automata-logic-and-games-2023"},{"key":"24_CR5","doi-asserted-by":"publisher","unstructured":"Bruse, F., Friedmann, O., Lange, M.: On guarded transformation in the modal $$\\mu $$-calculus. Log. J. IGPL 23(2), 194\u2013216 (2015). https:\/\/doi.org\/10.1093\/JIGPAL\/JZU030. https:\/\/doi.org\/10.1093\/jigpal\/jzu030","DOI":"10.1093\/JIGPAL\/JZU030"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Buchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295\u2013311 (1969). http:\/\/www.jstor.org\/stable\/1994916","DOI":"10.1090\/S0002-9947-1969-0280205-0"},{"key":"24_CR7","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/10722010_4","volume-title":"Mathematics of Program Construction","author":"E Cohen","year":"2000","unstructured":"Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) Mathematics of Program Construction, pp. 45\u201359. Springer, Heidelberg (2000)"},{"key":"24_CR8","doi-asserted-by":"publisher","unstructured":"Cranch, J., Laurence, M.R., Struth, G.: Completeness results for omega-regular algebras. J. Log. Algebraic Methods Program. 84(3), 402\u2013425 (2015). https:\/\/doi.org\/10.1016\/J.JLAMP.2014.10.002","DOI":"10.1016\/J.JLAMP.2014.10.002"},{"key":"24_CR9","doi-asserted-by":"publisher","unstructured":"Das, A., De, A.: A proof theory of right-linear ($$\\omega $$-)grammars via cyclic proofs. In: Sobocinski, P., Lago, U.D., Esparza, J. (eds.) Proceedings of the 39th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, 8\u201311 July 2024, pp. 30:1\u201330:14. ACM (2024). https:\/\/doi.org\/10.1145\/3661814.3662138","DOI":"10.1145\/3661814.3662138"},{"key":"24_CR10","doi-asserted-by":"publisher","unstructured":"Das, A., De, A.: A proof theory of right-linear (omega-)grammars via cyclic proofs (2024). https:\/\/doi.org\/10.48550\/ARXIV.2401.13382","DOI":"10.48550\/ARXIV.2401.13382"},{"key":"24_CR11","unstructured":"Das, A., De, A.: An algebraic theory of $$\\omega $$-regular languages, via $$\\mu \\nu $$-expressions (2025). https:\/\/arxiv.org\/abs\/2505.10303"},{"key":"24_CR12","unstructured":"Das, A., De, A.: Cyclic system for an algebraic theory of alternating parity automata (2025). https:\/\/arxiv.org\/abs\/2505.09000"},{"key":"24_CR13","doi-asserted-by":"publisher","unstructured":"Das, A., De, A., Saurin, A.: Decision problems for linear logic with least and greatest fixed points. In: Felty, A.P. (ed.) 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0228, pp. 20:1\u201320:20. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2022.20. https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.FSCD.2022.20","DOI":"10.4230\/LIPIcs.FSCD.2022.20"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-66902-1_16","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A Das","year":"2017","unstructured":"Das, A., Pous, D.: A cut-free cyclic proof system for Kleene algebra. In: Schmidt, R.A., Nalon, C. (eds.) TABLEAUX 2017. LNCS (LNAI), vol. 10501, pp. 261\u2013277. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66902-1_16"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/11944836_26","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"C Dax","year":"2006","unstructured":"Dax, C., Hofmann, M., Lange, M.: A proof system for the linear time $$\\mu $$-calculus. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 273\u2013284. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11944836_26"},{"key":"24_CR16","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-031-43513-3_14","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M Dekker","year":"2023","unstructured":"Dekker, M., Kloibhofer, J., Marti, J., Venema, Y.: Proof systems for the modal $$\\mu $$-calculus obtained by determinizing automata. In: Ramanayake, R., Urban, J. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods, pp. 242\u2013259. Springer, Cham (2023)"},{"key":"24_CR17","doi-asserted-by":"publisher","unstructured":"Doumane, A.: Constructive completeness for the linear-time $$\\mu $$-calculus. In: 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, 20\u201323 June 2017, pp. 1\u201312. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005075","DOI":"10.1109\/LICS.2017.8005075"},{"key":"24_CR18","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer Aided Verification, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"24_CR19","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-0-387-34892-6_1","volume-title":"Protocol Specification, Testing and Verification XV","author":"R Gerth","year":"1996","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV 1995. IAICT, pp. 3\u201318. Springer, Boston, MA (1996). https:\/\/doi.org\/10.1007\/978-0-387-34892-6_1"},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. Lecture Notes in Computer Science, 2002 edn. Springer, New York (2003)","DOI":"10.1007\/3-540-36387-4"},{"key":"24_CR21","doi-asserted-by":"publisher","unstructured":"Hazard, E., Kuperberg, D.: Cyclic proofs for transfinite expressions. In: Manea, F., Simpson, A. (eds.) 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, G\u00f6ttingen, Germany, 14\u201319 February 2022 (Virtual Conference). LIPIcs, vol.\u00a0216, pp. 23:1\u201323:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.CSL.2022.23","DOI":"10.4230\/LIPICS.CSL.2022.23"},{"key":"24_CR22","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional (2011)"},{"key":"24_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-60218-6_32","volume-title":"CONCUR \u201995: Concurrency Theory","author":"R Kaivola","year":"1995","unstructured":"Kaivola, R.: Axiomatising linear time $$\\mu $$-calculus. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 423\u2013437. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60218-6_32"},{"key":"24_CR24","doi-asserted-by":"publisher","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110(2), 366\u2013390 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1037. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540184710376","DOI":"10.1006\/inco.1994.1037"},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"Kozen, D.: On Action Algebras, pp. 78\u201388. MIT Press, Cambridge (1994)","DOI":"10.7551\/mitpress\/4286.003.0007"},{"key":"24_CR26","doi-asserted-by":"publisher","unstructured":"Krob, D.: Complete systems of b-rational identities. Theoret. Comput. Sci. 89(2), 207\u2013343 (1991). https:\/\/doi.org\/10.1016\/0304-3975(91)90395-I. https:\/\/www.sciencedirect.com\/science\/article\/pii\/030439759190395I","DOI":"10.1016\/0304-3975(91)90395-I"},{"key":"24_CR27","doi-asserted-by":"publisher","unstructured":"Kupke, C., Marti, J., Venema, Y.: Succinct graph representations of $$\\mu $$-calculus formulas. In: Manea, F., Simpson, A. (eds.) 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0216, pp. 29:1\u201329:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2022.29. https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.CSL.2022.29","DOI":"10.4230\/LIPIcs.CSL.2022.29"},{"key":"24_CR28","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-540-30579-8_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Lange","year":"2005","unstructured":"Lange, M.: Weak automata for the linear time $$\\mu $$-calculus. In: Cousot, R. (ed.) Verification, Model Checking, and Abstract Interpretation, pp. 267\u2013281. Springer, Heidelberg (2005)"},{"key":"24_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-33314-9_12","volume-title":"Relational and Algebraic Methods in Computer Science","author":"MR Laurence","year":"2012","unstructured":"Laurence, M.R., Struth, G.: On completeness of omega-regular algebras. In: Kahl, W., Griffin, T.G. (eds.) RAMICS 2012. LNCS, vol. 7560, pp. 179\u2013194. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33314-9_12"},{"key":"24_CR30","doi-asserted-by":"publisher","unstructured":"Niwinski, D., Walukiewicz, I.: Games for the $$\\mu $$-calculus. Theor. Comput. Sci. 163(1 &2), 99\u2013116 (1996). https:\/\/doi.org\/10.1016\/0304-3975(95)00136-0","DOI":"10.1016\/0304-3975(95)00136-0"},{"key":"24_CR31","unstructured":"Perrin, D., Pin, J.: Infinite Words - Automata, Semigroups, Logic and Games, Pure and Applied Mathematics Series, vol.\u00a0141. Elsevier Morgan Kaufmann (2004)"},{"key":"24_CR32","doi-asserted-by":"publisher","unstructured":"Pous, D.: On the positive calculus of relations with transitive closure. In: Niedermeier, R., Vall\u00e9e, B. (eds.) 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a096, pp. 3:1\u20133:16. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2018). https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2018.3. https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.STACS.2018.3","DOI":"10.4230\/LIPIcs.STACS.2018.3"},{"issue":"5","key":"24_CR33","doi-asserted-by":"publisher","first-page":"1025","DOI":"10.1090\/S0002-9904-1968-12122-6","volume":"74","author":"MO Rabin","year":"1968","unstructured":"Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Bull. Am. Math. Soc. 74(5), 1025\u20131029 (1968)","journal-title":"Bull. Am. Math. Soc."},{"key":"24_CR34","doi-asserted-by":"publisher","unstructured":"Richard B\u00fcchi, J.: On a decision method in restricted second order arithmetic. In: Nagel, E., Suppes, P., Tarski, A. (eds.) Logic, Methodology and Philosophy of Science, Studies in Logic and the Foundations of Mathematics, vol.\u00a044, pp. 1\u201311. Elsevier (1966). https:\/\/doi.org\/10.1016\/S0049-237X(09)70564-6. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0049237X09705646","DOI":"10.1016\/S0049-237X(09)70564-6"},{"issue":"1","key":"24_CR35","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1145\/321312.321326","volume":"13","author":"A Salomaa","year":"1966","unstructured":"Salomaa, A.: Two complete axiom systems for the algebra of regular events. J. ACM (JACM) 13(1), 158\u2013169 (1966)","journal-title":"J. ACM (JACM)"},{"key":"24_CR36","doi-asserted-by":"publisher","unstructured":"Streett, R.S., Emerson, E.A.: An automata theoretic decision procedure for the propositional $$\\mu $$-calculus. Inf. Comput. 81(3), 249\u2013264 (1989). https:\/\/doi.org\/10.1016\/0890-5401(89)90031-X","DOI":"10.1016\/0890-5401(89)90031-X"},{"key":"24_CR37","doi-asserted-by":"publisher","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994). https:\/\/doi.org\/10.1006\/inco.1994.1092. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540184710923","DOI":"10.1006\/inco.1994.1092"},{"key":"24_CR38","unstructured":"Wagner, K.W.: Eine axiomatisierung der theorie der regul\u00e4ren folgenmengen. J. Inf. Process. Cybern. 12, 337\u2013354 (1976). https:\/\/api.semanticscholar.org\/CorpusID:27249080"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-06085-3_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:21Z","timestamp":1758969921000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06085-3_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032060846","9783032060853"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06085-3_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,25]]},"assertion":[{"value":"25 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/tableaux\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}