Structure-Constrained Process Graphs for the Process Semantics of Regular Expressions

TL;DR

This paper refines the process semantics of regular expressions to produce process graphs with structural properties, enabling better representation and reasoning about expressible graphs in process algebra.

Contribution

It introduces a refined process semantics with 1-transitions to ensure process graphs satisfy the LEE property for a broader class of regular expressions.

Findings

Process graphs with 1-transitions satisfy LEE.

Not all regular expressions' process graphs satisfy LEE.

Refined semantics enable structural reasoning about expressible graphs.

Abstract

Milner (1984) introduced a process semantics for regular expressions as process graphs. Unlike for the language semantics, where every regular (that is, DFA-accepted) language is the interpretation of some regular expression, there are finite process graphs that are not bisimilar to the process interpretation of any regular expression. For reasoning about graphs that are expressible by regular expressions modulo bisimilarity it is desirable to have structural representations of process graphs in the image of the interpretation. For '1-free' regular expressions, their process interpretations satisfy the structural property LEE (loop existence and elimination). But this is not in general the case for all regular expressions, as we show by examples. Yet as a remedy, we describe the possibility to recover the property LEE for a close variant of the process interpretation. For this purpose we refine the process semantics of regular expressions to yield process graphs with 1-transitions, similar to silent moves for finite-state automata.