# A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity

arXiv: https://arxiv.org/abs/2004.12740 · HTML: https://mlsanity.com/paper/2004.12740/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 Apr 2020.

## Built on by (most cited first, 1 of 1)

- [The Image of the Process Interpretation of Regular Expressions is Not Closed under Bisimulation Collapse](https://mlsanity.com/paper/2303.08553/) (2023)

## Abstract (arXiv)

Robin Milner (1984) gave a sound proof system for bisimilarity of regular expressions interpreted as processes: Basic Process Algebra with unary Kleene star iteration, deadlock 0, successful termination 1, and a fixed-point rule. He asked whether this system is complete. Despite intensive research over the last 35 years, the problem is still open. This paper gives a partial positive answer to Milner's problem. We prove that the adaptation of Milner's system over the subclass of regular expressions that arises by dropping the constant 1, and by changing to binary Kleene star iteration is complete. The crucial tool we use is a graph structure property that guarantees expressibility of a process graph by a regular expression, and is preserved by going over from a process graph to its bisimulation collapse.