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

Clemens Grabmayer, Wan Fokkink

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

17 Downloads (Pure)

Abstract

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.

Original languageEnglish
Title of host publicationLICS'20
Subtitle of host publicationProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science
PublisherAssociation for Computing Machinery
Pages465-478
Number of pages14
ISBN (Electronic)9781450371049
DOIs
Publication statusPublished - Jul 2020
Event35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 - Saarbrucken, Germany
Duration: 8 Jul 202011 Jul 2020

Publication series

NameACM International Conference Proceeding Series

Conference

Conference35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
CountryGermany
CitySaarbrucken
Period8/07/2011/07/20

Keywords

  • bisimilarity
  • complete proof system
  • process algebra
  • process graphs
  • regular expressions

Fingerprint Dive into the research topics of 'A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity'. Together they form a unique fingerprint.

Cite this