Viðburðir eftir árum

Joint ICE-TCS and GSSI virtual seminars: Clemens Grabmayer (GSSI)

A Complete Proof System for 1-Free Regular Expressions modulo Bisimilarity

  • 12.6.2020, 13:30 - 14:30


---- Joint ICE-TCS@Reykjavik University/GSSI virtual seminars

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:



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.

Vinsamlegast athugið að á viðburðum Háskólans í Reykjavík (HR) eru teknar ljósmyndir og myndbönd sem notuð eru í markaðsstarfi HR. Hægt er að nálgast frekari upplýsingar á eða með því að senda tölvupóst á netfangið:
Please note that at events hosted at Reykjavik University (RU), photographs and videos are taken which might be used for RU marketing purposes. Read more about this on our or send an e-mail: