11institutetext: School of Mathematics and Statistics, Southwest University,
China
11email<EMAIL_ADDRESS><EMAIL_ADDRESS>
22institutetext: Institute of Software, Chinese Academy of Sciences, China
22email<EMAIL_ADDRESS>
# Image Reflection on LLEE Charts — Another Proof for the Completeness of an
Axiomatization of 1-Free Regular Expressions Modulo Bisimilarity

Yuanrui Zhang  11 0000-0002-0685-6905 Xinxin Liu  22 0000-0002-8334-8277

###### Abstract

We analyze a phenomenon called “image reflection” on a type of
characterization graphs — LLEE charts — of 1-free regular expressions modulo
bisimulation equivalence. Due to the correspondence between 1-free regular
expressions and the provable solutions of LEE/LLEE charts, this observation
naturally leads to a new proof for the completeness of the proof system BBP
for 1-free regular expressions modulo bisimulation equivalence. The critical
part of the previous proof is to show that bisimulation collapse, which plays
the role in linking the provable solutions of two LLEE charts, is still an
LLEE chart. The difference of our proof, compared to the previous one, is that
we do not rely on the graph transformations from LLEE charts into their
bisimulation collapses by merging two bisimular nodes in each transformation
step. Instead, we directly show that the bisimulation collapse of an LLEE
chart possesses an LEE/LLEE structure based on its set of images mapped
through the bisimulation function from the LLEE chart, and the constrained
relation between the images and their so-called “well-structured” looping-back
charts pre-images on the LLEE chart. Our approach provides a novel angle to
look at this problem and related problems, and might introduce a different way
for proving the completeness problem of Mil for regular expressions modulo
bisimulation equivalence, which had remained open until very recently.

###### Keywords:

1-Free Regular Expression Process Semantics Bisimulation Axiomatization
Completeness.

##  1 Introduction

Regular expression, proposed by Kleene [12], is a formal language consisting
of elements $a$ (_actions_), $0$ (_deadlock_), $1$ (_skip_) and their
compositions $e_{1}+e_{2}$ (_non-deterministic choice_), $e_{1}\cdot e_{2}$
(_sequence_) and $e^{*}$ (_iterations_). The original star operator was a
bianry one: $e_{1}\operatorname{*}e_{2}$ (meaning iterating $e_{1}$ for finite
times and then executing $e_{2}$, or iterating $e_{1}$ infinitely). Later Copi
et al. in their work [3] proposed to use the unary operator $e^{*}$ instead of
$e_{1}\operatorname{*}e_{2}$. Regular expression has many applications in the
field of computer science, especially it as (or when embedded into) a
formalism like Kleene algebra with test [13] or dynamic logic [11] can serve
for the specification and verification purposes of different systems (cf. work
such as [18, 1, 16, 20, 19]).

Equational axiomatisation of regular expressions is a basic problem. It asks
for a set of equational axioms and inference rules (together forming a _proof
system_) which are semantically correct (namely the proof system’s
_soundness_), and based on which other semantically-correct equations of
regular expressions can be derived. When all semantically-correct equations
are derivable, a proof system is called _complete_. Salomaa [17] gave a
complete axiomatisation for regular expressions under the semantics of
execution traces, where the behaviour of a regular expression is interpreted
as a set of traces of actions. Milner first studied the axiomatisation of
regular expressions under the _process semantics_. In this semantics, the
behaviour of a regular expression $e$ is interpreted as a set of _bisimular
charts_ , denoted by $[|e|]_{\textit{C}}$. In [15], Milner built a sound proof
system Mil for regular expressions (there he called regular expression “star
expression”). Mil is tailored from Solomaa’s proof system by removing the
critical left associative law (lass): $e_{3}\cdot(e_{1}+e_{2})=e_{3}\cdot
e_{1}+e_{3}\cdot e_{2}$, which does not hold under the process semantics
anymore. It was claimed that the completeness problem of Mil could be much
harder because the Solomaa’s proof approach, which relies on (lass), cannot be
applied. This work by Milner has prompted a series of research work since
then. Up to now, some partial solutions and a recent full solution have been
acquired, considering various subsets of regular expressions together with
their adapted proof systems from Mil:

[2] proposed an axiomatisation for a subset of regular expressions where there
are no $0$ and $1$, but a binary star operator $e_{1}\operatorname{*}e_{2}$
instead of $e^{*}$. Its completeness was proved in [4]. [5] built a complete
proof system for a sub-regular expression with $0$ and $1$, but with a
“terminal cycle” $e^{\omega}$ rather than $e^{*}$. $e^{\omega}$ is
semantically equivalent to $e^{*}\cdot 0$ in regular expression. Recently,
Grabmayer and Fokkink in [9] axiomatized the so-called _1-free regular
expressions_ , in which there are $0$ and a binary star operator
$e_{1}\operatorname{*}e_{2}$ (denoted by
$e_{1}\operatorname{{{}^{\circledast}}}e_{2}$ in [9]) instead of $e^{*}$, but
no $1$. The proof system tailored from Mil for 1-free regular expressions is
denoted by BBP. In order to prove the completeness of BBP, the authors
developed a special type of characterization graphs called _LEE/LLEE charts_
and adopted a nominal “minimization strategy” (introduced below) which relies
on a series of LLEE-structure-preservable graph transformations to minimize
LLEE charts. The critical LEE/LLEE structure developed in [9] was further
extended to the case for regular expressions [6]. Based on it a method to
prove the completeness of Mil was fully explored in [10], where the author
claimed that this open problem has finally been solved.

In this paper, we propose an alternative proof for the completeness of BBP. We
adopt a different proof strategy: to directly prove that the minimization
graph (also called _bisimulation collapse_) $\mathcal{H}$ of an LLEE chart
$\mathcal{G}$ is an LLEE chart, without performing the LLEE-structure-
preservable graph transformations from $\mathcal{G}$ to $\mathcal{H}$ as in
[9]. The idea is based on an observation that, the behaviour of each image on
$\mathcal{H}$ of the bisimulation function $\theta$ from $\mathcal{G}$ to
$\mathcal{H}$ is constrained by a so-called _well-structured_ LLEE sub-
structure (called _looping-back chart_), so that all of the images on
$\mathcal{H}$ form a hierarchy structure that satisfies the LEE property. We
call this phenomenon the _image reflection_ on $\mathcal{G}$ by $\mathcal{H}$
via $\theta$. Below in this paper, we will make this “hierarchy structure”
explicit. Our approach provides another angle to look at this problem or
related problems, and might be helpful for introducing a different way for
proving the completeness of Mil.

In the following, we briefly introduce the minimization strategy and our idea.
The concepts and notations below will be formally defined in Sect. 2 and 3.

$\mathcal{H}$(F1: $e$)$\mathcal{G}_{e_{1}}$(F3:
$\operatorname{\mbox{$\vdash_{\textit{BBP}}$}}e_{1}=e$)$\mathcal{G}_{e_{2}}$(F3:
$\operatorname{\mbox{$\vdash_{\textit{BBP}}$}}e_{2}=e$)$e_{1}$$e_{2}$$=$$?$$\operatorname{\mbox{$\vdash_{\textit{BBP}}$}}$$(F2)$$(F2)$(II)(II)$(F4)$$(F4)$

Figure 1: Minimization strategy

The minimization strategy is based on the following facts (cf. [9]):

  1. (F1)

Each LLEE chart $\mathcal{G}$ corresponds to a set of equations that has a
1-free expression as a _primary provable solution_ (simply _primary
solution_).

  2. (F2)

Each 1-free regular expression $e$ corresponds to an LLEE chart
$\mathcal{G}_{e}\in[|e|]_{\textit{C}}$ that captures its operational behavior;
moreover, $e$ is a primary solution of $\mathcal{G}_{e}$.

  3. (F3)

For any two primary solutions $e$ and $e^{\prime}$ of an LLEE chart
$\mathcal{G}$, equation $e=e^{\prime}$ is derivable.

  4. (F4)

For any bisimulation function $\theta$ from $\mathcal{G}$ to $\mathcal{H}$,
each primary solution of $\mathcal{H}$ is also a primary solution of
$\mathcal{G}$.

(F4) was also applied to solve the completeness of axiomatisations by [14].

The idea of minimization strategy (illustrated in Fig. 1) can be stated as
follows on two stages:

  1. (I)

To prove equation $e_{1}=e_{2}$, by (F2), this means there are two LLEE charts
$\mathcal{G}_{e_{1}}$ and $\mathcal{G}_{e_{2}}$ bisimular to each other
(denoted by $\mathcal{G}_{e_{1}}\sim\mathcal{G}_{e_{2}}$) that have $e_{1}$
and $e_{2}$ as their primary solutions respectively. Due to
$\mathcal{G}_{e_{1}}\sim\mathcal{G}_{e_{2}}$, $\mathcal{G}_{e_{1}}$ and
$\mathcal{G}_{e_{2}}$ have the common bisimulation collapse $\mathcal{H}$
through two bisimulation functions $\theta_{1}$ from $\mathcal{G}_{e_{1}}$ to
$\mathcal{H}$ and $\theta_{2}$ from $\mathcal{G}_{e_{2}}$ to $\mathcal{H}$
respectively. Assume that $\mathcal{H}$ is an LLEE chart. Then by (F1)
$\mathcal{H}$ has a primary solution, let us say $e$. By (F4), $e$ is also a
primary solution of $\mathcal{G}_{e_{1}}$ and $\mathcal{G}_{e_{2}}$. So by
(F3), $e_{1}=e$ and $e_{2}=e$ can both be derived. Therefore, $e_{1}=e_{2}$
can be derived simply by the symmetry and transitivity of equivalence $=$.

  2. (II)

To show that $\mathcal{H}$ is an LLEE chart, a graph transformation was
carried out from either $\mathcal{G}_{e_{1}}$ or $\mathcal{G}_{e_{2}}$ into
$\mathcal{H}$ step by step. During each step, the transformation merges two
bisimulation nodes in $\mathcal{G}_{e_{1}}$ (or $\mathcal{G}_{e_{2}}$), while
preserving that the graph after the merge is still an LLEE chart.

Our modification to the minimization strategy happens on stage (II), instead,
we propose stage (II’): We directly prove that $\mathcal{H}$ is an LEE chart
according to the bisimulation function $\theta_{1}$ from $\mathcal{G}_{e_{1}}$
to $\mathcal{H}$ (or $\theta_{2}$ from $\mathcal{G}_{e_{2}}$ to
$\mathcal{H}$), making use of the image reflection on $\mathcal{G}_{e_{1}}$
(or $\mathcal{G}_{e_{2}}$) by $\mathcal{H}$ through $\theta_{1}$ (or
$\theta_{2}$). Since each LEE chart is also an LLEE chart (by Prop. 9),
$\mathcal{H}$ is an LLEE chart.

$\underline{x}$$\underline{x^{\prime}}$$\underline{X}$$\hat{\mathcal{G}}/\mathcal{G}$$\hat{\mathcal{H}}/\mathcal{H}$$[2]$$a$$[2]$$b$$b$$[1]$$a$$[1]$$a$$[1]$$b$$\theta$$\theta$where
$s(X)=_{\textit{df}}(a+b)\operatorname{{{}^{\circledast}}}0$ $s(X)=a\cdot
s(X)+b\cdot s(X)$,$\mathcal{H}$’s equations$\left\\{\begin{aligned}
s(x)&=a\cdot s(x^{\prime})+b\cdot s(x^{\prime}),\\\ s(x^{\prime})&=a\cdot
s(x^{\prime})+b\cdot s(x),\end{aligned}\right.$ $\begin{aligned}
\mbox{where}&\\\ s(x)&=_{\textit{df}}((a+b)\cdot
a\operatorname{{{}^{\circledast}}}b)\operatorname{{{}^{\circledast}}}0,\\\
s(x^{\prime})&=_{\textit{df}}a\operatorname{{{}^{\circledast}}}b\cdot((a+b)\cdot
a\operatorname{{{}^{\circledast}}}b)\operatorname{{{}^{\circledast}}}0\end{aligned}$
$\mathcal{G}$’s
equations$\theta(\\{x^{\prime}\\})$reflect$\mathcal{G}_{x^{\prime}}$

Figure 2: A simple example illustrating our idea

Let us see a simple example. In Fig. 2 111To distinguish node names from
action names, in this paper, we underline all the node names (e.g.
$\underline{X}$) in figures. , expression
$(a+b)\operatorname{{{}^{\circledast}}}0$ is the primary solution of LLEE
chart $\mathcal{H}$, since it is the provable solution of the equation shown
on the left of $\mathcal{H}$ that $\mathcal{H}$ corresponds to. Expression
$((a+b)\cdot
a\operatorname{{{}^{\circledast}}}b)\operatorname{{{}^{\circledast}}}0$ is the
primary solution of LLEE chart $\mathcal{G}$, which corresponds to the set of
equations on its right. $X$ and $x$ are the initial nodes of the two charts
$\mathcal{H}$ and $\mathcal{G}$ respectively (that’s why expressions $s(X)$
and $s(x)$ are called ‘primary’ solutions). $\mathcal{H}$ is the bisimulation
collapse of $\mathcal{G}$, through a bisimulation function $\theta$ from
$\mathcal{G}$ to $\mathcal{H}$ defined as: $\theta=_{\textit{df}}\\{x\mapsto
X,x^{\prime}\mapsto X\\}$.

By (F4), $(a+b)\operatorname{{{}^{\circledast}}}0$ is also the primary
solution of $\mathcal{G}$. To see this, let
$s^{\prime}(x)=_{\textit{df}}(a+b)\operatorname{{{}^{\circledast}}}0$ and
$s^{\prime}(x^{\prime})=_{\textit{df}}(a+b)\operatorname{{{}^{\circledast}}}0$.
From that $s(X)=a\cdot s(X)+b\cdot s(X)$ can be derived, it is easy to see
that both $s^{\prime}(x)=a\cdot s^{\prime}(x^{\prime})+b\cdot
s^{\prime}(x^{\prime})$ and $s^{\prime}(x^{\prime})=a\cdot
s^{\prime}(x^{\prime})+b\cdot s^{\prime}(x)$ can be derived. Because $s(X)$,
$s^{\prime}(x)$ and $s^{\prime}(x^{\prime})$ are the same expression
$(a+b)\operatorname{{{}^{\circledast}}}0$. Therefore, by (F3) equation
$(a+b)\operatorname{{{}^{\circledast}}}0=((a+b)\cdot
a\operatorname{{{}^{\circledast}}}b)\operatorname{{{}^{\circledast}}}0$ can be
derived. This forms the proof of one side on stage (I).

Informally, to see that $\mathcal{G}$ is an LLEE chart, by removing all tagged
transitions in $\mathcal{G}$ in the order that the tagged number indicate:
i.e., removing transition $x^{\prime}\xrightarrow{a}x^{\prime}$, then
transition $x\xrightarrow{a}x^{\prime}$ and lastly transition
$x\xrightarrow{b}x^{\prime}$, all loops in $\mathcal{G}$ can be eliminated.
Similarly, it is easy to see that $\mathcal{H}$ is an LLEE chart. The looping-
back chart $\mathcal{G}_{x^{\prime}}$ consists of node $x^{\prime}$ and
transition $x^{\prime}\xrightarrow{a}x^{\prime}$. Informally, $\mathcal{H}$ is
the image of chart $\mathcal{G}_{x^{\prime}}$ through $\theta$, because
$\theta$ maps to each node of $\mathcal{H}$ (i.e. $X$) from a node in
$\mathcal{G}_{x^{\prime}}$ (i.e. $x^{\prime}$): i.e., $\theta(x^{\prime})=X$.
$\mathcal{G}_{x^{\prime}}$ is well-structured as there is no proper sub-chart
of $\mathcal{G}_{x^{\prime}}$ that has $\mathcal{H}$ as its image.

In this example, in order to prove that $\mathcal{H}$ is an LLEE chart, stage
(II) merges the two bisimular nodes $x$ and $x^{\prime}$ in $\mathcal{G}$ and
thus transforms $\mathcal{G}$ into $\mathcal{H}$. [9] generally proved that
this transformation process preserves the LLEE structure. Our approach (II’),
on the other hand, will show that $\mathcal{H}$, as the image of the looping-
back chart $\mathcal{G}_{x^{\prime}}$ through $\theta$, satisfies the LEE
property. Intuitively, the behaviour of $\mathcal{H}$ is contrained by the
behaviour of $\mathcal{G}_{x^{\prime}}$ through $\theta$ such that all loops
in $\mathcal{H}$ pass through $X$ and all paths starting from $X$ stay in
$\mathcal{H}$ before returning to $X$. This LEE structure (called _LEE sub-
chart_) on $\mathcal{H}$ enforced by its corresponding well-structured
looping-back chart $\mathcal{G}_{x^{\prime}}$ is called that $\mathcal{H}$
_reflects_ the LLEE structure of $\mathcal{G}_{x}$.

In this paper, by utilizing this image reflection between an image and its
correspondence well-structured looping-back chart, we will prove in general
case, that the bisimulation collapse of any LLEE chart itself is an LLEE
chart.

The main contributions of this paper are mainly twofolds:

  1. $\bullet$

We introduce the concepts of _images_ and _well-structured looping-back
charts_ on the bisimulation collapse $\mathcal{H}$ of an LLEE chart
$\mathcal{G}$ through the bisimulation function $\theta$ from $\mathcal{G}$ to
$\mathcal{H}$;

  2. $\bullet$

Based on these concepts, we propose a new proof for the completeness of BBP by
directly showing that every $\mathcal{H}$ is an LLEE chart.

The rest of the paper is organized as follows: Sect. 2 introduces the
necessary background knowledge needed to understand our work. In Sect. 3 we
define the concepts as the foundation of our proof method, while in Sect. 4 we
mainly focus on our proof. Sect. 5 makes a conclusion and discusses about
future work.

##  2 Preliminaries

In this section we introduce the necessary background related to this topic.
Note that some of them are not directly used in our proof method, but are
necessary for understanding the minimization strategy, which we tag as ‘(*)’.

###  2.1 1-Free Regular Expresssions and Charts

#### 1-Free Regular Expression

A 1-free regular expression $e\in\mbox{$\mathit{RExp}_{\textit{1-free}}$}$ is
defined as follows in BNF form:

$e=_{\textit{df}}a\ |\ 0\ |\ e+e\ |\ e\cdot e\ |\
e\operatorname{{{}^{\circledast}}}e,$

where $a\in\mathit{Act}$ is called an _action_ , ranged over by $a,b,c,d$.
$e\operatorname{{{}^{\circledast}}}e$ is the binary star operator, $e_{1}\cdot
e_{2}$ is sometimes abbreviated as $e_{1}e_{2}$. We use $\equiv$ to represent
the syntactic identity between two 1-free regular expressions.

#### Chart

A _chart_ is a 5-tuple $\mathcal{G}=\langle
V,A,v,\operatorname{\to},\surd\rangle$, where $V$ is a finite set of _nodes_ ,
usually ranged over by $x,y,z,X,Y,Z$; $A\subseteq\mathit{Act}$ is a set of
actions; $v\in V$ is the _initial node_ ; $\operatorname{\to}:V\times
A\times(V\cup\\{\surd\\})$ is a set of transitions; $\surd$ is a special node
called _termination_. Each transition $\langle
X,a,Y\rangle\in\operatorname{\to}$ and transition $\langle
X,a,\surd\rangle\in\operatorname{\to}$ are also written as $X\xrightarrow{a}Y$
and $X\xrightarrow{a}\surd$ respecitively, where $a\in A$. We also call
$X\xrightarrow{a}\surd$ a _terminal transition_. A sequence of transitions is
often written as:
$X_{1}\xrightarrow{a_{1}}X_{2}\xrightarrow{a_{2}}...\xrightarrow{a_{n}}X_{n}\xrightarrow{b}\xi$
($n>0$), where $\xi$ is a node or $\surd$, $X_{1}\xrightarrow{a_{1}}X_{2}$, …,
$X_{n}\xrightarrow{b}\xi$ are $n$ transitions.

Sometimes we ignore symbol $a$ and simply write a transition
$X\xrightarrow{a}Y$ as $X\xrightarrow{}Y$. We use $X\operatorname{\equiv}Y$ to
represent that nodes $X$ and $Y$ are identical. Use $\cdot$ to represent an
arbitrary node, e.g. a transition $X\xrightarrow{}\cdot$. The reflexive and
transitive closure of $\xrightarrow{}$ is defined as: $X\xrightarrow{}^{*}Y$
if either (i) $X\operatorname{\equiv}Y$ or (ii) $X\xrightarrow{}Z$ and
$Z\xrightarrow{}^{*}Y$ for some $Z$. The transitive closure
$X\xrightarrow{}^{+}Y$ is defined s.t. $X\xrightarrow{}Z$ and
$Z\xrightarrow{}^{*}Y$ for some $Z$. A _path_ is a finite or infinite sequence
of transitions. We use $X\xrightarrow[\not\operatorname{\equiv}Z]{}Y$,
$X\xrightarrow[\not\operatorname{\equiv}Z]{}^{*}Y$ or
$X\xrightarrow[\not\operatorname{\equiv}Z]{}^{+}Y$ to represent a path where
all intermediate nodes (not including $X$) are not $Z$. A _loop_ is a finite
path of the form: $X\xrightarrow{}^{+}X$, i.e., it starts from and returns to
the same node $X$.

#### Chart Interpretation (*)

The _chart interpretation_ of a 1-free regular expression
$e\in\mbox{$\mathit{RExp}_{\textit{1-free}}$}$ is a chart

$\mathcal{C}(e)=_{\textit{df}}\langle
V(e),A(e),e,\operatorname{\to}(e),\surd\rangle,$

which is obtained by expanding $e$ according to the operational semantics
given in Table 1. $e$ is the initial node. $\operatorname{\to}(e)$ consists of
all the transitions during the expansion of $e$ by applying the rules in Table
1. $V(e)$ is the finite set of expressions reachable from $e$ through
transitions in $\operatorname{\to}(e)$. $A(e)$ is the set of actions appeared
in $e$.

$a\xrightarrow{a}\surd$ $e_{1}+e_{2}\xrightarrow{a}\surd
e_{1}\xrightarrow{a}\surd$ $e_{1}+e_{2}\xrightarrow{a}\surd
e_{2}\xrightarrow{a}\surd$ $e_{1}\cdot
e_{2}\xrightarrow{a}e_{2}e_{1}\xrightarrow{a}\surd$
$e_{1}\operatorname{{{}^{\circledast}}}e_{2}\xrightarrow{a}e_{1}\operatorname{{{}^{\circledast}}}e_{2}e_{1}\xrightarrow{a}\surd$
$e_{1}\operatorname{{{}^{\circledast}}}e_{2}\xrightarrow{a}\surd
e_{2}\xrightarrow{a}\surd$
---
$e_{1}+e_{2}\xrightarrow{a}e^{\prime}_{1}+e_{2}e_{1}\xrightarrow{a}e^{\prime}_{1}$
$e_{1}+e_{2}\xrightarrow{a}e_{1}+e^{\prime}_{2}e_{2}\xrightarrow{a}e^{\prime}_{2}$
$e_{1}\cdot e_{2}\xrightarrow{a}e^{\prime}_{1}\cdot
e_{2}e_{1}\xrightarrow{a}e^{\prime}_{1}$
$e_{1}\operatorname{{{}^{\circledast}}}e_{2}\xrightarrow{a}e^{\prime}_{1}\cdot(e_{1}\operatorname{{{}^{\circledast}}}e_{2})e_{1}\xrightarrow{a}e^{\prime}_{1}$
$e_{1}\operatorname{{{}^{\circledast}}}e_{2}\xrightarrow{a}e^{\prime}_{2}e_{2}\xrightarrow{a}e^{\prime}_{2}$
Table 1: Operational semantics of 1-free regular expressions

###  2.2 Bisimulation Equivalence and Proof System BBP

#### Bisimulation Equivalence

A _bisimulation relation_ $\mathfrak{R}\subseteq\mathbb{V}\times\mathbb{V}$,
where $\mathbb{V}$ is the universal set of nodes, is a symmetric binary
relation satisfying that for any $(X,Y)\in\mathfrak{R}$, the following hold:

  1. (1)

if $X\xrightarrow{a}X^{\prime}$, then $Y\xrightarrow{a}Y^{\prime}$ and
$(X^{\prime},Y^{\prime})\in\mathfrak{R}$;

  2. (2)

if $Y\xrightarrow{a}Y^{\prime}$, then $X\xrightarrow{a}X^{\prime}$ and
$(X^{\prime},Y^{\prime})\in\mathfrak{R}$;

  3. (3)

$X\xrightarrow{a}\surd$ iff $Y\xrightarrow{a}\surd$.

Given two charts $\mathcal{G}=\langle
V_{1},A_{1},v_{1},\operatorname{\to}_{1},\surd\rangle$ and
$\mathcal{H}=\langle V_{2},A_{2},v_{2},\operatorname{\to}_{2},\surd\rangle$, a
bisimulation relation $\mathfrak{R}\subseteq V_{1}\times V_{2}$ between
$\mathcal{G}$ and $\mathcal{H}$ is a bisimulation relation satisfying that
$(v_{1},v_{2})\in\mathfrak{R}$. We also denote $\mathfrak{R}:V_{1}\times
V_{2}$ as $\mathfrak{R}:V_{1}\to V_{2}$. Call $V_{1}$ the _domain_ and $V_{2}$
the _codomain_ of relation $\mathfrak{R}$. Given $\mathfrak{R}:V_{1}\to
V_{2}$, for any set $A\subseteq V_{1}$ and $B\subseteq V_{2}$, we define
$\mathfrak{R}(A)=_{\textit{df}}\\{X\ |\ X\in V_{2},\exists y\in
A.(y,X)\in\mathfrak{R}\\}$; and define
$\mathfrak{R}^{-1}(B)=_{\textit{df}}\\{x\ |\ x\in V_{1},\exists Y\in
B.(x,Y)\in\mathfrak{R}\\}$. A bisimulation relation $\mathfrak{R}:V_{1}\to
V_{2}$ is called a _bisimulation function_ if $\mathfrak{R}$ is a function
from $V_{1}$ to $V_{2}$. We use $\theta$ to represent a bisimulation function.

Two nodes $X$ and $Y$ are _bisimular_ , denoted by $X\sim Y$, if there is a
bisimulation relation $\mathfrak{R}$ such that $(X,Y)\in\mathfrak{R}$. Two
charts $\mathcal{G}$ and $\mathcal{H}$ are said bisimular, denoted by
$\mathcal{G}\sim\mathcal{H}$, if there is a bisimulation relation
$\mathfrak{R}$ between $\mathcal{G}$ and $\mathcal{H}$. The _bisimulation
equivalence_ $e_{1}=e_{2}$ between two 1-free regular expressions
$e_{1},e_{2}\in\mbox{$\mathit{RExp}_{\textit{1-free}}$}$, is defined if
$\mathcal{C}(e_{1})\sim\mathcal{C}(e_{2})$.

#### Proof System BBP (*)

Proof system BBP for 1-free regular expressions modulo bisimulation
equivalence $=$ is given in Table 2 as a set of rules on equations, where (A1)
- (A9) are axioms, (R1) is an inference rule. Since our work in this paper
will not concern this proof system, we will not explain them. One can refer to
[9] for more details.

${e_{1}+e_{2}=e_{2}+e_{1}}\ (A1)$ ${(e_{1}+e_{2})+e_{3}=e_{1}+(e_{2}+e_{3})}\
(A2)$ ${e+e=e}\ (A3)$
---
${(e_{1}+e_{2})\cdot e_{3}=e_{1}\cdot e_{3}+e_{2}\cdot e_{3}}\ (A4)$
${(e_{1}\cdot e_{2})\cdot e_{3}=e_{1}\cdot(e_{2}\cdot e_{3})}\ (A5)$ ${e+0=e}\
(A6)$
${0\cdot e=0}\ (A7)$
${e_{1}\operatorname{{{}^{\circledast}}}e_{2}=e_{1}\cdot(e_{1}\operatorname{{{}^{\circledast}}}e_{2})+e_{2}}\
(A8)$ ${(e_{1}\operatorname{{{}^{\circledast}}}e_{2})\cdot
e_{3}=e_{1}\operatorname{{{}^{\circledast}}}(e_{2}\cdot e_{3})}\ (A9)$
$e=e_{1}\operatorname{{{}^{\circledast}}}e_{2}e=e_{1}\cdot e+e_{2}$
Table 2: Proof system BBP for 1-free regular expressions

Given an equation $e_{1}=e_{2}$, we write
$\operatorname{\mbox{$\vdash_{\textit{BBP}}$}}e_{1}=e_{2}$ to mean that
$e_{1}=e_{2}$ can be derived by applying the rules in Table 2. Proof system
BBP is sound, that is,
$\operatorname{\mbox{$\vdash_{\textit{BBP}}$}}e_{1}=e_{2}$ implies
$e_{1}=e_{2}$ for any
$e_{1},e_{2}\in\mbox{$\mathit{RExp}_{\textit{1-free}}$}$. The completeness of
BBP was first obtained as the main result in [9], which means that for every
true equation $e_{1}=e_{2}$ with
$e_{1},e_{2}\in\mbox{$\mathit{RExp}_{\textit{1-free}}$}$,
$\operatorname{\mbox{$\vdash_{\textit{BBP}}$}}e_{1}=e_{2}$.

#### Chart and 1-Free Regular Expression Equations (*)

An _evaluation_ $s:\mathbb{V}\to\mbox{$\mathit{RExp}_{\textit{1-free}}$}$
defines a function that maps each node to a 1-free regular expression. Given
an evaluation $s$, a chart
$\mathcal{G}=\langle\\{X_{i}\\}_{i\in[1,n]},A,X_{1},\operatorname{\to},\surd\\}\rangle$
corresponds to a set of equations w.r.t. $s$:

$s(\mathcal{G})=_{\textit{df}}\left\\{s(X_{i})=\sum^{n}_{j=1}e_{ij}\cdot
s(X_{j})+\sum^{m}_{k=1}f_{ik}\right\\}_{i\in[1,n]},$

in the sense that in each equation $s(X_{i})=\sum^{n}_{j=1}e_{ij}\cdot
s(X_{j})+\sum^{m}_{k=1}f_{ik}$, term $e_{ij}\cdot s(X_{j})$ ($e_{ij}\in A$)
appears iff $X_{i}\xrightarrow{e_{ij}}X_{j}$ is a transition in
$\operatorname{\to}$; term $f_{ik}$ appears iff
$X_{i}\xrightarrow{f_{ik}}\surd$ is a transition in $\operatorname{\to}$. An
evaluation $s$ is a _provable solution_ of $\mathcal{G}$, if each equation of
$s(\mathcal{G})$ can be derived according to proof system BBP in Table 2,
denoted by $\operatorname{\mbox{$\vdash_{\textit{BBP}}$}}s(\mathcal{G})$. Call
$s(X_{1})$ a _primary solution_ of $\mathcal{G}$.

###  2.3 Loop Charts, LEE Charts and LLEE Charts [9]

#### Loop Chart

A _loop chart_ $\mathcal{A}=\langle V,A,X,\operatorname{\to},\surd\rangle$ is
a chart with the initial node $X$ called _starting node_ and satisfying the
following three conditions:

  1. (L1)

There is an infinite path from $X$ in $\mathcal{A}$;

  2. (L2)

In $\mathcal{A}$ every infinite path from $X$ returns to $X$ after a finite
number of transitions;

  3. (L3)

$\surd$ is not in $\mathcal{A}$.

The set of transitions starting from $X$ is called _loop-entry transitions_.
Other transitions are called _body transitions_. Call
$V_{\mathcal{A}}/\\{X\\}$ the _body_ of $\mathcal{A}$.

For example, in Fig. 2, chart $\mathcal{H}$ is a loop chart. Chart
$\mathcal{G}$ with the starting node $x$ is not a loop chart as it violates
(L2).

In a chart $\mathcal{G}=\langle V,A,v,\operatorname{\to},\surd\rangle$, a
_$\langle X,\mathbf{E}\rangle$ -generated chart_ is a sub-chart
$\mathcal{C}=\langle V_{1},A,X,\operatorname{\to}_{1},\surd\rangle$ of
$\mathcal{G}$ consisting of all the transitions each of which is on a path
that starts from a transition $X\xrightarrow{}Y$ in $\mathbf{E}$, and
continues with other transitions of $\mathcal{G}$ until reaching $X$ again.
Formally, $\mathcal{C}$ satisfies that
$\operatorname{\to}_{1}=\mathbf{E}\cup\\{Y\xrightarrow{}Z\ |\
X\xrightarrow[\not\operatorname{\equiv}X]{}X_{1}\xrightarrow[\not\operatorname{\equiv}X]{}^{*}Y\xrightarrow{}Z,(X\xrightarrow{}X_{1})\in\mathbf{E}\\}\cup\\{Y\xrightarrow{}\surd\
|\
X\xrightarrow[\not\operatorname{\equiv}X]{}X_{1}\xrightarrow[\not\operatorname{\equiv}X]{}^{*}Y\xrightarrow{}\surd,(X\xrightarrow{}X_{1})\in\mathbf{E}\\}$,
$V_{1}=\\{X\ |\ X\xrightarrow{}\cdot\in\to_{1}\mbox{ or
}\cdot\rightarrow{}X\in\to_{1}\\}$.

A $\langle X,\mathbf{E}\rangle$-generated chart of $\mathcal{G}$ is called a
_loop sub-chart_ of $\mathcal{G}$ if it is a loop chart.

In Fig. 2, chart $\mathcal{H}$, as the $\langle
X,\\{X\xrightarrow{a}X,X\xrightarrow{b}X\\}\rangle$-generated chart, is a loop
sub-chart of itself. Chart
$\mathcal{G}_{x^{\prime}}:\langle\\{x^{\prime}\\},\\{a,b\\},x^{\prime},\\{x^{\prime}\xrightarrow{a}x^{\prime}\\},\surd\rangle$,
as the $\langle
x^{\prime},\\{x^{\prime}\xrightarrow{a}x^{\prime}\\}\rangle$-generated chart,
is a loop sub-chart of $\mathcal{G}$.

#### LEE Chart

An _elimination of a loop chart_ $\mathcal{A}$ startinig from $X$ is a
transformation process in which we first remove all of its loop-entry
transitions from $X$, then remove all the nodes and transitions that become
unreachable. A chart $\mathcal{G}$ is said to satisfy the _loop existence and
elimination_ (LEE) property, if there exists a transformation process in which
each loop sub-chart of $\mathcal{G}$ can be eliminated step by step, so that
after the process, $\mathcal{G}$ results in a chart without an infinite path.
A chart is called an _LEE chart_ if it satisfies the LEE property.

$\underline{x}$$\underline{x^{\prime}}$$\mathcal{G}$$a$$b$$b$$a$$\underline{x}$$\underline{x^{\prime}}$$\mathcal{G}^{\prime}$$a$$b$$b$$\underline{x}$$\mathcal{G}^{\prime\prime}$transformtransform$\underline{x}$$\underline{x^{\prime}}$$\hat{\mathcal{G}}/\mathcal{G}$$[2]$$a$$[2]$$b$$b$$[1]$$a$

Figure 3: An example of elimination processes

Fig. 3 shows how the LEE chart $\mathcal{G}$ of Fig. 2 can be eliminated in
two steps: firstly the loop sub-chart $\mathcal{G}_{x^{\prime}}$ is eliminated
by removing the loop-entry transition $x^{\prime}\xrightarrow{a}x^{\prime}$;
after that the resulted chart $\mathcal{G}^{\prime}$, which becomes a loop
sub-chart of itself, is then eliminated by removing two loop-entry transitions
$x\xrightarrow{a}x^{\prime}$ and $x\xrightarrow{b}x^{\prime}$, and then
removing node $x^{\prime}$ and transition $x^{\prime}\xrightarrow{b}x$ that
become unreachable. This leaves the resulted chart
$\mathcal{G}^{\prime\prime}$ having no infinite paths.

As illustrated in the example above, the process of loop elimination is
actually conducted in an inside-out manner, in the sense that a sub-chart
$\mathcal{A}$ of $\mathcal{G}$ can only become a loop sub-chart after all the
loop sub-charts of $\mathcal{A}$ have been eliminated previously. This is an
important intuition of our method purposed in Sect. 4.

For an elimination process on an LEE chart $\mathcal{G}$, a function
$\hat{\mathcal{G}}$, called an _LEE witness_ , is used to indicate the order
of removing the loop-entry transitions in $\mathcal{G}$. $\hat{\mathcal{G}}$
maps the transitions of $\mathcal{G}$ to a down-closed set of natural numbers,
we call _order numbers_. It maps a loop-entry transition $X\xrightarrow{}Y$ to
a number $n>0$, denoted by $X\xrightarrow{}_{[n]}Y$, if $X\xrightarrow{}Y$ is
removed at the $n$th step of the process; and maps body transitions to $0$,
denoted by $\cdot\xrightarrow{}_{[0]}\cdot$ or
$\cdot\rightarrow_{\textit{bo}}\cdot$. Write an LEE chart $\mathcal{G}$ as
$\hat{\mathcal{G}}/\mathcal{G}$.

In chart $\mathcal{G}$ of Fig. 3, the tagged numbers on arrows indicate an LEE
witness $\hat{\mathcal{G}}$ of the elimination process in Fig. 3, where
$\hat{\mathcal{G}}(x^{\prime}\xrightarrow{a}x^{\prime})=_{\textit{df}}1$,
$\hat{\mathcal{G}}(x\xrightarrow{a}x^{\prime})=_{\textit{df}}2$,
$\hat{\mathcal{G}}(x\xrightarrow{b}x^{\prime})=_{\textit{df}}2$,
$\hat{\mathcal{G}}(x^{\prime}\xrightarrow{b}x)=_{\textit{df}}0$.

#### LLEE Chart

The elimination process of an LEE chart is not necessarily unique. If in an
LEE chart there exists an elimination process in which no loop-entry
transitions are removed from a node in the body of a previously eliminated
loop sub-chart, then say the LEE chart satisfies the _layered loop existence
and elimination_ (LLEE) property. The LEE chart is then called an _LLEE
chart_. A witness $\hat{\mathcal{G}}$ of an LLEE chart $\mathcal{G}$ is thus
called an _LLEE witness_.

It is easy to see that chart $\mathcal{G}$ of Fig. 3 is also an LLEE chart.

Not all LEE witnesses are LLEE witnesses. Considering the chart
$\hat{\mathcal{E}_{1}}/\mathcal{E}_{1}$ in Fig. 4, from its elimination
process we see that $\hat{\mathcal{E}_{1}}$ is an LEE witness. However, it is
not an LLEE witness, because when performing its elimination at step 3, loop-
entry transition $X\xrightarrow{b_{1}}_{[3]}Z$ is from the body of the loop
sub-chart
$\langle\\{Z,X\\},\\{a_{1},a_{2},a_{3},a_{4},b_{1},d_{1},d_{2}\\},Z,\\{Z\xrightarrow{a_{2}}X,X\xrightarrow{b_{1}}Z\\},\surd\rangle$
of $\mathcal{E}_{1}^{\prime}$ after step 1.

$\underline{Z}$$\underline{X}$$\underline{Y}$$\underline{K}$$\hat{\mathcal{E}_{1}}/\mathcal{E}_{1}$$[2]$$a_{2}$$[3]$$b_{1}$$[1]$$a_{3}$$d_{1}$$[1]$$a_{1}$$a_{4}$$d_{2}$$\underline{Z}$$\underline{X}$$\underline{K}$$\mathcal{E}_{1}^{\prime}$$[2]$$a_{2}$$[3]$$b_{1}$$a_{4}$$d_{2}$$\underline{Z}$$\underline{X}$$\underline{K}$$\mathcal{E}_{1}^{\prime\prime}$$[3]$$b_{1}$$a_{4}$$d_{2}$$\underline{X}$$\mathcal{E}_{1}^{(3)}$$\underline{Z}$$\underline{X}$$\underline{Y}$$\underline{K}$$\hat{\mathcal{E}_{1}}^{\prime}/\mathcal{E}_{1}$$[2]$$a_{2}$$b_{1}$$[1]$$a_{3}$$d_{1}$$[1]$$a_{1}$$[3]$$a_{4}$$d_{2}$step
1step 2step 3

Figure 4: An example of a non-LLEE LEE witness

In an LLEE chart, a relation $X\operatorname{\curvearrowright}Y$ is defined if
there exists a path from $X$ to $Y$ that begins with a loop-entry transition
and continues through subsequent body transitions without reaching $X$ again.
Or formally,
$X\xrightarrow[\not\operatorname{\equiv}X]{}_{[m]}\cdot\xrightarrow[\not\operatorname{\equiv}X]{}^{*}_{\textit{bo}}Y$
for some $m>0$. The transitive closure $X\operatorname{\curvearrowright}^{+}Y$
is defined s.t. (i) $X\operatorname{\curvearrowright}Y$, or (ii)
$X\operatorname{\curvearrowright}^{+}Z$ and
$Z\operatorname{\curvearrowright}Y$ for some node $Z$.

The following property on relation $\operatorname{\curvearrowright}$ directly
comes from the LLEE property. Refer to [9] for more details.

###### Proposition 1

Relation $\operatorname{\curvearrowright}^{+}$ in an LLEE chart $\mathcal{G}$
is a well-founded, strict partially-ordered relation.

#### Sovability of LLEE Charts (*)

As stated in Sect. 1, LLEE charts characterize regular expressions modulo
bisimulation equivalence $=$ and possess the capability of deriving unique
1-free-expression solutions under BBP. We list the following results obtained
from [9]. They correspond to the facts (F1) - (F4) respectively. As they are
irrelevant to stage (II) and so are not concerned with our proof method
proposed in this paper, we omit their proofs and interesting readers can refer
to [9] for more details.

######  Proposition 2 (Corresponding to (F4))

Given two charts $\mathcal{G}=\langle
V_{1},A_{1},v_{1},\operatorname{\to}_{1},\surd\rangle$, $\mathcal{H}=\langle
V_{2},A_{2},v_{2},\operatorname{\to}_{2},\surd\rangle$ and a bisimulation
function $\theta:V_{1}\to V_{2}$ between them, if
$s:V_{2}\to\mbox{$\mathit{RExp}_{\textit{1-free}}$}$ is a provable solution of
$\mathcal{H}$, then
$s\circ\theta:V_{1}\to\mbox{$\mathit{RExp}_{\textit{1-free}}$}$ is a provable
solution of $\mathcal{G}$.

######  Proposition 3 (Corresponding to (F2))

For every 1-free regular expression $e$, there is an LLEE chart
$\hat{\mathcal{G}}/\mathcal{G}$ with an initial node $X$ such that
$\mathcal{G}$ has a provable solution $s$ with $s(X)=_{\textit{df}}e$.

######  Proposition 4 (Corresponding to (F1) and (F3))

Every LLEE chart $\hat{\mathcal{G}}/\mathcal{G}$ has a provable solution $s$.
For any provable solutions $s_{1}$ and $s_{2}$ of $\mathcal{G}$,
$\operatorname{\mbox{$\vdash_{\textit{BBP}}$}}s_{1}(X)=s_{2}(X)$ for any node
$X$ of $\mathcal{G}$.

##  3 Looping-back Charts and Images

As illustrated in Fig. 1 of Sect. 1, our proof method focuses on stage (II’)
of the minimization strategy, which concerns how to acquire an LLEE
bisimulation collapse $\mathcal{H}$ from one of two bisimulation functions:
$\theta_{1}$ from $\mathcal{G}_{e_{1}}$ to $\mathcal{H}$ and $\theta_{2}$ from
$\mathcal{G}_{e_{2}}$ to $\mathcal{H}$. In this section, we introduce the
basic concepts needed for the proofs given in Sect. 4.

###  3.1 Some Conventions of Notations

In the rest of the paper, for convenience, we use the conventions of notations
stated as follows.

Given a chart $\mathcal{G}$, we often use $V_{\mathcal{G}}$,
$A_{\mathcal{G}}$, $s_{\mathcal{G}}$ and $\operatorname{\to}_{\mathcal{G}}$ to
represent its components. We usually ignore the initial state
$s_{\mathcal{G}}\in V_{\mathcal{G}}$ and simply understand a chart $\langle
V_{\mathcal{G}},A_{\mathcal{G}},s_{\mathcal{G}},\operatorname{\to}_{\mathcal{G}},\surd\rangle$
as a 4-tuple: $\langle
V_{\mathcal{G}},A_{\mathcal{G}},\operatorname{\to}_{\mathcal{G}},\surd\rangle$.
This is because in our work, we do not need to distinguish the initial nodes
to relate to the concepts like chart interpretation and primary solution.

Given a set of nodes $N\subseteq V_{\mathcal{G}}$ of a chart $\mathcal{G}$,
$\textbf{G}_{\mathcal{G}}(N)$ (or simply $\textbf{G}(N)$ when $\mathcal{G}$ is
clear in the context) denotes the _chart of a set $N$ of nodes_ which consists
of all nodes and all transitions between these nodes. Formally,
$\textbf{G}_{\mathcal{G}}(N)=_{\textit{df}}\langle
N,A_{\mathcal{G}},\operatorname{\to},\surd\rangle$, where
$\operatorname{\to}=\\{X\xrightarrow{a}Y\ |\ X,Y\in N,a\in
A_{\mathcal{G}}\\}$. $\textbf{G}(\cdot)$ is often used as an abbreviation of a
sub-chart by its set of nodes.

We define
$\mathcal{A}_{1}\operatorname{\cup_{C}}\mathcal{A}_{2}=_{\textit{df}}\textbf{G}_{\mathcal{G}}(V_{\mathcal{A}_{1}}\cup
V_{\mathcal{A}_{2}})$ as the chart of the union of the nodes of
$\mathcal{A}_{1}$ and $\mathcal{A}_{2}$, provided that $\mathcal{A}_{1}$ and
$\mathcal{A}_{2}$ are sub-charts of a chart $\mathcal{G}$. We write
$\mathcal{G}\operatorname{\subseteq_{C}}\mathcal{H}$ (resp.
$\mathcal{G}\operatorname{\subset_{C}}\mathcal{H}$) if $\mathcal{G}$ is a sub-
chart (resp. proper sub-chart) of $\mathcal{H}$, and write
$\mathcal{G}\operatorname{\equiv_{C}}\mathcal{H}$ if charts $\mathcal{G}$ and
$\mathcal{H}$ are identical.

Given a bisimulation function $\theta:V_{\mathcal{G}}\to V_{\mathcal{H}}$ from
chart $\mathcal{G}$ to $\mathcal{H}$ and a sub-chart $\mathcal{A}$ of
$\mathcal{G}$, we use $\theta(\mathcal{A})$ to represent the sub-chart
$\textbf{G}_{\mathcal{H}}(\theta(V_{\mathcal{A}}))$ of the set
$\theta(V_{\mathcal{A}})$ of nodes of $\mathcal{H}$.

We usually use small alphabets like $x,y,z,...$ to represent nodes in a domain
$V_{\mathcal{G}}$, while using capital alphabets like $X,Y,Z,...$ to express
nodes in a co-domain $V_{\mathcal{H}}$, of a bisimulation relation
$\mathfrak{R}:V_{\mathcal{G}}\to V_{\mathcal{H}}$ from $\mathcal{G}$ to
$\mathcal{H}$. And we use the small and capital alphabets with the same name
and subscript, but different superscripts to express bisimular nodes in these
two graphs. For example, we can write bisimular-nodes as:
$x,x^{\prime},x^{\prime\prime},x^{(3)}$ in $\mathcal{G}$, and write bisimular
nodes $X,X^{\prime},X^{\prime\prime},X^{(3)}$ in $\mathcal{H}$, which are
bisimular to $x$.

###  3.2 Looping-back Charts

We first introduce an LLEE sub-structure called _looping-back charts_. It
together with its images defined in Sect. 3.3 plays the central role in our
method.

######  Definition 1 (Looping-back Chart)

The looping-back chart of an LLEE chart $\hat{\mathcal{G}}/\mathcal{G}$ w.r.t.
a node $x$, denoted by $\mathcal{L}_{x}$, is a chart defined as
$\mathcal{L}_{x}=_{\textit{df}}\textbf{G}_{\mathcal{G}}(\\{x\\}\cup\\{y\ |\
x\operatorname{\curvearrowright}^{+}y\\})$ and satisfying that
$\mathcal{L}_{x}$ contains at least one loop.

Call $x$ the “starting node” of $\mathcal{L}_{x}$.

Note that the stipulation that $\mathcal{L}_{x}$ must contain at least one
loop forbids trivial charts of the form:
$\langle\\{x\\},A,x,\emptyset,\surd\rangle$ as looping-back charts, which
contain only one node $x$ without any transitions.

A sub-chart $\mathcal{B}$ of a looping-back chart $\mathcal{A}$ is also called
a _looping-back sub-chart_ if it is a looping-back chart. Call
$V_{\mathcal{L}_{x}}/\\{x\\}$ the _body_ of looping-back chart
$\mathcal{L}_{x}$.

For instance, in the LLEE chart $\hat{\mathcal{E}_{2}}/\mathcal{E}_{2}$ of
Fig. 5, charts $\textbf{G}(\\{z^{\prime},x^{\prime}\\})_{z^{\prime}}$,
$\textbf{G}(\\{z^{\prime\prime},y\\})_{z^{\prime\prime}}$,
$\textbf{G}(\\{x,z^{\prime\prime},k,y\\})_{x}$ and the whole chart
$(\mathcal{E}_{2})_{z}$ are looping-back charts. Among them note that charts
$\textbf{G}(\\{z^{\prime},x^{\prime}\\})_{z^{\prime}}$ and
$\textbf{G}(\\{z^{\prime\prime},y\\})_{z^{\prime\prime}}$ are also loop sub-
charts of $\mathcal{E}_{2}$.

$\underline{z}$$\underline{x}$$\underline{z^{\prime}}$$\underline{x^{\prime}}$$\underline{k}$$\underline{z^{\prime\prime}}$$\underline{y}$$\hat{\mathcal{E}_{2}}/\mathcal{E}_{2}$$[3]$$a_{2}$$[2]$$a_{1}$$b_{1}$$a_{1}$$[1]$$a_{2}$$b_{1}$$[2]$$b_{1}$$a_{2}$$[1]$$a_{3}$$d_{1}$$[3]$$a_{3}$$[1]$$a_{1}$$a_{4}$$d_{2}$$[3]$$a_{4}$$a_{3}$$a_{4}$$\underline{Z}$$\underline{X}$$\underline{Y}$$\underline{K}$$\mathcal{E}_{1}$$a_{2}$$b_{1}$$a_{3}$$d_{1}$$a_{1}$$a_{4}$$d_{2}$$\theta$$\underline{Z}$$\underline{X}$$\underline{Y}$$\underline{K}$$\hat{\mathcal{E}_{1}}/\mathcal{E}_{1}$$[2]$$a_{2}$$[3]$$b_{1}$$[1]$$a_{3}$$d_{1}$$[1]$$a_{1}$$a_{4}$$d_{2}$

Figure 5: An example of images

The following properties about looping-back charts are straightforward from
LLEE charts.

###### Proposition 5

Given a looping-back chart $\mathcal{A}_{X}$ of an LLEE chart
$\hat{\mathcal{G}}/\mathcal{G}$, the following propositions hold:

  1. (i)

For any node $Y\in V_{\mathcal{A}_{X}}/\\{X\\}$ and the looping-back chart
$\mathcal{B}_{Y}$ (if there is one),
$\mathcal{B}_{Y}\operatorname{\subset_{C}}\mathcal{A}_{X}$;

  2. (ii)

There is no transition $Y\xrightarrow{}Z$ such that $Y\in
V_{\mathcal{A}_{X}}/\\{X\\}$ and $Z\notin V_{\mathcal{A}_{X}}$.

  3. (iii)

Any node $Y\in V_{\mathcal{A}_{X}}/\\{X\\}$ does not reach $\surd$ before
returning to $X$.

###### Proof

(i): By the transitivity of $\operatorname{\curvearrowright}^{+}$ indicated by
Prop. 1, for any $Z$ such that $Y\operatorname{\curvearrowright}^{+}Z$, since
$X\operatorname{\curvearrowright}^{+}Y$,
$X\operatorname{\curvearrowright}^{+}Z$. So $V_{\mathcal{B}_{Y}}\subseteq
V_{\mathcal{A}_{X}}$. By Def. 1,
$\mathcal{B}_{Y}\operatorname{\subseteq_{C}}\mathcal{A}_{X}$. If
$\mathcal{B}_{Y}\operatorname{\equiv_{C}}\mathcal{A}_{X}$, since
$Y\not\\!\\!\operatorname{\equiv}X$, Prop. 1 is violated. Because we have both
$X\operatorname{\curvearrowright}^{+}Y$ and
$Y\operatorname{\curvearrowright}^{+}X$. Hence
$\mathcal{B}_{Y}\operatorname{\subset_{C}}\mathcal{A}_{X}$.

(ii): Assume a transition $Y\xrightarrow{}Z$ with $Y\in
V_{\mathcal{A}_{X}}/\\{X\\}$ but $Z\notin V_{\mathcal{A}_{X}}$. Let
$X\operatorname{\curvearrowright}^{+}K\operatorname{\curvearrowright}Y$ for
some node $K$. Then by the definition of relation
$\operatorname{\curvearrowright}$ (Sect. 2.3), depending on whether
$Y\xrightarrow{}Z$ is a loop-entry or a body transition, we have either
$K\operatorname{\curvearrowright}Y\operatorname{\curvearrowright}Z$ or
$K\operatorname{\curvearrowright}Z$. So
$X\operatorname{\curvearrowright}^{+}K\operatorname{\curvearrowright}^{+}Z$.
But by Def. 5, $Z\in V_{\mathcal{A}_{X}}$. This leads to contradiction.

(iii): By Def. 1, for any node $Y\in V_{\mathcal{A}_{X}}/\\{X\\}$,
$X\operatorname{\curvearrowright}^{+}Y$. Proceed by induction on relation
$\operatorname{\curvearrowright}^{+}$.

Base case: Consider a node $Y$ with $X\operatorname{\curvearrowright}Y$. By
the definition of relation $\operatorname{\curvearrowright}$ and the LEE
property (Sect. 2.3), $Y$ is in the body of a sub-chart that is or will become
a loop sub-chart starting from $X$ during the elimination process indicated by
$\hat{\mathcal{G}}$. By (L3), $Y$ cannot reach $\surd$ before returning to
$X$.

Step case: Consider a node $Y$ such that
$X\operatorname{\curvearrowright}^{+}K\operatorname{\curvearrowright}Y$ for
some node $K$. Similarly, by the definition of relation
$\operatorname{\curvearrowright}$ and the LEE property, $Y$ is in the body of
a sub-chart that is or will become a loop sub-chart starting from $K$ during
the elimination process indicated by $\hat{\mathcal{G}}$. By (L3), $Y$ cannot
reach $\surd$ before returning to $K$. By induction hypothesis, $K$ cannot
reach $\surd$ before returning to $X$. Therefore, $Y$ cannot reach $\surd$
before returning to $X$. ∎

###  3.3 Images and Well-structured Pre-images

######  Definition 2 (Image)

Given a bisimulation function $\theta:V_{\hat{\mathcal{G}}/\mathcal{G}}\to
V_{\mathcal{H}}$ from an LLEE chart $\hat{\mathcal{G}}/\mathcal{G}$ to a
bismulation collapse $\mathcal{H}$, a sub-chart $\mathcal{I}$ of $\mathcal{H}$
is called an ‘image’, if there exists a looping-back chart $\mathcal{L}_{x}$
in $\mathcal{G}$ such that
$\mathcal{I}\operatorname{\equiv_{C}}\theta(\mathcal{L}_{x})=\textbf{G}_{\mathcal{H}}(\theta(V_{\mathcal{L}_{x}}))$.

Also call $\mathcal{I}$ “the image of $\mathcal{L}_{x}$” for each such
$\mathcal{L}_{x}$, and call $\mathcal{L}_{x}$ a ‘pre-image’ of $\mathcal{I}$.

Denote by $\mathcal{I}_{\theta}(\mathcal{H})$ the set of all images on
$\mathcal{H}$ (w.r.t. $\theta$).

Call $V_{\theta(\mathcal{L}_{x})}/\\{\theta(x)\\}$ the _body_ of image
$\theta(\mathcal{L}_{x})$ w.r.t. a pre-image $\mathcal{L}_{x}$.

An image can have more than one pre-image. Different images can overlap each
other in the sense that they share same nodes and transitions.

For example, Fig. 5 shows the bisimulation function
$\theta:V_{\hat{\mathcal{E}_{2}}/{\mathcal{E}_{2}}}\to V_{\mathcal{E}_{1}}$
from an LLEE chart $\hat{\mathcal{E}_{2}}/\mathcal{E}_{2}$ to its bisimulation
collapse $\mathcal{E}_{1}$. According to Sect. 3.1, the nodes with the same
alphabets (e.g. $x,x^{\prime}$ and $X$) are bisimular to each other. In this
example, there are totally 3 images on $\mathcal{E}_{1}$: $\mathcal{E}_{1}$,
$\textbf{G}(\\{Z,X\\})$ and $\textbf{G}(\\{Z,Y\\})$. Among them image
$\mathcal{E}_{1}$ has both looping-back charts $({\mathcal{E}_{2}})_{z}$ and
$\textbf{G}(\\{x,z^{\prime\prime},k,y\\})_{x}$ as its pre-images; image
$\textbf{G}(\\{Z,X\\})$ has the pre-image
$\textbf{G}(\\{z^{\prime},x^{\prime}\\})_{z^{\prime}}$; image
$\textbf{G}(\\{Z,Y\\})$ has the pre-image
$\textbf{G}(\\{z^{\prime\prime},y\\})_{z^{\prime\prime}}$. Images
$\textbf{G}(\\{Z,X\\})$ and $\textbf{G}(\\{Z,Y\\})$ are proper sub-images of
image $\mathcal{E}_{1}$. $\textbf{G}(\\{Z,X\\})$ and $\textbf{G}(\\{Z,Y\\})$
are not sub-images of each other but overlap each other.

A bisimulation function is monotonic w.r.t. sub-chart relation in the
following sense.

###### Proposition 6

A bisimulation function $\theta:V_{\hat{\mathcal{G}}/\mathcal{G}}\to
V_{\mathcal{H}}$ satisfies that
$\mathcal{A}_{1}\operatorname{\subseteq_{C}}\mathcal{A}_{2}$ implies
$\theta(\mathcal{A}_{1})\operatorname{\subseteq_{C}}\theta(\mathcal{A}_{2})$
for any sub-charts $\mathcal{A}_{1}$ and $\mathcal{A}_{2}$ of $\mathcal{G}$.

######  Proof (Proof Sketch)

$\mathcal{A}_{1}\operatorname{\subseteq_{C}}\mathcal{A}_{2}$ means
$V_{\mathcal{A}_{1}}\subseteq V_{\mathcal{A}_{2}}$. So
$\theta(V_{\mathcal{A}_{1}})\subseteq\theta(V_{\mathcal{A}_{2}})$. By the
definition of $\textbf{G}(\cdot)$ in Sect. 3.1, clearly
$\textbf{G}(\theta(V_{\mathcal{A}_{1}}))\operatorname{\subseteq_{C}}\textbf{G}(\theta(V_{\mathcal{A}_{2}}))$.
∎

Below we propose a critical property for images, called _well-structuredness_
, based on which we will show in Sect. 4 that we manage to directly determine
an LEE structure on images.

######  Proposition 7 (Well-structuredness)

Given a bisimulation function $\theta:V_{\hat{\mathcal{G}}/\mathcal{G}}\to
V_{\mathcal{H}}$ from an LLEE chart $\hat{\mathcal{G}}/\mathcal{G}$ to its
bisimulation collapse $\mathcal{H}$, for any image $\mathcal{I}$ of
$\mathcal{I}_{\theta}(\mathcal{H})$, there exists a looping-back chart
$\mathcal{L}_{x}$ as a pre-image of $\mathcal{I}$ such that for any
$\mathcal{L}_{y}\operatorname{\subset_{C}}\mathcal{L}_{x}$,
$\theta(\mathcal{L}_{y})\operatorname{\subset_{C}}\theta(\mathcal{L}_{x})\operatorname{\equiv_{C}}\mathcal{I}$.

We say $\mathcal{L}_{x}$ is ‘well structured’ (w.r.t. $\theta$), and call
$\mathcal{L}_{x}$ a “well-structured pre-image” of image $\mathcal{I}$.

The proof of Prop. 7 is trivial according to the condition in Prop. 7. We only
give a sketch of the proof as follows.

######  Proof (Proof of Prop. 7 (Sketch))

If a pre-image $\mathcal{L}_{x}$ of $\mathcal{I}$ is not well structured,
which means there exists a proper looping-back sub-chart $\mathcal{L}_{y}$ of
$\mathcal{L}_{x}$ such that
$\theta(\mathcal{L}_{y})\operatorname{\equiv_{C}}\theta(\mathcal{L}_{x})\operatorname{\equiv_{C}}\mathcal{I}$,
then $\mathcal{L}_{y}$ itself is a pre-image of $\mathcal{I}$. By that
$\operatorname{\subseteq_{C}}$ is a well-founded relation, we can always
obtain a well-structured pre-image for $\mathcal{I}$. ∎

In Fig. 5, the looping-back chart $({\mathcal{E}_{2}})_{z}$, as a pre-image of
image $\mathcal{E}_{1}$, is not well structured, since
$\textbf{G}(\\{x,z^{\prime\prime},k,y\\})_{x}\operatorname{\subset_{C}}(\mathcal{E}_{2})_{z}$
but
$\theta(\textbf{G}(\\{x,z^{\prime\prime},k,y\\})_{x})\operatorname{\equiv_{C}}\mathcal{E}_{1}\operatorname{\equiv_{C}}\theta((\mathcal{E}_{2})_{z})$.
However, chart $\textbf{G}(\\{x,z^{\prime\prime},k,y\\})_{x}$ is a well-
structured pre-image of image $\mathcal{E}_{1}$ w.r.t. $\theta$.

Prop. 7 guides us to consider the relation between an image and its well-
structured pre-images as looping-back charts.

##  4 Image Reflection on LLEE Charts

In this section, we give our proof of the completeness of BBP. This is
realized mainly by discussing the relation between images and their well-
structured pre-images as looping-back charts. We call that an image can
_reflect_ the LLEE structure of its well-structured pre-images, in the sense
that the image has an LEE structure (called _LEE sub-chart_ as defined below)
enforced by the LLEE sturcture of its well-structured pre-images.

The main result of this section is Theorem 4.1, which relies on Prop. 8 and
Lemma 1.

######  Definition 3 (LEE Sub-Chart)

A sub-chart $\mathcal{A}$ of a chart $\mathcal{G}$ is called an “LEE sub-
chart” if it is an LEE chart.

In a chart, by the definition of loop sub-chart (Sect. 2.3), every loop sub-
chart is an LEE sub-chart. Note that a chart has an LEE sub-chart does not
mean itself is an LEE chart.

Given the bisimulation collapse $\mathcal{H}$ of an LLEE chart $\mathcal{G}$
with a bisimulation function $\theta:V_{\hat{\mathcal{G}}/\mathcal{G}}\to
V_{\mathcal{H}}$, the main idea of our proof is that through $\theta$, the
behaviour of each image $\theta(\mathcal{L}_{x})$ of
$\mathcal{I}_{\theta}(\mathcal{H})$ is constrained by the behaviour of its
well-structured pre-image $\mathcal{L}_{x}$ so that $\theta(\mathcal{L}_{x})$
is in fact an LEE sub-chart of $\mathcal{H}$: By the sub-image relation
between images, we show that there exists an elimination process by which each
image $\theta(\mathcal{L}_{x})$ will eventually become a loop sub-chart itself
and thus can be eliminated further. By eliminating all the images as LEE sub-
charts of $\mathcal{H}$, we show that there would be no loops left in
$\mathcal{H}$ because the images of $\mathcal{I}_{\theta}(\mathcal{H})$ cover
all the loops of $\mathcal{H}$.

We use an example to illustrate our idea. Consider the chart $\mathcal{E}_{1}$
(Fig. 4, Fig. 5). The set of its images is
$\mathcal{I}_{\theta}(\mathcal{E}_{1})=\\{\mathcal{E}_{1},\textbf{G}(\\{Z,X\\}),\textbf{G}(\\{Z,Y\\})\\}$.
To prove $\mathcal{E}_{1}$ is an LEE chart, we conduct the following two steps
of reasoning in an inside-out manner w.r.t. the sub-image relation:

  * •

Firstly, for the minimum image
$\textbf{G}(\\{Z,Y\\})\operatorname{\equiv_{C}}\theta(\textbf{G}(\\{z^{\prime\prime},y\\})_{z^{\prime\prime}})$,
we see that $\textbf{G}(\\{Z,Y\\})$ is a loop sub-chart (so is an LEE sub-
chart) and can be eliminated in $\mathcal{E}_{1}$: As constrained by its well-
structured pre-image
$\textbf{G}(\\{z^{\prime\prime},y\\})_{z^{\prime\prime}}$, both loops
$Z\xrightarrow{a_{1}}Z$ and $Z\xrightarrow{a_{3}}Y\xrightarrow{d_{1}}Z$ pass
through $Z$ and each path in $\textbf{G}(\\{Z,Y\\})$ from $Z$ stays in
$\textbf{G}(\\{Z,Y\\})$ before returning to $Z$. Similarly, another minimum
image $\textbf{G}(\\{Z,X\\})$ can also be eliminated because it is a loop sub-
chart of $\mathcal{E}_{1}$.

  * •

Secondly, consider the image $\mathcal{E}_{1}$ which has images
$\textbf{G}(\\{Z,Y\\})$ and $\textbf{G}(\\{Z,X\\})$ as its two proper sub-
images. After $\textbf{G}(\\{Z,Y\\})$ and $\textbf{G}(\\{Z,X\\})$ are
eliminated (in an order for example first $\textbf{G}(\\{Z,Y\\})$ and then
$\textbf{G}(\\{Z,X\\})$), the remnant chart: chart
$\mathcal{E}_{1}^{\prime\prime}$ of Fig. 4, becomes a loop sub-chart and thus
can be eliminated. This is because its only loop
$X\xrightarrow{b_{1}}Z\xrightarrow{a_{4}}K\xrightarrow{d_{2}}X$, constrained
by the well-structured pre-image
$\textbf{G}(\\{x,z^{\prime\prime},k,y\\})_{x}$, passes through $X$ and each
path from $X$ stays in $\mathcal{E}_{1}^{\prime\prime}$ before returning to
$X$. Therefore, the image $\mathcal{E}_{1}$ is an LEE sub-chart (of itself).

Since $\mathcal{I}_{\theta}(\mathcal{E}_{1})$ covers all the loops of
$\mathcal{E}_{1}$, after eliminating $\mathcal{E}_{1}^{\prime\prime}$, we
obtain the chart $\mathcal{E}_{1}^{(3)}$ of Fig. 4 where there is no loops.
Therefore, the whole chart $\mathcal{E}_{1}$ is an LEE chart.

Following the main idea, below we give our formal proofs.

Prop. 8 indicates a correspondence between the loops of an LLEE chart
$\mathcal{G}$ and the loops of its bisimulation collapse $\mathcal{H}$ given a
bisimulation function $\theta:V_{\hat{\mathcal{G}}/\mathcal{G}}\to
V_{\mathcal{H}}$.

###### Proposition 8

Given a bisimulation function $\theta:V_{\hat{\mathcal{G}}/\mathcal{G}}\to
V_{\mathcal{H}}$ from an LLEE chart $\mathcal{G}$ to its bisimulation collapse
$\mathcal{H}$ and a loop $\mathcal{A}$ of $\mathcal{H}$, from a node $x$ of
$\mathcal{G}$ such that $\theta(x)$ is in $\mathcal{A}$, there exists a path
$\mathcal{S}$ reaching a loop $\mathcal{D}$ in $\mathcal{G}$ satisfying that
$\mathcal{A}\operatorname{\equiv_{C}}\theta(\mathcal{S}\operatorname{\cup_{C}}\mathcal{D})\operatorname{\equiv_{C}}\theta(\mathcal{D})$.

###### Proof

Assume loop $\mathcal{A}$ is of the form:
$X\xrightarrow{a_{1}}X_{1}\xrightarrow{a_{2}}...\xrightarrow{a_{n}}X_{n}\xrightarrow{a_{n+1}}X$
($n\geq 0$), with $X\operatorname{\equiv}\theta(x)$. From $x$, by the
bisimulation relation $\theta$ between $\mathcal{G}$ and $\mathcal{H}$, there
is a path of the form:
$x\xrightarrow{a_{1}}x_{1}\xrightarrow{a_{2}}...\xrightarrow{a_{n}}x_{n}\xrightarrow{a_{n+1}}x^{(1)}\xrightarrow{a_{1}}...\xrightarrow{a_{n+1}}x^{(k)}\xrightarrow{a_{1}}x^{(k)}_{1}\xrightarrow{a_{2}}...\xrightarrow{a_{n}}x^{(k)}_{n}\xrightarrow{a_{n+1}}x^{(k+1)}\xrightarrow{a_{1}}...$,
where $X_{i}\operatorname{\equiv}\theta(x^{(k)}_{i})$ for all $k\geq 1$ and
$1\leq i\leq n$, and $X\operatorname{\equiv}\theta(x^{(k)})$ for all $k\geq
1$. Since $\mathcal{G}$ is finite, we can always find the node $x^{(m)}$ with
the smallest $m>0$ such that $x^{(m)}\operatorname{\equiv}x^{(j)}$ for some
$1\leq j<m$. So from $x$ there is a path $\mathcal{S}$:
$x\xrightarrow{a_{1}}x_{1}\xrightarrow{a_{2}}...\xrightarrow{a_{n}}x_{n}\xrightarrow{a_{n+1}}x^{(1)}\xrightarrow{a_{1}}...\xrightarrow{a_{n+1}}x^{(j)}$
reaching the loop $\mathcal{D}$:
$x^{(j)}\xrightarrow{a_{1}}...\xrightarrow{a_{n+1}}x^{(m)}\operatorname{\equiv}x^{(j)}$.
And since $V_{\mathcal{A}}=\theta(V_{\mathcal{S}}\cup
V_{\mathcal{D}})=\theta(V_{\mathcal{D}})$, clearly
$\mathcal{A}\operatorname{\equiv_{C}}\theta(\mathcal{S}\operatorname{\cup_{C}}\mathcal{D})\operatorname{\equiv_{C}}\theta(\mathcal{D})$.
∎

###### Lemma 1

Given the set of images $\mathcal{I}_{\theta}(\mathcal{H})$ w.r.t. a
bisimulation function $\theta:V_{\hat{\mathcal{G}}/\mathcal{G}}\to
V_{\mathcal{H}}$ from an LLEE chart $\hat{\mathcal{G}}/\mathcal{G}$ to its
bisimulation collapse $\mathcal{H}$, the following conditions hold:

  1. (1)

For each loop $\mathcal{C}$ of $\mathcal{H}$, there exists an image
$\mathcal{I}$ of $\mathcal{I}_{\theta}(\mathcal{H})$ such that
$\mathcal{C}\operatorname{\subseteq_{C}}\mathcal{I}$;

  2. (2)

For each image $\theta(\mathcal{L}_{x})$ of
$\mathcal{I}_{\theta}(\mathcal{H})$ with a well-structured pre-image
$\mathcal{L}_{x}$, in $\theta(\mathcal{L}_{x})$ each loop either passes
through node $\theta(x)$ or is in a proper sub-image of
$\theta(\mathcal{L}_{x})$.

  3. (3)

For each image $\theta(\mathcal{L}_{x})$ of
$\mathcal{I}_{\theta}(\mathcal{H})$ with a pre-image $\mathcal{L}_{x}$, there
exists no transition $U\xrightarrow{}\surd$ such that $U\in
V_{\theta(\mathcal{L}_{x})}/\\{\theta(x)\\}$, and no transition
$U\xrightarrow{}W$ satisfying that $U\in
V_{\theta(\mathcal{L}_{x})}/\\{\theta(x)\\}$ and $W\notin
V_{\theta(\mathcal{L}_{x})}$.

Lemma 1 (1) states the coverage of the loops of $\mathcal{H}$ by
$\mathcal{I}_{\theta}(\mathcal{H})$. Lemma 1 (2) and (3) describe the
constrained relation between the behaviour of an image and that of any of its
well-structured pre-images. Lemma 1 (3) intuitively means that each path
starting from node $\theta(x)$ stays in $\theta(\mathcal{L}_{x})$ before
returning to $\theta(x)$.

######  Proof (Proof of Lemma 1)

(Proof of (1)). For each loop $\mathcal{C}$ of $\mathcal{H}$, by Prop. 8 there
is a loop $\mathcal{D}$ in $\mathcal{G}$ such that
$\mathcal{C}\operatorname{\equiv_{C}}\theta(\mathcal{D})$. Since $\mathcal{G}$
is an LLEE chart, $\mathcal{D}$ begins with a loop-entry transition in the
form: $x\xrightarrow{}_{[m]}\cdot\xrightarrow{}^{*}x$, $m>0$. By Def. 1,
$\mathcal{D}$ is a sub-chart of the looping-back chart $\mathcal{L}_{x}$. By
Prop. 6,
$\mathcal{C}\operatorname{\equiv_{C}}\theta(\mathcal{D})\operatorname{\subseteq_{C}}\theta(\mathcal{L}_{x})$.

(Proof of (2)). Let $\mathcal{C}$ be a loop of $\theta(\mathcal{L}_{x})$. By
Prop. 8, starting from a node $y$ in $\mathcal{L}_{x}$ such that $\theta(y)$
is in $\mathcal{C}$, there is a path $\mathcal{S}$ reaching a loop
$\mathcal{D}$ such that
$\mathcal{C}\operatorname{\equiv_{C}}\theta(\mathcal{S}\operatorname{\cup_{C}}\mathcal{D})$
(note that this loop $\mathcal{D}$ does not have to be a sub-chart of
$\mathcal{L}_{x}$). If $\mathcal{C}$ does not pass $\theta(x)$, then chart
$\mathcal{S}\operatorname{\cup_{C}}\mathcal{D}$ does not pass $x$, and $y\in
V_{\mathcal{L}_{x}}/\\{x\\}$. By Prop. 5 (ii) and (iii), since $y\in
V_{\mathcal{L}_{x}}/\\{x\\}$, loop $\mathcal{D}$ stays in $\mathcal{L}_{x}$
and is thus a sub-chart of $\mathcal{L}_{x}$. By that $\mathcal{G}$ is an LLEE
chart, loop $\mathcal{D}$ starts from a loop-entry transition
$k\xrightarrow{}_{[m]}\cdot$ with $m>0$. By Def. 1, it is not hard to see that
$\mathcal{D}$ must be a sub-chart of the looping-back chart $\mathcal{L}_{k}$.
So
$\mathcal{D}\operatorname{\subseteq_{C}}\mathcal{L}_{k}\operatorname{\subseteq_{C}}\mathcal{L}_{x}$.
Since $k\not\\!\\!\operatorname{\equiv}x$, by Prop. 5 (i),
$\mathcal{L}_{k}\operatorname{\subset_{C}}\mathcal{L}_{x}$. According to Prop.
7 and that $\mathcal{L}_{x}$ is well structured,
$\theta(\mathcal{L}_{k})\operatorname{\subset_{C}}\theta(\mathcal{L}_{x})$. So
$\mathcal{C}\operatorname{\equiv_{C}}\theta(\mathcal{S}\operatorname{\cup_{C}}\mathcal{D})\operatorname{\equiv_{C}}\theta(\mathcal{D})$
(by Prop. 8) $\operatorname{\subseteq_{C}}\theta(\mathcal{L}_{k})$ (by Prop.
6) $\operatorname{\subset_{C}}\theta(\mathcal{L}_{x})$. In other words,
$\mathcal{C}$ is in the proper sub-image $\theta(\mathcal{L}_{k})$ of
$\theta(\mathcal{L}_{x})$.

(Proof of (3)). We prove by contradiction. Assume there exists a transition
$U\xrightarrow{a}\surd$ such that $U\in
V_{\theta(\mathcal{L}_{x})}/\\{\theta(x)\\}$, or a transition
$U\xrightarrow{a}W$ such that $U\in
V_{\theta(\mathcal{L}_{x})}/\\{\theta(x)\\}$ but $W\notin
V_{\theta(\mathcal{L}_{x})}$. Let $u$ be the node in $\mathcal{L}_{x}$ such
that $\theta(u)\operatorname{\equiv}U$. Since $U\not\equiv\theta(x)$,
$u\not\equiv x$. So $u\in V_{\mathcal{L}_{x}}/\\{x\\}$. For the case of
$U\xrightarrow{a}\surd$, by Prop. 5 (iii), $u\not\xrightarrow{a}\surd$. So
this causes contradiction since $u\sim U$. For the case of
$U\xrightarrow{a}W$, there is a transition $u\xrightarrow{a}w$ such that
$\theta(w)\operatorname{\equiv}W$ and $w\notin V_{\mathcal{L}_{x}}$ (otherwise
$W\in V_{\theta(\mathcal{L}_{x})}$). But the fact that $u\in
V_{\mathcal{L}_{x}}/\\{x\\}$ and $w\notin V_{\mathcal{L}_{x}}$ violates Prop.
5 (ii). Therefore, transition $U\xrightarrow{a}W$ does not exist. ∎

######  Theorem 4.1 (Stage (II’))

For every bisimulation function $\theta:V_{\hat{\mathcal{G}}/\mathcal{G}}\to
V_{\mathcal{H}}$ from an LLEE chart $\hat{\mathcal{G}}/\mathcal{G}$ to a
bisimulation collapse $\mathcal{H}$, $\mathcal{H}$ is an LEE chart.

###### Proof

By the definition of LEE chart in Sect. 2.3, we show that there is an
elimination process on $\mathcal{H}$ by which $\mathcal{H}$ can be transformed
into a chart $\mathcal{H}^{\prime}$ without infinite paths. It is sufficient
to prove that each image of $\mathcal{I}_{\theta}(\mathcal{H})$ is an LEE sub-
chart of $\mathcal{H}$ by induction on the sub-image relations between images.
The elimination process on $\mathcal{H}$ can then be naturally induced by this
proof process.

Base case: Consider a minimum image $\mathcal{I}$ of
$\mathcal{I}_{\theta}(\mathcal{H})$ (in which there are no proper sub-images).
By Prop. 7, let $\mathcal{I}\operatorname{\equiv_{C}}\theta(\mathcal{L}_{r})$
for some $\mathcal{L}_{r}$ of its well-structured pre-images. If
$\theta(\mathcal{L}_{r})$ has at least one loop, we show that it is a loop
sub-chart of $\mathcal{H}$ (so is also an LEE sub-chart of $\mathcal{H}$).
(L1) is obvious since $\theta(\mathcal{L}_{r})$ has a loop. By Lemma 1 (2) and
that $\theta(\mathcal{L}_{r})$ is a minimum image, each loop in
$\theta(\mathcal{L}_{r})$ must pass through $\theta(r)$. By Lemma 1 (3), each
path in $\theta(\mathcal{L}_{r})$ starting from $\theta(r)$ cannot leave
$\theta(\mathcal{L}_{r})$ before returning to $\theta(r)$. So, for each
infinite path in $\theta(\mathcal{L}_{r})$ starting from $\theta(r)$, it can
only return to $\theta(r)$ after a finite number of transitions. That is, (L2)
holds. (L3) is direct from Prop. 5 (iii) satisfied by $\mathcal{L}_{r}$ and
the bisimulation relation $\theta$ itself.

Step case: Consider an arbitrary image $\mathcal{I}$ of
$\mathcal{I}_{\theta}(\mathcal{H})$. By Prop. 7, let
$\mathcal{I}\operatorname{\equiv_{C}}\theta(\mathcal{L}_{s})$ for some well-
structured pre-image $\mathcal{L}_{s}$. We show that $\theta(\mathcal{L}_{s})$
is an LEE sub-chart. By inductive hypothesis, each maximum proper sub-image
$\mathcal{I}^{\prime}$ of $\theta(\mathcal{L}_{s})$ is an LEE sub-chart. So
there exists an elimination process to eliminate each $\mathcal{I}^{\prime}$.
After eliminating all these sub-images, assume $\theta(\mathcal{L}_{s})$ is
transformed into a chart $(\theta(\mathcal{L}_{s}))^{\prime}$. By Lemma 1 (2),
all loops remained in $(\theta(\mathcal{L}_{s}))^{\prime}$ must pass through
$\theta(s)$. If $(\theta(\mathcal{L}_{s}))^{\prime}$ still has at least one
loop, then similarly as in the base case above, we show that
$(\theta(\mathcal{L}_{s}))^{\prime}$ is a loop sub-chart:

(L1) is obvious because $(\theta(\mathcal{L}_{s}))^{\prime}$ has a loop. By
Lemma 1 (3), each path in $\theta(\mathcal{L}_{s})$ cannot leave
$\theta(\mathcal{L}_{s})$ before returning to $\theta(s)$. So after the
eliminations, each path in the remnant $(\theta(\mathcal{L}_{s}))^{\prime}$
still cannot leave $(\theta(\mathcal{L}_{s}))^{\prime}$ before returning to
$\theta(s)$. By this and the fact that all loops in
$(\theta(\mathcal{L}_{s}))^{\prime}$ pass through $\theta(s)$ as obtained
above, it is easy to see that (L2) holds. (L3) is direct from Prop. 5 (iii)
satisfied by $\mathcal{L}_{s}$ and the bisimulation relation $\theta$ itself.

By that $(\theta(\mathcal{L}_{s}))^{\prime}$ is a loop sub-chart, it then can
be eliminated by an elimination process. So the whole image
$\theta(\mathcal{L}_{s})$ can be eliminated and is thus an LEE sub-chart.

Conclusion: Since each image is an LEE sub-chart of $\mathcal{H}$, as
indicated in the inductive reasoning above, we obtain an elimination process
that eliminates all images in $\mathcal{I}_{\theta}(\mathcal{H})$ in an
inside-out manner from the minimum sub-images according to the sub-image
relations. Let $\mathcal{H}^{\prime}$ be the chart $\mathcal{H}$ after the
elimination process. By Lemma 1 (1), there exists no loops left in
$\mathcal{H}^{\prime}$. So $\mathcal{H}^{\prime}$ is a chart without infinite
paths. ∎

$\underline{X}$$\underline{Y}$$\underline{Z}$$\underline{x}$$\underline{y}$$\underline{z}$$\underline{x^{\prime}}$$\underline{X}$$\underline{Y}$$\underline{Z}$$\underline{x}$$\underline{y}$$\underline{x^{\prime}}$$\underline{z}$$\underline{x^{\prime\prime}}$$\underline{y^{\prime}}$$\underline{x^{(3)}}$$a$$[1]$$a$$[1]$$c$$b$$b$$[2]$$a$$[1]$$a$$c$$b$$b$$a$$a$$a$$[1]$$c$$[2]$$b$$[2]$$b$$a$$[3]$$c$$a$$a$$b$$[2]$$b$$a$$a$$[1]$$c$$a$$\theta_{1}$$\theta_{2}$$\hat{\mathcal{E}_{3}}/\mathcal{E}_{3}$$\hat{\mathcal{E}_{3}}^{\prime}/\mathcal{E}_{3}$$\hat{\mathcal{E}_{4}}/\mathcal{E}_{4}$$\hat{\mathcal{E}_{5}}/\mathcal{E}_{5}$

Figure 6: An example of different image reflections by a same chart

In the above proof, for each image of $\mathcal{I}_{\theta}(\mathcal{H})$,
only one well-structured pre-image is needed to guarantee that the image is an
LEE sub-chart. The hierarchy structure of images indicated by the sub-image
relations between them is the key to determine the LEE elimination process on
$\mathcal{H}$.

For example, consider the chart $\mathcal{E}_{1}$ of Fig. 5. By the
elimination process of its images we have discussed earlier at the beginning
of this section, we obtained its LEE witness $\hat{\mathcal{E}_{1}}$ as also
shown on the left side in Fig. 5. In this example, image $\mathcal{E}_{1}$
reflects the LLEE structure of its well-structured pre-image
$\textbf{G}(\\{x,z^{\prime\prime},k,y\\})_{x}$; images $\textbf{G}(\\{Z,X\\})$
and $\textbf{G}(\\{Z,Y\\})$ reflect the LLEE structures of their well-
structured pre-images $\textbf{G}(\\{z^{\prime},x^{\prime}\\})_{z^{\prime}}$
and $\textbf{G}(\\{z^{\prime\prime},y\\})_{z^{\prime\prime}}$ respectively.

In fact, from Theorem 4.1, a bisimulation collapse $\mathcal{H}$ reflects the
LLEE structure of some parts of _any_ LLEE chart that has $\mathcal{H}$ as its
bisimulation collapse. This result coincides with the nature that an LLEE
chart can have multiple LEE/LLEE witnesses.

Consider another example firstly proposed in [9] as shown in Fig. 6. Given two
bisimulation functions
$\theta_{1}:V_{\hat{\mathcal{E}_{4}}/\mathcal{E}_{4}}\to V_{\mathcal{E}_{3}}$
and $\theta_{2}:V_{\hat{\mathcal{E}_{5}}/\mathcal{E}_{5}}\to
V_{\mathcal{E}_{3}}$ from LLEE charts $\mathcal{E}_{4}$ and $\mathcal{E}_{5}$
to their bisimulation collapse $\mathcal{E}_{3}$, $\mathcal{E}_{3}$ reflects
some parts of the LLEE structures of both $\mathcal{E}_{4}$ and
$\mathcal{E}_{5}$: $\mathcal{E}_{3}$ with the left witness
$\hat{\mathcal{E}_{3}}$ reflects the LLEE structure of the looping-back chart
$\textbf{G}(\\{y,z,x^{\prime}\\})_{y}$ of $\mathcal{E}_{4}$, whereas
$\mathcal{E}_{3}$ with the right witness $\hat{\mathcal{E}_{3}}^{\prime}$
reflects the LLEE structure of the looping-back chart
$\textbf{G}(\\{z,x^{\prime\prime},y^{\prime},x^{(3)}\\})_{z}$ of
$\mathcal{E}_{5}$. In our method, the different witnesses of
$\hat{\mathcal{E}_{3}}$ and $\hat{\mathcal{E}_{3}}^{\prime}$ come from
different structures of images on $\mathcal{E}_{3}$ through two different
bisimulation functions $\theta_{1}$ and $\theta_{2}$.

Now we illustrate that Theorem 4.1 is a result no weaker than the one obtained
in stage (II).

As stated in Sect. 2.3, not all LEE witnesses are LLEE witnesses. The
following property was firstly obtained in [7].

######  Proposition 9 ([7, 10])

Each LEE chart is also an LLEE chart.

Though not giving an explicit proof, [7] pointed out that a proof can be
obtained by showing that each LEE witness $\hat{\mathcal{G}}$ of $\mathcal{G}$
can be transformed into an LLEE witness $\hat{\mathcal{G}}^{\prime}$ so that
$\hat{\mathcal{G}}^{\prime}/\mathcal{G}$ satisfies the LLEE property. Here, we
give our version of the proof as below.

######  Proof (Proof of Prop. 9)

Assume $\hat{\mathcal{G}}/\mathcal{G}$ is an LEE chart with
$\hat{\mathcal{G}}$ an LEE witness. We obtain an LLEE witness
$\hat{\mathcal{G}}^{\prime}$ from $\hat{\mathcal{G}}$ by induction on the LEE
elimination process according to $\hat{\mathcal{G}}$. In the following proof,
without loss of generality, assume that every loop-entry transition has an
unique order number, starting from the smallest number $1$. We denote by
$\mathcal{D}(X\xrightarrow{}Y)$ a loop starting from transition
$X\xrightarrow{}Y$. We simply use $\langle X,\mathbf{E}\rangle$ to denote a
$\langle X,\mathbf{E}\rangle$-generated chart of $\mathcal{G}$.

Base case: Consider the $\langle
R_{1},\\{R_{1}\xrightarrow{}_{[1]}\cdot\\}\rangle$-generated chart with
$R_{1}\xrightarrow{}_{[1]}\cdot$ the smallest loop-entry transition. By LEE
property, $\langle R_{1},\\{R_{1}\xrightarrow{}_{[1]}\cdot\\}\rangle$ is a
loop sub-chart. For each loop-entry transition $X\xrightarrow{}_{[k]}\cdot$
from the body of chart $\langle
R_{1},\\{R_{1}\xrightarrow{}_{[1]}\cdot\\}\rangle$ with $k>1$ (thus violating
the LLEE property), we turn $X\xrightarrow{}_{[k]}\cdot$ into a body
transition: $X\xrightarrow{}_{[0]}\cdot$. For each loop
$\mathcal{D}(X\xrightarrow{}_{[0]}\cdot)$ that becomes a loop without loop-
entry transitions because of the transforming from
$X\xrightarrow{}_{[k]}\cdot$ to $X\xrightarrow{}_{[0]}\cdot$, since
$X\xrightarrow{}_{[0]}\cdot$ is from the body of $\langle
R_{1},\\{R_{1}\xrightarrow{}_{[1]}\cdot\\}\rangle$, by that $\langle
R_{1},\\{R_{1}\xrightarrow{}_{[1]}\cdot\\}\rangle$ is a loop sub-chart and
(L2), $\mathcal{D}(X\xrightarrow{}_{[0]}\cdot)$ must pass through $R_{1}$. Let
$\mathcal{D}(X\xrightarrow{}_{[0]}\cdot)$ be the form of:
$X\xrightarrow{}_{[0]}\cdot\xrightarrow{}^{*}R_{1}\xrightarrow{}Z_{1}\xrightarrow{}^{*}X$.
We then turn transition $R_{1}\xrightarrow{}Z_{1}$ into a loop-entry
transition $R_{1}\xrightarrow{}_{[k]}Z_{1}$. It is not hard to see that after
the loop-entry-transition-switching process described above for each
$X\xrightarrow{}_{[k]}\cdot$ with $k>1$, all transitions
$\cdot\xrightarrow{}_{[k]}\cdot$ from the body of $\langle
R_{1},\\{R_{1}\xrightarrow{}_{[1]}\cdot\\}\rangle$ are body transitions with
$k=0<1$.

Step case: Consider a $\langle
R_{n},\\{R_{n}\xrightarrow{}_{[n]}\cdot\\}\rangle$-generated chart starting
from a loop-entry transition $R_{n}\xrightarrow{}_{[n]}\cdot$ with $n>1$. By
induction hypothesis, in any $\langle
R_{l},\\{R_{l}\xrightarrow{}_{[l]}\cdot\\}\rangle$-generated chart with $l<n$,
any transition $\cdot\xrightarrow{}_{[o]}\cdot$ from the body of $\langle
R_{l},\\{R_{l}\xrightarrow{}_{[l]}\cdot\\}\rangle$ satisfies that $o<l$. For
each loop-entry transition $X\xrightarrow{}_{[k]}\cdot$ from the body of
$\langle R_{n},\\{R_{n}\xrightarrow{}_{[n]}\cdot\\}\rangle$ satisfying $k>n$,
we turn $X\xrightarrow{}_{[k]}\cdot$ into a body transition:
$X\xrightarrow{}_{[0]}\cdot$. For each loop
$\mathcal{D}(X\xrightarrow{}_{[0]}\cdot)$ that becomes a loop without loop-
entry transitions because of the transforming from
$X\xrightarrow{}_{[k]}\cdot$ to $X\xrightarrow{}_{[0]}\cdot$, we see that loop
$\mathcal{D}(X\xrightarrow{}_{[0]}\cdot)$ must pass through $R_{n}$. Because
by the LEE property, after eliminating all loop-entry transitions with an
order number $l<n$, chart $\langle
R_{n},\\{R_{n}\xrightarrow{}_{[n]}\cdot\\}\rangle$ becomes a loop sub-chart,
denoted by $\langle
R_{n},\\{R_{n}\xrightarrow{}_{[n]}\cdot\\}\rangle^{\prime}$. Since
$X\xrightarrow{}_{[k]}\cdot$ is not from the body of any chart $\langle
R_{l},\\{R_{l}\xrightarrow{}_{[l]}\cdot\\}\rangle$ with $l<n$ (by inductive
hypothesis above), loop $\mathcal{D}(X\xrightarrow{}_{[0]}\cdot)$ is still not
eliminated in $\langle
R_{n},\\{R_{n}\xrightarrow{}_{[n]}\cdot\\}\rangle^{\prime}$. So by (L2),
$\mathcal{D}(X\xrightarrow{}_{[0]}\cdot)$ passes through $R_{n}$. Let
$\mathcal{D}(X\xrightarrow{}_{[0]}\cdot)$ be of the form:
$X\xrightarrow{}_{[0]}\cdot\xrightarrow{}^{*}R_{n}\xrightarrow{}Z_{n}\xrightarrow{}^{*}X$,
then we turn the body transition $R_{n}\xrightarrow{}Z_{n}$ into a loop-entry
transition $R_{n}\xrightarrow{}_{[k]}Z_{n}$. After the loop-entry-transition-
switching process described above for each $X\xrightarrow{}_{[k]}\cdot$, we
see that all transitions $\cdot\xrightarrow{}_{[k]}\cdot$ from the body of
$\langle R_{n},\\{R_{n}\xrightarrow{}_{[n]}\cdot\\}\rangle$ satisfy that
$k<n$.

By the LLEE property, the witness $\hat{\mathcal{G}}^{\prime}$ obtained after
the transformations above is the LLEE witness as required. ∎

As an example, see the LEE chart
$\hat{\mathcal{E}_{1}}^{\prime}/\mathcal{E}_{1}$ with witness
$\hat{\mathcal{E}_{1}}^{\prime}$ in Fig. 4, which is an LLEE witness. From the
LEE witness $\hat{\mathcal{E}_{1}}$, we first turn the loop-entry transition
$X\xrightarrow{b_{1}}_{[3]}Z$ from the body of the $\langle
Z,\\{Z\xrightarrow{a_{2}}_{[2]}X\\}\rangle$-generated chart that violates the
LLEE property into a body transition $X\xrightarrow{b_{1}}_{[0]}Z$. This
causes loop $X\xrightarrow{b_{1}}Z\xrightarrow{a_{4}}K\xrightarrow{d_{2}}X$
become a loop without loop-entry transitions. Then we turn transition
$Z\xrightarrow{a_{4}}K$ into a loop-entry transition
$Z\xrightarrow{a_{4}}_{[3]}K$. By this loop-entry-transition-switching process
we transform $\hat{\mathcal{E}_{1}}$ into an LLEE witness
$\hat{\mathcal{E}_{1}}^{\prime}$.

We obtain the same result as in stage (II) as follows. It is straightforward
by Prop. 9 and Theorem 4.1.

######  Corollary 1 ([9])

For every bisimulation function $\theta:V_{\hat{\mathcal{G}}/\mathcal{G}}\to
V_{\mathcal{H}}$ from an LLEE chart $\hat{\mathcal{G}}/\mathcal{G}$ to a
bisimulation collapse $\mathcal{H}$, $\mathcal{H}$ is an LLEE chart.

##  5 Conclusion and Future Work

In this paper, we mainly propose an alternative proof for the completeness of
BBP for 1-free regular expressions modulo bisimulation equivalence. The
novelty of our method compared to the previous one lies in the part (stage
(II)) for showing the LLEE structure of a bisimulation collapse in the
minimization strategy. We propose a different approach by utilizing a
phenomenon we call “image reflection” that each image on the bisimulation
collapse of an LLEE chart is actually an LEE sub-chart enforced by its
corresponding well-structured looping-back charts of the LLEE chart, which we
also call that the image ‘reflects’ the LLEE structure of the LLEE chart.

Previous work further extended LEE/LLEE charts to characterize regular
expressions modulo bisimulation equivalence by introducing a silent (without
doing any action) _1-transition_ $X\xrightarrow{1}Y$ (cf. [6, 10]). The
LEE/LLEE charts with additional 1-transitions, called _LEE/LLEE 1-charts_ ,
are defined the same as shown in Sect. 2.3. With 1-transitions, a similar
correspondence between regular expressions and provable solutions of LLEE
1-charts can be built, analog to Prop. 3 and 4 for LLEE charts. The connection
of LLEE 1-charts to the completeness of Mil were fully explored in recent work
[10].

The extension of our idea to the case of LEE/LLEE 1-charts for proving the
completeness of Mil will not be trivial. There are mainly two reasons: (i) We
see that the properties Lemma 1 (2) and (3) generally do not hold when
1-transitions are involved; (ii) There exist bisimulation collapses of LLEE
1-charts that cannot be simply altered into an LLEE 1-chart by auxiliary
1-transitions. [10, 8] gave a counter-example showing this. (ii) is more of an
essential reason. Although we already have in mind a technique to restore
properties Lemma 1 (2) and (3) for a certain type of bisimulation collapses.
Because of the reason (ii), a restoration for all bisimulation collapses will
not be possible. More complex graph transformations are needed, for example,
the transformations that add additional but necessary bisimular nodes (and
transitions) from the bisimulation collapses in order for our restoration
technique to work. Our future work may focus on these aspects.

##  6 Acknowledgements

This work is partially supported by the Youth Project of National Science
Foundation of China (No. 62102329) and the Project of National Science
Foundation of Chongqing (No. cstc2021jcyj-bshX0120).

## References

  * [1] Beckert, B., Klebanov, V., Weiß, B.: Dynamic Logic for Java, pp. 49–106. Springer International Publishing, Cham (2016). https://doi.org/10.1007/978-3-319-49812-6_3, https://doi.org/10.1007/978-3-319-49812-6_3
  * [2] Bergstra, J.A., Bethke, I., Ponse, A.: Process Algebra with Iteration and Nesting. The Computer Journal 37(4), 243–258 (1994). https://doi.org/10.1093/comjnl/37.4.243, https://doi.org/10.1093/comjnl/37.4.243
  * [3] Copi, I.M., Elgot, C.C., Wright, J.B.: Realization of Events by Logical Nets. J. ACM 5(2), 181–196 (1958). https://doi.org/10.1145/320924.320931, https://doi.org/10.1145/320924.320931
  * [4] Fokkink, W.: On the Completeness of the Equations for the Kleene Star in Bisimulation. In: Wirsing, M., Nivat, M. (eds.) Algebraic Methodology and Software Technology. pp. 180–194. Springer Berlin Heidelberg, Berlin, Heidelberg (1996)
  * [5] Fokkink, W.J.: An Axiomatization for the Terminal Cycle. Nederlands Archief Voor Kerkgeschiedenis (1996), https://api.semanticscholar.org/CorpusID:6310338
  * [6] Grabmayer, C.: Structure-Constrained Process Graphs for the Process Semantics of Regular Expressions. In: TERMGRAPH@FSCD. pp. 29–45 (2020)
  * [7] Grabmayer, C.: A Coinductive Reformulation of Milner’s Proof System for Regular Expressions Modulo Bisimilarity (2023), https://doi.org/10.48550/arXiv.2203.09501
  * [8] Grabmayer, C.: The Image of the Process Interpretation of Regular Expressions is Not Closed under Bisimulation Collapse (2023), https://doi.org/10.48550/arXiv.2303.08553
  * [9] Grabmayer, C., Fokkink, W.: A complete proof system for 1-free regular expressions modulo bisimilarity. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. p. 465–478. LICS ’20, Association for Computing Machinery, New York, NY, USA (2020). https://doi.org/10.1145/3373718.3394744, https://doi.org/10.1145/3373718.3394744
  * [10] Grabmayer, C.A.: Milner’s Proof System for Regular Expressions Modulo Bisimilarity is Complete: Crystallization: Near-Collapsing Process Graph Interpretations of Regular Expressions. In: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS ’22, Association for Computing Machinery, New York, NY, USA (2022). https://doi.org/10.1145/3531130.3532430, https://doi.org/10.1145/3531130.3532430
  * [11] Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)
  * [12] Kleene, S.C.: Representation of Events in Nerve Nets and Finite Automata, pp. 3–42. Princeton University Press, Princeton (1956). https://doi.org/doi:10.1515/9781400882618-002, https://doi.org/10.1515/9781400882618-002
  * [13] Kozen, D.: Kleene Algebra with Tests. ACM Trans. Program. Lang. Syst. 19(3), 427–443 (1997). https://doi.org/10.1145/256167.256195, https://doi.org/10.1145/256167.256195
  * [14] Liu, X., Yu, T.: Canonical Solutions to Recursive Equations and Completeness of Equational Axiomatisations. In: Konnov, I., Kovács, L. (eds.) 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 171, pp. 35:1–35:17. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2020). https://doi.org/10.4230/LIPIcs.CONCUR.2020.35, https://drops.dagstuhl.de/opus/volltexte/2020/12847
  * [15] Milner, R.: A Complete Inference System for a Class of Regular Behaviours. Journal of Computer and System Sciences 28(3), 439–466 (1984). https://doi.org/https://doi.org/10.1016/0022-0000(84)90023-0, https://www.sciencedirect.com/science/article/pii/0022000084900230
  * [16] Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer Publishing Company, Incorporated, 1st edn. (2018)
  * [17] Salomaa, A.: Two Complete Axiom Systems for the Algebra of Regular Events. J. ACM 13(1), 158–169 (1966). https://doi.org/10.1145/321312.321326, https://doi.org/10.1145/321312.321326
  * [18] Smolka, S., Foster, N., Hsu, J., Kappé, T., Kozen, D., Silva, A.: Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time. Proc. ACM Program. Lang. 4(POPL) (2019). https://doi.org/10.1145/3371129, https://doi.org/10.1145/3371129
  * [19] Zhang, Y., Mallet, F., Liu, Z.: A dynamic logic for verification of synchronous models based on theorem proving. Frontiers of Computer Science 16, 164407 (2022)
  * [20] Zhang, Y., Wu, H., Chen, Y., Mallet, F.: A Clock-based Dynamic Logic for the Verification of CCSL Specifications in Synchronous Systems. Science of Computer Programming 203, 102591 (2021). https://doi.org/https://doi.org/10.1016/j.scico.2020.102591, https://www.sciencedirect.com/science/article/pii/S0167642320301994