Joint ICE-TCS and GSSI virtual seminars: Clemens Grabmayer (GSSI)
A Complete Proof System for 1-Free Regular Expressions modulo Bisimilarity
---- Joint ICE-TCS@Reykjavik
Date and time: 12 June 2020, 13:30 GMT/14:30 BST/15:30 Italian time
Title: A Complete Proof System for 1-Free Regular Expressions modulo Bisimilarity
Speaker: Clemens Grabmayer (GSSI) WWW: https://www.gssi.it/
 |
I am a postdoc in the Computer Science group of the Gran Sasso Science Institute since November 2018. Previously I was postdoc (webpage) at the Computer... |
Abstract: My talk concerns a conference paper with the same title that I wrote together with Wan Fokkink (VU Amsterdam). Robin Milner (1984) formulated a process semantics for regular expressions that refines the standard language semantics. Adapting a proof system for language equivalence by Salomaa, Milner then formulated 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. Noting that Salomaa's proof cannot be adapted easily, he put completeness as a research question. Our paper provides a partial positive answer to this problem that substantially extends the known partial results for when the constant 1 is absent. We prove that the adaptation of Milner’s system to the subclass of regular expressions that arises by dropping 1, and by changing from unary to binary Kleene star iteration is complete. As a crucial tool, we use 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.
