A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity
From MaRDI portal
Publication:6135767
Abstract: Milner (1984) defined an operational semantics for regular expressions as finite-state processes. In order to axiomatize bisimilarity of regular expressions under this process semantics, he adapted Salomaa's proof system that is complete for equality of regular expressions under the language semantics. Apart from most equational axioms, Milner's system Mil inherits from Salomaa's system a non-algebraic rule for solving single fixed-point equations. Recognizing distinctive properties of the process semantics that render Salomaa's proof strategy inapplicable, Milner posed completeness of the system Mil as an open question. As a proof-theoretic approach to this problem we characterize the derivational power that the fixed-point rule adds to the purely equational part Mil of Mil. We do so by means of a coinductive rule that permits cyclic derivations that consist of a finite process graph with empty steps that satisfies the layered loop existence and elimination property LLEE, and two of its Mil-provable solutions. With this rule as replacement for the fixed-point rule in Mil, we define the coinductive reformulation cMil as an extension of Mil. In order to show that cMil and Mil are theorem equivalent we develop effective proof transformations from Mil to cMil, and vice versa. Since it is located half-way in between bisimulations and proofs in Milner's system Mil, cMil may become a beachhead for a completeness proof of Mil. This article extends our contribution to the CALCO 2022 proceedings. Here we refine the proof transformations by framing them as eliminations of derivable and admissible rules, and we link coinductive proofs to a coalgebraic formulation of solutions of process graphs.
Cites work
- scientific article; zbMATH DE number 1183236 (Why is no real title available?)
- scientific article; zbMATH DE number 1304993 (Why is no real title available?)
- scientific article; zbMATH DE number 1064116 (Why is no real title available?)
- scientific article; zbMATH DE number 919844 (Why is no real title available?)
- scientific article; zbMATH DE number 7456061 (Why is no real title available?)
- scientific article; zbMATH DE number 3248792 (Why is no real title available?)
- scientific article; zbMATH DE number 7774242 (Why is no real title available?)
- A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity
- A complete inference system for a class of regular behaviours
- A complete proof system for 1-free regular expressions modulo bisimilarity
- A duality in proof systems for recursive type equality and for bisimulation equivalence on cyclic term graphs
- Actions speak louder than words: proving bisimilarity for context-free processes
- Algebra and Coalgebra in Computer Science
- Depth-First Search and Linear Graph Algorithms
- Partial derivatives of regular expressions and finite automaton constructions
- Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
- Regular expression containment, coinductive axiomatization and computational interpretation
- Two Complete Axiom Systems for the Algebra of Regular Events
Cited in
(4)- A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity
- scientific article; zbMATH DE number 7315073 (Why is no real title available?)
- Better automata through process algebra
- Milner's proof system for regular expressions modulo bisimilarity is complete. Crystallization: near-collapsing process graph interpretations of regular expressions
This page was built for publication: A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6135767)
