Title: On the Completeness of Axioms for the Kleene Star under Bisimilarity Equivalence /
Über die Vollständigkeit von Axiomen für die Kleenesche Hüllenoperator unter Bisimularitäts-Äquivalenz

Abstract: Milner conjectured in 1984 that a finite and complete axiomatization exists 
for the Kleene star under bisimilarity equivalence. This problem remains as of yet 
unsolved and Milner himself hypothesized that solving this problem may involve a 
significant effort. Essentially, this problem states that if two regular expressions 
can be related in such a way that they can always replicate each other's actions, they 
can also be shown to be equal axiomatically. I would like to explain how I transformed 
this problem into a normalization question under bisimilarity using strong induction 
towards the star nesting depth and the axiom RSP. This implies that the structure of 
the derivation tree of axiom applications is now clear. Discrete optimization or other 
methodologies of combinatorial nature may help in resolving the normalization question. 
This talk will be set up to invite suggestions from the attendees who may be able to 
relate patterns in this partial proof to their own ideas or insights.