A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity

DOI10.46298/LMCS-19(2:17)2023arXiv2203.09501MaRDI QIDQ6135767FDOQ6135767

Authors: Clemens Grabmayer 

Publication date: 26 August 2023

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/2203.09501

zbMATH Keywords

coinductionregular expressionsbisimilarityprocess theoryproof transformationsderivable and admissible inference rulesinterpretational proof theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Title not available (Why is that?)
• Depth-First Search and Linear Graph Algorithms
• Partial derivatives of regular expressions and finite automaton constructions
• Title not available (Why is that?)
• Two Complete Axiom Systems for the Algebra of Regular Events
• Title not available (Why is that?)
• Title not available (Why is that?)
• A complete inference system for a class of regular behaviours
• Regular expression containment
• Algebra and Coalgebra in Computer Science
• A duality in proof systems for recursive type equality and for bisimulation equivalence on cyclic term graphs
• Title not available (Why is that?)
• Actions speak louder than words: proving bisimilarity for context-free processes
• A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity
• Title not available (Why is that?)
• Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
• A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity
• Title not available (Why is that?)

Cited In (4)

• Title not available (Why is that?)
• A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity
• 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)