{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:14Z","timestamp":1753894394874,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Milner (1984) defined an operational semantics for regular expressions as\nfinite-state processes. In order to axiomatize bisimilarity of regular\nexpressions under this process semantics, he adapted Salomaa's proof system\nthat is complete for equality of regular expressions under the language\nsemantics. Apart from most equational axioms, Milner's system Mil inherits from\nSalomaa's system a non-algebraic rule for solving single fixed-point equations.\nRecognizing distinctive properties of the process semantics that render\nSalomaa's proof strategy inapplicable, Milner posed completeness of the system\nMil as an open question.\n  As a proof-theoretic approach to this problem we characterize the\nderivational power that the fixed-point rule adds to the purely equational part\nMil$^-$ of Mil. We do so by means of a coinductive rule that permits cyclic\nderivations that consist of a finite process graph with empty steps that\nsatisfies the layered loop existence and elimination property LLEE, and two of\nits Mil$^{-}$-provable solutions. With this rule as replacement for the\nfixed-point rule in Mil, we define the coinductive reformulation cMil as an\nextension of Mil$^{-}$. In order to show that cMil and Mil are theorem\nequivalent we develop effective proof transformations from Mil to cMil, and\nvice versa. Since it is located half-way in between bisimulations and proofs in\nMilner's system Mil, cMil may become a beachhead for a completeness proof of\nMil.\n  This article extends our contribution to the CALCO 2022 proceedings. Here we\nrefine the proof transformations by framing them as eliminations of derivable\nand admissible rules, and we link coinductive proofs to a coalgebraic\nformulation of solutions of process graphs.<\/jats:p>","DOI":"10.46298\/lmcs-19(2:17)2023","type":"journal-article","created":{"date-parts":[[2023,6,29]],"date-time":"2023-06-29T12:40:20Z","timestamp":1688042420000},"source":"Crossref","is-referenced-by-count":1,"title":["A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity"],"prefix":"10.46298","volume":"Volume 19, Issue 2","author":[{"given":"Clemens","family":"Grabmayer","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2023,6,29]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/11519\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/11519\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,29]],"date-time":"2023-06-29T12:40:21Z","timestamp":1688042421000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/9244"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,29]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-19(2:17)2023","relation":{"has-preprint":[{"id-type":"arxiv","id":"2203.09501v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2203.09501v2","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2203.09501","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2203.09501","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2023,6,29]]},"article-number":"9244"}}