A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity
Clemens Grabmayer, Wan J. Fokkink · 2020
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.