Allan van Hulst: Completeness of Axioms for the Kleene Star under Bisimulation Equivalence: Some Progress

Event Details

Robin Milner proposed a set of axioms for the Kleene star to capture bisimulation equivalence. It is an open question whether this (or any other) set of axioms is complete. I would like to take this opportunity to report on some progress which has been made regarding this problem: 1) It is sufficient to rewrite terms under bisimulation to solve this problem, 2) I have proved completeness for all cases where the star nesting depth is limited to two. In particular, the first result shows that the difficulty of this problem does not lie in deriving axiomatic equality, but in finding the correct normal form under bisimilarity.