# Axiomatizing NFAs Generated by Regular Grammars

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

###### Abstract

A subclass of nondeterministic Finite Automata generated by means of regular
Grammars (GFAs, for short) is introduced. A process algebra is proposed, whose
semantics maps a term to a GFA. We prove a representability theorem: for each
GFA $N$, there exists a process algebraic term $p$ such that its semantics is
a GFA isomorphic to $N$. Moreover, we provide a concise axiomatization of
language equivalence: two GFAs $N_{1}$ and $N_{2}$ recognize the same regular
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 6 axioms
plus 2 conditional axioms, only.

###### keywords:

Regular grammar , nondeterministic finite automaton , GFA , language
equivalence , axiomatization.

##  1 Introduction

Nondeterministic finite automata (NFA for short), originally proposed in [17],
are a well-known model of sequential computation (see, e.g., [11] 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 [12].

In a recent paper [10], we have introduced a simple process algebra, called
SFM1, that truly represent the class of all NFAs, up to isomorphism. There we
also showed that language equivalence over NFAs can be axiomatized by means of
a rather compact axiomatization, composed of 7 axioms plus 3 conditional
axioms. The main aim of this paper is to improve on this result by showing
that language equivalence (for regular languages) can be axiomatized by means
of a very concise axiomatization, composed of 6 axioms plus 2 conditional
axioms only.

The staring point is to consider regular grammars (see, e.g., [22] for an
introductory textbook), i.e., those context-free grammars whose productions
have the following shape: $A\rightarrow\gamma$, where $A$ is a nonterminal
symbol and $\gamma$ can be either a single terminal followed by a single
nonterminal (e.g., $aA$), or a single terminal (e.g., $a$), or the empty word
$\epsilon$. For instance, the following grammar

$\begin{array}[]{crcl}&A&\rightarrow&aA\;\;\big{|}\;\;aB\\\
&B&\rightarrow&bB\;\;\big{|}\;\;b\end{array}$

generating the language $L=\\{a^{n}b^{m}\;\;\big{|}\;\;n\geq 1,m\geq 1\\}$,
denoted by the regular expression $a^{+}b^{+}$, is regular. It is well-known
[22, 11] that the class of regular grammars generates all and only the regular
languages. Moreover, there is an obvious algorithm for mapping regular
grammars over NFAs (adapted from [22]), described as follows. Given a regular
grammar $G$, the non-final states of the associated NFA $N_{G}$ are the
nonterminals, the initial state of $N_{G}$ is the initial nonterminal symbol,
$N_{G}$ may contain only one final state (we often denote by 1), and the
transitions in $N_{G}$ are derived from the productions in $G$ as follows:

  * 1.

transition $A{\mbox{${\>\stackrel{{\scriptstyle a}}{{\longrightarrow}}\>}$}}B$
is in $N_{G}$ if $A\rightarrow aB$ is a production in $G$;

  * 2.

transition $A{\mbox{${\>\stackrel{{\scriptstyle
a}}{{\longrightarrow}}\>}$}}\mbox{\bf 1}$ is in $N_{G}$ if $A\rightarrow a$ is
a production in $G$;

  * 3.

transition
$A{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\longrightarrow}}\>}$}}\mbox{\bf
1}$ is in $N_{G}$ if $A\rightarrow\epsilon$ is a production in $G$.

For instance, the NFA associated to the grammar above is outlined in Figure 1,
following the usual drawing convention. It is easy to observe that the
language $L(G)$ generated by the regular grammar $G$ is the same as the
language $L[N_{G}]$ recognized by the NFA $N_{G}$. Note that the NFAs produced
by this algorithm have a special form, as $(i)$ there is at most one final
state, denoted by 1; $(ii)$ the final state 1, if present, cannot be initial;
$(iii)$ there are no outgoing transitions from the final state 1; and,
finally, $(iv)$ all the $\epsilon$-labeled transitions have target state 1.

$A$$B$1$a$$a$$b$$b$ Figure 1: An NFA recognizing the language $a^{+}b^{+}$

We call this kind of NFA by GFA (acronym of by regular Grammar generated
Finite Automaton). Of course, GFAs constitute a subclass of NFAs, but have the
same expressive power as language acceptors: both classes of automata
recognize all and only the regular languages. Moreover, it is easy to observe
that, given a GFA $N$, we can reconstruct a regular grammar $G_{N}$ as
follows: the nonterminals of $G_{N}$ are the non-final states of $N$, the
initial nonterminal symbol is the initial state of $N$ and

  * 1.

$q\rightarrow aq^{\prime}$ is a production in $G_{N}$ if transition
$q{\mbox{${\>\stackrel{{\scriptstyle a}}{{\longrightarrow}}\>}$}}q^{\prime}$
is in $N$;

  * 2.

$q\rightarrow a$ is a production in $G_{N}$ if transition
$q{\mbox{${\>\stackrel{{\scriptstyle a}}{{\longrightarrow}}\>}$}}\mbox{\bf 1}$
is in $N$;

  * 3.

$q\rightarrow\epsilon$ is a production in $G_{N}$ if transition
$q{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\longrightarrow}}\>}$}}\mbox{\bf
1}$ is in $N$.

Hence, GFAs and regular grammars are in perfect correspondence, up to language
equivalence.

In this paper, we propose a process algebra, called SFM0, that truly
represents GFAs, up to isomorphism. More precisely, SFM0, which is a slight
restriction of SFM1 we proposed in [10] in order to axiomatize the class of
NFAs, is a dialect of finite-state CCS [14, 15, 7], where (besides 0 denoting
a non-final state) an additional constant 1 is introduced in order to
distinguish the (unique) final state from the non-final ones. However, 1 is to
be used in a constrained manner, i.e., only as the target of a prefix
operator. Moreover, SFM0 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. (To be precise, the prefix $\epsilon$ can be
used only with 1.) 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, SFM0 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 [15, 7]), working in the same way as nonterminals are used in regular
grammars [22, 11]. For instance, consider a recursive constant $C$ defined as
$C\doteq a.C+a.\mbox{\bf 1}$; then, its semantics is a GFA with two states,
the initial one (corresponding to $C$) and the final one (corresponding to 1),
with an $a$-labeled self-loop on the initial state and an $a$-labeled
transition from the initial state to the final one; hence, $C$ recognizes the
language $\\{a^{n}\;\;\big{|}\;\;n\geq 1\\}$, denoted by the regular
expression $a^{+}$.

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

  * $(i)$

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

  * $(ii)$

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

  * $(iii)$

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

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

One advantage of this concrete representability theorem is that the algebra
SFM0 can be used as a basis to study all the possible equivalences that can be
defined over GFAs, not only language equivalence $\sim$ (as for regular
expressions), but also more concrete equivalences, such as bisimulation
equivalence [16, 15, 1, 7], or any in the linear-time/branching-time spectrum
[6, 7].

The main contribution of this paper is the proof that language equivalence can
be characterized over SFM0 terms by means of a very concise axiomatization,
comprising only 6 axioms (4 for disjunction and 2 for prefixing) and 2
conditional axioms (for recursion). The axioms we present are very similar to
known axioms [12, 18, 13, 14, 9]. 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 and the prefixing operator distributes over
a choice term. The axioms for recursion are also similar to axioms developed
for SFM [8, 9], in turn inspired to those for finite-state CCS [15]: the
unfolding axiom (stating that a constant $C$, defined as $C\doteq p\\{C/x\\}$,
can be equated to its body $p\\{C/x\\}$), and the folding axiom (stating that
if $C\doteq p\\{C/x\\}$ and $q=p\\{q/x\\}$, then $C=q$). Our axiomatization is
more concise than that proposed in [10], because the prefix $\epsilon$ is used
in a very restricted manner, so that we were able to remove the axiom stating
that the prefix $\epsilon$ can be absorbed and also the excision axiom,
stating that $\epsilon$-labeled self-loops can be removed (i.e., 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 GFAs, including language equivalence $\sim$, bisimulation equivalence
$\simeq$ and isomorphism equivalence $\equiv$. Section 3 introduces the
algebra SFM0 (i.e., its syntax and its denotational semantics in terms of
GFAs) and proves the representability theorem sketched in Figure 2. Section 4
shows that language equivalence $\sim$ is a congruence for all the operators
of SFM0, notably recursion. Section 5 studies the algebraic properties of
language equivalence over SFM0 terms, that are useful to prove the soundness
of the axiomatization. In Section 6, we first present the set of axioms and
then prove that the axiomatization is sound and complete. Section 7 adds
concluding remarks.

##  2 GFA: Finite Automata generated by regular Grammars

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 GFA is a tuple $N=(Q,A,$ $T,F,q_{0})$ where

  * 1.

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

  * 2.

$F$ is the set of final states, such that $|F|\leq 1$; $Q\cap F=\emptyset$ and
$Q\cup F$ is ranged over by $r$ (possibly indexed);

  * 3.

$A$ is a finite alphabet;

  * 4.

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

  * 5.

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

Given a transition $t=(q,\alpha,r)$, $q$ is called the source, $\alpha$ the
label of the transition (denoted also by $l(t)$), and $r$ the target; this is
usually represented as
$q{\mbox{${\>\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}\>}$}}r$.

A GFA $N=(Q,A,T,F,q_{0})$ is semi-deterministic if $\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$. A semi-deterministic GFA is called DGFA, for short.
$\Box$

By definiton, in a GFA $N=(Q,A,T,F,q_{0})$, $(i)$ there is at most one final
state, usually denoted by 1 (because $|F|\leq 1$); $(ii)$ the final state 1,
if present, cannot be initial ($q_{0}\in Q)$; $(iii)$ there are no outgoing
transitions from the final state 1 (because the source of a transition can
only be a non-final state); and, finally, $(iv)$ all the $\epsilon$-labeled
transitions have target state 1 (because of the definition of $T$).

Note that a semi-deterministic GFA is not deterministic, in the usual sense;
in fact, from a state there may be even two transitions with the same label:
one reaching the final state and another one reaching a non-final state.

###### Definition 2

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

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

###### 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{|}\;\;q_{0}{\mbox{${\>\stackrel{{\scriptstyle\sigma}}{{\Longrightarrow}}\>}$}}\mbox{\bf
1}\\}$. The language recognized by state $r\in Q\cup F$ is
$L[N,r]=\\{\sigma\in
A^{*}\;\;\big{|}\;\;r{\mbox{${\>\stackrel{{\scriptstyle\sigma}}{{\Longrightarrow}}\>}$}}\mbox{\bf
1}\\}$. Two states $r_{1}$ and $r_{2}$ are equivalent, denoted $r_{1}\sim
r_{2}$, if $L[N,r_{1}]=L[N,r_{2}]$. Two GFAs
$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$

Following the informal discussion in Section 1, it is clear that there is a
one-to-one correspondence between GFAs and regular grammars [22], preserving
language equivalence. Therefore, the class of languages recognized by GFAs is
the class of regular languages (see, e.g., [22, 11] for introductory
textbooks), i.e., the languages denotable by regular expressions (originally
proposed by Kleene in [12]; we assume the reader is familiar with this
algebra).

###### Example 1

Figure 3 outlines two finite automata: the left one is a GFA with initial
state $q_{0}$ and final state $r_{0}$, and the right one is a DGFA with
initial state $q_{2}$ and final state $r_{1}$. 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$

$q_{0}$$q_{1}$$r_{0}$$b$$\epsilon$$a$$\epsilon$$b$$q_{2}$$r_{1}$$q_{3}$$q_{4}$$\epsilon$$b$$a$$\epsilon$$a$$b$$a,b$
Figure 3: A GFA and a DGFA both recognizing the language $a^{*}b^{*}$

More concrete equivalences can be defined on GFAs, e.g., bisimulation
equivalence [16, 15, 1, 7] and isomorphism equivalence.

###### Definition 4

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

  * 1.

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

  * 2.

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

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

###### Example 2

Given an NFA $N=(Q,A,T,F,q_{0})$, it is easy to see that if $r_{1}\simeq
r_{2}$ then $r_{1}\sim r_{2}$. The converse implication does not hold. For
instance, consider Figure 3: of course, $q_{1}\sim q_{3}$ (both recognize the
language $b^{*}$), but $q_{1}\not\simeq q_{3}$ (as only $q_{3}$ has an
outgoing transition labeled $a$).  $\Box$

###### Remark 1

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

###### Definition 5

(Isomorphism) Two GFAs $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}\cup F_{1}\rightarrow
Q_{2}\cup F_{2}$ such that:

  * 1.

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

  * 2.

it preserves transitions:
$q{\mbox{${\>\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}\>}$}}r\in
T_{1}\;\mbox{ iff
}\;f(q){\mbox{${\>\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}\>}$}}f(r)\in
T_{2}$ for all $q,r\in Q_{1}\cup F_{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$

Note that if $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 via $f$, then the
relation $R=\\{(r,f(r))\;\;\big{|}\;\;r\in Q_{1}\cup F_{1}\\}$ is a
bisimulation over the union of $N_{1}$ and $N_{2}$. Hence, isomorphism
equivalence $\equiv$ is finer than bisimulation equivalence $\simeq$, in turn,
finer than language equivalence $\sim$.

##  3 SFM0: Syntax and Semantics

###  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 SFM0 terms are generated from alphabet symbols and
constants by the following abstract syntax:

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

where the constant 0 denotes a non-final state, $\alpha.\mbox{\bf 1}$ is a
process (and a non-final state) where the symbol $\alpha\in
A\cup\\{\epsilon\\}$ prefixes the final state 1, $a.p$ is a process (and a
non-final state) where $a\in A$ prefixes any process $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$.

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
0},I)&=&\emptyset&&\delta(\alpha.\mbox{\bf 1},I)&=&\emptyset\\\
\delta(a.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 SFM0 process if Const$(p)$ is finite and each constant in
Const$(p)$ is equipped with a defining equation (in category $s$). The set of
SFM0 processes is denoted by $\mathcal{P}_{SFM_{0}}$, while the set of its
guarded processes, i.e., those in syntactic category $s$, by
$\mathcal{P}_{SFM_{0}}^{grd}$.

###  3.2 Denotational Semantics

Now we provide a construction of the GFA $\llbracket p\rrbracket_{\emptyset}$
associated with process $p$, which is compositional and denotational in style.
The details of the construction are outlined in Table 1. 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 GFA are syntactic objects, i.e., SFM0 process terms (plus 1,
which, strictly speaking, is not an SFM0 process term). 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 GFA
$\llbracket p_{1}\rrbracket_{I}$ (or $\llbracket p_{2}\rrbracket_{I}$) is to
be kept in the GFA 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 GFA. Similarly, for the rule for constants. In Table
1 we denote by $T(q)=\\{t\in T\;\;\big{|}\;\;\exists\alpha\in
A\cup\\{\epsilon\\},\exists r\in Q\cup F.t=(q,\alpha,r)\\}$ the set of
transitions in $T$ with $q$ as source state.

$\begin{array}[]{rcllcllcl}\llbracket\mbox{\bf
0}\rrbracket_{I}&=&(\\{\mbox{\bf 0}\\},\emptyset,\emptyset,\emptyset,\mbox{\bf
0})&\llbracket\alpha.\mbox{\bf 1}\rrbracket_{I}\;=\;(\\{\alpha.\mbox{\bf
1},\mbox{\bf 1}\\},A,\\{(\alpha.\mbox{\bf 1},\alpha,\mbox{\bf
1})\\},\\{\mbox{\bf 1}\\},\alpha.\mbox{\bf 1})&\\\ &&&\mbox{where
}A=\begin{cases}\\{\alpha\\}\hskip 10.00002pt\mbox{ if
$\alpha\neq\epsilon$}\\\ \emptyset\hskip 40.00006pt\mbox{o.w.}\\\
\end{cases}\\\ \llbracket a.p\rrbracket_{I}&=&(Q,A,T,F,a.p)&\mbox{given
}\llbracket
p\rrbracket_{I}=(Q^{\prime},A^{\prime},T^{\prime},F^{\prime},p)\;\mbox{ and
where }Q=\\{a.p\\}\cup Q^{\prime}\\\ &&&F=F^{\prime},\,T=\\{(a.p,a,p)\\}\cup
T^{\prime},\,A=\\{a\\}\cup A^{\prime}\\\ \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}\\\ &&&F=F_{1}\cup F_{2},\;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,r)\;\;\big{|}\;\;(p_{i},\alpha,r)\in
T_{i},i=1,2\\}\\\ \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},F=F^{\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}\\\ \end{array}$

Table 1: Denotational semantics

###### Example 3

Consider constant $C\doteq(a.C+\epsilon.\mbox{\bf 1})+b.D$, where $D\doteq
b.D+\epsilon.\mbox{\bf 1}$. By using the definitions in Table 1, $\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\epsilon.\mbox{\bf 1}\rrbracket_{\\{C,D\\}}$
$=(\\{\epsilon.\mbox{\bf 1},\mbox{\bf 1}\\},\emptyset,\\{(\epsilon.\mbox{\bf
1},\epsilon,\mbox{\bf 1})\\},\\{\mbox{\bf 1}\\},\epsilon.\mbox{\bf 1})$. Then,
by summation

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

Now, the rule for constants ensures that

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

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

The rule for constants also ensures that $\llbracket
C\rrbracket_{\\{C\\}}=(\\{C\\},\emptyset,\emptyset,\emptyset,C)$. Then, by
prefixing, $\llbracket
a.C\rrbracket_{\\{C\\}}=(\\{a.C,C\\},\\{a\\},\\{(a.C,a,C)\\},\emptyset,a.C)$,
By summation, $\llbracket a.C+\epsilon.\mbox{\bf 1}\rrbracket_{\\{C\\}}=\\\
(\\{a.C+\epsilon.\mbox{\bf 1},C,\mbox{\bf
1}\\},\\{a\\},\\{(a.C+\epsilon.\mbox{\bf 1},a,C),(a.C+\epsilon.\mbox{\bf
1},\epsilon,\mbox{\bf 1})\\},\\{\mbox{\bf 1}\\},a.C+\epsilon.\mbox{\bf 1})$.

By summation, again, we get $\llbracket(a.C+\epsilon.\mbox{\bf
1})+b.D\rrbracket_{\\{C\\}}=(\\{(a.C+\epsilon.\mbox{\bf 1})+b.D,C,D,\mbox{\bf
1}\\},\\\ \\{a,b\\},\\{((a.C+\epsilon.\mbox{\bf
1})+b.D,a,C),((a.C+\epsilon.\mbox{\bf 1})+b.D,\epsilon,\mbox{\bf
1}),((a.C+\epsilon.\mbox{\bf 1})+b.D,b,D),\\\ (D,b,D),(D,\epsilon,\mbox{\bf
1})\\},\\{\mbox{\bf 1}\\},(a.C+\epsilon.\mbox{\bf 1})+b.D)$.

Finally, $\llbracket C\rrbracket_{\emptyset}=(\\{C,D,\mbox{\bf
1}\\},\\{a,b\\},\\{(C,a,C),(C,\epsilon,\mbox{\bf
1}),(C,b,D),(D,b,D),(D,\epsilon,\mbox{\bf 1})\\},$ $\\{\mbox{\bf 1}\\},C)$.
The resulting GFA is isomorphic to that on the left in Figure 3, where $q_{0}$
corresponds to $C$, $q_{1}$ to $D$ and $r_{0}$ to 1.  $\Box$

###### Theorem 1

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

###### Theorem 2

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

###### Corollary 1

SFM0 represents, up to isomorphism, the class of reduced GFAs.

###### Example 4

Let us consider the GFA on the left in Figure 3. According to the construction
in the proof of Theorem 2, its SFM0 representation is as follows:

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

Let us consider the DGFA in Figure 3. Its SFM0 representation is as follows:

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

Note that if the GFA is not reduced, then we cannot find an SFM0 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 GFA on
the left.

If we consider the first GFA in Figure 4, we get:

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

Finally, if we consider the second GFA in Figure 4, we get:

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

$q_{5}$$r_{0}$$a$$b$$q_{6}$$r_{1}$$q_{7}$$a$$b$$b$ Figure 4: Two GFAs for
Example 4

##  4 Congruence

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

###### Definition 6

Two SFM0 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(\alpha.\mbox{\bf 1})=\\{\alpha\\}$.

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

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

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

###### Proposition 2

1) For each $p,q\in\mathcal{P}_{SFM_{0}}$, if $p\sim q$, then $a.p\sim a.q$
for all $a\in A$.

2) For each $p,q\in\mathcal{P}_{SFM_{0}}^{grd}$, if $p\sim q$, then $p+r\sim
q+r\;$ for all $r\in\mathcal{P}_{SFM_{0}}^{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 SFM0 where terms can be constructed using
variables, such as $x,y,\ldots$ (which are in syntactic category $p$): this
defines an “open” SFM0 that has the following syntax:

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

where the semantic of $x$ is the GFA
$(\\{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 SFM0 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:

$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 SFM0 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 SFM0 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 SFM0 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 the constant $C$
for the variable $x$.  $\Box$

###### Theorem 3

Let $p$ and $q$ be two open guarded SFM0 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 0}$ generates a
GFA isomorphic to the one for $a.(\mbox{\bf 0}+\mbox{\bf 0})$; however, if we
consider the context $\\_+a.\mbox{\bf 0}$ we get two terms generating not
isomorphic GFAs: $a.\mbox{\bf 0}+a.\mbox{\bf 0}$ generates a two-state GFA,
while $a.(\mbox{\bf 0}+\mbox{\bf 0})+a.\mbox{\bf 0}$ generates a three-state
GFA. 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 SFM0, by means of standard proof
techniques (see, e.g., [15, 7, 1, 19, 9]).

##  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}_{SFM_{0}}^{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 [15, 7, 1, 19], 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+\epsilon.\mbox{\bf
1}$; then, it is easy to see that the GFA for $p+q$ (five states) is not
isomorphic to the GFA for $q+p$ (four states).

###### Proposition 4

(Laws of the prefixing operator) For each $p,q\in\mathcal{P}_{SFM_{0}}^{grd}$,
for each $a\in A$, the following hold:

$\begin{array}[]{lrcllllll}&a.\mbox{\bf 0}&\sim&\mbox{\bf
0}&&\;\mbox{(annihilation)}\\\
&a.(p+q)&\sim&a.p+a.q&&\;\mbox{(distributivity)}\\\ \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 is
discussed, then also the folding law, whose proof relies on some auxiliary
technical machinery (fixed point theorems on a complete lattice, see, e.g.,
[4, 19]).

###### Proposition 5

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

The unfolding law also holds for bisimilarity [15, 7, 8], but it does not hold
for isomorphism equivalence. For instance, consider $C\doteq
a.a.C+\epsilon.\mbox{\bf 1}$: it is easy to see that the GFA for $C$ has three
states, while the GFA for $a.a.C+\epsilon.\mbox{\bf 1}$ has four states.

In order to prove the folding law below, 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$.

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 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. However, by syntactic definition, the prefix $\epsilon$ can
be only used with target 1, so that $\epsilon\not\in L_{p}^{x}$. Therefore, by
the argument above we can conclude the following.

###### Proposition 6

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

It is possible to prove, with a standard bisimulation-based proof technique
[14, 8], that the more concrete bisimulation equivalence $\simeq$ satisfies
the folding law: For each $p\in\mathcal{P}_{SFM_{0}}^{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$.

##  6 Axiomatization

In this section we present a sound and complete, finite axiomatization of
language equivalence over SFM0, i.e., we show that it is possible to prove
syntactically, i.e., by means of an equational deductive proof, when two SFM0
processes recognize the same regular language. For a description of how
equational deduction is implemented in a process algebra with process
constants we refer the reader to [10].

For simplicity’s sake, the syntactic definition of open (i.e., with variables)
SFM0 is given with only one syntactic category, but each ground instantiation
of an axiom must respect the syntactic definition of SFM0 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 SFM0 processes (the constant
$C$ cannot be used as a summand).

###  6.1 The Axioms

The set of axioms is outlined in Table 2. The axioms A1-A4 are the usual
axioms for choice [12, 18, 13, 14]. The axiom schemata T1-T2 are those for
prefixing [12, 18, 13], that are finitely many as $A$ is finite. The
conditional axioms R1-R2 are about process constants and are similar to those
in [14, 8, 9]. 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-R2 are
finitely many as well.

We call $B$ the set of axioms $\\{$A1, A2, A3, A4, R1, R2$\\}$ that is a sound
and complete axiomatization for bisimilarity [14, 8, 9], while we call $W$ the
set of axioms $\\{$A1, A2, A3, A4, T1, T2, R1, R2$\\}$ that we will prove to
be a sound and complete axiomatization of language equivalence for SFM0
processes. By the notation $E\vdash p=q$ we mean that there exists an
equational deduction proof of the equality $p=q$, by using the axioms in $E$.

$\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}&\;\;a.\mbox{\bf
0}&=&\mbox{\bf 0}&\\\ {\bf
T2}&\;\;\mbox{Distributivity}&\;\;a.(x+y)&=&a.x+a.y&\\\ \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\;q=p\\{q/x\\}$}&\mbox{then}&\mbox{$C=q$}&\\\ \end{array}$

Table 2: Axioms for language equivalence

###### Theorem 4

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

###  6.2 Normal Forms and Unique Solutions

An SFM0 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 3. Examples of terms which are not in normal form are
$a.b.\mbox{\bf 1}$, $b.\mbox{\bf 0}$ and $C\doteq a.b.C+b.\epsilon.\mbox{\bf
1}$.

$\begin{array}[]{cccccc}\begin{array}[]{c}\\\ \hline\cr nf(\mbox{\bf
0},I)\end{array}&&\begin{array}[]{c}\\\ \hline\cr nf(\alpha.\mbox{\bf
1},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(a.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 3: Normal form predicate

Note that if $C$ is a normal form, then its body (ignoring all the possible
summands 0 that can be absorbed via axioms A3) is of the form
$\sum_{i=1}^{n}a_{i}.C_{i}+\sum_{j=1}^{m}\alpha_{j}.\mbox{\bf 1}$ (assuming
that $\sum_{i=1}^{n}a_{i}.C_{i}$ is 0 if $n=0$, as well as that
$\sum_{j=1}^{m}\alpha_{j}.\mbox{\bf 1}$ is 0 if $m=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 GFAs are in
normal form.

Now we show that, for each SFM0 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 7

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

###### Remark 3

(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)}a_{1i}.C_{f(1,i)}+\sum_{j=1}^{l(1)}\alpha_{1j}.\mbox{\bf
1}\\\
C_{2}&\doteq&\sum_{i=1}^{m(2)}a_{2i}.C_{f(2,i)}+\sum_{j=1}^{l(2)}\alpha_{2j}.\mbox{\bf
1}\\\ \ldots\\\
C_{n}&\doteq&\sum_{i=1}^{m(n)}a_{ni}.C_{f(n,i)}+\sum_{j=1}^{l(n)}\alpha_{nj}.\mbox{\bf
1}\\\ \end{array}$

where we assume $C_{i}\doteq\mbox{\bf 0}$ in case $m(i)=0=l(i)$. We sometimes
use the notation $body(C_{h})$ to denote the sumform
$\sum_{i=1}^{m(h)}a_{hi}.C_{f(h,i)}+\sum_{j=1}^{l(h)}\alpha_{hj}.\mbox{\bf
1}$.  $\Box$

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

###### Theorem 5

(Unique solution 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 SFM0 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}$) used in the following 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}$

Then, for $i=1,\ldots,n$, $W\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\vdash q_{i}=p_{i}\\{\widetilde{q}/\widetilde{X}\\}$, then $W\vdash
C_{i}=q_{i}$.

###  6.3 Semi-deterministic Normal Form

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

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

where function $f(i,j)$ returns a value $k$ such that $1\leq k\leq n$ and, for
$h=1,\ldots,n$, the multiset
$\\{\alpha_{h1},\alpha_{h2},\ldots,\alpha_{hl(h)}\\}$ is a actually a set.
Therefore, the body of each constant contains exactly one non-terminal summand
(i.e., ending with a constant) for each symbol $a_{i}\in A$ and at most one
terminal summand (i.e., ending with 1) for each symbol $\alpha_{i}\in
A\cup\\{\epsilon\\}$. Of course, the GFA associated to $C_{1}$, according to
the denotational semantics in Table 1, is semi-deterministic and has exactly
$A$ as its alphabet. Conversely, according to the construction in the proof of
Theorem 2, the process terms representing reduced DGFAs are in semi-
deterministic normal form.

Note that the concept of semi-determinism heavily depends on the chosen
alphabet. For instance, according to the denotational semantics in Table 1,
the GFA for $C\doteq\mbox{\bf 0}$ is semi-deterministic, because its alphabet
is empty. However, it is not semi-deterministic if we consider a nonempty
alphabet, say $A=\\{a\\}$, because there is not an arc for $a$. In such a
case, a DGFA 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\vdash C=E$ by means of axioms T1, R1, R2; in fact, by axiom T1, we have
$W\vdash\mbox{\bf 0}=a.\mbox{\bf 0}$; then, by axiom R2, from $E\doteq a.E$
and $W\vdash\mbox{\bf 0}=a.\mbox{\bf 0}$, we get $W\vdash E=\mbox{\bf 0}$;
then by axiom R1, we have $W\vdash C=\mbox{\bf 0}$, so that $W_{g}\vdash C=E$
follows by transitivity.

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

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

###### Example 6

Let us consider the following normal form

$\begin{array}[]{rcl}C_{1}&\doteq&a.C_{1}+a.C_{2}+a.C_{1}+\epsilon.\mbox{\bf
1}\\\ C_{2}&\doteq&a.C_{2}+\epsilon.\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 semi-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}+\epsilon.\mbox{\bf
1}\\\ B_{\\{2\\}}&\doteq&a.C_{2}+\epsilon.\mbox{\bf 1}\\\
B_{\\{1,2\\}}&\doteq&a.C_{1}+a.C_{2}+a.C_{1}+\epsilon.\mbox{\bf
1}+a.C_{2}+\epsilon.\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 semi-deterministic
definition. First, we can prove that, since $B_{\emptyset}=\mbox{\bf 0}$ by
axiom R1, also $W\vdash B_{\emptyset}=a.B_{\emptyset}+b.B_{\emptyset}$ by
axioms T1,A3.

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

In the same way, we can prove that $W\vdash
B_{\\{2\\}}=a.B_{\\{2\\}}+b.B_{\emptyset}+\epsilon.\mbox{\bf 1}$ and,
moreover, that $W\vdash
B_{\\{1,2\\}}=a.B_{\\{1,2\\}}+b.B_{\emptyset}+\epsilon.\mbox{\bf 1}$, where
the duplicated summand $\epsilon.\mbox{\bf 1}$ is taken only once (by axiom
A4).

Finally, we define a new semi-deterministic system of equations

$\begin{array}[]{rcl}D_{\\{1\\}}&\doteq&a.D_{\\{1,2\\}}+b.D_{\emptyset}+\epsilon.\mbox{\bf
1}\\\ D_{\\{2\\}}&\doteq&a.D_{\\{2\\}}+b.D_{\emptyset}+\epsilon.\mbox{\bf
1}\\\ D_{\\{1,2\\}}&\doteq&a.D_{\\{1,2\\}}+b.D_{\emptyset}+\epsilon.\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\vdash
B_{I}=D_{I}$ for $I=\\{1\\},\\{2\\},\\{1,2\\},\emptyset$. So, $W\vdash
C_{1}=D_{\\{1\\}}$ by transitivity.  $\Box$

###### Proposition 8

(Reduction to semi-deterministic normal form) Given the normal form

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

such that its alphabet is $A_{C}$ and $1\leq f(i,j)\leq n$, it is possible to
construct a semi-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)}+\sum_{j=1}^{k(1)}\alpha_{j}^{1}.\mbox{\bf
1}\\\
D_{2}&\doteq&\sum_{i=1}^{k}a_{i}.D_{g(2,i)}+\sum_{j=1}^{k(2)}\alpha_{j}^{2}.\mbox{\bf
1}\\\ \ldots\\\
D_{m}&\doteq&\sum_{i=1}^{k}a_{i}.D_{g(m,i)}+\sum_{j=1}^{k(m)}\alpha_{j}^{m}.\mbox{\bf
1}\\\ \end{array}$

where $m\geq n$ and $1\leq g(i,j)\leq m$, such that $W\vdash C_{1}=D_{1}$.

###  6.4 Completeness

Proposition 8 is at the basis of the lemma below, which, in turn, is crucial
for the proof of completeness that follows. The proof technique of the lemma
below is inspired to the proof of Theorem 5.10 in [14], in turn inspired to
the proof of Theorem 2 in [18].

###### Lemma 1

(Completeness for normal forms) For every
$p,p^{\prime}\in\mathcal{P}_{SFM_{0}}$ normal forms, if $p\sim p^{\prime}$,
then $W\vdash p=p^{\prime}$.

###### Theorem 6

(Completeness for all the SFM0 processes)

For every $p,q\in\mathcal{P}_{SFM_{0}}$, if $p\sim q$, then $W\vdash p=q$.

##  7 Conclusion

In this paper, we have shown how to use the process algebra SFM0, that truly
represents GFAs up to isomorphism, in order to find a sound and complete
axiomatization of language equivalence, and so also a sound and complete
axiomatization of regular languages, composed of 6 axioms and 2 conditional
axioms, outlined in Table 2.

In [10] we have proposed the process algebra SFM1, which truly represent NFAs
(with $\epsilon$ transitions), up to isomorphism. The axiomatization of
language equivalence proposed there contains one additional axiom:

T3 ($\epsilon$-absorption) $\epsilon.x=x\quad\mbox{ if $x\neq C$}$

and one additional conditional axiom:

R3 (Excision) if $C\doteq(\epsilon.x+p)\\{C/x\\}\wedge D\doteq p\\{D/x\\}$
then $C=D$.

However, if we consider the subcalculus SFM1-ϵ of SFM1, where $\epsilon$
cannot be used as a prefix, we get that this can represent all NFAs without
$\epsilon$ transitions, a model that can express all the regular languages,
too. The axiomatization of language equivalence over SFM1-ϵ is exactly the
same we have proposed for SFM0 in Table 2. Moreover, if we consider the
subcalculus SFM${}_{0}^{-\epsilon}$ of SFM0, where $\epsilon$ cannot be used
as a prefix, we get that it can represent all GFAs without $\epsilon$
transitions, a model that can express all the regular languages that do not
contain the empty word. The axiomatization of language equivalence over
SFM${}_{0}^{-\epsilon}$ is exactly the same we have proposed for SFM0. The
relations among these process algebras and the classes of finite automata they
represent (up to isomorphism) are outlined in Figure 5.

NFA $\;\;\leftrightarrow\;\;$ SFM1GFA $\;\;\leftrightarrow\;\;$
SFM0NFA${}^{-\epsilon}\;\;\leftrightarrow\;\;$ SFM1-ϵGFA-ϵ
$\;\leftrightarrow\;$ SFM${}_{0}^{-\epsilon}$

Legenda
$\begin{array}[]{lllllllll}\mbox{NFA}&\mbox{nondeterministic finite
automata}&\quad\mbox{SFM1}&\mbox{basic calculus with constants $\mbox{\bf 0}$
and $\mbox{\bf 1}$}\\\ \mbox{NFA${}^{-\epsilon}$}&\mbox{NFA without
$\epsilon$-transitions}&\quad\mbox{SFM1${}^{-\epsilon}$}&\mbox{SFM1 without
$\epsilon$ prefix}\\\ \mbox{GFA}&\mbox{NFA generated by regular
grammars}&\quad\mbox{SFM${}_{0}$}&\mbox{restriction of SFM1 with constants
$\mbox{\bf 0}$ and $\alpha.\mbox{\bf 1}$}\\\
\mbox{GFA${}^{-\epsilon}$}&\mbox{GFA without
$\epsilon$-transitions}&\quad\mbox{SFM${}_{0}^{-\epsilon}$}&\mbox{SFM${}_{0}$
without $\epsilon$ prefix}\\\ \end{array}$

Figure 5: Process algebras for finite automata

Other process algebras have been proposed in the literature for modeling NFAs
such as those in [20, 21, 1]. A precise comparison between the theory of SFM1
and these is given in [10].

Our axiomatization of regular languages is alternative to those based on the
Kleene algebra of regular expressions [18, 3, 13]. As a matter of fact, our
axiomatization, composed of 6 axioms and 2 conditional axioms, seems more
concise than these. In fact, the currently most concise axiomatization of this
sort [5] is composed of 13 axioms, only one of which is conditional. However,
it should be remarked that our axiomatization makes use of axiom schemata (in
particular, for recursion), while [5] does not.

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 GFAs. In fact, SFM0 has allowed us to study also
bisimulation equivalence on GFAs 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
SFM0 to other behavioral equivalences in the linear-time/branching-time
spectrum [6, 7]. For instance, we claim that simulation equivalence [16, 7]
can be axiomatized by replacing axiom T2 in the set $W$ with the axiom

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

Our axiomatization is based on results and techniques developed in the area of
process algebras [14, 15, 2, 1, 19, 7] 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] 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.
  * [2] J.A. Bergstra, A. Ponse, S.A. Smolka (eds.),  Handbook of Process Algebra,  Elsevier, 2001.
  * [3] J.H. Conway,  Regular Algebra and Finite Machines, Chapman and Hall, London, 1971. ISBN 0-412-10620-5.
  * [4] B.A. Davey, H.A. Priestley,  Introduction to Lattices and Order (second edition),  Cambridge University Press, 2002.
  * [5] 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.
  * [6] R.J. van Glabbeek,  The linear time - branching time spectrum I,  Chapter 1 of [2], 3-99, 2001.
  * [7] R. Gorrieri, C. Versari, Introduction to Concurrency Theory: Transition Systems and CCS, EATCS Texts in Theoretical Computer Science, Springer-Verlag, 2015.
  * [8] 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.
  * [9] R. Gorrieri,  Team equivalences for finite-state machines with silent moves,  Information and Computation Vol. 275, 2020, DOI:10.1016/j.ic.2020.104603
  * [10] R. Gorrieri,  The algebra of nondeterministic finite automata,  CoRR abs/2301.03435, 2023. https://arxiv.org/abs/2301.03435.
  * [11] J.E. Hopcroft, R. Motwani, J.D. Ullman,  Introduction to Automata Theory, Languages and Computation, 2nd ed.,  Addison-Wesley, 2001.
  * [12] 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.
  * [13] 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
  * [14] R. Milner,  A complete inference systems for a class of regular behaviors,  J. Comput. System Sci. 28: 439-466, 1984.
  * [15] R. Milner. Communication and Concurrency, Prentice-Hall, 1989.
  * [16] 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.
  * [17] M.O. Rabin, D. Scott,  Finite automata and their decision problems,  IBM Journal of Research and Development 3(2):114-125, 1959.
  * [18] 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
  * [19] D. Sangiorgi,  An Introduction to Bisimulation and Coinduction,  Cambridge University Press, 2012.
  * [20] A. Silva,  Kleene Coalgebra,  Ph.D. thesis, Radboud Universiteit Nijmegen, 2010. ISBN: 978-90-6464-433-7
  * [21] A. Silva, M.M. Bonsangue, and J.J.M.M. Rutten,  Non-deterministic Kleene coalgebras,  Logical Methods in Computer Science, 6(3), 2010.
  * [22] T.A. Sudkamp,  Languages and Machines (second edition),  Addison Wesley, 1997.