Image Reflection on Process Graphs -- A Novel Approach for the Completeness of an Axiomatization of 1-Free Regular Expressions Modulo Bisimilarity
Yuanrui Zhang, Xinxin Liu
TL;DR
This work targets the completeness problem for the BBP proof system applied to 1-free regular expressions modulo bisimulation. It introduces image reflection on LLEE charts, along with the notions of images and well-structured pre-images, to show that the bisimulation collapse $\mathcal{H}$ of any LLEE chart $\mathcal{G}$ inherits an $LEE/LLEE$ structure without performing graph transformations. The key theorem demonstrates that $\mathcal{H}$ is an $LEE$ chart by analyzing how images reflect the looping-back structure of well-structured pre-images, thereby yielding a new, transformation-free route to completeness. This approach provides a novel angle on the minimization strategy for proving equality of provable solutions and suggests potential simplifications for the completeness proofs in related systems, including Milner's axiomatisation for regular expressions modulo bisimulation. The results offer a conceptual shift toward loop-centric reasoning and may inform future extensions to more general forms of regular expressions and their axiomatizations.
Abstract
We analyze a phenomenon called ``image reflection'' on a type of characterization graphs -- LLEE charts -- of 1-free regular expressions. Due to the correspondence between 1-free regular expressions and the provable solutions of LEE/LLEE charts, this observation naturally leads to a new proof for the completeness of the proof system \MilIfree\ for 1-free regular expressions modulo bisimulation equivalence. The critical part of the previous proof is to show that bisimulation collapse, which plays the role in linking the provable solutions of two LLEE charts, is still an LLEE chart. The difference of our proof, compared to the previous one, is that we do not rely on the graph transformations from LLEE charts into their bisimulation collapses by merging two carefully-selected bisimilar nodes in each transformation step. Instead, we directly show that the bisimulation collapse of an LLEE chart possesses an LEE/LLEE structure based on its set of images mapped through the bisimulation function from the LLEE chart, and the constrained relation between the images and their so-called ``well-structured'' looping-back charts pre-images on the LLEE chart. Our approach provides a novel angle to look at this problem and related problems, and can also be used for simplifying the graph transformations in the proof of the completeness problem of the proof system \Mil\ for regular expressions modulo bisimulation equivalence, which had remained open until very recently.