Structure-Constrained Process Graphs
for the Process Semantics of Regular Expressions
Clemens Grabmayer
Gran Sasso Science Institute
Viale F. Crispi, 7, 67100 L’Aquila AQ, Italy
clemens.grabmayer@gssi.it

Milner (1984) introduced a process semantics for regular expressions as process graphs. Unlike forthe language semantics, where every regular (that is, DFA-accepted) language is the interpretation ofsome 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 a regular expression
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 always the case for general regular expressions, as weshow 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.

1

Introduction

Milner [7] (1984) defined a process semantics for regular expressions as process graphs: the interpretationof 0 is deadlock, of 1 is successful termination, letters a are atomic actions, the operators + and · stand for
choice and concatenation of processes, and (unary) Kleene star (·)∗ represents iteration with the option
to terminate successfully after each pass-through. In order to disambiguate the use of regular expressions
for denoting processes, Milner called them ‘star expressions’ in this context. Unlike for the standard language semantics, where every regular language is the interpretation of some regular expression, there are
finite process graphs that are not bisimilar to the process interpretation of any star expression.1 This phenomenon led Milner to the formulation of two natural questions: (R) the problem of recognizing whether
a given process graph is bisimilar to one in the image of the process interpretation of a star expression,and (A) whether a natural adaptation of Salomaa’s complete proof system for language equivalence ofregular expressions is complete for bisimilarity of the process interpretation of star expressions. While(R) has been shown to be decidable in principle, so far only partial solutions have been obtained for (A).
For tackling these problems it is expedient to obtain structural representations of process graphs in
the image of the interpretation. The result of Baeten, Corradini, and myself [1] that the problem (R) is
decidable (but not yet efficiently so) was based on the concept of ‘well-behaved (recursive) specifications’ that links process graphs with star expressions. Recently in [4, 5], Wan Fokkink and I obtained apartial solution for (A) in the form of a complete proof system for ‘1-free’ star expressions, which do notcontain 1, but are formed with binary Kleene star iteration (·) ~(·) instead of unary iteration. For this, wedefined the efficiently decidable ‘loop existence and elimination property (LEE)’ of process graphs that
holds for all process graph interpretations of 1-free star expressions, and for their bisimulation collapses.
The property LEE does unfortunately not hold for process interpretations of all star expressions. But
the aim of this extended abstract is to describe how LEE can nevertheless be made applicable, by stepping
1 E.g., the process graphs C (ne) and C (ne) in Ex. 2.1 on page 3 are not expressible by a star expression modulo bisimilarity.
1
2

Preliminary Report. Final version to appear in:
TERMGRAPH 2020

c C. Grabmayer
This work is licensed under theCreative Commons Attribution License.

2

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

over to a variant of the process interpretation. In Section 3 we explain the loop existence and elimination
property LEE for process graphs by means of an example, and define the concept of a ‘layered LEE-witness’, for short a ‘LLEE-witness’ for process graphs. That section is an adaptation of Section 3 in [4]from 1-free star expressions to general star expressions. LEE -witnesses arise by adding natural-number
labels to transitions that are subject to suitable constraints. In Section 4 we explain examples that showthat LEE does not hold in general for process interpretations of star expressions from the full class. Asa remedy, in Section 5 we introduce process graphs with 1-transitions (similar to silent moves for finitestate automata), and define a variant C (·) of the process interpretation C (·) that produces such graphs.
We formulate a theorem that states that the process interpretation C (e) of a star expression e and its
variant C (e) are bisimilar. Finally, we explain how the definition of the variant process interpretation
C (·) can be refined so as to also define LLEE-witnesses. In this way we obtain that process graphs with
1-transitions in the image of C (·) satisfy LEE.
We are hopeful that the extension of the applicability of the property LEE to the full class of star
expressions can be part of a solution of problem (A), based on the partial solution in [4]. We also expectthat it can lead to an efficient decision procedure for the recognition problem (R).
The idea to define structure-constrained process graphs via edge-labelings with constraints, on which
LEE is based, originated from ‘higher-order term graphs’ that can be used for representing functional
programs in a maximally compact, shared form (see [6, 3]). There, additional concepts (scope sets ofvertices, or abstraction-prefix labelings) are used to constrain the form of term graphs. The common
underlying idea with the situation we consider here is an enrichment of graphs that: (i) guarantees thatgraphs can be directly expressed by terms of some language, (ii) does not significantly hamper sharing ofrepresented subterms, (iii) is simple enough so as to keep reasoning about graph transformations feasible.

2

Preliminaries on the process semantics of star expressions

The set StExps(A) of star expressions over (actions in) A is defined by the following grammar:e, e1 , e2 ::= 0 | 1 | a | e1 + e2 | e1 · e2 | e∗(where a ∈ A) .
The (syntactic) star height |e|∗ of a star expression e ∈ StExps(A) denotes the maximal nesting depth ofstars in e via: |0|∗ := |1|∗ := |a|∗ := 0, |e1 + e2 |∗ := |e1 · e2 |∗ := max {|e1 |∗ , |e2 |∗ }, and |e∗ |∗ := 1 + |e|∗ .
The process semantics of star expressions is defined by the transition system specification (TSS) T :
ei ↓
e1 ↓
e2 ↓
(i ∈ {1, 2})1↓(e1 + e2 )↓(e1 · e2 )↓(e∗ )↓
a

a

ei →
− e0i
a

a→
− 1
a

a

e1 + e2 →− e0i(i ∈ {1, 2})

e1 →
− e01
a

e1 · e2 →− e01 · e2

e1 ↓

a

e2 →
− e02
a

e1 · e2 →
− e02

a

e→
− e0
a
e∗ →
− e0 · e∗

If e →− e0 is derivable in T , for e, e0 ∈ StExps(A), and a ∈ A, then we say that e0 is a derivative of e. If e↓
is derivable in T , for e ∈ StExps(A), then we say that e permits immediate termination.
(·)
The TSS T defines the labeled transition system (LTS) S (StExps(A)) = hStExps(A), A, −→, ↓i with(·)
transitions −→ ⊆ StExps(A) × A × StExps(A), and immediate-termination property ↓ ⊆ StExps(A) that are
defined in a natural way via derivations in T . For every set S ⊆ StExps(A) we denote by S (S) the
S-generated sub-LTS hVS , A, TS , FS i of S (StExps(A)), that is, the sub-LTS whose objects are those in S
together with all star expressions that are reachable from ones in S via transitions of S (StExps(A)).
A chart is a (rooted) LTS (with initial state) hV, A, vs , T, Fi that consists of a finite set V of vertices,a finite set A of actions, a specified start vertex (initial state) vs ∈ V , a set T ⊆ V × A × V of labeledtransitions between vertices with action labels, and a subset F ⊆ V of vertices with immediate termination.

C. Grabmayer

3

The chart interpretation C (e) = hV(e), A, e, T (e), F(e)i of a star expression e ∈ StExps(A) is of the{e}-generated sub-LTS S ({e}) = hV{e} , A, T{e} , F{e} i of S (StExps(A)).
Let Ci = hVi , A, vs,i , Ti , Fi i for i ∈ {1, 2} be charts. By C1 ↔ C2 we denote that C1 and C2 are bisimilar,that is, that there is a bisimulation between C1 and C2 : a relation B ⊆ V1 × V2 that relates their startvertices, and whose elements hv1 , v2 i ∈ B satisfy the customary forth-, back-, and termination conditions.
By C1 → C2 we denote the statement that there is a functional bisimulation between C1 and C2 , that is,there is a function f : V1 → V2 such that its graph {hv, f (v)i | v ∈ V1 } is a bisimulation between C1 and C2 .
Example 2.1. In the chart illustrations below and later, we indicate the start vertex by a brown arrow, andthe property of a vertex v to permit immediate termination by highlighting the bullet that symbolizes v byan additional boldface ring. Each of the vertices of the charts C1(ne) and C (e) below permits immediate
termination, but none of the vertices of the other charts does so.

C2(ne)C (g0)
c

C (f)

e

f

a1

g0

a2

a

g1

C (e)

a3

a1

a

b

a
a2

a3 a

e1

e2
b

b g2 baC1(ne)
b

a1

b

a

a3

a1

a1

f1
a3

a2

a2
a2

a1

a3

f3

f2

a2

a3
b1

b2

b3

sink

The charts C1(ne) and C2(ne) are not expressible by the process interpretation modulo ↔, as shown by Bosscher [2] and Milner [7]. That C2(ne) is not expressible, Milner proved by observing the absence of a ‘loop
behaviour’. That concept has inspired the stronger concept of ‘loop chart’ in Def. 3.1 below. The weaker
result that C1(ne) and C2(ne) are not expressible by 1-free star expressions will be argued in Remark 3.3.
The chart C (g0) on the left above is the interpretation of the star expression g0 = ((1 · a) · g) · 0 whereg = (c · a + a · (b + b · a))∗ , and with g1 = (1 · g) · 0, and g2 = ((1 · (b + b · a)) · g) · 0 as remaining vertices. The chart C (e) is the interpretation of e = (a∗ · b∗ )∗ with e1 = ((1 · a∗ ) · b∗ ) · e, and e2 = (1 · b∗ ) · e.
With f0 = a1 · (1 + b1 · 0) + a2 · (1 + b2 · 0)) + a3 · (1 + b3 · 0)), the chart C ( f ) is the interpretation off = f0∗ · 0 with fi = (1 · (1 + bi · 0) · f0∗ ) · 0 (for i ∈ {1, 2, 3}), and sink = ((1 · 0) · f0∗ ) · 0. The chartinterpretations C (e) and C ( f ), which will be used later, have been constructed as expressible variants of
the not expressible charts C1(ne) and C2(ne) . In particular, C (e) contains C1(ne) as a subchart, and C ( f ) contains C2(ne) as a subchart (where a ‘subchart’ arises by taking a part of a chart, and picking a start vertex).
We finally note that all of these charts with the exception of C (e) are bisimulation collapses.

3

Loop existence and elimination

The chart translation C (g0) of g0 as in Ex. 2.1 satisfies the ‘loop existence and elimination’ property LEE
that we will explain in this section. For this purpose we summarize Section 3 in [4], and in doing so
we adapt the concepts defined there from 1-free star expressions to the full class of star expressions as
defined in Section 2. The property LEE is defined by a dynamic elimination procedure that analyses the
structure of a chart by peeling off ‘loop subcharts’. Such subcharts capture, within the chart interpretationof a star expression e, the behavior of the iteration of f within innermost subterms f ∗ in e.

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

Definition 3.1. A chart L = hV, A, vs , T, Fi is a loop chart if:(L1) There is an infinite path from the start vertex vs .
(L2) Every infinite path from vs returns to vs after a positive number of transitions (and so visits vsinfinitely often).
(L3) Immediate termination is only permitted at the start vertex, that is, F ⊆ {vs }.
We call the transitions from vs loop-entry transitions, and all other transitions loop-body transitions. A
loop chart L is a loop subchart of a chart C if it is the subchart of C rooted at some vertex v ∈ V that is
generated, for a nonempty set U of transitions of C from v, by all paths that start with a transition in U
and continue onward until v is reached again (so the transitions in U are the loop-entry transitions of L ).
Both of the not expressible charts C1(ne) and C2(ne) in Ex. 2.1 are not loop charts: C1(ne) violates (L3),and C2(ne) violates (L2). Moreover, none of these charts contains a loop subchart. The chart C (g0) in
Ex. 2.1 is not a loop chart either, as it violates (L2). But we will see that C (g0) has loop subcharts.
Let L be a loop subchart of a chart C . Then the result of eliminating L from C arises by removing all
loop-entry transitions of L from C , and then removing all vertices and transitions that become unreachable. We say that a chart C has the loop existence and elimination property (LEE) if the procedure, started
on C , of repeated eliminations of loop subcharts results in a chart that does not have an infinite path.
For the not expressible charts C1(ne) and C2(ne) in Ex. 2.1 the procedure stops immediately, as they do
not contain loop subcharts. Since both of them have infinite paths, it follows that they do not satisfy LEE.
Now we consider three runs of the elimination procedure for the chart C (g0) in Ex. 2.1. The loopentry transitions of loop subcharts that are removed in each step are marked in bold.
v0

c

v0

elim

a

v0

elim

a

v1

v0

elim

a

v1

a

a

b v2 bb v2 b

v0

c

a

v1

a

v1

elim

c

v1

v0

v0 elim v0elim
a

a

v1

v1

a

c

v1

a

a

a

a

v2 b

v2

b v2 bb v2 bEach run witnesses that C (g0) satisfies LEE. Note that loop elimination does not yield a unique result.2
Runs can be recorded, in the original chart, by attaching a marking label to transitions that get removed in
the elimination procedure. That label is the sequence number of the corresponding elimination step. For
the three runs of loop elimination above we get the following marking labeled versions of C , respectively:
c

[1]

v0
a

v1
[2]

c

[2]

v0
a

[1] c

a

a

[1] a

v1
a [1]

b v2 bb v2 bb v2 b

[3]

v1

v0

Since all three runs were successful (as they yield charts without infinite paths), these recordings (markinglabeled charts) can be viewed as ‘LEE -witnesses’. We now will define the concept of a ‘layered LEE-witness’ (LLEE-witness), i.e., a LEE-witness with the added constraint that in the recorded run of the loop
2 Confluence can be shown if a pruning operation is added that permits to drop transitions to deadlocking vertices.

C. Grabmayer

5

elimination procedure it never happens that a loop-entry transition is removed from within the body of apreviously removed loop subchart. This refined concept has simpler properties, but is equally powerful.
By an entry/body-labeling of a chart C = hV, A, vs , T, Fi we mean a chart Cb = hV, A × N, vs , Tb, Fi thatarises from C by adding, for each transition τ = hv1 , a, v2 i ∈ T , to the action label a of τ a marking label
α ∈ N, yielding τb = hv1 , ha, αi, v2 i ∈ Tb. In such an entry/body-labeling we call transitions with markinglabel 0 body transitions, and transitions with marking labels in N+ entry-transitions.
Let Cb be an entry/body-labeling of C , and let v and w be vertices of C and Cb . We denote by v →bo w
ha,0ithat there is a body-transition v −−−→ w in Cb for some a ∈ A, and by v →[α] w, for α ∈ N+ that there is anha,αientry-transition v −−−→ w in Cb for some a ∈ A. By the set E(Cb ) of entry-transition identifiers we denotethe set of pairs hv, αi ∈ V × N+ such that an entry-transition →[α] departs from v in Cb . For hv, αi ∈ E(Cb ),we define by CCb (v, α) the subchart of C with start vertex vs that consists of the vertices and transitions
which occur on paths in C as follows: they start with a →[α] entry-transition from v, continue with bodytransitions only, and halt immediately if v is revisited.
The three recordings obtained above of the loop elimination procedure for the chart C (g0) in Ex. 2.1
indicate entry/body-labelings by signaling the entry-transitions but neglecting body-step labels 0.
Definition 3.2. Let chart C = hV, A, vs , T, Fi be a chart. A LLEE-witness (a layered LEE-witness) of C
is an entry/body-labeling Cb of C that satisfies the following two properties:(W1) There is no infinite path of →bo transitions from the start vertex vs of C .
(W2) For all hv, αi ∈ E(Cb ),(a) (loop condition) CCb (v, α) is a loop chart, and(b) (layeredness) if an entry-transition →[β ] departs from a vertex w 6= v of CCb (v, α), then its
marking label satisfies β < α.
The condition (W2)(a) justifies to call an entry-transition in a LLEE-witness a loop-entry transition. For a loop-entry transition →[β ] with β ∈ N+ , we call β its loop level.
The condition (W2)(b) on a LLEE-witness Cb of a chart C requires the loop structure defined by Cb to
be hierarchical. This permits to extract a star expression ẽ from Cb (defined in [4, 5]) that expresses C in
the sense that C (ẽ) ↔ C holds, intuitively by unfolding the underlying chart C to the syntax tree of ẽ.
For the three entry/body-labelings of the chart C (g0) in Ex. 2.1 that we have obtained above as recordings of runs of the loop elimination procedure it is easy to verify that they are LLEE-witnesses of C (g0).
Remark 3.3. In [4, 5] we established a connection between charts that have a LLEE-witness (and hence
satisfy LEE) and charts that are expressible by 1-free star expressions (that is, star expressions without 1,
and with binary star iteration instead of unary star iteration). By saying that a chart C ‘is expressible’
we mean here that C is bisimilar to the chart interpretation C (ẽ) of some star expression ẽ. Now Corollary 6.10 in [4, 5] states that if a chart is expressible by a 1-free star expression then its bisimulation
collapse has a LLEE-witness, and thus satisfies LEE. This statement entails that neither of the charts
C1(ne) and C2(ne) in Ex. 2.1 is expressible by a 1-free star expression, because both are bisimulation collapses, and neither of them satisfies LEE, as we have already observed above.

4

LEE may fail for process interpretations of star expressions

The chart interpretations C (e) of e, and C ( f ) of f in Ex. 2.1 do not satisfy LEE, contrasting with C (g0).
For C (e) we find the following run of the loop elimination procedure that successively eliminates the twoloop subcharts induced by the cycling transitions at e1 , and at e2 :

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

C (e)

e
a

e
elim

b
a

a

e1

elim

b
a

e2
b

a

b

e1

a

b
a

e2
b

C 00

e

b

e1

e2
b

The resulting chart C 00 does not contain loop subcharts any more, because taking, for example, a transition from e1 to e2 as an entry-transition does not yield a loop subchart, because in the induced subchart
immediate termination is not only possible at the start vertex e1 but also in the body vertex e2 , in contradiction to (L3). But while C 00 does not contain a loop subchart any more, it still has an infinite trace.
Therefore it follows that C (e) does not satisfy LEE.
In order to see that C ( f ) does not satisfy LEE, we can consider a run of the loop elimination procedurethat successively removes the cyclic transitions at f1 , f2 , and f3 . After these removals a variant of the notexpressible chart C2(ne) is obtained that still describes an infinite behavior, but that does not contain any
loop subchart. The latter can be argued analogously as for C2(ne) , namely that for all choices of entry-transitions between f1 , f2 , and f3 the loop condition (L2) fails. We conclude that C ( f ) does not satisfy LEE.
The reason for this failure of LEE is that, while the syntax trees of star expressions provide a nestedloop like structure, this is not guaranteed by the specific form of the TSS T . Execution of an iteration g∗in an expression g∗ · h leads eventually, in case that termination is reachable in g, to an iterated derivative(1 · g∗ ) · h. Also, as in the examples above, an iterated derivative (g̃ · g∗ ) · h with g̃↓ may be reached.
In these cases, continued execution will bypass the initial term g∗ · h, and either proceed with anotherexecution of the iteration to (g0 · g∗ ) · h, where g0 is a derivative of g, or take a step into the exit to h0 ,where h0 is a derivative of h. In both cases the execution does not return to the initial term g∗ of theexecution, as would be required for a loop subchart at g∗ to arise in accordance with loop condition (L2).

5

Recovering LEE for a variant definition of the process semantics

A remedy for the frequent failure of LEE for the chart translation of star expressions can consist in theuse of ‘1-transitions’. Such transitions may be used to create a back-link to an expression g∗ · h from aniterated derivative (g̃ · g∗ ) · h with g̃↓ (where g̃ is an iterated derivative of g) that is reached by a descentof the execution into the body of g. This requires an adapted refinement of the TSS T from page 2.
In particular we want to create transition rules that facilitate a back-link to an expression g∗ after
the execution has descended into g reaching g̃ · g∗ with g̃↓. In order to distinguish a concatenation
expression g̃ · g∗ that arises from the descent of the execution into an iteration g∗ from other concatenation
expressions we introduce a variant operation ∗. The rules of the refined TSS should guarantee that in
the example the reached iterated derivative of g∗ is a ‘stacked star expression’ G ∗ g∗ where G is itself astacked star expression that denotes an iterated derivative of g. If now G is also a star expression g̃ with g̃↓,then the expression G ∗ g∗ of the form g̃ ∗ g∗ should permit a 1-transition that returns to g∗ .
This intuition guided the definition of the rules of the TSS T (∗) in Def. 5.2 below, starting fromthe adaptation of the rule for steps from iterations e∗ , and the rule that creates 1-transition backlinks
to iterations e∗2 from stacked expressions e1 ∗ e∗2 with e1 ↓. The ‘stacked product’ ∗ has the following
features: E1 ∗ E2 never permits immediate termination; for defining transitions it behaves similarly as
concatenation · except that a transition from E1 ∗ E2 into E2 when E1 permits immediate termination now
requires a 1-transition to E2 first. The formulation of these rules of T (∗) led to the tailor-made set ofstacked star expressions as defined below.

C. Grabmayer

7

Definition 5.1. The set StExps(∗) (A) of stacked star expressions over (actions in) A is defined by:
E ::= e | E · e | E ∗ e∗(where e ∈ StExps(A)) .
The projection function π : StExps(∗) (A) → StExps(A) is defined by interpreting ∗ as · by the clauses:
π(E · e) := π(E) · e, π(E ∗ e∗) := π(E) · e∗ , and π(e) := e, for all E ∈ StExps(∗) (A), and e ∈ StExps(A).
Definition 5.2. The transition system specification T (∗) (A) has the following axioms and rules, where1∈/ A is an additional label (for representing empty steps), a ∈ A, a ∈ A := A ∪ {1}, stacked star expressions E1 , E2 , E10 , E20 , E 0 ∈ T (∗) (A), and star expressions e1 , e2 , e∗2 , e∗ ∈ StExps(A) (here and below wehighlight in red transitions that may involve 1-transitions):
ei ↓
e1 ↓
e2 ↓
(i ∈ {1, 2})1↓(e1 + e2 )↓(e1 · e2 )↓(e∗ )↓
a

a

− Ei0
ei →
a

a→
− 1

a

− Ei0
e1 + e2 →(i ∈ {1, 2})

E1 →
− E10
a

E1 · e2 →− E10 · e2
a

E1 →
− E10
a
E1 ∗ e∗2 →− E10 ∗ e∗2
(∗)

e1 ↓

a

a

− E20
e2 →
a

− E20
e1 · e2 →

e→
− E0
a

− E 0 ∗ e∗
e∗ →

e1 ↓
1

e1 ∗ e∗2 →− e∗2·− , ↓i with sepaVia its derivations the TSS T (∗) defines the 1-LTS S (StExps (A)) = hStExps(∗) (A), A, 1, →rate 1-transitions. For S ⊆ StExps(∗) (A), S-generated sub-LTSs are defined similarly as for S (StExps(A)).
A 1-chart is a (rooted) 1-LTS hV, A, 1, vs , T, Fi that consists of a finite set V of vertices, a finite set A
of proper actions, a specified symbol 1 with 1 ∈/ A, a start vertex vs ∈ V , a set T ⊆ V × A ×V of labeledtransitions with A := A ∪ {1}, and a set F ⊆ V of vertices with immediate termination. For such a 1-chart
we understand by a proper transition a transition in T ∩ (V × A ×V ) (labeled by a proper action), and by
a 1-transition a transition in T ∩ (V × {1} ×V ) (labeled by the empty-step symbol 1).
The 1-chart interpretation C (e) = hV(e), A, 1, e, T (e), F(e)i of a star expression e ∈ StExps(A) is the
e-rooted version of the {e}-generated sub-1-LTS S ({e}) = hV{e} , A, T{e} , F{e} i of S (StExps(A)).
In order to link the 1-LTS S (StExps(∗) (A)) to the LTS S (StExps(A)), we need to take accountof the semantics of 1-transitions as empty steps (see Vrancken [8]). For this, we introduce the ‘in( ·]duced LTS’ (S (StExps(∗) (A))] of S (StExps(∗) (A)) with induced transitions −→, and induced termination( a]↓(1)) that are defined as follows: E −→ E 0 holds if there is a sequence of 1-transitions from E to some Ẽ fromwhich there is an a-transition to E 0 , and E↓(1)) holds if there is a sequence of 1-transitions from E to some
( ·]Ẽ with Ẽ↓. The asymmetric notation −→ is intended to reflect the asymmetry that an induced transition
consists of an arbitrary number of leading 1-transitions that is trailed by a single proper transition.
( ·]Definition 5.3. The LTS (S (StExps(∗) (A))] = hStExps(∗) (A), A, ↓(1)) , −→i is defined via derivations in the
TSS (T (∗) ] that in addition to the axioms and rules of T (∗) also contains the following rules:
( a]
a
1
1
e↓
E→
− E0
E→
− Ẽ
Ẽ −→ E 0
E→
− ẼẼ↓(1))( a]( a]e↓(1))
E↓(1))
E −→ E 0
E −→ E 0
Now the following lemma explains the relationship between, on the one hand, the TSS T (A) and its
appertaining LTS S (StExps(A)), and on the other hand, the TSS (T (∗) ] and its LTS (S (StExps(∗) (A))].
Lemma 5.4. The LTS S (StExps(A)) is bisimilar to the LTS (S (StExps(∗) (A))] via the bisimulation thatis defined by the projection function π, that is, for all E, E 0 ∈ StExps(∗) (A), e0 ∈ StExps(A), and a ∈ A:
`T π(E)↓ ⇐= `(T (∗) ] E↓(1)) ,a`T π(E) →− π(E 0) ⇐=`T π(E)↓a`T π(E) →
− e0

( a]

`(T (∗) ] E −→ E 0 ,=⇒ `(T (∗) ] E↓(1)) ,
=⇒



( a]
∃E 0 ∈ StExps(∗) π(E 0) = e0 ∧ `(T (∗) ] E −→ E 0 .

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

The induced chart (C (e)] = hV, A, vs , (T ], (F)i of a 1-chart C = hV, A, 1, vs , T, Fi is defined analogously as the induced LTS of a 1-LTS with transitions in (T ] that are induced by those in T , and verticesin (F) with induced termination with respect to vertices with immediate termination in F. With this, we
now obtain the following connection between the chart, and the 1-chart, interpretation from Lemma 5.4.
Theorem 5.1. (C (e)] → C (e) holds for all e ∈ StExps(A), that is, there is a functional bisimulation fromthe induced chart of the 1-chart interpretation of a star expression e to the chart interpretation of e.
Now we define, similarly as we have done so for 1-free star expressions in [4, 5], a refinement of the
TSS T (∗) into a TSS that will supply entry/body-labelings for LLEE-witnesses, by adding marking labels
to the rules of T (∗) . In particular, body labels are added to transitions that cannot return to their source
expression. The rule for transitions from an iteration e∗ is split into the case in which e is normed or not(e is called normed if it enables an execution to an expression with immediate termination). Only if e
is normed can e∗ return to itself, and then a (loop-) entry-transition with the star height |e∗ |∗ of e∗ as its
level is created; otherwise a body label is introduced.
c(∗) has the following rules, where l ∈ {bo} ∪ {[α] | α ∈ N+ }:Definition 5.5. The TSS T
ei ↓(i ∈ {1, 2})(e1 + e2 )↓

1↓

e1 ↓
e2 ↓
(e1 · e2 )↓
a

a

ei →
− l Ei0aae1 + e2 →− bo Ei0a→− bo 1ae→− l E0
a
e∗ →
−

bo

a

E1 →
− l E10(i ∈ {1, 2})

e1 ↓

a

e→
− l E0(e normed)

E 0 ∗ e∗ae∗ →−E 0 ∗ e∗ae2 →− l E20ae1 · e2 →− bo E20

E1 · e2 →− l E10 · e2

(e not normed)[|e∗ |∗ ](e∗ )↓aE1 →− l E10e1 ↓1∗e1 ∗ e2 →− bo e∗2aE1 ∗ e∗2 →− l E10 ∗ e∗2

For every star expression e ∈ StExps(A) we denote by Cd(e) the entry/body-labeling of the 1-chart(∗)
cinterpretation C (e) that is defined according to the TSS T . For this entry/body-labeling we can show
the following theorem that recovers the property LEE for the 1-chart interpretation of star expressions.
Theorem 5.2. For every e ∈ StExps(A), the entry/body-labeling Cd(e) of C (e) is a LLEE-witness of C (e).
Consequently the 1-chart interpretation C (e) of a star expression e satisfies the property LEE.
We consider again the chart interpretations C (e) and C ( f ) for the star expressions e and f in Ex. 2.1
for which we saw in Section 4 that LEE fails. The picture below shows the 1-chart interpretations C (e)[of e (left) and C ( f ) of f (right), together with the entry/body-labelings Cd(e) of C (e) and C( f ) of C ( f ):C (e), Cd
(e)
1
E1
1

a

[1]

[2] [2]a

E10(C (e)]

e
1
E2

b
b

b

[1]

E20

E1
1

f

e

a

b

a

b

E2

a

b
E10

E20

[
C ( f ), C(f)

1 a1 [1] [1] a2 1
F1
F2
a3 [1]
1
b1
b2
F3

b3

Sink

The dotted transitions indicate 1-transitions. The non-initial vertices in the 1-chart interpretations arederivatives obtained via the TSS T (∗) , for C (e): E10 = ((1 ∗ a∗ ) · b∗ ) ∗ e, E1 = (a∗ · b∗ ) ∗ e, E2 = b∗ ∗ e,and E20 = (1 ∗ b∗ ) ∗ e, and for C ( f ): Fi = (1 · (1 + bi · 0)) ∗ f for i ∈ {1, 2, 3}, and Sink = (1 · 0) ∗ f .

C. Grabmayer

9

The chart interpretations C (e) of e, and C ( f ) of f arise as images of functional bisimulations fromthe induced charts (C (e)] of C (e), and (C ( f )] of C ( f ), as stated by Thm. 5.1. We argue this as follows.
The transitions of the induced chart (C (e)] (above in the middle) of the 1-chart interpretation C (e)of e correspond to paths in C (e) that start with a (potentially empty) 1-transition path and have a final
proper action transition, which also provides the label of the induced transition. For example the b-transition from E10 to E20 in (C (e)] arises as the induced transition in C (e) that is the path that consists of the
1-transitions from E10 to E1 , and from E1 to e, followed by the final b-transition from e to E20 . The vertices
with immediate termination in (C (e)] are all those that permit 1-transition paths in C (e) to vertices withimmediate termination. Therefore in C (e) only e needs to permit immediate termination in order to get
induced termination in (C (e)] also at all other vertices (like in C (e)). Now clearly the function that maps
e 7→ e, and Ei , Ei0 7→ ei for i ∈ {1, 2} defines a bisimulation from (C (e)] to C (e). Indeed this function
defines an isomorphism, if the unreachable vertices E1 and E2 are removed by garbage collection.
In the second example, the function that maps f 7→ f , Sink 7→ sink, and Fi 7→ fi for i ∈ {1, 2, 3} defines
a functional bisimulation from (C ( f )] to C ( f ), which in fact is an isomorphism.
[(e) of C (e), and C( f ) of C ( f ) as illustrated above can be
Furthermore, the entry/body-labelings Cd
readily checked to be LLEE-witnesses of C (e) and C ( f ), respectively.
In this way we have verified the joint claims of Thm. 5.1 and of Thm. 5.2 for the two examples e and fof star expressions from Ex. 2.1 for which, as we saw in Section 4, LEE fails for their chart interpretations
C (e) and C ( f ): the property LEE can be recovered for the 1-chart interpretations C (e) of e, and C ( f )of f (by Thm. 5.2), and also, the induced charts (C (e)] of C (e), and (C ( f )] of C ( f ) map to the original
process interpretations C (e) of e, and C ( f ) of f , respectively, via a functional bisimulation (by Thm. 5.1).
Acknowledgement. I want to thank my co-author Wan Fokkink for suggesting to define LLEE-witnesses
directly from the transition system specification, which we worked out for 1-free star expressions in [4, 5].
That inspired me for the generalization here to the full class of star expressions. Also, I want to thank Luca
Aceto for his comments on a draft, and the reviewers for their observations, questions, and suggestions.

References[1] J.C.M. Baeten, F. Corradini & C.A. Grabmayer (2007): A Characterization of Regular Expressions Under
Bisimulation. Journal of the ACM 54(2), doi:10.1145/1219092.1219094.
[2] Doeko Bosscher (1997): Grammars Modulo Bisimulation. Ph.D. thesis, University of Amsterdam.
[3] Clemens Grabmayer (2019): Modeling Terms by Graphs with Structure-Constrains (Two Illustrations). In:
TERMGRAPH 2018 post-proceedings, 288, pp. 1–13, doi:10.4204/EPTCS.288.
[4] Clemens Grabmayer & Wan Fokkink (2020): A Complete Proof System for 1-Free Regular Expressions Modulo
Bisimilarity. In: Proceedings of LICS 2020, ACM, New York, NY, p. To appear. Extended report [5] on arXiv.
[5] Clemens Grabmayer & Wan Fokkink (2020): A Complete Proof System for 1-Free Regular Expressions Modulo
Bisimilarity. Technical Report arXiv:2004.12740, arxiv.org.
[6] Clemens Grabmayer & Jan Rochel (2014): Maximal Sharing in the Lambda Calculus with Letrec. ACM
SIGPLAN Notices 49(9), p. 67–80, doi:10.1145/2692915.2628148.
[7] Robin Milner (1984): A Complete Inference System for a Class of Regular Behaviours. Journal of Computerand System Sciences 28, pp. 439–466.
[8] J.L.M. Vrancken (1997): The Algebra of Communicating Processes with Empty Process. Theoretical Computer
Science 177(2), pp. 287 – 328, doi:https://doi.org/10.1016/S0304-3975(96)00250-2.