# The Algebra of Nondeterministic Finite Automata

Roberto Gorrieri<EMAIL_ADDRESS>Dipartimento di Informatica -
Scienza e Ingegneria
Università di Bologna,
Mura A. Zamboni 7, 41027 Bologna, Italy

###### Abstract

A process algebra is proposed, whose semantics maps a term to a
nondeterministic finite automaton (NFA, for short). We prove a
representability theorem: for each NFA $N$, there exists a process algebraic
term $p$ such that its semantics is an NFA isomorphic to $N$. Moreover, we
provide a concise axiomatization of language equivalence: two NFAs $N_{1}$ and
$N_{2}$ recognize the same language if and only if the associated terms
$p_{1}$ and $p_{2}$, respectively, can be equated by means of a set of axioms,
comprising 7 axioms plus 3 conditional axioms, only.

###### keywords:

Finite automaton , language equivalence , axiomatization.

##  1 Introduction

Nondeterministic finite automata (NFA for short), originally proposed in [25],
are a well-known model of sequential computation (see, e.g., [16] for an
introductory textbook), specifically tailored to recognize the class of
regular languages, i.e., those languages that can be described by means of
regular expressions [17].

Kleene’s algorithm [17] (see, e.g, [15, 16] for a more readable and accessible
description) transforms a given nondeterministic finite automaton $N$ into a
regular expression $e_{N}$ that describes the same regular language accepted
by $N$. Conversely, McNaughton and Yamada’s algorithm [23] converts any
regular expression $e$ into an equivalent NFA. Hence, by a combination of
these two results, we get a Representability Theorem (see Figure 1) stating
that the Kleene algebra of regular expressions truly represents the class of
NFAs, up to language equivalence $\sim$. In fact,

  * $(i)$

Given an NFA $N$, we construct an equivalent regular expression $e_{N}$ by
Kleene’s algorithm: so all NFAs can be represented by regular expressions; and

  * $(ii)$

from each regular expression $e$ (hence also from $e_{N}$) we construct an
equivalent NFA $N^{\prime}(e)$ (hence, also $N^{\prime}(e_{N})$) by McNaughton
and Yamada’s algorithm: so only NFAs can be represented by regular
expressions; and, finally,

  * $(iii)$

the NFAs $N$ and $N^{\prime}(e_{N})$ are language equivalent, denoted by
$N\sim N^{\prime}(e_{N})$.

NFAs$N$$N^{\prime}(e_{N})$$\sim$Regular Expressions$e_{N}$Kleene’s
algorithmMcNaughton & Yamada’s algorithm Figure 1: Graphical description of
the representability theorem, up to language equivalence

In this paper, we propose an algebra, called SFM1, that also truly represents
NFAs, but up to isomorphism. More precisely, SFM1 is a slight extension to a
dialect of finite-state CCS [20, 22, 11], called SFM in [12, 14], where an
additional constant 1 is introduced in order to distinguish final states from
non-final ones, as introduced in BPA and related languages (see, e.g., [4] for
an extensive investigation of this issue). Besides the two constants 1 and 0,
used to represent a final state and a non-final state, respectively, SFM1
comprises a disjunction operator (as for regular expressions), denoted by
$\\_+\\_$ (like the choice operator of finite-state CCS), and a prefixing
operator $\alpha.\\_$ for each $\alpha\in A\cup\\{\epsilon\\}$, where $A$ is a
finite alphabet and $\epsilon$ is the symbol denoting the empty word. The
prefixing operator is a weaker form of the concatenation operator
$\\_\cdot\\_$ of regular expressions, because it may concatenate only one
single symbol to a term, like in $a.p$. To compensate the lack of expressivity
of this weaker operator, SFM1 replaces the iteration operator $\\_^{*}$ (or
Kleene star) of regular expressions with the more powerful recursion operator,
implemented by means of process constants (as in CCS [22, 11]), working in the
same way as nonterminals are used in right-linear grammars [16]. For instance,
consider a recursive constant $C$ defined as $C\doteq a.C+\mbox{\bf 1}$; then,
its semantics is an NFA with one state, that is both initial and final, with
an $a$-labeled self-loop; hence, $C$ recognizes the language
$\\{a^{n}\;\;\big{|}\;\;n\geq 0\\}$, denotable by the regular expression
$a^{*}$.

For SFM1, we get a Representability Theorem (see Figure 2) stating that SFM1
truly represents the class of NFAs, up to isomorphism $\equiv$. In fact,

  * $(i)$

Given an NFA $N$, we compile it to an SFM1 term representation $p_{N}$ by an
algorithm described in the proof of Theorem 2: so all NFAs can be represented
by SFM1; and

  * $(ii)$

to each SFM1 term $p$ (hence also to $p_{N}$), we associate, by means of a
denotational semantics described in Table 2, an NFA $N^{\prime}(p)$ (hence
also $N^{\prime}(p_{N})$): so only NFAs can be represented by SFM1; and,
finally,

  * $(iii)$

the NFAs $N$ and $N^{\prime}(p_{N})$ are isomorphic, denoted by $N\equiv
N^{\prime}(p_{N})$.

NFAs$N$$N^{\prime}(p_{N})$$\equiv$SFM1$p_{N}$compilationdenotational semantics
Figure 2: Graphical description of the representability theorem, up to
isomorphism

One advantage of this more concrete representability theorem is that the
algebra SFM1 can be used as a basis to study all the possible equivalences
that can be defined over NFAs, not only language equivalence $\sim$ (as for
regular expressions), but also more concrete equivalences, such as
bisimulation equivalence [24, 22, 4, 11], or any in the linear-time/branching-
time spectrum [10, 11].

The main contribution of this paper is the proof that language equivalence can
be characterized over SFM1 terms by means of a very concise axiomatization,
comprising only 7 axioms (4 for disjunction and 3 for prefixing) and 3
conditional axioms (for recursion). The axioms we present are very similar to
known axioms [17, 27, 18, 20, 21, 14]. In fact, for disjunction they are the
usual ones: the choice operator is an idempotent, commutative monoid, with 0
as neutral element. The axioms for prefixing are similar to those for
concatenation: 0 is an annihilator, the prefixing operator distributes over a
choice term, and the prefix $\epsilon$ can be absorbed. The axioms for
recursion are also similar to axioms developed for SFM [13, 14], in turn
inspired to those for finite-state CCS [21, 22]: the unfolding axiom (stating
that a constant $C$, defined as $C\doteq p\\{C/x\\}$, can be equated to its
body $p\\{C/x\\}$), the folding axiom (stating, roughly, that if $C\doteq
p\\{C/x\\}$ and $q=p\\{q/x\\}$, then $C=q$), and the excision axiom (stating
that if $C\doteq(\epsilon.x+q)\\{C/x\\}$ and $D\doteq q\\{D/x\\}$, then
$C=D$).

The paper is organized as follows. Section 2 recalls the basic definitions
about NFAs, including language equivalence $\sim$, bisimulation equivalence
$\simeq$ and isomorphism equivalence $\equiv$. Section 3 introduces the
algebra SFM1 (i.e., its syntax and its denotational semantics in terms of
NFAs) and proves the representability theorem sketched in Figure 2. Section 4
shows that language equivalence $\sim$ is a congruence for all the operators
of SFM1, notably recursion. Section 5 studies the algebraic properties of
language equivalence over SFM1 terms, that are useful to prove the soundness
of the axiomatization. A particular care is devoted to prove, by means of the
theory of fixed points [8, 28], the folding law for recursion, which holds
only if the recursively defined constant $C$ is observationally guarded, i.e.,
cannot perform an $\epsilon$-labeled loop:
$C{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\nRightarrow}}\>}$}}C$. In
Section 6, we describe how equational deduction is performed in an algebra
using process constants for recursion. In Section 7, we first present the set
of axioms and prove that the axiomatization is sound. Furthermore, we show
that the axiomatization is complete; we prove this result first for
observationally guarded SFM1 terms (by first turning an observationally
guarded term into an $\epsilon$-free normal form and then proving the
completeness for these normal forms using only 9 axioms), and then we extend
the completeness proof also to observationally unguarded SFM1 terms, by
showing that, by means of the additional conditional recursion axiom of
excision, each observationally unguarded term can be equated to an
observationally guarded one. Section 8 adds concluding remarks and hints for
future research.

##  2 Nondeterministic Finite Automata

Let $A$ denote a finite alphabet, ranged over by $a,b,\ldots$. Let $A^{*}$
denote the set of all the words over $A$ (including the empty word
$\epsilon$), ranged over by $\sigma$. Let $\alpha$ range over
$A\cup\\{\epsilon\\}$. Let $\mathcal{P}(A^{*})$ denote the set of all formal
languages over $A$, ranged over by $L$, possibly indexed.

###### Definition 1

A nondeterministic finite automaton (NFA for short) is a tuple $N=(Q,A,$
$T,F,q_{0})$ where

  * 1.

$Q$ is a finite set of states, ranged over by $q$ (possibly indexed);

  * 2.

$A$ is a finite alphabet;

  * 3.

$T\subseteq Q\times(A\cup\\{\epsilon\\})\times Q$ is the set of transitions,
ranged over by $t$ (possibly indexed);

  * 4.

$F\subseteq Q$ is the set of final states;

  * 5.

$q_{0}\in Q$ is the initial state.

Given a transition $t=(q,\alpha,q^{\prime})$, $q$ is called the source,
$\alpha$ the label of the transition (denoted also by $l(t)$), and
$q^{\prime}$ the target; this is usually represented as
$q{\mbox{${\>\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}\>}$}}q^{\prime}$.
An NFA $N=(Q,A,T,F,q_{0})$ is deterministic if:

  * 1.

$\forall t\in T\;l(t)\in A$ (i.e., there are no $\epsilon$ labeled
transitions), and

  * 2.

$\forall q\in Q\,\forall a\in A$ there exists exactly one state $q^{\prime}\in
Q$ such that $(q,a,q^{\prime})\in T$, i.e., $T$ can be equivalently
represented as a function of type $Q\times A\rightarrow Q$.

A deterministic NFA is called a deterministic finite automaton \- DFA, for
short.  $\Box$

###### Definition 2

(Reachability relation and reduced NFA) Given $N=(Q,A,T,F,q_{0})$, the
reachability relation ${\Rightarrow}\subseteq Q\times A^{*}\times Q$ is the
least relation induced by the following axiom and rules:

$\begin{array}[]{llllllllll}\begin{array}[]{c}\\\ \hline\cr
q{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\Longrightarrow}}\>}$}}q\end{array}&&\begin{array}[]{c}q{\mbox{${\>\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}\>}$}}q^{\prime}\\\
\hline\cr
q{\mbox{${\>\stackrel{{\scriptstyle\alpha}}{{\Longrightarrow}}\>}$}}q^{\prime}\end{array}&&\begin{array}[]{c}q_{1}{\mbox{${\>\stackrel{{\scriptstyle\sigma}}{{\Longrightarrow}}\>}$}}q_{2}\;\;\;q_{2}{\mbox{${\>\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}\>}$}}q_{3}\\\
\hline\cr
q_{1}{\mbox{${\>\stackrel{{\scriptstyle\sigma\alpha}}{{\Longrightarrow}}\>}$}}q_{3}\end{array}\\\
\end{array}$
where, of course, we assume that $\epsilon$ is the identity of concatenation:
$\sigma\epsilon=\sigma=\epsilon\sigma$. We simply write $q_{1}\Rightarrow
q_{2}$ to state that $q_{2}$ is reachable from $q_{1}$ when there exists a
word $\sigma$ such that
$q_{1}{\mbox{${\>\stackrel{{\scriptstyle\sigma}}{{\Longrightarrow}}\>}$}}q_{2}$.
We can also define $reach(q)$ as follows:
$reach(q)=\\{q^{\prime}\;\;\big{|}\;\;q\Rightarrow q^{\prime}\\}$. An NFA
$N=(Q,A,T,F,q_{0})$ is reduced if $reach(q_{0})=Q$.  $\Box$

$q_{0}$$q_{1}$$\epsilon$$a$$b$$q_{2}$$q_{3}$$q_{4}$$a$$b$$b$$a$$a,b$ Figure 3:
An NFA and a DFA both recognizing the language $a^{*}b^{*}$

###### Definition 3

(Recognized language and equivalence) Given $N=(Q,A,T,$ $F,q_{0})$, the
language recognized by $N$ is $L[N]=\\{\sigma\in A^{*}\;\;\big{|}\;\;\exists
q\in
F.q_{0}{\mbox{${\>\stackrel{{\scriptstyle\sigma}}{{\Longrightarrow}}\>}$}}q\\}$.
The language recognized by state $q\in Q$ is $L[N,q]=\\{\sigma\in
A^{*}\;\;\big{|}\;\;\exists q^{\prime}\in
F.q{\mbox{${\>\stackrel{{\scriptstyle\sigma}}{{\Longrightarrow}}\>}$}}q^{\prime}\\}$.
Two states $q_{1}$ and $q_{2}$ are equivalent, denoted $q_{1}\sim q_{2}$, if
$L[N,q_{1}]=L[N,q_{2}]$. Two NFAs $N_{1}=(Q_{1},A_{1},T_{1},F_{1},q_{01})$ and
$N_{2}=(Q_{2},A_{2},T_{2},F_{2},q_{02})$ are equivalent if they recognize the
same language, i.e., $L[N_{1}]=L[N_{2}]$.  $\Box$

It is well-known that the class of languages recognized by NFAs is the class
of regular languages (see, e.g., [16] for an introductory textbook), i.e., the
languages denotable by regular expressions (originally proposed by Kleene in
[17]; we assume the reader is familiar with this algebra).

###### Example 1

Figure 3 outlines two finite automata: the left one is an NFA with initial
state $q_{0}$ and final state $q_{1}$, and the right one is a DFA with initial
state $q_{2}$ and final states $q_{2}$ and $q_{3}$. Both recognize the same
regular language $\\{a^{n}b^{m}\;\;\big{|}\;\;n,m\geq 0\\}$, expressible by
the regular expression $a^{*}b^{*}$. As a matter of fact, $q_{0}\sim q_{2}$
because $L[N,q_{0}]=L[N,q_{2}]$, where $N$ is the union of the two automata
(union that can be done because the sets of states are disjoint).  $\Box$

More concrete equivalences can be defined on NFAs, e.g., bisimulation
equivalence [24, 22, 4, 11] and isomorphism equivalence.

###### Definition 4

(Bisimulation) Let $N=(Q,A,T,F,q_{0})$ be an NFA. A bisimulation is a relation
$R\subseteq Q\times Q$ such that if $(q_{1},q_{2})\in R$, then for all
$\alpha\in A\cup\\{\epsilon\\}$

  * 1.

$\forall q_{1}^{\prime}$ such that
$q_{1}{\mbox{${\>\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}\>}$}}q_{1}^{\prime}$,
$\exists q_{2}^{\prime}$ such that
$q_{2}{\mbox{${\>\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}\>}$}}q_{2}^{\prime}$
and $(q_{1}^{\prime},q_{2}^{\prime})\in R$,

  * 2.

$\forall q_{2}^{\prime}$ such that
$q_{2}{\mbox{${\>\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}\>}$}}q_{2}^{\prime}$,
$\exists q_{1}^{\prime}$ such that
$q_{1}{\mbox{${\>\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}\>}$}}q_{1}^{\prime}$
and $(q_{1}^{\prime},q_{2}^{\prime})\in R$, and

  * 3.

$q_{1}\in F$ iff $q_{2}\in F$.

Two states $q$ and $q^{\prime}$ are bisimilar, denoted $q\simeq q^{\prime}$,
if there exists a bisimulation $R$ such that $(q,q^{\prime})\in R$.  $\Box$

###### Example 2

Given an NFA $N=(Q,A,T,F,q_{0})$, it is easy to see that if $q_{1}\simeq
q_{2}$ then $q_{1}\sim q_{2}$. The converse implication does not hold. For
instance, consider Figure 3: of course, $q_{0}\sim q_{2}$, but
$q_{0}\not\simeq q_{2}$.  $\Box$

###### Remark 1

It is interesting to observe that if $N=(Q,A,T,F,q_{0})$ is a DFA, then
language equivalence coincides with bisimulation equivalence. As a matter of
fact, it is easy to see that for DFAs the relation
$R=\\{(q_{1},q_{2})\;\;\big{|}\;\;q_{1}\sim q_{2}\\}$ is a bisimulation.
$\Box$

###### Definition 5

(Isomorphism) Two NFAs $N_{1}=(Q_{1},A_{1},T_{1},F_{1},q_{01})$ and
$N_{2}=(Q_{2},A_{2},T_{2},$ $F_{2},q_{02})$ are isomorphic, denoted by
$N_{1}\equiv N_{2}$, if there exists a bijection $f:Q_{1}\rightarrow Q_{2}$
such that:

  * 1.

it is type-preserving: $q_{1}\in F_{1}$ iff $f(q_{1})\in F_{2}$;

  * 2.

it preserves transitions:
$q{\mbox{${\>\stackrel{{\scriptstyle\alpha}}{{\longrightarrow_{1}}}\>}$}}q^{\prime}\mbox{
iff
}f(q){\mbox{${\>\stackrel{{\scriptstyle\alpha}}{{\longrightarrow_{2}}}\>}$}}f(q^{\prime})$
for all $q,q^{\prime}\in Q_{1}$ and for all $\alpha\in A_{1}\cup
A_{2}\cup\\{\epsilon\\}$; and

  * 3.

it preserves the initial states: $f(q_{01})=q_{02}$.

$\Box$

##  3 SFM1: Syntax and Semantics

The process algebra SFM1 we are going to define is a slight extension to a
dialect of finite-state CCS [22, 11], called SFM in [12], where an additional
constant 1 is introduced in order to distinguish final states from non-final
ones, as introduced in BPA and related languages (see, e.g., [4] for an
extensive investigation of this issue).

###  3.1 Syntax

Let $\mathcal{C}$ be a finite set of constants, disjoint from the alphabet
$A$, ranged over by $C,D,\ldots$ (possibly indexed). The size of the finite
sets $A$ and $\mathcal{C}$ is not important: we assume that they can be chosen
as large as needed. The SFM1 terms are generated from alphabet symbols and
constants by the following abstract syntax:

$\begin{array}[]{llllllllllllll}s&::=&\mbox{\bf 1}&|&\mbox{\bf
0}&|&\alpha.p&|&s+s&\hskip 28.45274pt\mbox{{\em guarded processes}}\\\
p&::=&s&|&C&&&&&\hskip 28.45274pt\mbox{{\em processes}}\\\ \end{array}$

where the special constants 1 and 0 denote, respectively, a final state and a
non-final state, $\alpha.p$ is a process where the symbol $\alpha\in
A\cup\\{\epsilon\\}$ prefixes the residual $p$ ($\alpha.-$ is a family of
prefixing operators, one for each $\alpha$), $s_{1}+s_{2}$ denotes the
disjunction of $s_{1}$ and $s_{2}$ ($-+-$ is the choice operator), and $C$ is
a constant. A constant $C$ may be equipped with a definition, but this must be
a guarded process, i.e., $C\doteq s$. A term $p$ is final if $p\downarrow$
holds, where the predicate $\downarrow$ is the least one generated by the
axiom and the rules outlined in Table 1.

By Const$(p)$ we denote the set of process constants $\delta(p,\emptyset)$
used by $p$, where the auxiliary function $\delta$, which has, as an
additional parameter, a set $I$ of already known constants, is defined as
follows:

$\begin{array}[]{rcllrclrcl}\delta(\mbox{\bf
1},I)&=&\emptyset&&\delta(\mbox{\bf 0},I)&=&\emptyset\\\
\delta(\alpha.p,I)&=&\delta(p,I)&&\delta(p_{1}+p_{2},I)&=&\delta(p_{1},I)\cup\delta(p_{2},I)\\\
\end{array}$
$\begin{array}[]{rclrclrcl}\quad\delta(C,I)&=&\begin{cases}\emptyset&\\!\\!\mbox{$C\in
I$,}\\\ \\{C\\}&\\!\\!\mbox{$C\not\in I\wedge C$ undefined,}\\\
\\{C\\}\cup\delta(p,I\cup\\{C\\})&\\!\\!\mbox{$C\not\in I\wedge C\doteq
p$.}\\\ \end{cases}\end{array}$

A term $p$ is a SFM1 process if Const$(p)$ is finite and each constant in
Const$(p)$ is equipped with a defining equation (in category $s$). The set of
SFM1 processes is denoted by $\mathcal{P}_{SFM1}$, while the set of its
guarded processes, i.e., those in syntactic category $s$, by
$\mathcal{P}_{SFM1}^{grd}$.

$\begin{array}[]{llllllllllll}\begin{array}[]{c}\\\ \hline\cr\mbox{\bf
1}\downarrow\end{array}&&\begin{array}[]{c}p_{1}\downarrow\\\
\hline\cr(p_{1}+p_{2})\downarrow\end{array}&&\begin{array}[]{c}p_{2}\downarrow\\\
\hline\cr(p_{1}+p_{2})\downarrow\end{array}&&\begin{array}[]{c}p\downarrow\;\;C\doteq
p\\\ \hline\cr C\downarrow\end{array}\end{array}$

Table 1: Final states: predicate $\downarrow$

###  3.2 Denotational Semantics

Now we provide a construction of the NFA $\llbracket p\rrbracket_{\emptyset}$
associated with process $p$, which is compositional and denotational in style.
The details of the construction are outlined in Table 2. The encoding is
parametrized by a set of constants that has already been found while scanning
$p$; such a set is initially empty and it is used to avoid looping on
recursive constants. The definition is syntax driven and also the states of
the constructed NFA are syntactic objects, i.e., SFM1 process terms. A bit of
care is needed in the rule for choice: in order to include only strictly
necessary states and transitions, the initial state $p_{1}$ (or $p_{2}$) of
the NFA $\llbracket p_{1}\rrbracket_{I}$ (or $\llbracket p_{2}\rrbracket_{I}$)
is to be kept in the NFA for $p_{1}+p_{2}$ only if there exists a transition
reaching the state $p_{1}$ (or $p_{2}$) in $\llbracket p_{1}\rrbracket_{I}$
(or $\llbracket p_{2}\rrbracket_{I}$), otherwise $p_{1}$ (or $p_{2}$) can be
safely removed in the new NFA. Similarly, for the rule for constants. In Table
2 we denote by $T(q)=\\{t\in T\;\;\big{|}\;\;\exists\alpha\in
A\cup\\{\epsilon\\},\exists q^{\prime}\in Q.t=(q,\alpha,q^{\prime})\\}$ the
set of transitions in $T$ with $q$ as source state.

$\begin{array}[]{rcllcllcl}\llbracket\mbox{\bf
1}\rrbracket_{I}&=&(\\{\mbox{\bf 1}\\},\emptyset,\emptyset,\\{\mbox{\bf
1}\\},\mbox{\bf 1})&\\\ \llbracket\mbox{\bf 0}\rrbracket_{I}&=&(\\{\mbox{\bf
0}\\},\emptyset,\emptyset,\emptyset,\mbox{\bf 0})&\\\
\llbracket\alpha.p\rrbracket_{I}&=&(Q,A,T,F,\alpha.p)&\mbox{given }\llbracket
p\rrbracket_{I}=(Q^{\prime},A^{\prime},T^{\prime},F^{\prime},p)\;\mbox{ and
where }Q=\\{\alpha.p\\}\cup Q^{\prime}\\\
&&&F=F^{\prime},\,T=\\{(\alpha.p,\alpha,p)\\}\cup
T^{\prime},\,A=\begin{cases}\\{\alpha\\}\cup A^{\prime}\hskip 10.00002pt\mbox{
if $\alpha\neq\epsilon$}\\\ A^{\prime}\hskip 40.00006pt\mbox{o.w.}\\\
\end{cases}\\\ \llbracket
p_{1}+p_{2}\rrbracket_{I}&=&(Q,A,T,F,p_{1}+p_{2})&\mbox{given }\llbracket
p_{i}\rrbracket_{I}=(Q_{i},A_{i},T_{i},F_{i},p_{i})\;\mbox{ for $i=1,2$, and
where}\\\ &&&Q=\\{p_{1}+p_{2}\\}\cup Q_{1}^{\prime}\cup Q_{2}^{\prime},\mbox{
with, for $i=1,2$, }\\\ &&&Q^{\prime}_{i}=\begin{cases}Q_{i}\hskip
10.00002pt\mbox{ $\exists t\in T_{i}$ such that $t=(q,\alpha,p_{i})$}\\\
Q_{i}\setminus\\{p_{i}\\}\hskip 40.00006pt\mbox{o.w.}\\\ \end{cases}\\\
&&&A=A_{1}\cup A_{2},\;T=T^{\prime}\cup T^{\prime}_{1}\cup
T^{\prime}_{2},\mbox{ with, for $i=1,2$, }\\\
&&&T^{\prime}_{i}=\begin{cases}T_{i}\hskip 40.00006pt\mbox{ $\exists t\in
T_{i}.\,t=(q,\alpha,p_{i})$}\\\ T_{i}\setminus T_{i}(p_{i})\hskip
20.00003pt\mbox{o.w.}\\\ \end{cases}\\\
&&&T^{\prime}=\\{(p_{1}+p_{2},\alpha,q)\;\;\big{|}\;\;(p_{i},\alpha,q)\in
T_{i},i=1,2\\}\\\ &&&F^{\prime}_{i}=F_{i}\cap Q^{\prime}_{i}\mbox{ for
$i=1,2$, and }\\\ &&&F=\begin{cases}F^{\prime}_{1}\cup
F^{\prime}_{2}\cup\\{p_{1}+p_{2}\\}\hskip 10.00002pt\mbox{ if $p_{1}\in F_{1}$
or $p_{2}\in F_{2}$}\\\ F^{\prime}_{1}\cup F^{\prime}_{2}\hskip
60.00009pt\mbox{o.w.}\\\ \end{cases}\\\ \llbracket
C\rrbracket_{I}&=&(\\{C\\},\emptyset,\emptyset,\emptyset,C)&\mbox{if $C\in I$
}\\\ \llbracket C\rrbracket_{I}&=&(Q,A,T,F,C)&\mbox{if $C\not\in I$, given
$C\doteq p$ and }\llbracket
p\rrbracket_{I\cup\\{C\\}}=(Q^{\prime},A^{\prime},T^{\prime},F^{\prime},p)\\\
&&&A=A^{\prime},Q=\\{C\\}\cup Q^{\prime\prime},\mbox{ where }\\\
&&&Q^{\prime\prime}=\begin{cases}Q^{\prime}\hskip 10.00002pt\mbox{ $\exists
t\in T^{\prime}$ such that $t=(q,\alpha,p)$}\\\
Q^{\prime}\setminus\\{p\\}\hskip 40.00006pt\mbox{o.w.}\\\ \end{cases}\\\
&&&T=\\{(C,\alpha,q)\;\;\big{|}\;\;(p,\alpha,q)\in T^{\prime}\\}\cup
T^{\prime\prime}\mbox{ where }\\\
&&&T^{\prime\prime}=\begin{cases}T^{\prime}\hskip 40.00006pt\mbox{$\exists
t\in T^{\prime}$. $t=(q,\alpha,p)$}\\\ T^{\prime}\setminus T^{\prime}(p)\hskip
40.00006pt\mbox{o.w.}\\\ \end{cases}\\\ &&&F^{\prime\prime}=F^{\prime}\cap
Q^{\prime\prime}\mbox{ and }F=\begin{cases}F^{\prime\prime}\cup\\{C\\}\hskip
10.00002pt\mbox{ if $p\in F^{\prime}$ }\\\ F^{\prime\prime}\hskip
40.00006pt\mbox{o.w.}\\\ \end{cases}\\\ \end{array}$

Table 2: Denotational semantics $C$$D$$b.D+\mbox{\bf 1}$$b$$a$$b$ Figure 4:
The NFA for $C\doteq b.D$, where $D\doteq a.(b.D+\mbox{\bf 1})$, of Example 3

###### Example 3

Consider constant $C\doteq b.D$, where $D\doteq a.(b.D+\mbox{\bf 1})$. By
using the definitions in Table 2, $\llbracket
D\rrbracket_{\\{C,D\\}}=(\\{D\\},\emptyset,\emptyset,\emptyset,D)$. Then, by
prefixing,

$\llbracket b.D\rrbracket_{\\{C,D\\}}$
$=(\\{b.D,D\\},\\{b\\},\\{(b.D,b,D)\\},\emptyset,b.D)$.

Now, $\llbracket\mbox{\bf 1}\rrbracket_{\\{C,D\\}}$ $=(\\{\mbox{\bf
1}\\},\emptyset,\emptyset,\\{\mbox{\bf 1}\\},\mbox{\bf 1})$. Then, by
summation

$\llbracket b.D+\mbox{\bf 1}\rrbracket_{\\{C,D\\}}$ $=(\\{b.D+\mbox{\bf
1},D\\},\\{b\\},\\{(b.D+1,b,D)\\},\\{b.D+\mbox{\bf 1}\\},b.D+\mbox{\bf 1})$.

Note that the states $b.D$ and 1 have been removed, as no transition in
$\llbracket b.D\rrbracket_{\\{C,D\\}}$ reaches $b.D$ and no transition in
$\llbracket\mbox{\bf 1}\rrbracket_{\\{C,D\\}}$ reaches 1.

Again, by prefixing, $\llbracket a.(b.D+\mbox{\bf
1})\rrbracket_{\\{C,D\\}}=(\\{a.(b.D+\mbox{\bf 1}),b.D+\mbox{\bf
1},D\\},\\{a,b\\},$

$\\{(a.(b.D+\mbox{\bf 1}),a,b.D+\mbox{\bf 1}),(b.D+\mbox{\bf
1},b,D)\\},\\{b.D+\mbox{\bf 1}\\},a.(b.D+\mbox{\bf 1}))$.

Now, the rule for constants ensures that

$\llbracket D\rrbracket_{\\{C\\}}=(\\{D,b.D+\mbox{\bf
1}\\},\\{a,b\\},\\{(D,a,b.D+\mbox{\bf 1}),(b.D+\mbox{\bf
1},b,D)\\},\\{b.D+\mbox{\bf 1}\\},D)$.

Note that state $a.(b.D+\mbox{\bf 1})$ has been removed, as no transition in
$\llbracket a.(b.D+\mbox{\bf 1})\rrbracket_{\\{C,D\\}}$ reaches that state. By
prefixing,

$\llbracket b.D\rrbracket_{\\{C\\}}=(\\{b.D,D,b.D+\mbox{\bf
1}\\},\\{a,b\\},\\{(b.D,b,D),(D,a,b.D+\mbox{\bf 1}),(b.D+\mbox{\bf
1},b,D)\\},$ $\\{b.D+\mbox{\bf 1}\\},b.D)$,

Finally, $\llbracket C\rrbracket_{\emptyset}=(\\{C,D,b.D+\mbox{\bf
1}\\},\\{a,b\\},\\{(C,b,D),(D,a,b.D+\mbox{\bf 1}),(b.D+\mbox{\bf 1},b,D)\\},$

$\\{b.D+\mbox{\bf 1}\\},C)$. The resulting NFA is outlined in Figure 4.
$\Box$

###### Theorem 1

For each SFM1 process $p$, $\llbracket p\rrbracket_{\emptyset}$ is a reduced
NFA.

###### Theorem 2

(Representability) For any reduced NFA $N$, there exists an SFM1 process $p$
such that $\llbracket p\rrbracket_{\emptyset}$ is isomorphic to $N$.

###### Corollary 1

SFM1 represents, up to isomorphism, the class of reduced NFAs.

###### Example 4

Let us consider the NFA in Figure 3. According to the construction in the
proof of Theorem 2, the SFM1 representation is as follows:

$\begin{array}[]{rcl}C_{0}&\doteq&a.C_{0}+\epsilon.C_{1}\\\
C_{1}&\doteq&b.C_{1}+\mbox{\bf 1}\\\ \end{array}$

If we consider the DFA in Figure 3, the SFM1 representation is as follows:

$\begin{array}[]{rcl}C_{2}&\doteq&a.C_{2}+b.C_{3}+\mbox{\bf 1}\\\
C_{3}&\doteq&b.C_{3}+a.C_{4}+\mbox{\bf 1}\\\ C_{4}&\doteq&a.C_{4}+b.C_{4}\\\
\end{array}$

Note that if the NFA is not reduced, then we cannot find an SFM1 process that
represents it. For instance, if we take the union of the two automata in
Figure 3 with initial state $q_{0}$, then $C_{0}$ represents only the NFA on
the left.

If we consider the first NFA in Figure 5, we get:

$\begin{array}[]{rcl}C_{5}&\doteq&a.C_{6}+b.C_{5}\\\ C_{6}&\doteq&\mbox{\bf
1}\\\ \end{array}$

Finally, if we consider the second NFA in Figure 5, we get:

$\begin{array}[]{rcl}C_{7}&\doteq&a.C_{8}+b.C_{9}\\\ C_{8}&\doteq&\mbox{\bf
0}\\\ C_{9}&\doteq&a.C_{8}+b.C_{9}+\mbox{\bf 1}\\\ \end{array}$

$\Box$

$q_{5}$$q_{6}$$a$$b$$q_{7}$$q_{9}$$q_{8}$$a$$b$$a$$b$ Figure 5: Two NFAs for
Example 4

##  4 Congruence

In the following, for each SFM1 process $p$, its associated language $L(p)$ is
the language recognized by the reduced NFA $\llbracket
p\rrbracket_{\emptyset}$, computed according to the denotational semantics in
Table 2.

###### Definition 6

Two SFM1 processes $p$ and $q$ are language equivalent, denoted $p\sim q$, if
$L(p)=L(q)$, i.e., they recognize the same language.  $\Box$

###### Proposition 1

The following hold:

1) $L(\mbox{\bf 0})=\emptyset$.

2) $L(\mbox{\bf 1})=\\{\epsilon\\}$.

3) For each $p\in\mathcal{P}_{SFM1}$, for all $a\in A$, we have that
$L(a.p)=\\{aw\;\;\big{|}\;\;w\in L(p)\\}$.

4) For each $p\in\mathcal{P}_{SFM1}$, we have that $L(\epsilon.p)=\\{\epsilon
w\;\;\big{|}\;\;w\in L(p)\\}=L(p)$.

5) For each $p,q\in\mathcal{P}_{SFM1}^{grd}$, $L(p+q)=L(p)\cup L(q)$.

Now we show that language equivalence is a congruence for all the SFM1
operators.

###### Proposition 2

1) For each $p,q\in\mathcal{P}_{SFM1}$, if $p\sim q$, then
$\alpha.p\sim\alpha.q$ for all $\alpha\in A\cup\\{\epsilon\\}$.

2) For each $p,q\in\mathcal{P}_{SFM1}^{grd}$, if $p\sim q$, then $p+r\sim
q+r\;$ for all $r\in\mathcal{P}_{SFM1}^{grd}$.

Note that the symmetric case $r+p\sim r+q$ is implied by the fact that the
operator of choice is commutative w.r.t. $\sim$ (see Proposition 3).

Still there is one construct missing: recursion, defined over guarded terms
only. Consider an extension of SFM1 where terms can be constructed using
variables, such as $x,y,\ldots$ (which are in syntactic category $p$): this
defines an “open” SFM1 that has the following syntax:

$\begin{array}[]{lccccccccccl}s&::=&\mbox{\bf 1}&|&\mbox{\bf
0}&|&a.p&|&s+s&\\\ p&::=&s&|&C&|&x&&\\\ \end{array}$

where the semantic of $x$ is the NFA
$(\\{x\\},\emptyset,\emptyset,\emptyset,x)$.

Sometimes we use the notation $p(x_{1},\ldots,x_{n})$ to state explicitly that
term $p$ is open on the tuple of variables $(x_{1},\ldots,x_{n})$. For
instance, $p_{1}(x)=a.(b.\mbox{\bf 1}+c.x)$ and $p_{2}(x)=a.c.x+a.b.\mbox{\bf
1}$ are open guarded SFM1 terms. Similarly, $C_{1}(x)\doteq a.x$ denotes
explicitly that the constant $C_{1}$ is defined by a term open on $x$.

An open term $p(x_{1},\ldots,x_{n})$ can be closed by means of a substitution
as follows (see also Section 6 for the definition of substitution application,
also in the case of process constants):

$p(x_{1},\ldots,x_{n})\\{r_{1}/x_{1},\ldots,r_{n}/x_{n}\\}$

with the effect that each occurrence of the free variable $x_{i}$ is replaced
by the closed SFM1 process $r_{i}$, for $i=1,\ldots,n$. For instance,
$p_{1}(x)\\{d.\mbox{\bf 0}/x\\}=a.(b.\mbox{\bf 1}+c.d.\mbox{\bf 0})$, as well
as $C_{1}(x)\\{d.\mbox{\bf 0}/x\\}$ is $C_{1}\doteq a.d.\mbox{\bf 0}$ (i.e.,
we close the open term $a.x$ defining the body of $C_{1}$). A natural
extension of language equivalence $\sim$ over open guarded terms is as
follows: $p(x_{1},\ldots,x_{n})\sim q(x_{1},\ldots,x_{n})$ if for all tuples
of closed SFM1 terms $(r_{1},\ldots,r_{n})$,

$p(x_{1},\ldots,x_{n})\\{r_{1}/x_{1},\ldots,r_{n}/x_{n}\\}$ $\sim$
$q(x_{1},\ldots,x_{n})\\{r_{1}/x_{1},\ldots,r_{n}/x_{n}\\}$.

E.g., it is easy to see that $p_{1}(x)\sim p_{2}(x)$. As a matter of fact, for
all $r$, $p_{1}(x)\\{r/x\\}=a.(b.\mbox{\bf 1}+c.r)$ $\sim$
$a.c.r+a.b.\mbox{\bf 1}$ = $p_{2}(x)\\{r/x\\}$, which can be easily proved by
means of the algebraic properties (see the next section) and the congruence
ones of $\sim$.

For simplicity’s sake, let us now restrict our attention to open guarded terms
using a single undefined variable. We can recursively close an open term
$p(x)$ by means of a recursively defined constant. For instance, $C\doteq
p(x)\\{C/x\\}$. The resulting process constant $C$ is a closed SFM1 process.
By saying that language equivalence is a congruence for recursion we mean the
following: If $p(x)\sim q(x)$ and $C\doteq p(x)\\{C/x\\}$ and $D\doteq
q(x)\\{D/x\\}$, then $C\sim D$. The following theorem states this fact. For
simplicity’s sake, in the following a term $p$, open on a variable $x$, is
annotated as $p(x)$ only when it is unclear from the context, because we work
with real terms and not with annotated ones.

###### Remark 2

Throughout the paper, it is assumed that whenever a constant $C$ is defined by
$C\doteq p\\{C/x\\}$, then the open guarded term $p$ does not contain
occurrences of $C$, i.e., $C\not\in\mbox{{\it Const}$(p)$}$, so that all the
instances of $C$ in $p\\{C/x\\}$ are due to substitution of $C$ for $x$.
Moreover, it is assumed that for each constant definition we use a different
variable, for instance, $D\doteq q\\{D/y\\}$.  $\Box$

###### Theorem 3

Let $p$ and $q$ be two open guarded SFM1 terms, with one variable $x$ at most.
Let $C\doteq p\\{C/x\\}$, $D\doteq q\\{D/x\\}$ and $p\sim q$. Then $C\sim D$.

###### Example 5

Consider $p_{1}(x)=a.(b.\mbox{\bf 1}+c.x)$ and $p_{2}(x)=a.c.x+a.b.\mbox{\bf
1}$. Of course, they are language equivalent and indeed
$L_{p_{1}}^{\downarrow}=\\{ab\\}=L_{p_{2}}^{\downarrow}$ and
$L_{p_{1}}^{x}=\\{ac\\}=L_{p_{2}}^{x}$. If we consider $C\doteq
p_{1}\\{C/x\\}$ and $D\doteq p_{2}\\{D/x\\}$, then we get that $C\sim D$, as
both recognize the regular language $(ac)^{*}ab$.  $\Box$

The generalization to open terms over a set $\\{x_{1},\ldots,x_{n}\\}$ of
variables is rather obvious. Consider a set of pairs of equivalent open terms
of this form:

$\begin{array}[]{lrcllllll}\mbox{$p_{1}(x_{1},\ldots,x_{n})\sim
q_{1}(x_{1},\ldots,x_{n})$}\\\ \mbox{$p_{2}(x_{1},\ldots,x_{n})\sim
q_{2}(x_{1},\ldots,x_{n})$}\\\ \mbox{$\ldots$}\\\
\mbox{$p_{n}(x_{1},\ldots,x_{n})\sim q_{n}(x_{1},\ldots,x_{n})$}\\\
\end{array}$

where, for $i=1,\ldots,n$, $p_{i}(x_{1},\ldots,x_{n})\sim
q_{i}(x_{1},\ldots,x_{n})$ if and only if
$L_{p_{i}}^{\downarrow}=L_{q_{i}}^{\downarrow}$ and
$L_{p_{i}}^{x_{j}}=L_{q_{i}}^{x_{j}}$ for $j=1,\ldots,n$. Then, we can
recursively close these terms as follows:

$\begin{array}[]{lrcllllll}\mbox{$C_{1}\doteq
p_{1}\\{C_{1}/x_{1},\ldots,C_{n}/x_{n}\\}\hskip 30.00005ptD_{1}\doteq
q_{1}\\{D_{1}/x_{1},\ldots,D_{n}/x_{n}\\}$}\\\ \mbox{$C_{2}\doteq
p_{2}\\{C_{1}/x_{1},\ldots,C_{n}/x_{n}\\}\hskip 30.00005ptD_{2}\doteq
q_{2}\\{D_{1}/x_{1},\ldots,D_{n}/x_{n}\\}$}\\\ \mbox{$\ldots$}\\\
\mbox{$C_{n}\doteq p_{n}\\{C_{1}/x_{1},\ldots,C_{n}/x_{n}\\}\hskip
30.00005ptD_{n}\doteq q_{n}\\{D_{1}/x_{1},\ldots,D_{n}/x_{n}\\}$}\\\
\end{array}$

Then, the thesis is that $C_{i}\sim D_{i}$ for all $i=1,2,\ldots,n$.

Finally, a comment on the more concrete equivalences we have defined in
Section 2. Isomorphism equivalence is the most concrete and it is not a
congruence for the choice operator. For instance, $a.\mbox{\bf 1}$ generates
an NFA isomorphic to the one for $a.(\mbox{\bf 1}+\mbox{\bf 0})$; however, if
we consider the context $\\_+a.\mbox{\bf 1}$ we get two terms generating not
isomorphic NFA: $a.\mbox{\bf 1}+a.\mbox{\bf 1}$ generates a two-state NFA,
while $a.(\mbox{\bf 1}+\mbox{\bf 0})+a.\mbox{\bf 1}$ generates a three-state
NFA. On the contrary, it is possible to prove that bisimulation equivalence
$\simeq$, which is strictly finer than language equivalence $\sim$, is a
congruence for all the operators of SFM1, by means of standard proof
techniques (see, e.g., [22, 11, 4, 28, 14]).

##  5 Algebraic Properties

Now we list some algebraic properties of language equivalence and discuss
whether they hold for bisimulation equivalence or isomorphism equivalence.

###### Proposition 3

(Laws of the choice op.) For each $p,q,r\in\mathcal{P}_{SFM1}^{grd}$ , the
following hold:

$\begin{array}[]{lrcllllll}&p+(q+r)&\sim&(p+q)+r&&\;\mbox{(associativity)}\\\
&p+q&\sim&q+p&&\;\mbox{(commutativity)}\\\ &p+\mbox{\bf
0}&\sim&p&&\;\mbox{(identity)}\\\
&p+p&\sim&p&&\;\mbox{(idempotency)}\end{array}$

The laws of the choice operator hold also for bisimilarity [22, 11, 4, 28],
but they do not hold for isomorphism equivalence. For instance, consider
$p=a.A$, with $A\doteq a.(b.B+a.A)$, and $q=b.B$, with $B\doteq b.B+\mbox{\bf
1}$; then, it is easy to see that the NFA for $p+q$ (four states) is not
isomorphic to the NFA for $q+p$ (three states).

###### Proposition 4

(Laws of the prefixing operator) For each $p,q\in\mathcal{P}_{SFM1}^{grd}$,
for each $r\in\mathcal{P}_{SFM1}$, for each $\alpha\in A\cup\\{\epsilon\\}$,
the following hold:

$\begin{array}[]{lrcllllll}&\alpha.\mbox{\bf 0}&\sim&\mbox{\bf
0}&&\;\mbox{(annihilation)}\\\
&\alpha.(p+q)&\sim&\alpha.p+\alpha.q&&\;\mbox{(distributivity)}\\\
&\epsilon.r&\sim&r&&\;\mbox{($\epsilon$-absorption)}\end{array}$

It is easy to see that none of the laws for prefixing hold for bisimilarity,
and so not even for isomorphism equivalence.

We now focus on the properties of constants. First, the unfolding law (which
holds also for bisimilarity), then the excision law (useful to remove loops of
$\epsilon$ transitions) and finally, in the next subsection, the folding law,
whose proof relies on some auxiliary technical machinery (fixed point theorems
on a complete lattice, see, e.g., [8, 28]).

###### Proposition 5

(Unfolding) For each $p\in\mathcal{P}_{SFM1}^{grd}$ and each
$C\in\mathcal{C}$, if $C\doteq p$ then $C\sim p$.

The unfolding law also holds for bisimilarity [22, 11, 13], but it does not
hold for isomorphism equivalence. For instance, consider $C\doteq
a.a.C+\mbox{\bf 1}$: it is easy to see that the NFA for $C$ has two states,
while the NFA for $a.a.C+\mbox{\bf 1}$ has three states.

###### Remark 3

The $\epsilon$-absorption law in Proposition 4 is better split in two separate
laws:

  * $(i)$

$\epsilon.p\sim p\;$ if $\;p\neq C$, and

  * $(ii)$

$\epsilon.C\sim p\;$ if $\;C\doteq p$,

where the second law is derivable from the first one and the unfolding law. In
fact, if $C\doteq p$, then by unfolding we have $C\sim p$; then, by
congruence, $\epsilon.C\sim\epsilon.p$ and then, by the first law,
$\epsilon.p\sim p$, so that the equality $\epsilon.C\sim p$ follow by
transitivity.

The usefulness of the first law $(i)$ instead of the more general
$\epsilon$-absorption law in Proposition 4 is that it preserves guardedness;
for instance, if $C\doteq\epsilon.D+\mbox{\bf 1}$ and $D\doteq a.\mbox{\bf
1}$, then by using (unfolding and) the more general law we can derive $C\sim
D+\mbox{\bf 1}$, where the r.h.s. is not a guarded term; on the contrary, by
using (recursion congruence and) $(i)$, we can derive $C\sim a.\mbox{\bf
1}+\mbox{\bf 1}$, where the r.h.s. is a guarded term.  $\Box$

###### Proposition 6

(Excision) For each $p\in\mathcal{P}_{SFM1}^{grd}$, and each
$C,D\in\mathcal{C}$, if $C\doteq(\epsilon.x+p)\\{C/x\\}$ and $D\doteq
p\\{D/x\\}$, then $C\sim D$.

Of course, the excision law does not hold for bisimilarity, and so not even
for isomorphism equivalence.

###  5.1 The Folding Law

In order to prove the folding law, we first observe that
$(\mathcal{P}(A^{*}),\subseteq)$ is a complete lattice, i.e., with the
property that all the subsets of $\mathcal{P}(A^{*})$ ( e.g.,
$\\{L_{i}\\}_{i\in I}$) have joins (i.e., $\bigcup_{i\in I}L_{i}$) and meets
(i.e., $\bigcap_{i\in I}L_{i}$), whose top element $\top$ is $A^{*}$ and
bottom element $\bot$ is $\emptyset$.

At a first approximation, the folding law states that if $C\doteq p\\{C/x\\}$
and $q\sim p\\{q/x\\}$, then $C\sim q$. Of course, we can easily realize that
$L(C)=L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot L(C))$ as well as
$L(q)=L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot L(q))$. Therefore, both $L(C)$ and
$L(q)$ are a fixed point of the mapping
$T(W)=L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot W)$. We want to show that, under
one mild condition, there exists exactly one fixed point of $T$, so that
$L(C)=L(q)$ and so $C\sim q$, as required.

If the mapping $T$ is continuous (i.e., for all increasing sequences
$L_{0}\subseteq L_{1}\subseteq L_{2}\ldots$ we have that
$T(\bigcup_{i}L_{i})=\bigcup_{i}T(L_{i})$), then the least fixed point
lfp$(T)=\bigcup_{n\geq 0}T^{n}(\emptyset)$, where $T^{0}(L)=L$ and
$T^{n+1}(L)=T(T^{n}(L))$. Indeed, $T$ is continuous because
$T(\bigcup_{i}L_{i})=L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot\bigcup_{i}L_{i})$
$=L_{p}^{\downarrow}\cup\bigcup_{i}(L_{p}^{x}\cdot L_{i})=$
$\bigcup_{i}(L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot
L_{i}))=\bigcup_{i}T(L_{i})$. The least fixed point lfp$(T)=\bigcup_{n\geq
0}T^{n}(\emptyset)$ can be computed as follows:

$\begin{array}[]{rcl}T^{0}(\emptyset)&=&\emptyset\\\
T^{1}(\emptyset)&=&L_{p}^{\downarrow}\\\
T^{2}(\emptyset)&=&L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot
L_{p}^{\downarrow})\\\
T^{3}(\emptyset)&=&L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot
L_{p}^{\downarrow})\cup(L_{p}^{x}\cdot(L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot
L_{p}^{\downarrow}))=L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot
L_{p}^{\downarrow})\cup L_{p}^{x}\cdot(L_{p}^{x}\cdot L_{p}^{\downarrow})\\\
\ldots\\\ \end{array}$

whose union is the language lfp$(T)=(L_{p}^{x})^{*}\cdot L_{p}^{\downarrow}$.

Dually, if $T$ is co-continuous (i.e., for all decreasing sequences
$L_{0}\supseteq L_{1}\supseteq L_{2}\ldots$ we have that
$T(\bigcap_{i}L_{i})=\bigcap_{i}T(L_{i})$), then the greatest fixed point
gfp$(T)=\bigcap_{n\geq 0}T^{n}(A^{*})$. Indeed, $T$ is co-continuous because
$T(\bigcap_{i}L_{i})=L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot\bigcap_{i}L_{i})$
$=L_{p}^{\downarrow}\cup\bigcap_{i}(L_{p}^{x}\cdot L_{i})=$
$\bigcap_{i}(L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot
L_{i}))=\bigcap_{i}T(L_{i})$. The greatest fixed point gfp$(T)=\bigcap_{n\geq
0}T^{n}(A^{*})$ can be computed as follows:

$\begin{array}[]{rcl}T^{0}(A^{*})&=&A^{*}\\\
T^{1}(A^{*})&=&L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot A^{*})\\\
T^{2}(A^{*})&=&L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot(L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot
A^{*}))=L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot L_{p}^{\downarrow})\cup
L_{p}^{x}\cdot(L_{p}^{x}\cdot A^{*})\\\
T^{3}(A^{*})&=&L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot(L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot
L_{p}^{\downarrow})\cup L_{p}^{x}\cdot(L_{p}^{x}\cdot A^{*}))=$ $\\\
&&L_{p}^{\downarrow}\cup(L_{p}^{x}\cdot L_{p}^{\downarrow})\cup
L_{p}^{x}\cdot(L_{p}^{x}\cdot L_{p}^{\downarrow})\cup
L_{p}^{x}\cdot(L_{p}^{x}\cdot(L_{p}^{x}\cdot A^{*}))\\\ \ldots\\\ \end{array}$

whose intersection is the language gfp$(T)=(L_{p}^{x})^{*}\cdot
L_{p}^{\downarrow}$, unless $L_{p}^{x}$ does contain the empty word
$\epsilon$, because in such a case the application of $T$ does not restrict
the newly computed language, so that $T^{n}(A^{*})=A^{*}$ for all $n\geq 0$,
and so the greatest fixed point of $T$ is the top element $A^{*}$ of the
complete lattice. We can characterize this condition syntactically as follows.

###### Definition 7

(Observationally guarded) A (possibly open) SFM1 process $p$ is
observationally guarded if $og(p)$ holds, where $og(-)$ is defined as the
least predicate generated by the axioms and the rules in Table 3.  $\Box$

$\begin{array}[]{llllllllllll}\begin{array}[]{c}\\\ \hline\cr og(\mbox{\bf
0})\end{array}&\begin{array}[]{c}\\\ \hline\cr og(\mbox{\bf
1})\end{array}&\begin{array}[]{c}a\in A\\\ \hline\cr
og(a.p)\end{array}&\begin{array}[]{c}og(p)\\\ \hline\cr
og(\epsilon.p)\end{array}&\begin{array}[]{c}og(p)\quad C\doteq p\\{C/x\\}\\\
\hline\cr og(C)\end{array}&\begin{array}[]{c}og(p)\quad og(q)\\\ \hline\cr
og(p+q)\end{array}\\\ \end{array}$

Table 3: Observationally guarded predicate

Note that $C\doteq p\\{C/x\\}$ is observationally guarded if and only if
$C{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\nRightarrow}}\>}$}}C$, or
equivalently, if and only if
$p{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\nRightarrow}}\>}$}}x$, i.e.,
if and only if $\epsilon\not\in L_{p}^{x}$.

###### Proposition 7

(Folding) For each $p\in\mathcal{P}_{SFM1}^{grd}$ (open on $x$), and each
$C\in\mathcal{C}$, if $C\doteq p\\{C/x\\}$, $og(p)$ and $q\sim p\\{q/x\\}$,
then $C\sim q$.

Observe that the requirement that $p$ is observationally guarded is crucial
for the correctness of the folding property. For instance, consider
$p=\epsilon.x+a.\mbox{\bf 1}$, which is not observationally guarded. Then,
$C\doteq\epsilon.C+a.\mbox{\bf 1}$ defines a process that can recognize only
$a$, so it is language equivalent to $a.\mbox{\bf 1}$. However, $q=a.\mbox{\bf
1}+b.\mbox{\bf 1}$ is such that $q\sim\epsilon.q+a.\mbox{\bf 1}$, but
$C\not\sim q$.

###### Remark 4

(Folding Law for Bisimulation Equivalence) It is possible to prove, with a
standard bisimulation-based proof technique [20, 13], that the more concrete
bisimulation equivalence $\simeq$ satisfies a stronger folding law: For each
$p\in\mathcal{P}_{SFM1}^{grd}$ (open on $x$), and each $C\in\mathcal{C}$, if
$C\doteq p\\{C/x\\}$ and $q\simeq p\\{q/x\\}$, then $C\simeq q$.  $\Box$

##  6 Equational Deduction with Process Constants

In the following, we show that it is possible to prove syntactically, i.e., by
means of an equational deductive proof, when two SFM1 processes recognize the
same language. First, in this section we describe how equational deduction is
implemented in a process algebra with process constants; then in the next
section we provide a sound and complete axiomatization of language equivalence
for observationally guarded SFM1 processes, composed of 7 axioms and 2
conditional axioms; finally, we show that each observationally unguarded
process can be equated to an observationally guarded one with the help of one
additional conditional axiom. Hence, the finite axiomatization of language
equivalence over SFM1 is composed of 7 axioms and 3 conditional axioms, only.
Let us start with an equational deduction primer.

Given a (one-sorted) signature $\Sigma$ (i.e., a finite set of constants, a
finite set of process constants and a finite set of function symbols with
their arities), we can define the set of terms over $\Sigma$ and over a finite
set of variables $V$ (notation $\mathcal{T}(\Sigma,V)$) as the smallest set
that satisfies the following:

  * $(i)$

each variable $x$ in $V$ is a term in $\mathcal{T}(\Sigma,V)$;

  * $(ii)$

each constant $c$ in $\Sigma$ is a term of $\mathcal{T}(\Sigma,V)$;

  * $(iii)$

each process constant $C$ in $\Sigma$ is a term of $\mathcal{T}(\Sigma,V)$;
moreover, each constant $C$ must be equipped with a definition, e.g., $C\doteq
t$, with $t$ a term in $\mathcal{T}(\Sigma,V)$;

  * $(iv)$

if $f$ is a $n$-ary function symbol and $t_{1},\ldots,t_{n}$ are terms in
$\mathcal{T}(\Sigma,V)$, then also $f(t_{1},\ldots,t_{n})$ is a term in
$\mathcal{T}(\Sigma,V)$.

Moreover, we have that $\mathcal{T}(\Sigma)$ denotes the set of closed (or
ground) terms, where a term $t\in\mathcal{T}(\Sigma)$ when:

  * 1.

there are no variable occurrences in $t$

  * 2.

$\forall C\in\mbox{{\it Const}$(t)$}$, if $C\doteq p$, then
$p\in\mathcal{T}(\Sigma)$.

The definition is apparently recursive, but this is not a problem, because we
can define it keeping track of already encountered process constants, like we
did in the denotational semantics of SFM1.

A substitution $\rho$ is a mapping from $V$ to $\mathcal{T}(\Sigma,V)$. For
any term $t$, by $t[\rho]$ we denote the term obtained as follows:

  * $(i)$

for each variable $x$ in $V$, $x[\rho]=\rho(x)$,

  * $(ii)$

for each constant $c$ in $\Sigma$, $c[\rho]=c$,

  * $(iii)$

for each process constant $C$ in $\Sigma$ such that $C\doteq t$, $C[\rho]=C$
with $C\doteq t[\rho]$

  * $(iv)$

for any $n$-ary function symbol $f$ and terms $t_{1},\ldots,t_{n}$,
$f(t_{1},\ldots,t_{n})[\rho]$ is the term $f(t_{1}[\rho],\ldots,t_{n}[\rho])$.

A substitution $\rho$ is closed if $\rho(x)\in\mathcal{T}(\Sigma)$ for each
variable $x\in V$. Hence, the application of a closed substitution to an open
term yields a closed (or ground) term.

$\begin{array}[]{llllll}1.&\;\;\mbox{Reflexivity}&\;\;\begin{array}[]{c}\\\
\hline\cr t\,=\,t\end{array}\\\
2.&\;\;\mbox{Symmetry}&\;\;\begin{array}[]{c}t_{1}\,=\,t_{2}\\\ \hline\cr
t_{2}\,=\,t_{1}\end{array}\\\
3.&\;\;\mbox{Transitivity}&\;\;\begin{array}[]{c}t_{1}\,=\,t_{2}\;\;\;t_{2}\,=\,t_{3}\\\
\hline\cr t_{1}\,=\,t_{3}\end{array}\\\
4.1&\;\;\mbox{Substitutivity}&\;\;\begin{array}[]{c}t_{i}\,=\,t^{\prime}_{i}\\\
\hline\cr f(t_{1},\ldots t_{i},\ldots t_{k})\,=\,f(t_{1},\ldots
t^{\prime}_{i},\ldots t_{k})\end{array}&\mbox{for any $f$ and $1\leq i\leq
n$}\\\ 4.2&\;\;\mbox{Recursion}&\;\;\begin{array}[]{c}t_{1}=t_{2}\wedge
C\doteq t_{1}\\{C/x\\}\wedge D\doteq t_{2}\\{D/x\\}\\\ \hline\cr
C=D\end{array}&\\\
5.&\;\;\mbox{Instantiation}&\;\;\begin{array}[]{c}t_{1}\,=\,t_{2}\\\ \hline\cr
t_{1}[\rho]\,=\,t_{2}[\rho]\end{array}&\mbox{for any substitution $\rho$}\\\
6.&\;\;\mbox{Axioms}&\;\;\begin{array}[]{c}\\\ \hline\cr
t_{1}\,=\,t_{2}\end{array}&\mbox{for all axioms $t_{1}=t_{2}$ in $E$}\\\
\end{array}$

Table 4: Rules of equational deduction

###### Remark 5

The (one-sorted) signature $\Sigma$ for our language open SFM1 is as follows:

  * 1.

variables: $x\in Var$ (where $Var$ is finite);

  * 2.

two constants: 1 and 0;

  * 3.

process constants: $C\in\mathcal{C}$ (where $\mathcal{C}$ is finite);

  * 4.

operators:

    * (a)

$\alpha.\\_$ (a finite family of prefixing operators, one for each $\alpha\in
A\cup\\{\epsilon\\}$),

    * (b)

$\\_+\\_$ (one binary operator of alternative composition).

This means that, in this section, the syntactic definition of open SFM1 is
given with only one syntactic category in the following way:

$\begin{array}[]{lccccccccccccccl}p&::=&\mbox{\bf 1}&|&\mbox{\bf
0}&|&\alpha.p&|&p+p&|&C&|&x\\\ \end{array}$

so that it is possible to write terms, such as $x+(y+z)$, which cannot be
described in the syntax of open SFM1 of Section 4.  $\Box$

An equational theory is a tuple $(\Sigma,E)$, where $\Sigma$ is a signature
and $E$ is a set of equations of the form $t_{1}\,=\;t_{2}$, where $t_{1}$ and
$t_{2}$ are terms in $\mathcal{T}(\Sigma,V)$. The equations in $E$ are usually
called axioms and the equational theory $(\Sigma,E)$ is often called an
axiomatization.

For any equational theory $(\Sigma,E)$, there is a standard set of proof rules
for deriving equalities on $\mathcal{T}(\Sigma,V)$. This set of proof rules
forms an equational deductive proof system $D(E)$, composed of the rules in
Table 4.

A proof is a finite sequence of equalities
$t_{1}\,=\,t^{\prime}_{1},\;t_{2}\,=\,t^{\prime}_{2},\ldots
t_{k}\,=\,t^{\prime}_{k}$ such that each $t_{i}\,=\,t^{\prime}_{i}$ is either
an axiom (rule $1$ or $6$) or can be derived by using one of the rules $2-5$
with premises some of the previous equalities
$t_{1}\,=\,t^{\prime}_{1},\;t_{2}\,=\,t^{\prime}_{2},\ldots
t_{i-1}\,=\,t^{\prime}_{i-1}$. This linear representation of a proof can be
more conveniently expressed in the form of a tree (proof tree).

We use the notation $E\vdash t_{1}\,=\,t_{2}$ if there exists a proof with
$t_{1}\,=\,t_{2}$ as its last equality, using only the axioms in $E$ (plus the
axiom in rule $1$). This directly determines a congruence over the set of
terms: $t_{1}=_{E}t_{2}$ if and only if $E\vdash t_{1}\,=\,t_{2}$. Indeed,
note that rules $1-3$ ensure that the relation $=_{E}$ that $D(E)$ is inducing
on $\mathcal{T}(\Sigma,V)$ is an equivalence relation; similarly, rules $4.1$
and $4.2$ ensures substitutivity of equals for equals in any context, i.e.,
that the relation $=_{E}$ that $D(E)$ is inducing is a congruence.

Let $S\subseteq\mathcal{T}(\Sigma)$ be the set of terms of interest (we may
think that $S$ is the set $\mathcal{P}_{SFM1}$ of SFM1 processes, which is
included in the larger set of all the closed terms of the syntax of open SFM1
in Remark 5).

Let $R\subseteq S\times S$ be a relation on closed (or ground) terms. The
equational deductive proof system $D(E)$ for the equational theory
$(\Sigma,E)$ is (ground) sound w.r.t. $R$ if

$\forall(t_{1},t_{2})\in S\times S,\quad E\vdash t_{1}\,=\,t_{2}\;\;\mbox{
implies }\;\;(t_{1},t_{2})\in R.$

$D(E)$ is (ground) complete w.r.t. $R$ if

$(t_{1},t_{2})\in R\;\;\mbox{ implies }\;\;E\vdash t_{1}\,=\,t_{2}.$

In other words, a sound and complete axiomatization $(\Sigma,E)$ of a
congruence $R$ on $S\subseteq\mathcal{T}(\Sigma)$ is such that the congruence
$t_{1}=_{E}t_{2}$ induced by $D(E)$ on $S$ is exactly the same congruence
defined by $R$.

##  7 Axiomatization

In this section we present a sound and complete, finite axiomatization of
language equivalence over SFM1. As hinted in the previous section (cf. Remark
5), for simplicity’s sake, the syntactic definition of open SFM1 is given with
only one syntactic category, but each ground instantiation of an axiom must
respect the syntactic definition of SFM1 given in Section 4; this means that
we can write the axiom $x+(y+z)=(x+y)+z$, but it is invalid to instantiate it
to $C+(a.\mbox{\bf 1}+b.\mbox{\bf 1})=(C+a.\mbox{\bf 1})+b.\mbox{\bf 1}$
because these are not legal SFM1 processes (the constant $C$ cannot be used as
a summand).

###  7.1 The Axioms

The set of axioms is outlined in Table 5. The axioms A1-A4 are the usual
axioms for choice [17, 27, 18, 20]. The axiom schemata T1-T3 are those for
prefixing, that are finitely many as $A$ is finite. Note that T3 has the side
condition $x\neq C$, meaning that it can be used only if $x$ is not
instantiated to a process constant: this is necessary to preserve constant
guardedness (see Remark 3). The conditional axioms R1-R3 are about process
constants and are similar to those in [20, 21, 13, 14]. Note that these
conditional axioms are actually a finite collection of axioms, one for each
constant definition: since the set $\mathcal{C}$ of process constants is
finite, the instances of R1-R3 are finitely many as well.

The folding axiom R2 has some similarities with this ‘iterative’ conditional
axiom, due to Arden [2] and Salomaa [27]:

$x=(y\cdot x)+z\;\Rightarrow\;x=y^{*}z$,

provided that $y$ does not have the empty word property (ewp, for short),
meaning that $\epsilon\not\in L(y)$. Kozen [18] considers this conditional
axiom not algebraic, in the sense that it is not preserved by substitution.
The side condition $og(p)$ (being equivalent to $\epsilon\not\in L^{x}_{p}$)
of R2 is essentially the negation of the ewp property. However, the
conditional axiom R2 is algebraic because the term $p$ is a concrete one (not
a variable), depending on the actual definition of the constant $C$. The
excision axiom R3 has some similarities with one law proposed by Salomaa in
[27], namely $(x+\mbox{\bf 1})^{*}=x^{*}$.

Besides the folding axiom R2, we consider also a stronger variant, called R2′,
where the side condition $og(p)$ is omitted:

R2′ (B-Folding) if $C\doteq p\\{C/x\\}\;\wedge q=p\\{q/x\\}$ then $C=q$

which holds for bisimilarity [20, 13].

We call $B$ the set of axioms $\\{$A1, A2, A3, A4, R1, R2′$\\}$ that are sound
and complete for bisimilarity [20, 13, 14], while we call $W_{g}$ the set of
axioms $\\{$A1, A2, A3, A4, T1, T2, T3, R1, R2$\\}$ that we will prove to be a
sound and complete axiomatization of language equivalence for observationally
guarded SFM1 processes, while $W=W_{g}\cup\\{$R3$\\}$ is the full
axiomatization of language equivalence over the whole of SFM1. By the notation
$W\vdash p=q$ we mean that there exists an equational deduction proof of the
equality $p=q$, by using the axioms in $W$.

$\begin{array}[]{llrcll}{\bf
A1}&\;\;\mbox{Associativity}&\;\;x+(y+z)&=&(x+y)+z&\\\ {\bf
A2}&\;\;\mbox{Commutativity}&\;\;x+y&=&y+x&\\\ {\bf
A3}&\;\;\mbox{Identity}&\;\;x+\mbox{\bf 0}&=&x&\\\ {\bf
A4}&\;\;\mbox{Idempotence}&\;\;x+x&=&x&\\\ \end{array}$

$\begin{array}[]{llrcll}{\bf T1}&\;\;\mbox{Annihilation}&\;\;\alpha.\mbox{\bf
0}&=&\mbox{\bf 0}&\\\ {\bf
T2}&\;\;\mbox{Distributivity}&\;\;\alpha.(x+y)&=&\alpha.x+\alpha.y&\\\ {\bf
T3}&\;\;\mbox{$\epsilon$-absorption}&\;\;\epsilon.x&=&x&\quad\mbox{ if $x\neq
C$}\\\ \end{array}$

$\begin{array}[]{llrcllll}{\bf R1}&\;\mbox{Unfolding}&\;\;\mbox{if $C\doteq
p\;$}&\mbox{then}&\mbox{$C=p$}&\\\ {\bf R2}&\;\mbox{Folding}&\mbox{if $C\doteq
p\\{C/x\\}\;\wedge\;og(p)\;\wedge\;q=p\\{q/x\\}$}&\mbox{then}&\mbox{$C=q$}&\\\
{\bf R3}&\;\mbox{Excision}&\mbox{if $C\doteq(\epsilon.x+p)\\{C/x\\}\wedge
D\doteq p\\{D/x\\}$}&\mbox{then}&C=D&\\\ \end{array}$

Table 5: Axioms for language equivalence

###### Theorem 4

(Soundness) For every $p,q\in\mathcal{P}_{SFM1}$, if $W\vdash p=q$, then
$p\sim q$.

###  7.2 Normal Forms, Unique Solutions and $\epsilon$-free Normal Forms

An SFM1 process $p$ is a normal form if the predicate $nf(p)$ holds. This
predicate stands for $nf(p,\emptyset)$, whose inductive definition is
displayed in Table 6. Examples of terms which are not in normal form are
$a.b.\mbox{\bf 1}$ and $C\doteq a.b.C+\mbox{\bf 1}$.

$\begin{array}[]{cccccc}\begin{array}[]{c}\\\ \hline\cr nf(\mbox{\bf
1},I)\end{array}&&\begin{array}[]{c}\\\ \hline\cr nf(\mbox{\bf
0},I)\end{array}&&\begin{array}[]{c}nf(p,I\cup\\{C\\})\quad C\doteq p\quad
C\not\in I\\\ \hline\cr nf(C,I)\end{array}\\\ \begin{array}[]{c}nf(C,I)\\\
\hline\cr nf(\alpha.C,I)\end{array}&&\begin{array}[]{c}nf(p,I)\quad nf(q,I)\\\
\hline\cr nf(p+q,I)\end{array}&&\begin{array}[]{c}C\in I\\\ \hline\cr
nf(C,I)\end{array}\\\ \end{array}$

Table 6: Normal form predicate

Note that if $C$ is a normal form, then its body (ignoring all the possible
summands 0 or duplicated summands 1, that can be absorbed via axioms A3-A4) is
of the form $\sum_{i=1}^{n}\alpha_{i}.C_{i}$ or
$\sum_{i=1}^{n}\alpha_{i}.C_{i}+\mbox{\bf 1}$, (assuming that
$\sum_{i=1}^{n}\alpha_{i}.C_{i}$ is 0 if $n=0$) where, in turn, each $C_{i}$
is a normal form. As a matter of fact, according to the construction in the
proof of Theorem 2, the processes representing reduced NFAs are in normal
form.

Now we show that, for each SFM1 process $p$, there exists a normal form $q$
such that $B\vdash p=q$. Since bisimilarity is finer than language
equivalence, this ensures that the normal form $q$ is language equivalent to
$p$.

###### Proposition 8

(Reduction to normal form) Given an SFM1 process $p$, there exists a normal
form $q$ such that $B\vdash p=q$.

###### Corollary 2

(Reduction to observationally guarded normal form) Given an observationally
guarded SFM1 process $p$, there exists an observationally guarded normal form
$q$ such that $W_{g}\vdash p=q$.

###### Remark 6

(Normal forms as systems of equations) As a matter of fact, we can restrict
our attention only to normal forms defined by constants: if $p$ is a normal
form and $p$ is not a constant, then take a new constant $D\doteq p$, which is
a normal form such that $B\vdash D=p$ by axiom R1. For this reason, in the
following we restrict our attention to normal forms that can be defined by
means of a system of equations: a set
$\widetilde{C}=\\{C_{1},C_{2},\ldots,C_{n}\\}$ of defined constants in normal
form, such that $\mbox{{\it Const}$(C_{1})$}=\widetilde{C}$ and $\mbox{{\it
Const}$(C_{i})$}\subseteq\widetilde{C}$ for $i=1,\ldots,n$. The equations of
the system $E(\widetilde{C})$ are of the following form (where function
$f(i,j)$ returns a value $k$ such that $1\leq k\leq n$):

$\begin{array}[]{lcllcllcl}C_{1}&\doteq&\sum_{i=1}^{m(1)}\alpha_{1i}.C_{f(1,i)}\\{+\mbox{\bf
1}\\}\\\ C_{2}&\doteq&\sum_{i=1}^{m(2)}\alpha_{2i}.C_{f(2,i)}\\{+\mbox{\bf
1}\\}\\\ \ldots\\\
C_{n}&\doteq&\sum_{i=1}^{m(n)}\alpha_{ni}.C_{f(n,i)}\\{+\mbox{\bf 1}\\}\\\
\end{array}$

where by the notation $\\{+\mbox{\bf 1}\\}$ we mean that the additional
summand 1 is optional, and where we assume $C_{i}\doteq\mbox{\bf 0}$ in case
$m(i)=0$. We sometimes use the notation $body(C_{h})$ to denote the sumform
$\sum_{i=1}^{m(h)}\alpha_{hi}.C_{f(h,i)}\\{+\mbox{\bf 1}\\}$.  $\Box$

###### Remark 7

(Observationally guarded system of equations) We say that a system of
equations $E(\widetilde{C})$, not necessarily in normal form like the one
above, is observationally guarded if, for each $C_{i}\in\widetilde{C}$, there
is no silent cycle
$C_{i}{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\Longrightarrow}}\>}$}}C_{i}$.
This definition is coherent with Definition 7. For instance, consider the
following example:

$\begin{array}[]{lcllcllcl}C_{1}&\doteq&a.C_{2}+\epsilon.a.C_{1}\\\
C_{2}&\doteq&b.C_{2}+\epsilon.C_{1}\\\ \end{array}$

Of course,
$C_{i}{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\nRightarrow}}\>}$}}C_{i}$
for $i=1,2$, so that the system is observationally guarded. And indeed we can
prove that $og(C_{1})$ and $og(C_{2})$ hold.  $\Box$

The next theorem shows that every observationally guarded system of equations
(not necessarily in normal form) has a unique solution up to provably
equality.

###### Theorem 5

(Unique solution for $W_{g}$) Let $\widetilde{X}=(x_{1},x_{2},\ldots,x_{n})$
be a tuple of variables and let $\widetilde{p}=(p_{1},p_{2},\ldots,p_{n})$ be
a tuple of open guarded SFM1 terms, using the variables in $\widetilde{X}$.
Let $\widetilde{C}=(C_{1},C_{2},\ldots,C_{n})$ be a tuple of constants (not
occurring in $\widetilde{p}$) such that the system of equations

$\begin{array}[]{lcllcllcl}C_{1}&\doteq&p_{1}\\{\widetilde{C}/\widetilde{X}\\}\\\
C_{2}&\doteq&p_{2}\\{\widetilde{C}/\widetilde{X}\\}\\\ \ldots\\\
C_{n}&\doteq&p_{n}\\{\widetilde{C}/\widetilde{X}\\}\end{array}$

is observationally guarded. Then, for $i=1,\ldots,n$, $W_{g}\vdash
C_{i}=p_{i}\\{\widetilde{C}/\widetilde{X}\\}$.

Moreover, if the same property holds for
$\widetilde{q}=(q_{1},q_{2},\ldots,q_{n})$, i.e., for $i=1,\ldots,n$
$W_{g}\vdash q_{i}=p_{i}\\{\widetilde{q}/\widetilde{X}\\}$, then $W_{g}\vdash
C_{i}=q_{i}$.

A system of equations is $\epsilon$-free if there are no occurrences of the
prefix $\epsilon$. Formally, an $\epsilon$-free normal form must be of the
form

$\begin{array}[]{lcllcllcl}C_{1}&\doteq&\sum_{i=1}^{m(1)}a_{1i}.C_{f(1,i)}\\{+\mbox{\bf
1}\\}\\\ C_{2}&\doteq&\sum_{i=1}^{m(2)}a_{2i}.C_{f(2,i)}\\{+\mbox{\bf 1}\\}\\\
\ldots\\\ C_{n}&\doteq&\sum_{i=1}^{m(n)}a_{ni}.C_{f(n,i)}\\{+\mbox{\bf
1}\\}\\\ \end{array}$

where all the actions $a_{ij}\in A$.

We want to show that an observationally guarded normal form can be equated to
an $\epsilon$-free normal form by using the axioms in $W_{g}$, in particular
T3. In fact, assume that

$C_{h}\doteq\sum_{i=1}^{m(h)}a_{hi}.C_{f(h,i)}+\sum_{i=1}^{m^{\prime}(h)}\epsilon.C_{g(h,i)}\\{+\mbox{\bf
1}\\}$

and that $C_{g(h,i)}\doteq p_{g(h,i)}$. Then, by R1, T3 and substitutivity, we
have that

$W_{g}\vdash
C_{h}=\sum_{i=1}^{m(h)}a_{hi}.C_{f(h,i)}+\sum_{i=1}^{m^{\prime}(h)}p_{g(h,i)}\\{+\mbox{\bf
1}\\}$.

Of course, in $p_{g(h,i)}$ there may be still occurrences of $\epsilon$, but,
since the system of equations is observationally guarded, we may proceed as
above starting from the constant with no prefix $\epsilon$ and then going
backward till reaching the initial constant $C_{1}$, as illustrated in the
following example.

###### Example 6

Consider the following observationally guarded normal form:

$\begin{array}[]{rcl}C_{1}&\doteq&a.C_{1}+\epsilon.C_{2}+\mbox{\bf 1}\\\
C_{2}&\doteq&b.C_{2}+\epsilon.C_{3}\\\ C_{3}&\doteq&a.C_{3}+\mbox{\bf 1}\\\
\end{array}$

It is easily seen that $W_{g}\vdash C_{3}=a.C_{3}+\mbox{\bf 1}$, $W_{g}\vdash
C_{2}=b.C_{2}+a.C_{3}+\mbox{\bf 1}$ and so also $W_{g}\vdash
C_{1}=a.C_{1}+b.C_{2}+a.C_{3}+\mbox{\bf 1}$. Therefore, we can define a new
$\epsilon$-free system of equations:

$\begin{array}[]{rcl}D_{1}&\doteq&a.D_{1}+b.D_{2}+a.D_{3}+\mbox{\bf 1}\\\
D_{2}&\doteq&b.D_{2}+a.D_{3}+\mbox{\bf 1}\\\ D_{3}&\doteq&a.D_{3}+\mbox{\bf
1}\\\ \end{array}$

Finally, by Theorem 5, we get $W_{g}\vdash C_{i}=D_{i}$ for $i=1,2,3$.  $\Box$

###### Proposition 9

(Reduction to $\epsilon$-free normal form) Let
$\widetilde{X}=(x_{1},x_{2},\ldots,x_{n})$ be a tuple of variables. Let
$\widetilde{p}=(p_{1},p_{2},\ldots,p_{n})$ be a tuple of open guarded SFM1
terms, using the variables in $\widetilde{X}$, of the form
$p_{h}=\sum_{i=1}^{m(h)}\alpha_{hi}.x_{f(h,i)}\\{+\mbox{\bf 1}\\}$ for
$h=1,\ldots,n$ and where $f$ is such that $1\leq f(h,i)\leq n$. Let
$\widetilde{C}=(C_{1},C_{2},\ldots,C_{n})$ be a tuple of constants such that
the system of equations in normal form

$\begin{array}[]{lcllcllcl}C_{1}&\doteq&p_{1}\\{\widetilde{C}/\widetilde{X}\\}\\\
C_{2}&\doteq&p_{2}\\{\widetilde{C}/\widetilde{X}\\}\\\ \ldots\\\
C_{n}&\doteq&p_{n}\\{\widetilde{C}/\widetilde{X}\\}\end{array}$

is observationally guarded. Then, there exist a tuple
$\widetilde{q}=(q_{1},q_{2},\ldots,q_{n})$ of open guarded SFM1 terms, using
the variables in $\widetilde{X}$, and a tuple of constants
$\widetilde{D}=(D_{1},D_{2},\ldots,D_{n})$ such that the system of equations
in normal form

$\begin{array}[]{lcllcllcl}D_{1}&\doteq&q_{1}\\{\widetilde{D}/\widetilde{X}\\}\\\
D_{2}&\doteq&q_{2}\\{\widetilde{D}/\widetilde{X}\\}\\\ \ldots\\\
D_{n}&\doteq&q_{n}\\{\widetilde{C}/\widetilde{X}\\}\end{array}$

is $\epsilon$-free and, for $i=1,\ldots,n$, $W_{g}\vdash C_{i}=D_{i}$.

###  7.3 Deterministic Normal Form

Given an alphabet $A=\\{a_{1},\ldots,a_{k}\\}$, we say that an $\epsilon$-free
normal form is deterministic if it is of the form

$\begin{array}[]{lcllcllcl}C_{1}&\doteq&\sum_{i=1}^{k}a_{i}.C_{f(1,i)}\\{+\mbox{\bf
1}\\}\\\ C_{2}&\doteq&\sum_{i=1}^{k}a_{i}.C_{f(2,i)}\\{+\mbox{\bf 1}\\}\\\
\ldots\\\ C_{n}&\doteq&\sum_{i=1}^{k}a_{i}.C_{f(n,i)}\\{+\mbox{\bf 1}\\}\\\
\end{array}$

i.e., the body of each constant contains exactly one summand for each action
$a_{i}\in A$. Of course, the NFA associated to $C_{1}$, according to the
denotational semantics in Table 2, is deterministic and has exactly $A$ as its
alphabet.

Note that the concept of determinism heavily depends on the chosen alphabet.
For instance, according to the denotational semantics in Table 2, the NFA for
$C\doteq\mbox{\bf 0}$ is deterministic, because its alphabet is empty.
However, it is not deterministic if we consider a nonempty alphabet, say
$A=\\{a\\}$, because there is not an arc for $a$. In such a case, a DFA w.r.t.
$A$, language equivalent to $C\doteq\mbox{\bf 0}$, could be the one associated
to $E\doteq a.E$. Indeed, it is possible to prove that $W_{g}\vdash C=E$ by
means of axioms T1, R1, R2; in fact, by axiom T1, we have
$W_{g}\vdash\mbox{\bf 0}=a.\mbox{\bf 0}$; then, by axiom R2, from $E\doteq
a.E$ and $W_{g}\vdash\mbox{\bf 0}=a.\mbox{\bf 0}$, we get $W_{g}\vdash
E=\mbox{\bf 0}$; then by axiom R1, we have $W_{g}\vdash C=\mbox{\bf 0}$, so
that $W_{g}\vdash C=E$ follows by transitivity.

Similarly, the NFA for $C\doteq\mbox{\bf 1}$ is deterministic, because its
alphabet is empty. However, it is not deterministic if we consider the
nonempty alphabet $A=\\{a\\}$. In such a case, a DFA w.r.t. $A$, language
equivalent to $C\doteq\mbox{\bf 1}$, could be the one associated to $D\doteq
a.E+\mbox{\bf 1}$, where $E\doteq a.E$ denotes a sink, i.e., an error state.
We can prove that $W_{g}\vdash C=D$ as follows. First, we already know that
$W_{g}\vdash E=\mbox{\bf 0}$; so, by substitutivity and R1, we have
$W_{g}\vdash D=a.\mbox{\bf 0}+\mbox{\bf 1}$; then by T1, $W_{g}\vdash
D=\mbox{\bf 0}+\mbox{\bf 1}$; then by axioms A2,A3, we have $W_{g}\vdash
D=\mbox{\bf 1}$, so that $W_{g}\vdash C=D$ follows easily.

Now we prove that, given an $\epsilon$-free normal form, it is possible to
construct a provably equivalent deterministic normal form. The idea behind the
proof, that follows the classic Rabin-Scott subset construction [25], is
illustrated by the following example.

###### Example 7

Let us consider the following $\epsilon$-free normal form

$\begin{array}[]{rcl}C_{1}&\doteq&a.C_{1}+a.C_{2}+a.C_{1}\\\
C_{2}&\doteq&a.C_{2}+\mbox{\bf 1}\\\ \end{array}$

whose alphabet $A_{C}$ is $\\{a\\}$. Let us take an alphabet $A=\\{a,b\\}$,
w.r.t. which we want to define an equivalent deterministic normal form. First,
we define a collection of set-indexed constants $B_{I}$, where
$I\subseteq\\{1,2\\}$, as $B_{I}\doteq\sum_{i\in I}body(C_{i})$. More
explicitly,

$\begin{array}[]{rcl}B_{\\{1\\}}&\doteq&a.C_{1}+a.C_{2}+a.C_{1}\\\
B_{\\{2\\}}&\doteq&a.C_{2}+\mbox{\bf 1}\\\
B_{\\{1,2\\}}&\doteq&a.C_{1}+a.C_{2}+a.C_{1}+a.C_{2}+\mbox{\bf 1}\\\
B_{\emptyset}&\doteq&\mbox{\bf 0}\\\ \end{array}$

Now, for each of them, we prove that it can be equated to a deterministic
definition. First, we can prove that, since $B_{\emptyset}=\mbox{\bf 0}$ by
axiom R1, also $W_{g}\vdash B_{\emptyset}=a.B_{\emptyset}+b.B_{\emptyset}$ by
axioms T1,A3.

Now, by axiom R1, we know that $W_{g}\vdash
B_{\\{1\\}}=a.C_{1}+a.C_{2}+a.C_{1}$, so that $W_{g}\vdash C_{1}=B_{\\{1\\}}$.
Then, by axioms A1-A4,T2,R1, we can derive $W_{g}\vdash
B_{\\{1\\}}=a.(body(C_{1})+body(C_{2}))$. Then, we can also derive
$W_{g}\vdash B_{\\{1\\}}=a.B_{\\{1,2\\}}+b.B_{\emptyset}$ by axioms R1,T1,A3.

In the same way, we can prove that $W_{g}\vdash
B_{\\{2\\}}=a.B_{\\{2\\}}+b.B_{\emptyset}+\mbox{\bf 1}$ and that $W_{g}\vdash
B_{\\{1,2\\}}=a.B_{\\{1,2\\}}+b.B_{\emptyset}+\mbox{\bf 1}$.

Finally, we define a new deterministic system of equations

$\begin{array}[]{rcl}D_{\\{1\\}}&\doteq&a.D_{\\{1,2\\}}+b.D_{\emptyset}\\\
D_{\\{2\\}}&\doteq&a.D_{\\{2\\}}+b.D_{\emptyset}+\mbox{\bf 1}\\\
D_{\\{1,2\\}}&\doteq&a.D_{\\{1,2\\}}+b.D_{\emptyset}+\mbox{\bf 1}\\\
D_{\emptyset}&\doteq&a.D_{\emptyset}+b.D_{\emptyset}\\\ \end{array}$

where $D_{\\{2\\}}$ is redundant as $D_{\\{2\\}}\not\in\mbox{{\it
Const}$(D_{\\{1\\}})$}$, such that, by Theorem 5, we have $W_{g}\vdash
B_{I}=D_{I}$ for $I=\\{1\\},\\{2\\},\\{1,2\\},\emptyset$. So, $W_{g}\vdash
C_{1}=D_{\\{1\\}}$ by transitivity.  $\Box$

###### Proposition 10

(Reduction to deterministic normal form) Given the $\epsilon$-free normal form

$\begin{array}[]{lcllcllcl}C_{1}&\doteq&\sum_{i=1}^{m(1)}a_{1i}.C_{f(1,i)}\\{+\mbox{\bf
1}\\}\\\ C_{2}&\doteq&\sum_{i=1}^{m(2)}a_{2i}.C_{f(2,i)}\\{+\mbox{\bf 1}\\}\\\
\ldots\\\ C_{n}&\doteq&\sum_{i=1}^{m(n)}a_{ni}.C_{f(n,i)}\\{+\mbox{\bf
1}\\}\\\ \end{array}$

such that its alphabet is $A_{C}$, it is possible to construct a deterministic
normal form w.r.t. a chosen $A=\\{a_{1},a_{2},\ldots,a_{k}\\}$, with
$A_{C}\subseteq A$, of the form

$\begin{array}[]{lcllcllcl}D_{1}&\doteq&\sum_{i=1}^{k}a_{i}.D_{g(1,i)}\\{+\mbox{\bf
1}\\}\\\ D_{2}&\doteq&\sum_{i=1}^{k}a_{i}.D_{g(2,i)}\\{+\mbox{\bf 1}\\}\\\
\ldots\\\ D_{m}&\doteq&\sum_{i=1}^{k}a_{i}.D_{g(m,i)}\\{+\mbox{\bf 1}\\}\\\
\end{array}$

where $m\geq n$, such that $W_{g}\vdash C_{1}=D_{1}$.

###  7.4 Completeness for Observationally Guarded Processes

Proposition 10 is at the basis of the lemma below, which, in turn, is crucial
for the proof of completeness for observationally guarded processes that
follows. The proof technique of the lemma below is inspired to the proof of
Theorem 5.10 in [20], in turn inspired to the proof of Theorem 2 in [27].

###### Lemma 1

(Completeness for $\epsilon$-free normal forms) For every
$p,p^{\prime}\in\mathcal{P}_{SFM1}$ $\epsilon$-free normal forms, if $p\sim
p^{\prime}$, then $W_{g}\vdash p=p^{\prime}$.

###### Theorem 6

(Completeness for observationally guarded processes)

For every $p,q\in\mathcal{P}_{SFM1}$ observationally guarded, if $p\sim q$,
then $W_{g}\vdash p=q$.

###  7.5 Completeness for Unguarded Processes

In the following we restrict our attention to systems of equations, not
necessarily in normal form. In fact, if $p$ is a process and $p$ is not a
constant, then we can take a new constant $D\doteq p$ (such that $W\vdash D=p$
by axiom R1), so that $p$ is equivalently represented by the system of
equations over the set of constants Const$(D)$.

We now prove that the addition of axiom R3 to $W_{g}$ is enough to equate any
SFM1 process $p$ to an observationally guarded SFM1 process $q$. In order to
prove this result, we need some auxiliary notation.

First of all, we denote by $n_{x}(p)$ the number of unguarded occurrences of
$x$ in $p$ (including the bodies of the constants occurring in $p$). E.g., if
$C\doteq p\\{C/x\\}$ and $p=\epsilon.x+a.x+\epsilon.D$, with
$D\doteq\epsilon.D+\epsilon.x$, then $n_{x}(p)=2$; moreover, we set
$n_{x}(C)=n_{x}(p)$.

Then, we need to introduce a measure of the length of all the
$\epsilon$-labeled computations leading to an occurrence of an unguarded
variable $x$. This value $\mbox{$len$}(p)$ for the SFM1 term $p$ (which may be
open on $x$, but the definition applies also to closed terms) is computed by
the length function defined in Table 7. Note that if a symbol, say $a$, of the
alphabet prefixes a process, then the returned value is $0$, while the
variable $x$ returns $1$. Moreover, in case of composition with the choice
operator, $p+p^{\prime}$, we take the sum of $\mbox{$len$}(p)$ and
$\mbox{$len$}(p^{\prime})$. The crucial rule is that for the constant: if
$C\doteq p\\{C/x\\}$, then, even if $C$ is closed, its length is computed on
the open term $p$. It is an easy exercise to show that the open term $p$ is
observationally guarded (cf. Definition 7) if and only if
$\mbox{$len$}(p)=n_{x}(p)=0$. Moreover, if $p$ is closed (actually a closed
system of equations), then $p$ is observationally guarded (cf. Remark 7) if
and only if $\mbox{$len$}(p)=n_{x}(p)=0$.

$\begin{array}[]{rcllrcllllll}\mbox{$len$}(\mbox{\bf
1})&=&0&&\mbox{$len$}(\mbox{\bf 0})&=&0\\\
\mbox{$len$}(p+p^{\prime})&=&\mbox{$len$}(p)+\mbox{$len$}(p^{\prime})&&\mbox{$len$}(C)&=&\mbox{$len$}(p)\quad\mbox{if
$C\doteq p\\{C/x\\}$}\\\
\mbox{$len$}(x)&=&1&&\mbox{$len$}(\epsilon.p)&=&\begin{cases}1+\mbox{$len$}(p)&\mbox{if
$\mbox{$len$}(p)\neq 0$}\\\ 0&\mbox{otherwise}\end{cases}\\\
\mbox{$len$}(a.p)&=&0&&\\\\[-5.69046pt] \end{array}$

Table 7: Length function

###### Proposition 11

(Reduction to observationally guarded process for $W$) Let
$\widetilde{X}=(x_{1},x_{2},\ldots,x_{n})$ be a tuple of variables and let
$\widetilde{p}=(p_{1},p_{2},\ldots,p_{n})$ be a tuple of open guarded SFM1
terms, using the variables in $\widetilde{X}$. Let
$\widetilde{C}=(C_{1},C_{2},\ldots,C_{n})$ be a tuple of constants (not
occurring in $\widetilde{p}$) such that the system of equations

$\begin{array}[]{lcllcllcl}C_{1}&\doteq&p_{1}\\{\widetilde{C}/\widetilde{X}\\}\\\
C_{2}&\doteq&p_{2}\\{\widetilde{C}/\widetilde{X}\\}\\\ \ldots\\\
C_{n}&\doteq&p_{n}\\{\widetilde{C}/\widetilde{X}\\}\end{array}$

is observationally unguarded. Then, there exist a tuple
$\widetilde{q}=(q_{1},q_{2},\ldots,q_{n})$ of open guarded SFM1 terms, using
the variables in $\widetilde{X}$, and a tuple
$\widetilde{D}=(D_{1},D_{2},\ldots,D_{n})$ (not occurring in $\widetilde{q}$)
such that the system of equations

$\begin{array}[]{lcllcllcl}D_{1}&\doteq&q_{1}\\{\widetilde{D}/\widetilde{X}\\}\\\
D_{2}&\doteq&q_{2}\\{\widetilde{D}/\widetilde{X}\\}\\\ \ldots\\\
D_{n}&\doteq&q_{n}\\{\widetilde{C}/\widetilde{X}\\}\end{array}$

is observationally guarded and, for $i=1,\ldots,n$, $W\vdash C_{i}=D_{i}$.

###### Theorem 7

(Completeness of $W$ over the whole of SFM1) For every
$p,q\in\mathcal{P}_{SFM1}$, if $p\sim q$, then $W\vdash p=q$.

##  8 Conclusion and Future Research

In this paper, we have shown how to use the process algebra SFM1, that truly
represents NFAs up to isomorphism, in order to find a sound and complete
axiomatization of language equivalence, and so also a sound and complete,
finite axiomatization of regular languages, which is alternative to those
based on the Kleene algebra of regular expressions [27, 7, 18]. As a matter of
fact, our axiomatization, composed of 7 axioms and 3 conditional axioms, seems
more concise than these. On the one hand, the classic axiomatization by Kozen
[18] is composed of 11 axioms for disjunction and concatenation, and 4 axioms
for iteration (two of which are conditional). However, this is not the so far
optimal axiomatization of language equivalence with Kleene algebras; in fact,
[19] showed that one of Kozen’s conditional axioms can be removed at the price
of adding a few equational axioms, and then [9] improved this result by
showing that language equivalence can be axiomatized by a (left-handed) Kleene
algebra defined by 13 axioms, only one of which is conditional. On the other
hand, it should be remarked that our axiomatization makes use of axiom
schemata (in particular, for recursion), while [18, 9] do not.

NFAs without $\epsilon$-labeled transitions have been investigated by
Alexandra Silva in her Ph.D. thesis [29], using co-algebraic techniques [26].
In chapter 5, based on a joint work with Bonsangue and Rutten [30], she
considers a (co-)algebra to describe such NFAs that, similarly to SFM1,
features an action prefixing operator (but the prefix $\epsilon$ is not
considered) instead of concatenation, and recursion (implemented by means of
the standard fixpoint operator of [20]) instead of Kleene star, but this
algebra also contains a few additional operators. For this (co-)algebra, she
proved a sort of representability theorem, up to language equivalence.
Moreover, she defines an axiomatization of language equivalence that, for the
syntactic peculiarities of her (co-)algebra, turns out to be rather verbose,
as it is composed of 18 axioms (while our axiomatization for SFM1 without the
prefix $\epsilon$, is composed of 8 axioms only, as T3 and R3 are not
necessary, and, moreover, R2 can be replaced by the simpler R2′).

Another goal of this paper is to show the usefulness of representability
theorems, up to isomorphism (like Theorem 2), for the algebraic study of
semantic models, like NFAs. In fact, SFM1 has allowed us to study also
bisimulation equivalence on NFAs and to hint a sound and complete
axiomatization for it (the set $B$), composed of 4 axioms and 2 conditional
axioms, only. Future research may be devoted to extend the axiomatic theory of
SFM1 to other behavioral equivalences in the linear-time/branching-time
spectrum [10, 11]. For instance, we claim that weak simulation equivalence
[24, 1] can be axiomatized by replacing axiom T2 in the set $W$ with the axiom

T2′ $a.(x+y)=a.(x+y)+a.y$.

Interestingly enough, we have proposed similar representability theorems about
various classes of Petri nets in [12], offering for each class a specific
process algebra truly representing the models of that class, up to
isomorphism. In [13, 14] one of these results has been exploited for
axiomatizing bisimulation-based, behavioral equivalences over a small class of
finite Petri nets.

In the literature there are other process algebras that describe regular
behaviors, the most prominent one being BPA∗ (see, e.g., [5, 3, 11]), which
corresponds syntactically to the definition of regular expressions. The
abstract syntax of BPA∗ is

$p\;::=\;\mbox{\bf 0}\;\;\big{|}\;\;\mbox{\bf
1}\;\;\big{|}\;\;\alpha\;\;\big{|}\;\;p+p\;\;\big{|}\;\;p\cdot
p\;\;\big{|}\;\;p^{*}$

where $p_{1}\cdot p_{2}$ is the operator of sequential composition, and
$p^{*}$ is the iteration operator. The semantic models used to give semantics
to this process algebra are NFAs. For instance, the semantics of $(a\cdot
b)^{*}+a\cdot(b\cdot a)^{*}$ is isomorphic to the NFA outlined in Figure 6(b).
Note that the language recognized by the NFA associated to the BPA∗ process
$(a\cdot b)^{*}+a\cdot(b\cdot a)^{*}$ is exactly the language associated to
the regular expression $(a\cdot b)^{*}+a\cdot(b\cdot a)^{*}$.

Interestingly enough, this process algebra is strictly less expressive than
SFM1. In fact, Milner already observed in [20] that there are NFAs that are
not bisimulation equivalent to any process of BPA∗: for instance, the NFA in
Figure 6(a), which instead can be represented in SFM1, up to isomorphism
(hence, also up to bisimilarity), simply by the system of equations

$\begin{array}[]{rcl}C_{0}&\doteq&a.C_{1}+\mbox{\bf 1}\\\
C_{1}&\doteq&b.C_{0}+\mbox{\bf 1}\\\ \end{array}$

However, BPA∗ can represent all the regular languages: given a regular
language $L$, there exists a BPA∗ process $p$ such that its associated NFA
recognizes $L$. For instance, a BPA∗ process, which is language equivalent to
the one in Figure 6(a), is actually $(a\cdot b)^{*}+a\cdot(b\cdot a)^{*}$,
whose associated semantics is isomorphic to the NFA in Figure 6(b). This is
not very surprising, as we already noted in the introduction (cf. Figure 1)
that regular expressions are a formalism that can represent all the NFAs, but
only up to language equivalence. An interesting study about the subclass of
NFAs that are actually expressible, up to bisimilarity, with BPA∗ is described
in [3].

$q_{0}$$q_{1}$$a$$b$$q_{2}$$q_{3}$$q_{4}$$q_{5}$$q_{6}$$a$$a$$b$$a$$b$$a$
Figure 6: An NFA not representable in BPA∗, up to bisimilarity, in (a); and in
(b) one expressible in BPA∗ that is language equivalent to the NFA in (a)

Our axiomatization is based on results and techniques developed in the area of
process algebras [20, 22, 6, 4, 28, 11] for bisimulation-based equivalences,
that we have applied and adapted to language equivalence, an equivalence
relation usually not deeply investigated in the context of process algebras.

## References

## References

  * [1] L. Aceto, D. de Frutos Escrig, C. Gregorio-Rodriguez, A. Ingólfsdóttir,  Axiomatising weak simulation semantics over BCCSP,  Theoretical Computer Science 537:42-71, 2014.
  * [2] D.N. Arden,  Delayed logic and finite state machines,  In Theory of Computing Machine Design, pp. 1-35. University of Michigan Press, 1960.
  * [3] J.C.M. Baeten, F. Corradini, C.A. Grabmayer,  A characterization of regular expressions under bisimulation,  Journal of the ACM 54(2:6),1-28, 2007.
  * [4] J.C.M. Baeten, T. Basten, M.A. Reniers,  Process Algebra: Equational Theories of Communicating Processes,  Cambridge Tracts in Theoretical Computer Science 50, Cambridge University Press, 2010.
  * [5] J.A. Bergstra, W.J. Fokkink, A. Ponse,  Process algebra with recursive operations,  Chapter 5 of [6], 333-389, 2001.
  * [6] J.A. Bergstra, A. Ponse, S.A. Smolka (eds.),  Handbook of Process Algebra,  Elsevier, 2001.
  * [7] J.H. Conway,  Regular Algebra and Finite Machines, Chapman and Hall, London, 1971. ISBN 0-412-10620-5.
  * [8] B.A. Davey, H.A. Priestley,  Introduction to Lattices and Order (second edition),  Cambridge University Press, 2002.
  * [9] A. Das, A. Doumane, D. Pous, Left-handed completeness for Kleene algebra, via cyclic proofs,  in: Gilles Barthe, Geoff Sutcliffe, Margus Veanes (Eds.), LPAR-22, 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EPiC Series in Computing, vol. 57, pp. 271-289, 2018.
  * [10] R.J. van Glabbeek,  The linear time - branching time spectrum I,  Chapter 1 of [6], 3-99, 2001.
  * [11] R. Gorrieri, C. Versari, Introduction to Concurrency Theory: Transition Systems and CCS, EATCS Texts in Theoretical Computer Science, Springer-Verlag, 2015.
  * [12] R. Gorrieri,  Process Algebras for Petri Nets: The Alphabetization of Distributed Systems,  EATCS Monographs in Theoretical Computer Science, Springer-Verlag, 2017.
  * [13] R. Gorrieri,  Axiomatizing team equivalence for finite-state machines,  The Art of Modeling Computational Systems (Catuscia Palamidessi’s Festschrift), LNCS 11760, 14-32, Springer, 2019.
  * [14] R. Gorrieri,  Team equivalences for finite-state machines with silent moves,  Information and Computation Vol. 275, 2020, DOI:10.1016/j.ic.2020.104603
  * [15] Gross J.L., Yellen J. (Eds.),  Handbook of Graph Theory. Discrete Mathematics and it Applications. CRC Press, 2004.
  * [16] J.E. Hopcroft, R. Motwani, J.D. Ullman,  Introduction to Automata Theory, Languages and Computation, 2nd ed.,  Addison-Wesley, 2001.
  * [17] S.C. Kleene,  Representation of events in nerve nets and finite automata,  Automata Studies, Annals of Mathematical Studies, Princeton Univ. Press. 34 (sect.7.2, p.26-27), 1956.
  * [18] D. Kozen,  A completeness theorem for Kleene algebras and the algebra of regular events,  Information and Computation 110(2):366-390, 1994. doi:10.1006/inco.1994.1037
  * [19] D. Kozen, A. Silva,  Left-handed completeness,  Theoretical Computer Science 807:220-233, 2020. doi:10.1016/j.tcs.2019.10.040
Previous conference version appeared in: Wolfram Kahl, Timothy G. Griffin
(Eds.), Relational and Algebraic Methods in Computer Science (RAMiCS 2012),
Lecture Notes in Computer Science, vol. 7560, pp. 162-178, Springer, 2012.

  * [20] R. Milner,  A complete inference systems for a class of regular behaviors,  J. Comput. System Sci. 28: 439-466, 1984.
  * [21] R. Milner,  A complete axiomatisation for observational congruence of finite-state behaviours,  Information and Computation 81: 227-247, 1989.
  * [22] R. Milner. Communication and Concurrency, Prentice-Hall, 1989.
  * [23] R. McNaughton, H. Yamada,  Regular expressions and state graphs for automata,  IEEE Trans. Electronic Computers 9(1):39-47, 1960.
  * [24] D.M.R. Park,  Concurrency and automata on infinite sequences,  In Proc. 5th GI-Conference on Theoretical Computer Science, LNCS 104, 167-183, Springer-Verlag, 1981.
  * [25] M.O. Rabin, D. Scott,  Finite automata and their decision problems,  IBM Journal of Research and Development 3(2):114-125, 1959.
  * [26] J.J.M.M. Rutten,  Universal coalgebra: A theory of systems,  Theor. Comput. Sci., 249(1):3-80, 2000.
  * [27] A. Salomaa,  Two complete axiom systems for the algebra of regular events,  Journal of the ACM 13(1): 58-169, 1966. doi:10.1145/321312.321326
  * [28] D. Sangiorgi,  An Introduction to Bisimulation and Coinduction,  Cambridge University Press, 2012.
  * [29] A. Silva,  Kleene Coalgebra,  Ph.D. thesis, Radboud Universiteit Nijmegen, 2010. ISBN: 978-90-6464-433-7
  * [30] A. Silva, M.M. Bonsangue, and J.J.M.M. Rutten,  Non-deterministic Kleene coalgebras,  Logical Methods in Computer Science, 6(3), 2010.