TY - GEN

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

AU - Grabmayer, Clemens

AU - Fokkink, Wan

PY - 2020/7

Y1 - 2020/7

N2 - 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 that is preserved when going over from a process graph to its bisimulation collapse.

AB - 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 that is preserved when going over from a process graph to its bisimulation collapse.

KW - bisimilarity

KW - complete proof system

KW - process algebra

KW - process graphs

KW - regular expressions

UR - http://www.scopus.com/inward/record.url?scp=85085911756&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85085911756&partnerID=8YFLogxK

U2 - 10.1145/3373718.3394744

DO - 10.1145/3373718.3394744

M3 - Conference contribution

AN - SCOPUS:85085911756

T3 - ACM International Conference Proceeding Series

SP - 465

EP - 478

BT - LICS'20

PB - Association for Computing Machinery

T2 - 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020

Y2 - 8 July 2020 through 11 July 2020

ER -