Document Open Access Logo

A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity

Author Clemens Grabmayer



PDF
Thumbnail PDF

File

LIPIcs.CALCO.2021.16.pdf
  • Filesize: 0.85 MB
  • 23 pages

Document Identifiers

Author Details

Clemens Grabmayer
  • Gran Sasso Science Institute, L'Aquila, Italy

Acknowledgements

I want to thank Luca Aceto for his comments on the introduction. I am also very grateful to the anonymous reviewers for their careful reading, for spotting distracting oversights, and for asking for additional clarifications, such as concerning the motivation of coinductive proofs.

Cite AsGet BibTex

Clemens Grabmayer. A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 16:1-16:23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CALCO.2021.16

Abstract

By adapting Salomaa’s complete proof system for equality of regular expressions under the language semantics, Milner (1984) formulated a sound proof system for bisimilarity of regular expressions under the process interpretation he introduced. He asked whether this system is complete. Proof-theoretic arguments attempting to show completeness of this equational system are complicated by the presence of a non-algebraic rule for solving fixed-point equations by using star iteration. We characterize the derivational power that the fixed-point rule adds to the purely equational part Mil- of Milner’s system Mil: it corresponds to the power of coinductive proofs over Mil- that have the form of finite process graphs with the loop existence and elimination property LEE. We define a variant system cMil by replacing the fixed-point rule in Mil with a rule that permits LEE-shaped circular derivations in Mil- from previously derived equations as a premise. With this rule alone we also define the variant system CLC for combining LEE-shaped coinductive proofs over Mil-. We show that both cMil and CLC have proof interpretations in Mil, and vice versa. As this correspondence links, in both directions, derivability in Mil with derivation trees of process graphs, it widens the space for graph-based approaches to finding a completeness proof of Milner’s system.

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
Keywords
  • regular expressions
  • process theory
  • bisimilarity
  • coinduction
  • proof theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Roberto M. Amadio and Luca Cardelli. Subtyping Recursive Types. ACM Trans. Program. Lang. Syst., 15(4):575-631, September 1993. URL: https://doi.org/10.1145/155183.155231.
  2. Valentin Antimirov. Partial Derivatives of Regular Expressions and Finite Automaton Constructions. Theoretical Computer Science, 155(2):291-319, 1996. URL: https://doi.org/10.1016/0304-3975(95)00182-4.
  3. Michael Brandt and Fritz Henglein. Coinductive Axiomatization of Recursive Type Equality and Subtyping. Fundamenta Informaticae, 33(4):309-338, December 1998. URL: https://doi.org/10.1007/3-540-62688-3_29.
  4. Clemens Grabmayer. Relating Proof Systems for Recursive Types. PhD thesis, Vrije Universiteit Amsterdam, March 2005. URL: http://www.phil.uu.nl/~clemens/linkedfiles/proefschrift.pdf.
  5. Clemens Grabmayer. Using Proofs by Coinduction to Find "Traditional" Proofs. In José Luiz Fiadeiro, Neal Harman, Markus Roggenbach, and Jan Rutten, editors, Proceedings of CALCO 2005, volume 3629 of LNCS, pages 175-193. Springer, 2005. Google Scholar
  6. Clemens Grabmayer. A Coinductive Axiomatisation of Regular Expressions under Bisimulation. Technical report, University of Nottingham, 2006. Short Contribution to CMCS 2006, March 25-27, 2006, Vienna Institute of Technology, Austria. Google Scholar
  7. Clemens Grabmayer. Modeling Terms by Graphs with Structure Constraints (Two Illustrations). In Proc. TERMGRAPH@FSCD'18, volume 288, pages 1-13, http://www.eptcs.org/, 2019. EPTCS. URL: https://doi.org/10.4204/EPTCS.288.1.
  8. Clemens Grabmayer. Structure-Constrained Process Graphs for the Process Semantics of Regular Expressions. Technical report, http://arxiv.org, December 2020. URL: http://arxiv.org/abs/2012.10869.
  9. Clemens Grabmayer. A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity. Technical report, http://arxiv.org, August 2021. Extended version of this paper. URL: http://arxiv.org/abs/2108.13104.
  10. Clemens Grabmayer. Structure-Constrained Process Graphs for the Process Semantics of Regular Expressions. In Patrick Bahr, editor, Proceedings 11th International Workshop on Computing with Terms and Graphs, Online, 5th July 2020, volume 334 of Electronic Proceedings in Theoretical Computer Science, pages 29-45. Open Publishing Association, 2021. URL: https://doi.org/10.4204/EPTCS.334.3.
  11. Clemens Grabmayer and Wan Fokkink. A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity. In Proceedings of LICS 2020, New York, NY, 2020. ACM. Extended report see [Clemens Grabmayer and Wan Fokkink, 2020]. Google Scholar
  12. Clemens Grabmayer and Wan Fokkink. A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity. Technical report, http://arxiv.org, April 2020. URL: http://arxiv.org/abs/2004.12740.
  13. Robin Milner. A Complete Inference System for a Class of Regular Behaviours. Journal of Computer and System Sciences, 28(3):439-466, 1984. Google Scholar
  14. Arto Salomaa. Two Complete Axiom Systems for the Algebra of Regular Events. Journal of the ACM, 13(1):158-169, 1966. URL: https://doi.org/10.1145/321312.321326.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail