# Axiomatizing recursion-free, regular monitors111This article is based on
material presented at the 31st Nordic Workshop on Programming Theory, NWPT
2019, in Tallinn. The authors were supported by the projects ‘Open Problems in
the Equational Logic of Processes’ (OPEL) (grant No 196050-051) and ‘Mode(l)s
of Verification and Monitorability’ (MoVeMent) (grant No 217987) of the
Icelandic Research Fund, and ‘Runtime and Equational Verification of
Concurrent Programs’ (ReVoCoP) (grant No 222021), of the Reykjavik University
Research Fund. Luca Aceto’s work was also partially supported by the Italian
MIUR PRIN 2017 project FTXR7S IT MATTERS ‘Methods and Tools for Trustworthy
Smart Systems’.

Luca Aceto<EMAIL_ADDRESS><EMAIL_ADDRESS>Antonis Achilleos<EMAIL_ADDRESS>Elli Anastasiadi<EMAIL_ADDRESS>Anna Ingolfsdottir<EMAIL_ADDRESS>ICE-TCS,
Department of Computer Science, Reykjavik University, Iceland  Gran Sasso
Science Institute, L’Aquila, Italy

###### Abstract

Monitors are a key tool in the field of runtime verification, where they are
used to verify system properties by analyzing execution traces generated by
processes. Work on runtime monitoring carried out in a series of papers by
Aceto et al. has specified monitors using a variation on the regular fragment
of Milner’s CCS and studied two trace-based notions of equivalence over
monitors, namely verdict and $\omega$-verdict equivalence. This article is
devoted to the study of the equational logic of monitors modulo those two
notions of equivalence. It presents complete equational axiomatizations of
verdict and $\omega$-verdict equivalence for closed and open terms over
recursion-free monitors. It is also shown that verdict equivalence has no
finite equational axiomatization over open monitors when the set of actions is
finite and contains at least two actions.

###### keywords:

Monitors , Formal Verification , CCS , Equational Logic , Processes , Process
Algebra , Axiomatization , Trace Equivalence , Verdicts.

††journal: Journal of Logical and Algebraic Methods in Programming

##  1 Introduction

The search for equational axiomatizations of a notion of equivalence over some
process description language is one of the classic topics in concurrency
theory, as witnessed by the literature on this subject over the last forty
years. (See, for instance, [7, 8, 9, 16, 18, 27, 33, 34, 35, 43, 44] for early
references as well as survey and textbook accounts, and the papers [4, 5, 28,
37] for examples of the rich body of recent contributions to this field.) This
research avenue has its intellectual roots in the time-honored study of the
existence of finite, (conditional) equational proof systems for equality of
regular expressions, as presented in [20, 38, 39, 48, 49].

There are manifold reasons for studying equational axiomatizations of
equivalences over processes. For example, the existence of a finite, or at
least finitely specified, equational axiomatization for some notion of process
equivalence is often considered as one of the yardsticks to assess its
mathematical tractability. Additionally, equational axiomatizations provide a
purely syntactic description of the chosen notion of equivalence over
processes and characterize the essence of a process semantics by means of a
few revealing axioms, which can be used to compare a variety of semantics in a
model-independent way (as done, for instance, in [27]). Moreover, such
axiomatizations pave the way to the use of theorem-proving techniques to
establish that two process descriptions express the same behavior modulo the
chosen notion of behavioral equivalence [21, 29, 41], and also play an
important role in the partial evaluation of programs [32].

In this paper, we study the equational logic of the _monitors_ studied by
Aceto et al. in, for instance, [1, 2, 26]. Monitors are a key tool in the
field of runtime verification (see [13, 24, 30, 31, 40, 46, 51, 52] and the
references therein for an overview of this active research area), where they
are used to check for system properties by analyzing execution traces
generated by processes and are often expressed using some automata-based
formalism. The notion of monitorable property has been defined in a seminal
paper by Pnueli and Zaks [46]. Intuitively, a property of finite and infinite
system executions is $s$-monitorable, for some finite trace of observable
events $s$, if there is an extension of $s$ after which a monitor will be able
to determine conclusively whether the observed system execution satisfies or
violates the property. This means that verdicts issued by monitors are
_irrevocable_. In that work by Pnueli and Zaks, a property is described by the
set of finite and infinite executions that satisfy it. However, in the theory
and practice of runtime verification, one often specifies properties finitely
using formalisms such as automata or (variations on) temporal logics and
studies what specifications in the chosen formalism are ‘monitorable’ and with
what correctness guarantees—see, for instance, [12, 15, 47]. Since monitors
are part of the trusted computing base, the automated, correct-by-design
_monitor synthesis_ from the formal specification of properties has been
thoroughly studied in the literature and is often accompanied by the
experimental evaluation of the overhead induced by monitoring—see, for
example, the study of various approaches to the automated monitor synthesis
for systemC specifications given in [52] and the framework for benchmarking of
runtime verification tools presented in [3].

In [1, 2, 26], Aceto et al. specified monitors using a variation on the
regular fragment of Milner’s CCS [42] and studied two trace-based notions of
equivalence over monitors, namely verdict and $\omega$-verdict equivalence.
Intuitively, two monitor descriptions are verdict equivalent when they accept
and reject the same finite execution traces of the systems they observe. The
notion of $\omega$-verdict equivalence is the ‘asymptotic version’ of verdict
equivalence, in that it is solely concerned with the infinite traces that are
accepted and rejected by monitors. In their work, Aceto et. al. focus on
determining the ‘monitorable’ fragment of Hennessy-Milner Logic with recursion
[1, 26] and provide monitor-synthesis algorithms for properties that can be
expressed in that fragment. The key (and non-negotiable) property that the
monitor synthesized from a formula $\varphi$ in the monitorable fragment of
that logic should satisfy is _soundness_ , which means that a verdict issued
by the monitor as it examines a system execution determines whether that
execution satisfies $\varphi$ or not correctly. Naturally, sound monitors
cannot produce contradictory verdicts for a given trace.

##### Our contribution

When monitors are described by expressions in some monitor-specification
language, such as the one employed by Aceto et al. in _op. cit._ , it is
natural to ask oneself whether one can (finitely) axiomatize notions of
monitor equivalence over (fragments of) that language. This study is devoted
to addressing that question in the simplest non-trivial setting. In
particular, in order to stay within the realm of classic equational logic over
total algebras, we consider a language that allows one to specify unsound
monitors. However, all the results we present in the paper specialize to sub-
languages consisting of (sound) monitors that can only issue either positive
or negative verdicts.

The main results we present in this paper are complete equational
characterizations of verdict equivalence over both closed (that is, variable-
free) and open, recursion-free regular monitors. More specifically, we first
provide an equational axiomatization of verdict equivalence over closed terms
from the language of monitors we study that is finite if so is the set of
actions monitors can observe (Theorem 2). The landscape of axiomatizability
results for verdict equivalence over open terms turns out to be more varied.
This variety is witnessed by the fact that there are three different
axiomatizations, depending on whether the set of actions is infinite (Theorem
4), finite and containing at least two actions (Theorem 5) or a singleton
(Theorem 6). Only the axiomatization given in Theorem 6 is finite and we show
that this is unavoidable. Indeed, verdict equivalence has no finite equational
basis when the set of actions is finite and of cardinality at least two
(Theorem 10).

It turns out that the above-mentioned axiomatizations are also complete for
$\omega$-verdict equivalence if the set of actions that monitors may observe
is infinite, as in that case the two notions of equivalence coincide. On the
other hand, if the set of actions is finite, $\omega$-verdict equivalence is
strictly coarser than verdict equivalence. We also provide a finite, complete
axiomatization of $\omega$-verdict equivalence for closed monitors in the
setting of a finite set of actions (Theorem 3). Our Theorem 8 gives a complete
axiomatization of $\omega$-verdict equivalence over open monitors when the set
of actions contains at least two actions. If the set of actions is a
singleton, $\omega$-verdict equivalence has a finite equational basis (Theorem
7).

The equational axiomatizations we present in this article capture the ‘laws of
monitor programming’ [35] for an admittedly rather inexpressive language.
Indeed, recursion-free regular monitors describe essentially tree-like finite-
state automata with distinguished accept and reject states at their ‘leaves’
with self-loops labeled by every action. (See the operational semantics of
monitors in Table 1. Note, however, that those automata may have infinitely
many transitions, if the set of actions monitors can observe is infinite. As
shown already by Milner in his classic books on CCS [42, 44], this feature is
useful when modeling system events that carry data values. See, for instance,
the paper [11] for one of the earliest attempts to incorporate data into
runtime verification.) However, as witnessed by our results and their proofs,
the study of the equational theory of monitors modulo the notions of
equivalence we consider is non-trivial even for the minimal language studied
in this paper. In our, admittedly biased, opinion, it is therefore worthwhile
to map the territory of axiomatizability results for recursion-free regular
monitors, since results for more expressive languages will have to build upon
those we obtain in this article. We remark, in passing, that the non-finite
axiomatizability result in Theorem 10 is obtained over a substantially more
restrictive syntax than classic negative results for the algebra of regular
expressions, which rely on the hardness of expressing the interplay between
Kleene star and concatenation equationally [6, 20, 48].

The contribution of this paper is entirely theoretical and we make no claims
pertaining to the applicability of our current results in the practice of
runtime verification. However, apart from their intrinsic theoretical
interest, (extensions of) the equational axiomatizations we present might be
used in the automatic, syntax-driven synthesis of monitors from specifications
of ‘monitorable properties’, as presented in [1, 2, 25], to rewrite monitor
expressions in an ‘equivalent, but simpler’ syntactic form, for instance by
eliminating ‘redundant’ sub-expressions. As witnessed by the study of
optimized temporal monitors for SystemC presented in [52], the investigation
of monitor optimizations based on equational rewriting or other techniques
requires a substantial experimental research effort and is outside the scope
of this article. We discuss other avenues for future research in Section 6.

##  2 Preliminaries

We begin by introducing recursion-free regular monitors (or simply monitors in
this study) and the two notions of verdict equivalence that we study in this
paper. We refer the interested reader to [1, 26] for background motivation and
more information.

##### Syntax of monitors

Let $\mathit{Act}$ be a set of visible actions, ranged over by $a,b$.
Following Milner [44], we use $\tau\not\in\mathit{Act}$ to denote an
unobservable action. The symbol $\alpha$ ranges over
$\mathit{Act}\cup\\{\tau\\}$. Let $\mathit{Var}$ be a countably infinite set
of variables, ranged over by $x,y,z$. We assume that
$\mathit{Act}\cup\\{\tau\\}$ and $\mathit{Var}$ are disjoint.

We write $\mathit{Act}^{\omega}$ for the set of infinite sequences over
$\mathit{Act}$. As usual, $\mathit{Act}^{*}$ stands for the set of finite
sequences over $\mathit{Act}$. Let $A$ be a set of finite sequences and $B$ be
a set of sequences. We write $A\cdot B$ for the concatenation of $A$ and $B$.

The collection $Mon_{F}$ of (regular, recursion-free) monitors is the set of
terms generated by the following grammar:

$\begin{split}&m,n::=~{}v~{}~{}\mid~{}~{}a.m~{}~{}\mid~{}~{}m+n~{}~{}\mid~{}~{}x\\\
&v::=~{}\mathit{end}~{}\mid~{}\mathit{yes}~{}\mid~{}\mathit{no}\end{split}$

where $a\in\mathit{Act}$ and $x\in\mathit{Var}$. The terms $\mathit{end}$,
$\mathit{yes}$ and $\mathit{no}$ are called _verdicts_. Intuitively,
$\mathit{yes}$ stands for the acceptance verdict, $\mathit{no}$ denotes a
rejection verdict and $\mathit{end}$ is the inconclusive verdict, namely the
state a monitor reaches when, based on the sequence of observations it has
processed so far, it realizes that it will not be able to issue an acceptance
or rejection verdict in the future. As will be formalized by the operational
semantics of monitors to follow, verdicts are irrevocable. This means that
once a monitor reaches a verdict, it will stick to it regardless of what
further observations it makes. See, for instance, [1, 13, 26] for a detailed
technical discussion.

Intuitively, a monitor of the form $a.m$ can observe action $a$ and behave
like $m$ thereafter. On the other hand, a monitor of the form $m+n$ can behave
either like $m$ or like $n$.

######  Remark 1.

The work on which we build in this paper considers a setting with three
verdicts, two of which are ‘conclusive.’ There are a number of other
approaches in the field of runtime verification that consider many-valued
verdicts. We refer the interested reader to, for instance, [10, 12, 14, 17,
23] for further information.

Closed monitors are those that do not contain any occurrences of variables. A
(closed) _substitution_ is a mapping $\sigma$ from variables to (closed)
monitors. We write $\sigma(m)$ for the monitor that results when applying the
substitution $\sigma$ to $m$. Note that $\sigma(m)$ is closed, if $\sigma$ is
a closed substitution.

######  Definition 1 (Notation).

We use $m~{}[+v]$ for a verdict $v$ to indicate that $v$ is an optional
summand of $m$, that is, that the term can be either $m$ or $m+v$. In addition
a monitor will be called $v$-free for a verdict $v$, when it does not contain
any occurrences of $v$.

For a finite index set $I=\\{i_{1},\ldots,i_{k}\\}$ and indexed set of
monitors $\\{m_{i}\\}_{i\in I}$, we write $\sum_{i\in I}m_{i}$ to stand for
$\mathit{end}$ if $I=\emptyset$ and for $m_{i_{1}}+\ldots+m_{i_{k}}$
otherwise. This notation is justified by the fact that $+$ is associative and
commutative, and has $\mathit{end}$ as a neutral element, in all of the
semantics we use in this paper.

We now associate a notion of syntactic depth with each monitor. Intuitively,
the decision a monitor $m$ takes when reading a string $s\in\mathit{Act}^{*}$
only depends on the prefixes of $s$ whose length is at most the syntactic
depth of $m$.

######  Definition 2 (Syntactic Depth).

For any closed monitor $m\in$ $Mon_{F}$, we define $0pt(m)$ as follows:

  * •

$0pt(a.m)=1+0pt(m)$,

  * •

$0pt(m_{1}+m_{2})=\max(0pt(m_{1}),0pt(m_{2}))$ and

  * •

$0pt(v)=0$ for a verdict $v$.

##### Semantics of monitors

For each $\alpha\in\mathit{Act}\cup\\{\tau\\}$, we define the transition
relation $\xrightarrow[\text{}]{~{}\alpha~{}}\subseteq$ $Mon_{F}$ $\times$
$Mon_{F}$ as the least one that satisfies the axioms and rules in Table 1.

$\displaystyle\scalebox{1.0}{$$}\,\frac{\displaystyle}{\displaystyle
a.m\xrightarrow[\text{}]{a}m}\qquad\scalebox{1.0}{$$}\,\frac{\displaystyle
m\xrightarrow[\text{}]{~{}\alpha~{}}m^{\prime}}{\displaystyle
m+n\xrightarrow[\text{}]{~{}\alpha~{}}m^{\prime}}\qquad\scalebox{1.0}{$$}\,\frac{\displaystyle
n\xrightarrow[\text{}]{~{}\alpha~{}}n^{\prime}}{\displaystyle
m+n\xrightarrow[\text{}]{~{}\alpha~{}}n^{\prime}}\qquad\scalebox{1.0}{$$}\,\frac{\displaystyle}{\displaystyle
v\xrightarrow[\text{}]{~{}\alpha~{}}v}\qquad$ Table 1:  Operational semantics
of processes in $Mon_{F}$.

For example, $\mathit{yes}+x\xrightarrow[]{\tau}\mathit{yes}$ and
$a.\mathit{yes}+\mathit{end}\xrightarrow[]{b}\mathit{end}$, for each
$a,b\in\mathit{Act}$. A useful fact based on the above operational semantics
is that if $m\xrightarrow[]{\tau}m^{\prime}$, then $m^{\prime}=v$ for some
verdict $v$.

Note that variables have no transitions. They represent under-specification in
monitor behavior. For instance, monitor $a.\mathit{yes}+x$ is one that we know
can reach the verdict $\mathit{yes}$ after having observed an $a$ action.
Further information on the behavior of that monitor can only be gleaned once
the variable $x$ has been instantiated via a (closed) substitution.

For $m,m^{\prime}$ in $Mon_{F}$ and $s=a_{1}\ldots a_{k}$ in
$\mathit{Act}^{*},~{}k\geq 0,$ $m\xrightarrow[]{s}m^{\prime}$ holds iff there
are $m_{0},,\ldots,m_{k}$ such that

$m=m_{0}\xrightarrow[]{a_{1}}m_{1}\cdots
m_{k-1}\xrightarrow[]{a_{k}}m_{k}=m^{\prime}.$

Additionally, for $s\in\mathit{Act}^{*}$, we use $m\xRightarrow{s}m^{\prime}$
to mean that:

  1. 1.

$m~{}(\xrightarrow[]{\tau})^{*}~{}m^{\prime}$ if $s=\varepsilon$, where
$\varepsilon$ stands for the empty string,

  2. 2.

$m\xRightarrow{\varepsilon}m_{1}\xrightarrow[]{a}m_{2}\xRightarrow{\varepsilon}m^{\prime}$
for some $m_{1},m_{2}$ if $s=a\in\mathit{Act}$ and

  3. 3.

$m\xRightarrow{a}m_{1}\xRightarrow{s^{\prime}}m^{\prime}$ for some $m_{1}$ if
$s=a.s^{\prime}$ , for some $s^{\prime}\neq\varepsilon$.

If $m\xRightarrow{s}m^{\prime}$ for some $m^{\prime}$, we call $s$ a _trace_
of $m$.

######  Lemma 1.

For all $s\in\mathit{Act}^{*},~{}m,n\in$ $Mon_{F}$, and verdict $v$,
$m+n\xRightarrow{s}v$ iff $m\xRightarrow{s}v$ or $n\xRightarrow{s}v$.

###### Proof.

We prove both implications separately, by induction on the length of $s$. The
details are straightforward and are therefore omitted. Here we limit ourselves
to remarking that, in the proof of the implication from right to left, if
$s=\varepsilon$ and $m=v$, say, then $v+n\xrightarrow[]{\tau}v$ by the rules
in Table 1. ∎

######  Remark 2.

Note that the implication from right to left in Lemma 1 would not hold in the
absence of rule $v\xrightarrow[]{\tau}v$ in Table 1.

##### Verdict and $\omega$-verdict equivalence

Let $m$ be a (closed) monitor. We define:

$\begin{split}&L_{a}(m)=\\{s\in\mathit{Act}^{*}\mid
m\xRightarrow{s}\mathit{yes}\\}~{}\text{and}\\\
&L_{r}(m)=\\{s\in\mathit{Act}^{*}\mid
m\xRightarrow{s}\mathit{no}\\}.\end{split}$

Intuitively, $L_{a}(m)$ denotes the set of traces that are accepted by $m$,
whereas $L_{r}(m)$ stands for the set of traces that $m$ rejects. The sets
$L_{a}(m)$ and $L_{r}(m)$ will also be referred to as the acceptance and
rejection set of $m$ respectively. Note that we allow for monitors that may
both accept and reject the same trace. This is necessary to maintain our
monitors closed under $+$ and to work with classic total algebras rather than
partial ones. Of course, in practice, one is interested in monitors that are
consistent in their verdicts. One way to ensure consistency in monitor
verdicts, which was considered in [26], is to restrict oneself to monitors
that use only one of the conclusive verdicts $\mathit{yes}$ and $\mathit{no}$.
All the results that we present in the remainder of this paper apply to such
monitors.

######  Remark 3.

The reader might wonder about the connection between the languages that are
accepted/rejected by recursion-free regular monitors and star-free languages
[50]. A simple argument by induction on the structure of monitors shows that
every recursion-free regular monitor denotes a pair of star-free languages,
one for its acceptance set and one for its rejection set. Moreover, this means
that recursion-free regular monitors correspond to properties that can be
expressed in LTL [36]. However, there are star-free languages (and therefore
LTL properties) that cannot be described by recursion-free regular monitors.
For example, the language $(ab)^{*}$ is star-free (see, for instance, [22,
page 267]) but does not correspond to any recursion-free regular monitor.

The monitors we consider in this paper output a positive or negative verdict
after a finite number of computational steps, if they do so at all. This means
that the linear-time temporal properties to which their acceptance and
rejection set correspond are both ‘Always Finitely Refutable’ and ‘Always
Finitely Satisfiable’ in the sense of [45], as proven in [1].

######  Definition 3.

Let $m$ and $n$ be closed monitors.

  * •

We say that $m$ and $n$ are verdict equivalent, written $m\simeq n$, if
$L_{a}(m)=L_{a}(n)~{}$ and $~{}L_{r}(m)=L_{r}(n)$.

  * •

We say that $m$ and $n$ are $\omega$-verdict equivalent, written
$m\simeq_{\omega}n$, if
$L_{a}(m)\cdot\mathit{Act}^{\omega}=L_{a}(n)\cdot\mathit{Act}^{\omega}~{}$ and
$~{}L_{r}(m)\cdot\mathit{Act}^{\omega}=L_{r}(n)\cdot\mathit{Act}^{\omega}$.

For open monitors $m$ and $n$, we say that $m\simeq n$ if
$\sigma(m)\simeq\sigma(n)$, for all closed substitutions $\sigma$. The
relation $\simeq_{\omega}$ is extended to open monitors in similar fashion.

######  Example 1.

It is easy to see that $m+\mathit{end}\simeq m$ holds for each
$m\in$$Mon_{F}$. Moreover, since $L_{a}(\mathit{end})=\emptyset$ and
$L_{r}(\mathit{end})=\emptyset$, $a.\mathit{end}\simeq\mathit{end}$ holds for
each $a\in\mathit{Act}$.

One can intuitively see that the notion of $\omega$-verdict equivalence refers
to a form of asymptotic behavior. Indeed, monitors $m$ and $n$ are
$\omega$-verdict equivalent if, and only if, they accept and reject the same
infinite traces in the sense of [1]. Next we provide a lemma that clarifies
the relations between the two notions of equivalence defined above.

######  Lemma 2.

The following statements hold:

  * •

$\simeq$ and $\simeq_{\omega}$ are both congruences.

  * •

$\simeq\subseteq\simeq_{\omega}$ and the inclusion is strict when
$\mathit{Act}$ is finite.

  * •

If $\mathit{Act}$ is infinite then $\simeq=\simeq_{\omega}$.

###### Proof.

For the first claim, it suffices to prove that $\simeq$ and $\simeq_{\omega}$
are equivalence relations and that they are preserved by $a.\\_$ and $+$. The
proof is standard and is thus omitted.

For the second claim, the inclusion $\simeq\subseteq\simeq_{\omega}$ is easy
to check using the definitions of the two relations. The fact that the
inclusion is strict when the set of actions is finite follows from the
validity of the equivalence
$\mathit{yes}\simeq_{\omega}\displaystyle\sum_{a\in\mathit{Act}}a.\mathit{yes}$.

However, that equivalence is not valid modulo verdict equivalence since the
first monitor accepts the empty string $\varepsilon$, but
$\displaystyle\sum_{a\in\mathit{Act}}a.\mathit{yes}$ cannot.

Finally, suppose that $\mathit{Act}$ is infinite. Assume that $m$ and $n$ are
$\omega$-verdict equivalent and that $s$ is a finite trace accepted by $m$. We
will argue that $n$ also accepts $s$. To this end, note that, since
$\mathit{Act}$ is infinite, there is some action $a$ that does not occur in
$m$ and $n$. Since $m$ accepts $s$, the infinite trace $sa^{\omega}$ is in
$L_{a}(m)\cdot\mathit{Act}^{\omega}$. By the assumption that $m$ and $n$ are
$\omega$-verdict equivalent, we have that $sa^{\omega}$ is in
$L_{a}(n)\cdot\mathit{Act}^{\omega}$. As $a$ does not occur in $n$, it is not
hard to see that $n$ accepts $s$. Therefore, by symmetry, $m$ and $n$ accept
the same traces. The same argument shows that $L_{r}(m)=L_{r}(n)$, and
therefore $m\simeq n$. ∎

##### Equational logic

An axiom system $\mathcal{E}$ over $Mon_{F}$ is a collection of equations
$m=n$ expressed in the syntax of $Mon_{F}$. An equation $m=n$ is derivable
from an axiom system $\mathcal{E}$ (notation $\mathcal{E}\vdash m=n$) if it
can be proven from the axioms in $\mathcal{E}$ using the rules of equational
logic (reflexivity, symmetry, transitivity, substitution and closure under the
$Mon_{F}$ contexts). See Table 2. In the rest of this work we shall always
implicitly assume, without loss of generality, that equational axiom systems
are closed with respect to symmetry, i.e., that if $m=n$ is an axiom, so is
$n=m$.

Reflexivity |
---|---
| $t=t$
Symmetry |
| $\frac{\displaystyle t=t^{\prime}}{\displaystyle t^{\prime}=t}$
Transitivity |
| $\frac{\displaystyle t_{1}=t_{2},~{}t_{2}=t_{3}}{\displaystyle t_{1}=t_{3}}$
Congruence (For any $n$-ary $f$) |
| $\frac{\displaystyle t_{i}=t_{i}^{\prime},~{}i=1,2,\ldots,n}{\displaystyle
f(t_{1},\ldots t_{n})=f(t_{1}^{\prime},\ldots,t_{n}^{\prime})}$
Substitutivity (For each substitution $\sigma$) |
| $\frac{\displaystyle
t=t^{\prime}}{\displaystyle\sigma(t)=\sigma(t^{\prime})}$
Table 2: Rules of equational logic

We say that $\mathcal{E}$ is _sound_ with respect to $\simeq$ when $m\simeq n$
holds whenever $\mathcal{E}\vdash m=n$. We say that $\mathcal{E}$ is
_complete_ with respect to $\simeq$ when $\mathcal{E}$ can prove all the valid
equations $m\simeq n$. Similar definitions apply for $\omega$-verdict
equivalence. The notion of completeness, when limited to closed terms, is
referred to as ground completeness.

##  3 A ground-complete axiomatization of verdict and $\omega$-verdict
equivalence

Our goal in this paper is to study the equational theory of $\simeq$ and
$\simeq_{\omega}$ over $Mon_{F}$. Our first main result is to give a ground-
complete axiomatization of verdict equivalence over $Mon_{F}$. To this end,
consider the axiom system $\mathcal{E}_{v}$, whose axioms are listed in Table
3.

$\begin{split}&\textbf{(A1)}~{}x+y=y+x\\\ &\textbf{(A2)}~{}x+(y+z)=(x+y)+z\\\
&\textbf{(A3)}~{}x+x=x\\\ &\textbf{(A4)}~{}x+\mathit{end}=x\end{split}$

$\begin{split}&\mathbf{(E_{a})}~{}a.\mathit{end}=\mathit{end}~{}(a\in\mathit{Act})\\\
&\mathbf{(Y_{a})}~{}\mathit{yes}=\mathit{yes}+a.\mathit{yes}~{}(a\in\mathit{Act})\\\
&\mathbf{(N_{a})}~{}\mathit{no}=\mathit{no}+a.\mathit{no}~{}(a\in\mathit{Act})\\\
&\mathbf{(D_{a})}~{}a.(x+y)=a.x+a.y~{}(a\in\mathit{Act})\end{split}$

Table 3: The axioms of $\mathcal{E}_{v}$

######  Remark 4.

Note that $\mathcal{E}_{v}$ is finite, if so is $\mathit{Act}$.

The subscript v in the naming scheme of the axiom set refers to the kind of
equivalence that it axiomatizes, namely verdict equivalence. It will later be
replaced with ω when we study $\omega$-verdict equivalence and used
accordingly from that point forward.

We provide now the following lemma as an observation on the number of
necessary axioms when $\mathit{Act}$ is finite and as an example proof based
on these axioms.

######  Lemma 3.

When $\mathit{Act}$ is finite, the family of axioms $(Y_{a})$ can be replaced
with

$\mathbf{(Y)}~{}\mathit{yes}=\mathit{yes}+\displaystyle\sum_{a\in\mathit{Act}}a.\mathit{yes}\text{.}$

Similarly the family of axioms $(N_{a})$ can be replaced with

$\mathbf{(N)}~{}\mathit{no}=\mathit{no}+\displaystyle\sum_{a\in\mathit{Act}}a.\mathit{no}\text{.}$

###### Proof.

It is not hard to see that the equation $Y$ can be proved by using the family
of equations $Y_{a}$. For the converse we can use axioms $A3$ and $Y$ to prove
any equation $\mathit{yes}=\mathit{yes}+b.\mathit{yes}$ of the family
$\\{Y_{a}\mid a\in\mathit{Act}\\}$. Indeed, $\mathcal{E}_{v}$ proves

$\mathit{yes}=\mathit{yes}+\displaystyle\sum_{a\in\mathit{Act}}a.\mathit{yes}=\mathit{yes}+\displaystyle\sum_{a\in\mathit{Act}}a.\mathit{yes}+b.\mathit{yes}=\mathit{yes}+b.\mathit{yes}.$

∎

######  Theorem 1.

$\mathcal{E}_{v}$ is sound modulo $\simeq$. That is, if $\mathcal{E}_{v}\vdash
m=n$ then $m\simeq n$, for all $m,n\in$$Mon_{F}$.

###### Proof.

It suffices to prove soundness for each of the axioms separately. The details
of the proof are standard and therefore omitted. ∎

In what follows, we will consider terms up to axioms $A1$-$A4$.

A fact that will be proven useful later on is the following: If
$m\xrightarrow[]{a}n$ then $A1-A4,E_{a},Y_{a},N_{a}~{}\vdash m=m+a.n.$ This
follows easily by induction on the size of $m$ and a case analysis on its form
and it is thus omitted.

We will now prove that the axiom system $\mathcal{E}_{v}$ is ground complete
for verdict equivalence.

######  Theorem 2.

$\mathcal{E}_{v}$ is ground complete for $\simeq$ over $Mon_{F}$. That is, if
$m,n$ are closed monitors in $Mon_{F}$ and $m\simeq n$ then
$\mathcal{E}_{v}\vdash m=n$.

As a first step towards proving that $\mathcal{E}_{v}$ is complete over closed
terms, we isolate a notion of normal form for monitors and prove that each
closed monitor in $Mon_{F}$ can be proved equal to a normal form using the
equations in $\mathcal{E}_{v}$.

######  Definition 4.

(Normal Form) A normal form is a closed term $m\in$ $Mon_{F}$ of the form:

$\displaystyle\sum_{a\in A}a.m_{a}~{}[+\mathit{yes}]~{}[+\mathit{no}]$

for some finite $A\subseteq\mathit{Act}$, where each $m_{a}$ is a term in
normal form that is different from $\mathit{end}$.

Note that, by taking $A=\emptyset$ in the definition above, we obtain that
$\mathit{end}$ is a normal form. In fact, it is the normal form with the
smallest size.

######  Lemma 4.

The only normal form that does not contain occurrences of $\mathit{yes}$ and
$\mathit{no}$ is $\mathit{end}$.

###### Proof.

We proceed by induction on the size of a normal form $m$. Our base case is a
verdict $v$. The only such verdict that does not contain an occurrence of
either $\mathit{yes}$ or $\mathit{no}$ is $\mathit{end}$, which trivially
satisfies the lemma. Assume now that $m=\displaystyle\sum_{a\in A}a.m_{a}$ is
a normal form satisfying the statement of the lemma. Since each $m_{a}$ is
$\mathit{yes}$\- and $\mathit{no}$-free, by inductive hypothesis,
$m_{a}=\mathit{end}$. This is only possible if $A=\emptyset$. Thus
$m=\mathit{end}$. ∎

######  Lemma 5.

(Normalization) Each closed term $m\in$$Mon_{F}$ is provably equal to some
normal form $m^{\prime}$ with $0pt(m^{\prime})\leq 0pt(m)$.

###### Proof.

We prove the claim by induction on the lexicographic ordering $\prec$ over
pairs $(0pt(m),size(m))$ of a monitor $m$, where $size(m)$ denotes the length
of $m$ in symbols. We proceed with a case analysis on the form $m$ may have.
Our induction basis will be a verdict $v$. If $v=\mathit{end}$ then the
monitor is already in normal form. Otherwise: If $m=v$ for some verdict
$v=\mathit{yes}$ or $\mathit{no}$ then it is proved equal to $v+\mathit{end}$
(from axiom $A4$). Indeed this normal form of a non-$\mathit{end}$ verdict has
depth less or equal to that of the initial monitor.

Our induction hypothesis is that, for all monitors $m_{0}\in$ $Mon_{F}$ up
such that $(0pt(m_{0}),size(m_{0}))\prec(0pt(m),size(m))$, we have that
$\mathcal{E}_{v}\vdash m_{0}=m_{0}^{\prime}$ with $m_{0}^{\prime}$ in normal
form and $0pt(m_{0}^{\prime})\leq 0pt(m_{0})$.

Assume that $m=a.n$ then clearly $n$ has depth less than that of $m$ and
therefore by the inductive hypothesis $\mathcal{E}\vdash n\simeq n^{\prime}$
where $n^{\prime}$ is in normal form and of depth less or equal than $n$. If
$n^{\prime}=\mathit{end}$ then $\mathcal{E}_{v}\vdash m=\mathit{end}$ (using
$E_{a}$) which is a normal form of smaller depth. Otherwise $a.n^{\prime}$ is
also a normal form.

Assume that $m=m_{1}+m_{2}$. By applying the induction hypothesis we have that

$\mathcal{E}_{v}\vdash m_{1}=\sum_{a\in
A_{1}}a.m_{1a}~{}[+\mathit{yes}][+\mathit{no}]~{}\text{and}~{}\mathcal{E}_{v}\vdash
m_{2}=\sum_{a\in A_{2}}a.m_{2a}~{}[+\mathit{yes}][+\mathit{no}].$

Therefore by applying axioms from $\mathcal{E}_{v}$ we can rewrite $m$ as:

$m=\displaystyle\sum_{a\in A_{1}\setminus A_{2}}a.m_{1a}^{\prime}+\sum_{a\in
A_{2}\setminus A_{1}}a.m_{2a}^{\prime}+\sum_{b\in A_{1}\cap
A_{2}}b.(m_{1b}^{\prime}+m_{2b}^{\prime})~{}[+\mathit{yes}][+\mathit{no}].$

Where by the statement of the lemma we have:

$depth\left(\displaystyle\sum_{a\in A_{1}\setminus
A_{2}}a.m_{1a}^{\prime}\right)\leq depth(m_{1})\leq 0pt(m)$

and similarly:

$0pt\left(\displaystyle\sum_{a\in A_{2}\setminus
A_{1}}a.m_{2a}^{\prime}\right)\leq depth(m_{2})\leq 0pt(m).$

It remains to show that the summand $\displaystyle\sum_{b\in A_{1}\cap
A_{2}}b.(m_{1b}^{\prime}+m_{2b}^{\prime})$ is equal to a normal form and that
it has depth less or equal to that of $m$. However, this is not trivial to
see, since the terms $m_{1a}^{\prime}$ and $m_{2b}^{\prime}$ have been
rewritten by the normalization procedure and therefore we cannot guarantee
that their summation has size less of that of $m$ (applying the inductive
hypothesis only results in terms of smaller depth but not size as we saw for
instance in the case of normalization of verdicts). However we have the
following:

$0pt(m_{1b}^{\prime}+m_{2b}^{\prime})=max[0pt(m_{1b}^{\prime}),0pt(m_{2b}^{\prime})]$
$<~{}max[0pt(m_{1}^{\prime}),0pt(m_{2}^{\prime})].$

The later of the above quantities is guaranteed to be less than or equal to
$0pt(m)$ by the inductive hypothesis. Therefore we still have that the monitor
$m_{1b}^{\prime}+m_{2b}^{\prime}$ appears earlier in the lexicographic
ordering and therefore $\mathcal{E}_{v}$ can prove it equal to a normal form
of smaller depth. We will call this normal form $m_{b}^{\prime}$. We have
therefore that that $0pt(m_{b}^{\prime})\leq
depth(m_{1b}^{\prime}+m_{2b}^{\prime})$. We now have the necessary result that

$\mathcal{E}_{v}\vdash m=m^{\prime}=\displaystyle\sum_{a\in A_{1}\cup
A_{2}}a.m_{a}~{}[+\mathit{yes}][+\mathit{no}],$

where each $m_{a}$ is in normal form and of depth strictly less than that of
$m$ which means that $0pt(m^{\prime})\leq 0pt(m)$ and we are done. ∎

Since now we have that each term in $Mon_{F}$ is provably equal to a normal
form, we might attempt to prove Theorem 2 by arguing that the normal forms of
two verdict equivalent monitors are identical. However, it turns out that this
is not true. Consider, for example, the case were $m=\mathit{yes}$ and
$n=\mathit{yes}+a.a.a.\mathit{yes}$. These two monitors are clearly verdict
equivalent as $L_{a}(m)=L_{a}(n)=\mathit{Act}^{*}$ and
$L_{r}(m)=L_{r}(n)=\emptyset$. However, even though they are in normal form
they are not syntactically equal. Intuitively, $a.a.a.\mathit{yes}$ in monitor
$n$ is redundant, as it can be absorbed by $\mathit{yes}$. In what follows, we
will show how to reduce the normal form of a monitor further using equations
in $\mathcal{E}_{v}$ in order to eliminate such redundant sub-terms.

######  Lemma 6.

The following statements hold for any monitor in $Mon_{F}$:

  1. 1.

For each action $a$, if $m$ is a closed $\mathit{no}$-free term then
$\mathcal{E}_{v}\vdash\mathit{yes}+a.m=\mathit{yes}$.

  2. 2.

For each action $a$, if $m$ is a closed monitor that contains occurrences of
both $\mathit{yes}$ and $\mathit{no}$ then
$\mathcal{E}_{v}\vdash\mathit{yes}+a.m=\mathit{yes}+a.n$ for some
$\mathit{yes}$-free closed monitor n.

  3. 3.

For each action $a$, if $m$ is a closed $\mathit{yes}$-free term then
$\mathcal{E}_{v}\vdash\mathit{no}+a.m=\mathit{no}$.

  4. 4.

For each action $a$, if $m$ is a closed monitor that contains occurrences of
both $\mathit{yes}$ and $\mathit{no}$ then
$\mathcal{E}_{v}\vdash\mathit{no}+a.m=\mathit{no}+a.n$ for some
$\mathit{no}$-free closed monitor n.

###### Proof.

We only prove statements 1 and 2 as the proofs of 3 and 4 are similar. We will
use structural induction on $m$.

  1. 1.

If $m$ is a verdict other than $\mathit{no}$ then the claim follows using
axioms $E_{a},~{}Y_{a}$ and $A4$ appropriately. If $m=b.m^{\prime}$ where
$m^{\prime}$ is $\mathit{no}$-free then $\mathcal{E}_{v}$ derives:

$\mathit{yes}+a.m\overset{\mathrm{Y_{a}}}{=}\mathit{yes}+a.\mathit{yes}+a.m\overset{\mathrm{D_{a}}}{=}\mathit{yes}+a.(\mathit{yes}+b.m^{\prime})\overset{\mathrm{\textbf{I.H.}}}{=}\mathit{yes}+a.\mathit{yes}\overset{\mathrm{Y_{a}}}{=}\mathit{yes}.$

If $m$ is of the form $m_{1}+m_{2}$ where $m_{1},m_{2}$ are
$\mathit{no}$-free, then it suffices to apply axiom $D_{a}$ and the induction
hypothesis.

  2. 2.

Assume that $m$ contains occurrences of both $\mathit{yes}$ and $\mathit{no}$.
We will show that $\mathcal{E}_{v}\vdash\mathit{yes}+a.m=\mathit{yes}+a.n$ for
some $\mathit{yes}$-free monitor $n$.

If $m=v$ for some verdict $v$ then the claim follows vacuously.

If $m=b.m^{\prime}$ for some $m^{\prime}$ that contains both $\mathit{yes}$
and $\mathit{no}$ then there is some $\mathit{yes}$-free $n^{\prime}$, such
that $n=b.n^{\prime}$, and $\mathcal{E}_{v}$ derives :

$\mathit{yes}+a.m=\mathit{yes}+a.b.m^{\prime}\overset{\mathrm{Y_{a}}}{=}\mathit{yes}+a.\mathit{yes}+a.b.m^{\prime}\overset{\mathrm{D_{a}}}{=}\mathit{yes}+a.(\mathit{yes}+b.m^{\prime})$

and for some $\mathit{yes}$-free $n^{\prime}$ s.t. $n=b.n^{\prime}$:

$\overset{\mathrm{I.H}}{=}\mathit{yes}+a.(\mathit{yes}+b.n^{\prime})\overset{\mathrm{D_{a}}}{=}\mathit{yes}+a.\mathit{yes}+a.b.n^{\prime}\overset{\mathrm{Y_{a}}}{=}\mathit{yes}+a.n.$

Finally if $m=m_{1}+m_{2}$ then $\mathcal{E}_{v}$ can derive:

$\mathit{yes}+a.(m_{1}+m_{2})\overset{\mathrm{D_{a}}}{=}\mathit{yes}+a.m_{1}+a.m_{2}.$

We now isolate the following cases based on what verdicts the monitors
$m_{i},~{}i\in\\{1,2\\}$ contain. If any $m_{i},~{}i\in\\{1,2\\}$ is both
$\mathit{yes}$\- and $\mathit{no}$-free it must be equal to $\mathit{end}$ as
it is in normal form and therefore
$\mathcal{E}_{v}\vdash\mathit{yes}+a.m_{i}=\mathit{yes}$. If
$m_{i},~{}i\in\\{1,2\\}$ contains occurrences of both $\mathit{yes}$ and
$\mathit{no}$, then the induction hypothesis yields that

$\mathcal{E}_{v}\vdash\mathit{yes}+a.m_{i}=\mathit{yes}+a.n_{i}$

for some $\mathit{yes}$-free $n_{i}$. If $m_{i},i\in\\{1,2\\}$ is
$\mathit{yes}$-free we already have the result that
$\mathcal{E}_{v}\vdash\mathit{yes}+a.m_{i}=\mathit{yes}+a.n_{i}$ for some
$\mathit{yes}$-free monitor $n_{i}$ (which in this case coincides with
$m_{i}$). Finally, if some $m_{i}$ is $\mathit{no}$-free then, by statement 1
in the lemma,

$\mathcal{E}_{v}\vdash\mathit{yes}+a.m_{i}=\mathit{yes}.$

Combining these observations, we have that:

$\mathcal{E}_{v}\vdash\mathit{yes}+a.m=\mathit{yes}+a.n_{1}+a.n_{2}~{}~{}$

where both $n_{1}$ and $n_{2}$ are $\mathit{yes}$-free and therefore by axiom
$D_{a}$:

$\mathcal{E}_{v}\vdash\mathit{yes}+a.m=\mathit{yes}+a.n$

for some $\mathit{yes}$-free monitor $n$.

∎

The above lemma suggests the notion of a reduced normal form.

######  Definition 5.

(Reduced normal form)  A reduced normal form is a term

$m=\displaystyle\sum_{a\in A}a.m_{a}~{}[+\mathit{yes}]~{}[+\mathit{no}]$

in normal form, where if $v\in\\{\mathit{yes},\mathit{no}\\}$ is a summand of
$m$ then each $m_{a}$ is $v$-free and in reduced normal form.

######  Remark 5.

Note here that if $\displaystyle\sum_{a\in A}a.m_{a}+\mathit{yes}+\mathit{no}$
is in reduced normal form then $A=\emptyset$.

######  Lemma 7.

Each monitor in normal form is provably equal to a monitor in reduced normal
form.

###### Proof.

The claim follows from Lemma 6, using induction on the depth of the normal
form. ∎

We are now ready to complete the proof of Theorem 2.

###### Proof of Theorem 2.

Since each monitor is provably equal to a reduced normal form (Lemma 7), and
by the soundness of $\mathcal{E}_{v}$ (Theorem 1), it suffices to prove the
claim for verdict equivalent reduced normal forms $m$ and $n$. We proceed by
induction on the sum of the sizes of $m$ and $n$, and a case analysis on the
possible form $m$ may have.

  1. 1.

Assume that $m=\mathit{yes}+\mathit{no}\simeq n$. Since
$L_{a}(m)=L_{r}(m)=\mathit{Act}^{*}$, it follows that $n$ has both
$\mathit{yes}$ and $\mathit{no}$ as summands. Since $n$ is in reduced normal
form it must be the case that $n=\mathit{yes}+\mathit{no}$, and we are done.

  2. 2.

Assume that $m=\displaystyle\sum_{a\in A}a.m_{a}+\mathit{yes}\simeq n$, where,
for all $a\in A,~{}m_{a}$ is $\mathit{yes}$-free and in reduced normal form
and $n=\displaystyle\sum_{b\in B}b.n_{b}[+\mathit{yes}][+\mathit{no}]$, where
each $n_{b}$ is in reduced normal form and is $v$-free, if $v$ is a summand of
$n$. Since $\varepsilon\in L_{a}(m)\setminus L_{r}(m)$, we have that
$\mathit{yes}$ is a summand of $n$ and $\mathit{no}$ is not. Thus
$n=\displaystyle\sum_{b\in B}b.n_{b}+\mathit{yes}$, and each $n_{b}$ is
$\mathit{yes}$-free. We claim that:

    1. (C1)

$A=B$ and

    2. (C2)

for all $a\in A,~{}m_{a}\simeq n_{a}$.

To prove that $A=B$, we assume that $a\in A$. Since $m_{a}$ is
$\mathit{yes}$-free and different from $\mathit{end}$, there is some
$s\in\mathit{Act}^{*}$ such that $a.s\in L_{r}(m)$. As $m\simeq n$, we have
that $a.s\in L_{r}(n)$. We conclude that $a\in B$ and $s\in L_{r}(n_{a})$. By
symmetry, claim 2(C1) follows.

We now show that $m_{a}\simeq n_{a}$ for each $a\in A$. Since $m_{a}$ and
$n_{a}$ are $\mathit{yes}$-free, $L_{a}(m_{a})=L_{a}(n_{a})=\emptyset$. We
pick now some arbitrary $s\in L_{r}(m_{a})$ ($L_{r}(m_{a})\neq\emptyset$
because $m_{a}\neq\mathit{end}$). This means that $a.s\in L_{r}(m)=L_{r}(n)$
and therefore $s\in L_{r}(n_{a})$. The claim follows by symmetry. By the
induction hypothesis, $\mathcal{E}_{v}\vdash m_{a}=n_{a}$ for each $a\in A=B$.
Therefore

$m=\displaystyle\sum_{a\in A}a.m_{a}+\mathit{yes}=\displaystyle\sum_{b\in
B}b.n_{b}+\mathit{yes}=n$

is provable from $\mathcal{E}_{v}$ and we are done.

  3. 3.

We are left with the case where $m=\displaystyle\sum_{a\in
A}a.m_{a}+\mathit{no}\simeq n$ and the case $m=\displaystyle\sum_{a\in
A}a.m_{a}$. The proofs for those cases are similar to the one for case 2 and
are thus omitted. ∎

###  3.1 Axiomatizing $\omega$-verdict equivalence

When $\mathit{Act}$ is infinite, by Lemma 2 and Theorem 2, $\mathcal{E}_{v}$
gives a ground-complete axiomatization of $\omega$-verdict equivalence as
well. However, when $\mathit{Act}$ is finite, $\mathcal{E}_{v}$ is not
powerful enough to prove all the equalities between closed terms that are
valid with respect to $\omega$-verdict equivalence. The new axioms needed to
achieve a ground complete axiomatization in this setting are:
$\mathbf{(Y_{\omega})}$
$\mathit{yes}=\displaystyle\sum_{a\in\mathit{Act}}a.\mathit{yes}$
$\mathbf{(N_{\omega})}$
$\mathit{no}=\displaystyle\sum_{a\in\mathit{Act}}a.\mathit{no}$. The resulting
axiom system is called $\mathcal{E}_{\omega}$.

######  Remark 6.

The soundness of the new axioms is trivially shown since

$L_{a}(\mathit{yes})\cdot\mathit{Act}^{\omega}=\mathit{Act}^{*}\cdot\mathit{Act}^{\omega}=\mathit{Act}^{+}\cdot\mathit{Act}^{\omega}=L_{a}(\displaystyle\sum_{a\in\mathit{Act}}a.\mathit{yes})\cdot\mathit{Act}^{\omega}$

while
$L_{r}(\mathit{yes})=L_{r}(\displaystyle\sum_{a\in\mathit{Act}}a.\mathit{yes})=\emptyset$
(and symmetrically for the $N_{\omega}$ equation).

######  Theorem 3.

$\mathcal{E}_{\omega}$ is ground complete for $\simeq_{\omega}$ over closed
terms when $\mathit{Act}$ is finite. That is if $m,n$ are closed monitors in
$Mon_{F}$ and $m\simeq_{\omega}n$ then $\mathcal{E}_{\omega}\vdash m=n$.

###### Proof.

By Lemma 7 we may assume that $m$ and $n$ are in reduced normal form. We will
prove the claim by induction on the sizes of $m$ and $n$ for two
$\omega$-verdict equivalent monitors $m,n$ in reduced normal form.

We will proceed by a case analysis of the form $m$ may have and limit
ourselves to presenting the proof for a few selected cases that did not arise
in the proof of Theorem 2.

  * •

Assume that $m=\mathit{yes}+\mathit{no}\simeq_{\omega}\displaystyle\sum_{a\in
A}a.n_{a}=n$. First of all note that $A=\mathit{Act}$. Indeed if
$a\in\mathit{Act}\setminus A$ then
$a^{\omega}\in(L_{a}(m)\cdot\mathit{Act}^{\omega})\setminus(L_{a}(n)\cdot\mathit{Act}^{\omega})$
which contradicts our assumption that $m\simeq_{\omega}n$. Moreover, it is not
hard to see that, for each $a\in\mathit{Act}$,
$L_{a}(n_{a})\cdot\mathit{Act}^{\omega}=L_{r}(n_{a})\cdot\mathit{Act}^{\omega}=\mathit{Act}^{\omega}$.
This means that, for each $a\in\mathit{Act}$,
$n_{a}\simeq_{\omega}\mathit{yes}+\mathit{no}$. By induction, for each
$a\in\mathit{Act}$, we have that $\mathcal{E}_{\omega}\vdash
n_{a}=\mathit{yes}+\mathit{no}$. Thus, $\mathcal{E}_{\omega}\vdash
n=\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})$. From
axiom $D_{a}$, $\mathcal{E}_{\omega}\vdash
n=\displaystyle\sum_{a\in\mathit{Act}}a.\mathit{yes}+\sum_{a\in\mathit{Act}}a.\mathit{no}$
which from our two new axioms $Y_{\omega},N_{\omega}$ yields
$\mathcal{E}_{\omega}\vdash n=\mathit{yes}+\mathit{no}=m$, and we are done.

  * •

Assume that $m=\mathit{yes}+\mathit{no}\simeq_{\omega}\displaystyle\sum_{a\in
A}a.n_{a}+\mathit{yes}$, with each $n_{a}$ being $\mathit{yes}$-free and
different from $\mathit{end}$. Again, reasoning as in the previous case, we
have that $A=\mathit{Act}$. Moreover for each $a\in\mathit{Act}$,
$L_{r}(n_{a})\cdot\mathit{Act}^{\omega}=\mathit{Act}^{\omega}$. Following the
same argument as above only for the $\mathit{no}$ verdict we arrive at the
conclusion that $\mathcal{E}_{\omega}\vdash
n=\mathit{yes}+\displaystyle\sum_{a\in\mathit{Act}}a.\mathit{no}=\mathit{yes}+\mathit{no}=m$.

  * •

The case $m=\mathit{yes}+\mathit{no}\simeq_{\omega}\displaystyle\sum_{a\in
A}a.n_{a}+\mathit{no}$ is symmetrical to the one above.

  * •

Assume that $m=\mathit{yes}+\displaystyle\sum_{a\in
A}a.m_{a}\simeq_{\omega}\sum_{b\in B}b.n_{b}$ where both $m$ and $n$ are in
reduced normal form. First of all, we follow an argument similar to the first
case analyzed above, to the point where $\mathcal{E}_{\omega}\vdash
n=\mathit{yes}+\displaystyle\sum_{b\in B^{\prime}}b.n_{b}^{\prime}$ for some
$\mathit{yes}$-free monitors $n_{b}^{\prime}$. For the proof of this final
case we will use the following facts, whose validity can be easily
established:

    1. (S1)

$B=\mathit{Act}$,

    2. (S2)

for all $b\in\mathit{Act}$, $L_{a}(n_{b})=\mathit{Act}^{\omega}$, and

    3. (S3)

for all $a\in A$, $L_{r}(m_{a})=L_{r}(n_{a})$.

So, for each $a\in A$, $\mathit{yes}+m_{a}\simeq_{\omega}n_{a}$. Since both of
these monitors have smaller depth that the original ones, we have that by
induction:

$\mathcal{E}_{\omega}\vdash\mathit{yes}+m_{a}=n_{a},~{}\forall~{}a\in
A\texttt{.}$ (1)

For each $b\in\mathit{Act}\setminus A$, we have that
$\mathit{yes}\simeq_{\omega}n_{b}$ (because
$L_{r}^{\omega}(n_{b})=\emptyset$). Again, we have that, by induction:

$\mathcal{E}_{\omega}\vdash\mathit{yes}=n_{a},~{}\forall~{}b\in\mathit{Act}\setminus
B\texttt{.}$ (2)

So:

$\mathcal{E}_{\omega}\vdash
n=\displaystyle\sum_{b\in\mathit{Act}}b.n_{b}=\sum_{a\in
A}a.n_{a}+\sum_{b\in\mathit{Act}\setminus A}b.\mathit{yes}$

By equations (1) and (2):

$\mathcal{E}_{\omega}\vdash n=\displaystyle\sum_{a\in
A}a.(\mathit{yes}+m_{a})+\sum_{b\in\mathit{Act}\setminus A}b.\mathit{yes}$

$=\displaystyle\sum_{a\in A}a.\mathit{yes}+\sum_{a\in
A}a.m_{a}+\sum_{b\in\mathit{Act}\setminus A}b.\mathit{yes}$

$=\displaystyle\sum_{a\in\mathit{Act}}a.\mathit{yes}+\sum_{a\in
A}a.m_{a}=\mathit{yes}+\sum_{a\in A}a.m_{a},$

using axiom $Y_{\omega}$, and we are done.

The above analysis can be applied symmetrically for the cases:

    * –

$m=\mathit{no}+\displaystyle\sum_{a\in A}a.m_{a}\simeq_{\omega}\sum_{b\in
B}b.n_{b}=n$ and

    * –

$m=\displaystyle\sum_{a\in A}a.m_{a}\simeq_{\omega}\sum_{b\in B}b.n_{b}=n.$

This completes the proof. ∎

##  4 Open Terms

Thus far, we have only studied the completeness of equational axiom systems
for $\simeq$ and $\simeq_{\omega}$ over closed terms. However, in our grammar
we allow for variables and it is natural to wonder whether the ground-complete
axiomatizations we have presented in Theorems 2 and 3 are also complete for
verdict equivalence and $\omega$-verdict equivalence over open terms.
Unfortunately, this turns out to be false. Indeed, the equation

$(\mathbf{O1})~{}~{}\mathit{yes}+\mathit{no}=\mathit{yes}+\mathit{no}+x$

is valid with respect to $\simeq$ (as both sides trivially accept and reject
all traces), but cannot be proved using the equations in
$\mathcal{E}_{\omega}$. This is because all the equations in that axiom system
have the same variables on their left- and right-hand sides. Our goal in the
remainder of this section is to study the equational theory of $\simeq$ and
$\simeq_{\omega}$ over open terms. Subsection 4.1 will present our results
when $\mathit{Act}$ is infinite as this case turns out to be more
straightforward. We consider the setting of a finite set of actions in
Subsection 4.2. In what follows, we use $\mathcal{E}_{v}^{\prime}$ for the
axiom system that results by adding $O1$ to $\mathcal{E}_{v}$. The superscript
′ will be used in the name of an axiom set to denote that the axiom set is
complete for one notion of equivalence over open terms. The absence of a
superscript refers respectively to a ground complete axiom set.

Towards a completeness theorem, we modify the notion of normal form, to take
variables into account. To that end we define:

######  Definition 6.

A term $m\in$ $Mon_{F}$ is in open normal form if it has the form:

$m=\displaystyle\sum_{a\in A}a.m_{a}+\displaystyle\sum_{i\in
I}x_{i}~{}[+\mathit{yes}]~{}[+\mathit{no}]$

where $\\{x_{i}\mid i\in I\\}$ is a finite set of variables, $A$ is a finite
subset of $\mathit{Act}$ and each $m_{a}$ is an (open) term in open normal
form that is different from $\mathit{end}$.

######  Lemma 8.

Each open term $m\in$$Mon_{F}$ is provably equal to some open normal form
$m^{\prime}$ with $0pt(m^{\prime})\leq 0pt(m)$.

The proof of the above result follows the lines of the one for Lemma 5 for
closed terms and is thus omitted.

As in the case of closed terms, we now proceed to characterize a class of open
normal forms for open terms whose verdict equivalence can be detected
“structurally”. The following example highlights the role that equation $(O1)$
plays in that characterization.

######  Example 2.

Consider the following monitor in open normal form:

$m=x+\mathit{yes}+a.b.(\mathit{no}+b.a.x).$

Monitor $m$ contains two occurrences of the variable $x$. However, because of
the interplay between the two verdicts, one of them is redundant and can be
removed thus:

$\displaystyle\mathcal{E}_{v}^{\prime}\vdash m$
$\displaystyle=x+\mathit{yes}+a.b.(\mathit{no}+b.a.x)$
$\displaystyle\overset{\mathrm{Y_{a}}}{=}x+\mathit{yes}+a.\mathit{yes}+a.b.(\mathit{no}+b.a.x)$
$\displaystyle\overset{\mathrm{Y_{b}}}{=}x+\mathit{yes}+a.(\mathit{yes}+b.\mathit{yes})+a.b.(\mathit{no}+b.a.x)$
$\displaystyle\overset{\mathrm{D_{a}}}{=}x+\mathit{yes}+a.(\mathit{yes}+b.\mathit{yes}+b.(\mathit{no}+b.a.x))$
$\displaystyle\overset{\mathrm{D_{b}}}{=}x+\mathit{yes}+a.(\mathit{yes}+b.(\mathit{yes}+\mathit{no}+b.a.x))$
$\displaystyle\overset{\mathrm{O_{1}}}{=}x+\mathit{yes}+a.(\mathit{yes}+b.(\mathit{yes}+\mathit{no}))$
$\displaystyle\overset{\mathrm{D_{b}}}{=}x+\mathit{yes}+a.(\mathit{yes}+b.\mathit{yes}+b.\mathit{no})$
$\displaystyle\overset{\mathrm{Y_{b}}}{=}x+\mathit{yes}+a.(\mathit{yes}+b.\mathit{no})$
$\displaystyle\overset{\mathrm{D_{a}}}{=}x+\mathit{yes}+a.\mathit{yes}+a.b.\mathit{no}$
$\displaystyle\overset{\mathrm{Y_{a}}}{=}x+\mathit{yes}+a.b.\mathit{no}.$

The above example motivates the following notion of reduced normal form for
open terms.

######  Definition 7.

An open reduced normal form is a term

$m=\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in
I}x_{i}~{}[+\mathit{yes}]~{}[+\mathit{no}]$

where if $v\in\\{\mathit{yes},\mathit{no}\\}$ is a summand of m then each
$m_{a}$ is $v$-free, different from $\mathit{end}$ and in open reduced normal
form. In addition:

  * •

if both $\mathit{yes}$ and $\mathit{no}$ are summands of $m$ then $m$ is equal
to $\mathit{yes}+\mathit{no}$,

  * •

if $\mathit{yes}$ is a summand of $m$ and
$m\xrightarrow[]{s}\mathit{no}+m^{\prime}$, for some $s$ and $m^{\prime}$ then
$m^{\prime}$ is equal to $\mathit{end}$,

  * •

if $\mathit{no}$ is a summand of $m$ and
$m\xrightarrow[]{s}\mathit{yes}+m^{\prime}$, for some $s$ and $m^{\prime}$
then $m^{\prime}$ is equal to $\mathit{end}$.

In what follows we will omit the word “open” when referring to the normal form
of a term that contains variables.

######  Lemma 9.

For each open monitor $m\in$ $Mon_{F}$, its normal form is provably equal to a
reduced normal form.

###### Proof.

By Lemma 8 we may assume that $m$ is in in normal form. The proof is by
induction on the size of $m$ and we isolate the following cases, depending on
the verdicts $v\in\\{\mathit{yes},\mathit{no}\\}$ $m$ has as summands:

  1. 1.

Case $m=\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in I}x_{i}$. In this case we
use the induction hypothesis on the $m_{a}$ monitors. These are different from
$\mathit{end}$ and have smaller size than $m$ and therefore they are provably
equal to a reduced normal form, i.e $\mathcal{E}_{v}^{\prime}\vdash
m_{a}=m_{a}^{\prime}$ where $m_{a}^{\prime}$ is in reduced normal form. Thus
$\mathcal{E}_{v}^{\prime}$ proves $m=\displaystyle\sum_{a\in
A}a.m^{\prime}_{a}+\sum_{i\in I}x_{i}$, and we are done since
$\displaystyle\sum_{a\in A}a.m^{\prime}_{a}+\sum_{i\in I}x_{i}$ is in reduced
normal form.

By applying the congruence closure equational law we have that
$\mathcal{E}_{v}^{\prime}\vdash m=m^{\prime}$, where $m^{\prime}$ is in
reduced normal form.

  2. 2.

Case $m=\mathit{yes}+\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in I}x_{i}$. In
this case by the induction hypothesis each $m_{a}$ is provably equal to a
reduced normal form. The extra step here is that if
$m\xrightarrow[]{s}\mathit{no}+m^{\prime}$, for some $s$ and $m^{\prime}$ then
$m^{\prime}$ is equal to $\mathit{end}$. In such a scenario we have that:

If $s=\varepsilon$, then the claim follows trivially from $O1$. Otherwise
$s=a.s^{\prime}$ for some action $a\in\mathit{Act}$ and
$m\xrightarrow[]{a}m_{a}\xrightarrow[]{s^{\prime}}\mathit{no}+m^{\prime}$. We
now apply our axioms as follows:

$m=\mathit{yes}+\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in
I}x_{i}\overset{\mathrm{Y_{a}}}{=}\mathit{yes}+\displaystyle\sum_{b\in
A\setminus\\{a\\}}b.m_{b}+a.\mathit{yes}+a.m_{a}+\sum_{i\in I}x_{i}$
$\overset{\mathrm{D_{a}}}{=}\mathit{yes}+\displaystyle\sum_{b\in
A\setminus\\{a\\}}b.m_{b}+a.(\mathit{yes}+a.m_{a})+\sum_{i\in I}x_{i}.$

This means that since $\mathit{yes}+m_{a}$ has size smaller than $m$ it is
provably equal to a reduced normal form. Additionally, since it contains a
$\mathit{yes}$ summand and
$m_{a}\xrightarrow[]{s^{\prime}}\mathit{no}+m^{\prime}$, by the induction
hypothesis we have that $m^{\prime}$ is equal to $\mathit{end}$ and we are
done.

  3. 3.

Case $m=\mathit{no}+\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in I}x_{i}$. The
proof of this case is symmetrical to Case $2$ and therefore omitted.

  4. 4.

Case $m=\mathit{yes}+\mathit{no}+\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in
I}x_{i}$. In this case we use the following simple argument. Starting for
axiom $O_{1}$ we use the substitution $\sigma(x)=\displaystyle\sum_{a\in
A}a.m_{a}+\sum_{i\in I}x_{i}$ and we get:

$\mathit{yes}+\mathit{no}=\mathit{yes}+\mathit{no}+\displaystyle\sum_{a\in
A}a.m_{a}+\sum_{i\in I}x_{i},$

and by applying the equational law of transitivity we have that
$\mathcal{E}_{v}^{\prime}\vdash m=\mathit{yes}+\mathit{no}$. ∎

The normal form defined above for open terms is adjusted over the closed terms
case. This is because now our syntax is allowing for variables and therefore
it is convenient for proofs to take these variables into account in a
controlled and consistent manner. The further reducing that occurred towards
defining the open reduced normal forms was possible due to the existence of
the new axiom $O_{1}$, which gave us the option to remove variable
occurrences. The new axiom $O_{1}$ is the only axiom we have currently
available that does not contain every variable occurrence in both of its sides
and it is therefore the only rule we have available that can help us remove
variables from equations. In the presence of other axioms with this property
we can further reduce our normal forms, as we will see later on.

In the following subsections, we will study the full equational theory of
verdict and omega-verdict equivalence over open terms.

###  4.1 Infinite set of actions

We begin by considering the equational theory of open monitors when the set of
actions is infinite. Apart from its theoretical interest, this scenario has
also some practical relevance. Indeed, as shown already by Milner in [42, 44],
infinite sets of uninterpreted actions are useful when modeling system events
that carry data values. Runtime monitoring of systems with data-dependent
behavior has been an active field of research for over 15 years—see, for
instance, the paper [11] for an early reference.

When the set of actions $\mathit{Act}$ is infinite, it is easy to define a
one-to-one mapping from open to closed terms that will help us prove
completeness of the axiom system $\mathcal{E}_{v}^{\prime}$.

######  Theorem 4.

(Completeness for open terms modulo $\simeq$) $\mathcal{E}_{v}^{\prime}$ is
complete for $\simeq$ over open monitors in $Mon_{F}$ when $\mathit{Act}$ is
infinite. That is, for all $m,n\in$ $Mon_{F}$, if $m\simeq n$, then
$\mathcal{E}_{v}^{\prime}\vdash m=n$.

###### Proof.

Assume $m\simeq n$. By Lemma 9, we may assume that $m$ and $n$ are in reduced
normal form.

Let

$m=\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in
I}x_{i}~{}[+\mathit{yes}]~{}[+\mathit{no}]$

and

$n=\displaystyle\sum_{b\in B}b.n_{b}+\sum_{j\in
J}y_{j}~{}[+\mathit{yes}]~{}[+\mathit{no}]\text{.}$

We will show that $\mathcal{E}_{v}^{\prime}\vdash m=n$ by induction on the sum
of the sizes of $m$ and $n$. To this end, we will establish a strong
structural correspondence between $m$ and $n$. Consider a substitution
$\sigma$ defined as follows: $\sigma(x)=a_{x}.(\mathit{yes}+\mathit{no})$
where

  * •

for all variables $x$ and $y,~{}a_{x}=a_{y}$ implies $x=y$, and

  * •

$\\{a_{x}\mid x\in\mathit{Var}\\}$ is disjoint from the set of actions
occurring in $m$ or $n$.

Note that such a substitution $\sigma$ exists because $\mathit{Act}$ is
infinite. By induction on the sizes of $m$ and $n$, we will prove that if
$\sigma(m)\simeq\sigma(n)$ then:

  1. (C1)

$v$ is a summand of $m$ iff $v$ is a summand of $n$, for
$v\in\\{\mathit{yes},\mathit{no}\\}$,

  2. (C2)

$\\{x_{i}\mid i\in I\\}=\\{y_{j}\mid j\in J\\}$,

  3. (C3)

$A=B$ and

  4. (C4)

for each $a\in A,~{}\sigma(m_{a})\simeq\sigma(n_{a})$.

In what follows, we first show that $\mathcal{E}_{v}^{\prime}$ proves $m=n$
assuming claims (C1)-(C4) and then we prove those claims. To prove that
$\mathcal{E}_{v}^{\prime}$ proves $m=n$ follows from
$\sigma(m)\simeq\sigma(n)$ for reduced normal forms $m$ and $n$, we proceed by
induction on the sum of the sizes of $m$ and $n$. By claim $\mathbf{C4}$, we
have that $\sigma(m_{a})\simeq\sigma(n_{a})$ and, from the induction
hypothesis, $\mathcal{E}_{v}^{\prime}\vdash m_{a}=n_{a}$. By C1-3 we also have
that $\mathcal{E}_{v}^{\prime}\vdash\displaystyle\sum_{i\in I}x_{i}=\sum_{j\in
J}y_{j}$ and that $\displaystyle\sum_{a\in A}a.m_{a}=\sum_{b\in B}b.n_{b}$,
which means that by using the equational law of closure under summation we
also have that $\mathcal{E}_{v}^{\prime}\vdash m=n$.

We present now the proofs of (C1)-(C4).

C1: Assume $\mathit{yes}$ is a summand of $m$. Then $\varepsilon\in
L_{a}(\sigma(m))$. Since $\sigma(m)\simeq\sigma(n)$, we have that
$\varepsilon\in L_{a}(\sigma(n))$. Note that $\varepsilon\not\in
L_{a}(\sigma(x))$ for each $x$. Thus $\mathit{yes}$ must be a summand of $n$.
The case for $v=\mathit{no}$ is similar. By symmetry the claim follows.

C2: Assume that $x\in\\{x_{i}\mid i\in I\\}$. By the definition of $\sigma$,
it follows that $\sigma(m)$ both accepts and rejects the trace $a_{x}$. Since
$m\simeq n$, we have that $\sigma(n)$ also accepts and rejects the trace
$a_{x}$. As $n$ does not contain any occurrence of $a_{x}$ and has at most one
of the verdicts $\mathit{yes}$ and $\mathit{no}$ as a summand, it follows that
$x\in\\{y_{j}\mid j\in J\\}$. Therefore, by symmetry, $\\{x_{i}\mid i\in
I\\}=\\{y_{j}\mid j\in J\\}$ and we are done.

C3: Assume, towards a contradiction, that $a\in A\setminus B$. Then $m$ cannot
have both $\mathit{yes}$ and $\mathit{no}$ as summands, since $m$ is in
reduced normal form.

If $m$ has none of the verdicts as a summand, we know that $m_{a}$ is
different from $\mathit{end}$ since $m$ is in reduced normal form. Therefore
$\sigma(m_{a})$ will either accept or reject some trace $s$, which implies
that $\sigma(m)$ will also accept or reject $as$. However, $\sigma(n)$ cannot
do the same because $a\not\in B$, $\sigma(x)\not\xRightarrow{a}$ for each $x$,
and neither $\mathit{yes}$ nor $\mathit{no}$ are summands of $n$. This
contradicts our assumption that $m\simeq n$.

Assume now, without loss of generality, that $m$ has only the verdict
$\mathit{yes}$ as summand. Observe that $m_{a}$ is $\mathit{yes}$-free and
different from $\mathit{end}$, since $m$ is in reduced normal form. This means
that $\sigma(m_{a})$ can reject some trace $s$ and, therefore, that
$\sigma(m)$ will reject $a.s$. On the other hand, $\sigma(n)$ cannot do the
same because $a\not\in B$, $\sigma(x)\not\xRightarrow{a}$ for each $x$ and
$\mathit{no}$ is not a summand of $n$. Again, this contradicts our assumption
that $m\simeq n$.

The above analysis yields that $A\subseteq B$. By symmetry, $A=B$ follows.

C4: Our final claim (and the one with the most involved proof) is that
$\sigma(m_{a})\simeq\sigma(n_{a})$, for each $a\in A$.

If the reduced normal forms of the monitors do not contain any verdict
$v\in\\{\mathit{yes},\mathit{no}\\}$ as a summand, then the argument is
simplified significantly. Therefore, we limit ourselves to presenting here the
most complicated case, where $m$ and $n$ both contain exactly one verdict
$v\in\\{yes,\mathit{no}\\}$ as a summand. Without loss of generality, we
assume that this verdict is $\mathit{yes}$, namely that

$m=\mathit{yes}+\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in I}x_{i}$

and

$n=\mathit{yes}+\displaystyle\sum_{b\in B}b.n_{b}+\sum_{j\in J}y_{i}.$

Since the claims C1-3 have already been proven, we know for $m$ and $n$ that:

$m=\mathit{yes}+\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in I}x_{i}\text{ and
}n=\mathit{yes}+\displaystyle\sum_{a\in A}a.n_{a}+\sum_{i\in I}x_{i}~{}.$

We remind the reader that our purpose is to prove that
$\sigma(m_{a})\simeq\sigma(n_{a})$, for each $a\in A$, so that we can apply
our induction hypothesis to infer that $\mathcal{E}_{v}^{\prime}\vdash
m_{a}=n_{a}$.

We first prove that the rejection sets of $\sigma(m_{a})$ and $\sigma(n_{a})$
are equal. To this end, assume that $s\in L_{r}(\sigma(m_{a}))$. It follows
that $a.s\in L_{r}(\sigma(m))=L_{r}(\sigma(n))$. By the form of $n$ and from
the definition of $\sigma$, we conclude that $s\in L_{r}(\sigma(n_{a}))$.
Therefore, $L_{r}(\sigma(m_{a}))\subseteq L_{r}(\sigma(n_{a}))$. By symmetry
we have that $L_{r}(\sigma(m_{a}))=L_{r}(\sigma(n_{a}))$ and we are done.

It remains to prove that the acceptance sets of $\sigma(m_{a})$ and
$\sigma(n_{a})$ are also identical. (It is important here to point out that,
since both $m$ and $n$ contain a $\mathit{yes}$ verdict as a summand, the
acceptance sets of $\sigma(m)$ and $\sigma(n)$ are both equal to
$\mathit{Act}^{*}$. However, for our inductive argument to work, we need to be
able to prove that $L_{a}(\sigma(m_{a}))=L_{a}(\sigma(n_{a}))$.) To that end
and towards a contradiction, consider a shortest trace $s$ that is accepted by
monitor $\sigma(m_{a})$, but not by $\sigma(n_{a})$. Consequently, monitor
$\sigma(m)$ accepts the trace $a.s$.

Since monitors $m_{a}$ and $n_{a}$ are $\mathit{yes}$-free, as a result of $m$
and $n$ being in reduced normal form, the acceptance of $s$ must be the result
of a variable $x$ mapped to $a_{x}.(\mathit{yes}+\mathit{no})$ through the
substitution $\sigma$. Since $s$ is a shortest trace that is accepted by
monitor $\sigma(m_{a})$, but not by $\sigma(n_{a})$, none of its prefixes is
accepted by $\sigma(m_{a})$ and therefore the last action that is in $s$ must
be the action $a_{x}$ stemming from $\sigma(x)$. This means that monitor
$m_{a}$ can perform the transition
$m_{a}\xRightarrow{s^{\prime}}m_{a}^{\prime}$, where $m_{a}^{\prime}$ contains
$x$ as a summand and $s=s^{\prime}.a_{x}$. Therefore the monitor
$\sigma(m_{a})$ can perform the transitions:

$\sigma(m_{a})\xRightarrow{s^{\prime}}\sigma(m_{a}^{\prime})\xrightarrow[]{a_{x}}\mathit{yes}+\mathit{no}\xrightarrow[]{\tau}\mathit{yes}.$

Since $s^{\prime}.a_{x}$ is accepted by $\sigma(m_{a})$, it must also be
rejected by it because $a_{x}$ is an action that can only be observed after
the substitution of the variable $x$ in $m_{a}$. We have already argued that
the rejection sets of $\sigma(m_{a})$ and $\sigma(n_{a})$ are equal and
therefore $\sigma(n_{a})$ also rejects the trace $s^{\prime}.a_{x}$. Since the
action $a_{x}$ is a unique action corresponding to the variable $x$, there are
only two ways in which $\sigma(n_{a})$ could reject the trace
$s^{\prime}.a_{x}$. The first case is that $\sigma(n_{a})$ can also perform
the transitions

$\sigma(n_{a})\xRightarrow{s^{\prime}}\sigma(n_{a}^{\prime})\xrightarrow[]{a_{x}}\mathit{yes}+\mathit{no}$

wfor some $n_{a}^{\prime}$. However, this would guarantee that $\sigma(n_{a})$
accepts $s$, whereas we assumed that it does not.

The most complicated case is when $\sigma(n_{a})$ can reject a prefix $s_{0}$
of $s^{\prime}$. By the already proven equality of the rejection sets of the
two sub-monitors, $\sigma(m_{a})$ would also reject $s_{0}$. This can only
happen if both $n_{a}$ and $m_{a}$ rejected that prefix independently of the
substitution $\sigma$, since every action preceding $a_{x}$ along the trace
$s^{\prime}$ is not an action corresponding to the mapping of a variable
through $\sigma$ as explained above. This means that both $m_{a}$ and $n_{a}$
can perform the transitions
$m_{a}\xRightarrow{s_{0}}\mathit{no}+m_{a}^{\prime}$ and
$n_{a}\xRightarrow{s_{0}}\mathit{no}+n_{a}^{\prime}$, for some
$m_{a}^{\prime}$ and $n_{a}^{\prime}$. However, since $m$ and $n$ are in
reduced normal form, this implies that $m_{a}^{\prime}$ and $n_{a}^{\prime}$
are equal to $\mathit{end}$. This leads us to a contradiction, as we assumed
that $\sigma(m_{a})$ accepts the trace $s$ which can no longer be the case if
$m_{a}\xrightarrow[]{s_{0}}\mathit{no}+\mathit{end}$ where $s_{0}$ is a prefix
of $s$.

Therefore every trace accepted by $\sigma(m_{a})$ is also accepted by
$\sigma(n_{a})$. By symmetry, we have that the acceptance sets of $m_{a}$ and
$n_{a}$ are equal.

This means that $\sigma(m_{a})\simeq\sigma(n_{a})$, which completes the proof
of C4 and consequently of the whole theorem. ∎

######  Corollary 1.

$\mathcal{E}_{v}^{\prime}$ is complete for $\simeq_{\omega}$ over open
monitors in $Mon_{F}$ when $\mathit{Act}$ is infinite. That is, for all
$m,n\in$ $Mon_{F}$, if $m\simeq n$, then $\mathcal{E}_{v}^{\prime}\vdash m=n$.

###### Proof.

The claim follows from Lemma 2. ∎

###  4.2 Finite set of actions

The study of the equational theory of $\simeq$ when $\mathit{Act}$ is finite
turns out to be more interesting and complicated. In this setting, we can
identify equations whose validity depends on the cardinality of
$\mathit{Act}$, which is not the case for any of the axioms we used so far. To
see this, consider the equation

$(\mathbf{V_{1}})~{}~{}x=x+a.x,$

which is sound when $\mathit{Act}=\\{a\\}$ but cannot be derived by the
equations in $\mathcal{E}_{v}^{\prime}$, as it is not sound when
$\mathit{Act}\neq\\{a\\}$.

As a first step in our study of the equational theory of $\simeq$ when
$\mathit{Act}$ is finite, we characterize some properties of sound equations.

######  Lemma 10.

Let $m\simeq n$ be a sound equation, where $m,n\in$ $Mon_{F}$ and $m$ is in
reduced normal form. Assume that

  * •

$m\xrightarrow[\text{}]{s}x+m^{\prime}$, for some $s$ in $\mathit{Act}^{*}$,
variable $x$ and $m^{\prime}$ in $Mon_{F}$, and

  * •

$m\not\xrightarrow[\text{}]{s_{p}}x+m_{s_{p}}$, for each proper prefix $s_{p}$
of $s$ and $m_{s_{p}}\in$ $Mon_{F}$.

Then, $n\xrightarrow[\text{}]{s}x+n^{\prime}$ for some $n^{\prime}$ in
$Mon_{F}$.

###### Proof.

Consider the substitution

$\sigma(y)=\begin{cases}\mathit{yes}+\mathit{no},&\text{if}~{}y=x\\\
\mathit{end},&\text{if}~{}y\neq x.\end{cases}$

Since $m\xrightarrow[\text{}]{s}x+m^{\prime}$ by one of the assumptions of the
lemma, we have that $\sigma(m)$ will both accept and reject $s$. Since
$m\simeq n$ is sound we have that $\sigma(n)$ must do the same. If
$n\not\xrightarrow[\text{}]{s}x+n^{\prime}$ for every $n^{\prime}$ then it is
not hard to see that there are two ways in which $n$ could accept and reject
$s$:

  1. 1.

$n\xRightarrow[\text{}]{s^{\prime}}\mathit{yes}$ and
$n\xRightarrow[\text{}]{s^{\prime}}\mathit{no}$ where $s^{\prime}$ is a prefix
of $s$ (including $s$ itself), or

  2. 2.

$n\xrightarrow[\text{}]{s^{\prime}}x+n^{\prime}$ where $s^{\prime}$ is a
prefix of $s$ (so that $\sigma(n)$ would accept and reject $s^{\prime}$ and
therefore $s$).

In the first case, consider the substitution $\sigma_{e}$ that maps all
variables to $\mathit{end}$. Since
$n\xRightarrow[\text{}]{s^{\prime}}\mathit{yes}$ and
$n\xRightarrow[\text{}]{s^{\prime}}\mathit{no}$, we have that $\sigma_{e}(n)$
accepts and rejects $s^{\prime}$. From $m\simeq n$, we have that
$\sigma_{e}(m)$ also accepts and rejects $s^{\prime}$. It is not hard to see
that this means that $m\xRightarrow[\text{}]{s^{\prime}}\mathit{yes}$ and
$m\xRightarrow[\text{}]{s^{\prime}}\mathit{no}$ However, this is impossible
because $m$ is a reduced normal form and
$m\xrightarrow[\text{}]{s}x+m^{\prime}$ by the proviso of the lemma.

In the second case, even though both monitors accept and reject $s$, we also
have that $\sigma_{e}(n)$ also accepts and rejects $s^{\prime}$. Again, since
the two monitors are verdict equivalent, we know that $\sigma_{e}(m)$ must do
the same. Since $m$ is in reduced normal form and
$m\not\xRightarrow[\text{}]{s_{p}}x+m^{\prime}$ for any prefix $s_{p}$ of $s$
(and therefore neither for $s^{\prime}$) we have that $\sigma(m)$ can only
accept and reject $s^{\prime}$ by performing the transitions
$m\xRightarrow[\text{}]{s_{1}^{\prime\prime}}\mathit{yes}$ and
$m\xRightarrow[\text{}]{s_{2}^{\prime\prime}}\mathit{no}$, for
$s_{1}^{\prime\prime}$ and $s_{2}^{\prime\prime}$ prefixes of $s^{\prime}$.
This however is not allowed since it contradicts the fact that $m$ is in
reduced normal form and $m\xrightarrow[\text{}]{s}x+m^{\prime}$. Since both
cases have led to a contradiction, we can infer that there is some
$n^{\prime}$ such that $n\xRightarrow[\text{}]{s}x+n^{\prime}$, which was to
be shown. ∎

######  Corollary 2.

Let $m\simeq n$ be a sound equation, where $m,n\in$ $Mon_{F}$ and $m$ is in
reduced normal form. Assume that

  * •

$m\xrightarrow[\text{}]{s}x+m^{\prime}$, for some $s$ in $\mathit{Act}^{*}$,
variable $x$ and $m^{\prime}$ in $Mon_{F}$, and

  * •

$n\not\xrightarrow[\text{}]{s}x+n^{\prime}$, for any $n^{\prime}\in$
$Mon_{F}$.

then we have that there exists an $s_{p}$ prefix of $s$ such that

  * •

$m\xrightarrow[\text{}]{s_{p}}x+m_{s_{p}}$ and
$n\xrightarrow[\text{}]{s_{p}}x+n_{s_{p}}$ for some $m_{s_{p}}$ and
$n_{s_{p}}$ in $Mon_{F}$, and

  * •

for any prefix $s_{0}$ of $s_{p}$ we have that
$m\not\xRightarrow[\text{}]{s_{0}}x+m^{\prime}$ and
$n\not\xRightarrow[\text{}]{s_{0}}x+n^{\prime}$ for any $m^{\prime}$ and
$n^{\prime}$ in $Mon_{F}$.

###### Proof.

Assume a sound equation $m\simeq n$ for witch we have
$m\xrightarrow[\text{}]{s}x+m^{\prime}$, for some $s$ in $\mathit{Act}^{*}$,
variable $x$ and $m^{\prime}$ in $Mon_{F}$. If this is the first occurrence of
$x$ along the trace $s$ in $m$ (i.e.
$m\not\xrightarrow[\text{}]{s_{p}}x+m_{s_{p}}$, for each proper prefix $s_{p}$
of $s$ and $m_{s_{p}}\in$ $Mon_{F}$), then by Lemma 10, we would have that $n$
must be able to perform the transitions
$n\xrightarrow[\text{}]{s}x+n^{\prime}$, for some $n^{\prime}$ in $Mon_{F}$.
Since this cannot be the case as the proviso of the corollary forbids it we
have that there must be a prefix $s_{p}$ of $s$ such that
$m\xrightarrow[\text{}]{s_{p}}x+m_{s_{p}}$.

Without loss of generality we assume $s_{p}$ to be the shortest such trace,
which means there are no other occurrences of the variable $x$ along the trace
$s_{p}$. We can therefore see that now for the trace $s_{p}$, Lemma 10 holds
and therefore $n\xrightarrow[\text{}]{s_{p}}x+n_{s_{p}}$ for some $n_{s_{p}}$
in $Mon_{F}$. Additionally since we assumed $s_{p}$ t be the shortest trace of
the necessary property we already have that
$m\not\xRightarrow[\text{}]{s_{0}}x+m^{\prime}$ for any $m^{\prime}$ in
$Mon_{F}$.

It remains to show that the same must hold for $n$. This can be easily seen to
be the case since if we assumed the opposite where for some prefix $s_{0}$ of
$s_{p}$ we had $n\xrightarrow[\text{}]{s_{0}}x+n_{0}$ for some $n_{0}$ then by
the symmetric analysis and by using the previous lemma and this corollary we
would arrive at a contradiction of $s_{p}$ being the shortest prefix of $s$
for witch $m\xrightarrow[\text{}]{s_{p}}x+m_{s_{p}}$. ∎

######  Remark 7.

In what follows, when studying open equations, we will refer to occurrences of
variables such as the one mentioned in the above corollary, where only one of
the monitors involved in the equation can reach a term of the form $x+m_{x}$
after observing a trace $s$, as “one-sided” variable occurrences.

Intuitively Lemma 10 states that on each sound equation (including axioms) of
which at least one side is in reduced normal form, the first occurrence of
each variable per distinct trace leading to the variable is common for both
sides of the equation.This gives us some handy intuition on what restrictions
an equation that is sound must satisfy.

The following example shows Lemma 10 in action.

######  Example 3.

The equation

$x+a.(x+a.(\mathit{yes}+\mathit{no})+b.(\mathit{yes}+\mathit{no}))=x+a.(a.(\mathit{yes}+\mathit{no})+b.(\mathit{yes}+\mathit{no}))~{}$

is sound over the set of actions $\mathit{Act}=\\{a,b\\}$, but

$x+a.(x+a.(\mathit{yes}+\mathit{no})+b.(\mathit{yes}+\mathit{no}))=a.(x+a.(\mathit{yes}+\mathit{no})+b.(\mathit{yes}+\mathit{no}))$

is not since the first occurrence of the variable $x$ in the second example
happens after the prefix $\varepsilon$ on the left-hand side but after the
prefix $a$ on the right. In the second equation, the earliest occurrence of
the variable $x$ (after the prefix $\varepsilon$) is one-sided.

Also notice here the importance of the sub-term
$a.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})$. We will
see that this type of sub-term is crucial for the soundness of the open
equations with one-sided variable occurrences we encounter later on.

The following notation will be used in what follows to describe a family of
sound equations that generalize the one given in Example 3.

######  Definition 8.

(Notation) Let $s\in\mathit{Act}^{*}$.

  1. 1.

We use $\mathit{pre}(s)$ to denote the set of prefixes of $s$ (including $s$).

  2. 2.

We use $s^{i}$, $i\geq 1$, to denote the trace $s$ if $i=1$ and $ss^{i-1}$
otherwise.

  3. 3.

We use $s.m$ to stand for a monitor that can perform exactly the actions along
the finite trace $s$ and then become $m$.

  4. 4.

We define
$\overline{s}^{\leq}(m)=\displaystyle\sum_{\begin{subarray}{c}|s^{\prime}|\leq|s|,~{}\\\
s^{\prime}\not\in\mathit{pre}(s)\end{subarray}}s^{\prime}.m$ . The monitor
$\overline{s}^{\leq}(m)$ is one that behaves like $m$ after having observed
any trace of length at most $|s|$ that is not a prefix of $s$.

  5. 5.

The term $\overline{s}(m)$ is defined thus:
$\overline{s}^{\leq}(m)+s.\displaystyle\sum_{a\in\mathit{Act}}a.m$ .

Intuitively $\overline{s}(\mathit{yes}+\mathit{no})$ stands for the monitor
that accepts and rejects all traces that _do not_ cause the acceptance or
rejection of the string $s$. Those are exactly the traces that are shorter
than $s$ but not its prefixes, and also the ones extending $s$.

  6. 6.

With the term $\overline{s}^{(k)}(m)$, for $k\geq 1$, we will mean the
summation:

$\overline{s}(m)~{}\text{if}~{}k=1~{}\text{and}~{}\displaystyle\sum_{1\leq
i<k-1}s^{i}.\overline{s}^{\leq}(m)+s^{k-1}.\overline{s}(m)$ if $k\geq 2$.

Intuitively $\overline{s}^{(k)}(\mathit{yes}+\mathit{no})$ stands for a
monitor that, after observing the fixed trace $s$, accepts and rejects
everything except the trace $s^{k}$ (and its prefixes).

We now present an example of the usage of the above notation in order to help
the reader understand the equations presented later involving these new
notions.

######  Example 4.

For a set of actions $\mathit{Act}=\\{a,b\\}$, the monitor
$m=\mathit{yes}+\mathit{no}$ and a trace $s=ab$ we have that:

  * •

$\mathit{pre}(s)=\\{\varepsilon,a,ab\\}$

  * •

$\overline{s}^{\leq}(m)=b.(\mathit{yes}+\mathit{no})+a.a.(\mathit{yes}+\mathit{no})+b.b.(\mathit{yes}+\mathit{no})+b.a.(\mathit{yes}+\mathit{no})$

  * •

$\overline{s}(m)=b.(\mathit{yes}+\mathit{no})+a.a.(\mathit{yes}+\mathit{no})+b.b.(\mathit{yes}+\mathit{no})+b.a.(\mathit{yes}+\mathit{no})+a.b.\displaystyle\sum_{c\in\mathit{Act}}c.(\mathit{yes}+\mathit{no})$

  * •

and for $k=3$ we get

$\overline{s}^{(3)}(m)=s.\overline{s}^{\leq}(m)+s^{2}.\overline{s}(m)=$
$a.b.(b.(\mathit{yes}+\mathit{no})+a.a.(\mathit{yes}+\mathit{no}))+$
$a.b.a.b.(b.(\mathit{yes}+\mathit{no})+a.a.(\mathit{yes}+\mathit{no})+b.b.(\mathit{yes}+\mathit{no})+$
$b.a.(\mathit{yes}+\mathit{no})+a.b.\displaystyle\sum_{c\in\mathit{Act}}c.(\mathit{yes}+\mathit{no}))$

This notation defined and presented above is very useful once one understands
a very particular form equations among open monitors take when they involve
one-sided variable occurrences. Consider, for instance, the following sound
equation (for a fixed constant $k$):

$x+a^{k}.x+\overline{a^{k}}^{3}(\mathit{yes}+\mathit{no})\simeq
x+\overline{a^{k}}^{3}(\mathit{yes}+\mathit{no})~{}.$

We will formally prove the soundness of (a more general form of) this equation
later on. We can intuitively see from the examples above that when an equation
contains a one-sided variable occurrence, then the rest of the terms involved
in the equation must have some specific form as well so that the equation will
stay sound under all possible substitutions. This means that certain traces
must always be accepted and rejected by both sides independently of a
substitution.

The following lemma formalizes this intuition.

######  Lemma 11.

Assume $m\simeq n$, where $m,n$ are in reduced normal form. If
$m\xrightarrow[\text{}]{s}x+m^{\prime}$ for some $m^{\prime}$ but
$n\not\xrightarrow[\text{}]{s}x+n^{\prime}$ for any $n^{\prime}$, then there
exist $s^{\prime},s^{\prime\prime}$ such that $s=s^{\prime}s^{\prime\prime}$
and, for all $s_{b}=ss_{p}$ where
$s_{p}\not\in\mathit{pre}(s^{\prime\prime})$, either:

  * •

$m\xRightarrow[\text{}]{s_{b}}\mathit{yes}$,
$m\xRightarrow[\text{}]{s_{b}}\mathit{no}$,
$n\xRightarrow[\text{}]{s_{b}}\mathit{yes}$ and
$n\xRightarrow[\text{}]{s_{b}}\mathit{no}$ or

  * •

$\exists s_{0},m^{\prime\prime},n^{\prime\prime}$ such that
$m\xrightarrow[\text{}]{s_{0}}x+m^{\prime\prime}$ and
$n\xrightarrow[\text{}]{s_{0}}x+n^{\prime\prime}$ and
$s_{0}.s_{b}\in\mathit{pre}(s.s_{b})$.

###### Proof.

We have an equation $m\simeq n$, with $m$ and $n$ in reduced normal form, for
which we assume that: $m\xrightarrow[\text{}]{s}x+m^{\prime}$ but
$n\not\xrightarrow[\text{}]{s}x+n^{\prime}$ for any $n^{\prime}$. Let $s$ be
the shortest trace meeting the proviso of the lemma. It is not hard to see
that $s\neq\varepsilon$ because $m\simeq n$ and $m$ and $n$ are in reduced
normal form. This means that indeed in the monitors $m,n$ all other earlier
occurrences of $x$ happen at both sides. By Corollary 2 we know that there is
a prefix of $s$ called $s^{\prime}$ ($s=s^{\prime}.s^{\prime\prime}$) such
that both $m$ and $n$ can perform the transitions
$m\xrightarrow[\text{}]{s^{\prime}}x+m_{0}^{\prime}$ and
$n\xrightarrow[\text{}]{s^{\prime}}x+n_{0}^{\prime}$, and in addition for
every prefix of $s^{\prime}$ we have that
$n\not\xrightarrow[\text{}]{s^{\prime}}x+n^{\prime}$ and
$m\not\xrightarrow[\text{}]{s^{\prime}}x+m^{\prime}$ for every $m^{\prime}$
and $n^{\prime}$.

This means that there are no other one-sided occurrences of the variable $x$
“between” $s^{\prime}$ and $s^{\prime\prime}$ (otherwise $s$ would not be the
shortest trace). Since $m\simeq n$ is sound, we know that under any
substitution the resulting monitors are verdict equivalent.

Consider the set of traces

$A=\\{t\mid(|t|\leq|s^{\prime\prime}|\wedge
t\not\in\mathit{pre}(s^{\prime\prime}))\vee
t=s^{\prime\prime}.t^{\prime},~{}t^{\prime}\in\mathit{Act}^{+}\\}~{}.$

We now associate with this set of traces the class $\mathcal{S}_{A}$ of
substitutions $\sigma$ as the ones that for at least one trace $s_{p}\in A$ we
have that $\sigma(x)\xRightarrow[\text{}]{s_{p}}\mathit{yes}$ or
$\sigma(x)\xRightarrow[\text{}]{s_{p}}\mathit{no}$. Note that the class of
substitution $\mathcal{S}_{A}$ contains many substitution for each trace
$s_{p}$ and, additionally, since the set $A$ is infinite, $\mathcal{S}_{A}$ is
infinite as well.

Fix now a $s_{p}$ and a substitution $\sigma\in\mathcal{S}_{A}$ such that
$\sigma(x)\xRightarrow[\text{}]{s_{p}}\mathit{yes}$. We have therefore that
$\sigma(m)\xRightarrow{s^{\prime}s_{p}}\mathit{yes}$,
$\sigma(n)\xRightarrow{s^{\prime}s_{p}}\mathit{yes}$ and
$\sigma(m)\xRightarrow[\text{}]{ss_{p}}\mathit{yes}$. By the construction of
$A$, $s^{\prime}s_{p}$ is not a prefix of $ss_{p}$ and therefore it is not
necessary that $\sigma(n)\xRightarrow[\text{}]{ss_{p}}\mathit{yes}$. However,
since $m\simeq n$ is sound we have that $\sigma(n)$ must also be able to
accept $s.s_{p}$. One way this could happen is if both monitors, $m$ and $n$
accept and reject the trace $s_{b}=s.s_{p}$ where $s_{p}\in A$ independently
of a substitution, i.e. $m\xRightarrow[\text{}]{s_{b}}\mathit{yes}$,
$m\xRightarrow[\text{}]{s_{b}}\mathit{no}$,
$n\xRightarrow[\text{}]{s_{b}}\mathit{yes}$ and
$n\xRightarrow[\text{}]{s_{b}}\mathit{no}$. Note that if one monitor can
perform these transitions independently of a substitution then the other one
must do so as well since they are verdict equivalent. If this is the case then
for the traces $s^{\prime},s^{\prime\prime}$ with
$s=s^{\prime}s^{\prime\prime}$ an for all $s_{b}=ss_{p}$ where
$s_{p}\not\in\mathit{pre}(s^{\prime\prime})$ the first bullet of the lemma
holds.

If this is not the case however we have that for a trace $s_{p}$ and a
substitution $\sigma\in\mathcal{S}_{A}$ such that
$\sigma(x)\xRightarrow[\text{}]{s_{p}}\mathit{yes}$ the monitor $n$ must
somehow accept the trace $ss_{p}$ and this is not done because
$n\xRightarrow[\text{}]{s_{b}}\mathit{yes}$.

We remind to the reader here that $s$ is the shortest we could find that
satisfied the proviso of the lemma. Therefore there are no other one-sided
variable occurrences along the trace $s$.

This means that the only way than $n$ could accept $s_{b}$ is another variable
occurrence (not one-sided as $s$ is the shortest trace satisfying the proviso
of the the lemma) happening after some other prefix $s_{0}$ of $s$. I.e.
$n\xrightarrow[\text{}]{s_{0}}x+n_{1}$, $m\xrightarrow[\text{}]{s_{0}}x+m_{1}$
for some monitors $n_{1}$ and $m_{1}$ and trace $s_{0}.s_{p}$ is a prefix of
$s^{\prime}.s^{\prime\prime}.s_{p}=s.s_{p}$. Note here that by Corollary 2 we
know that $s^{\prime}$ is the shortest trace after which the variable $x$
occurs. Therefore our only options for the trace $s_{0}$ would be the trace
$s^{\prime}$ and its extensions which falls in the second case of the lemma as
$s_{0}.s_{p}$ is a prefix of $s.s_{p}$.

This concludes the case analysis for the shortest $s$ leading to a one-sided
variable occurrence of a variable. We continue with a trace $s_{1}$ as the
immediately longer than $s$. For this $s_{1}$ with $|s_{1}|\geq|s|$ we can
generalize the result as follows:

If $s\in\mathit{pre}(s_{1})$ then the trace $s^{\prime}$ we identified with
the case analysis $s$ is also a prefix of $s_{1}$ (i.e.
$s_{1}=s^{\prime}.s_{1}^{\prime\prime}$) and the same transitions we proved
for the traces $s_{b}$ are also enough for the result to hold for the trace
$s_{1}$. Assume now that $s\not\in\mathit{pre}(s_{1})$. Then Corollary 2 still
holds and the one-sided variable occurrence after the trace $s_{1}$ also does
not have any other one-sided variable occurrences between itself and the
prefix guaranteed by the corollary which means we can apply the same analysis.
∎

####  4.2.1 Completeness of verdict equivalence

In this section we will present our axiom system for open monitors over a
finite number of actions. We start by providing an axiom set, which we prove
to be sound and complete for verdict equivalence over $Mon_{F}$. In order to
do so, we first use these axioms to further reduce a normal form of a term.
Then, by utilizing this new reduced normal form we use structural induction to
prove the completeness of our axiom set. The axiom set we provide is infinite.
It is therefore natural to ask whether $\simeq$ is finitely axiomatizable over
$Mon_{F}$. We answer this question negatively by proving that no complete
finite axiom set exists for this algebra. This final part follows a different
type of argument which we will present in Section 5.

When studying open equations over a finite set of actions one would hope that
one of the axiom systems presented already would be complete. However, we can
guarantee that the equations provided in $\mathcal{E}_{v}^{\prime}$ are
definitely unable to prove every sound open equation. To see this consider the
equation used in Example 4 (where $k$ is a constant):

$x+a^{k}.x+\overline{a^{k}}^{(3)}(\mathit{yes}+\mathit{no})\simeq
x+\overline{a^{k}}^{(3)}(\mathit{yes}+\mathit{no})~{}.$

We can clearly see that one of the sides of this equations contains a one-
sided variable occurrence (remember that we are considering terms up to
$A1-A4$). The only axiom which has a similar behavior is $O1$. However for
axiom $O1$ to be applied it must be the case that a variable is occurring
simultaneously with a $\mathit{yes}$ and a $\mathit{no}$ verdict. Since this
does not apply for the equation we are examining it is easy to see that no
proof involving only the axioms of $\mathcal{E}_{v}^{\prime}$ could prove it.

Towards proving this kind of equations and when $\mathit{Act}$ is finite, we
consider the family of axioms

$\mathcal{O}=\\{O2_{s,k}\mid s\in\mathit{Act}^{*},k\geq 0\\}$

where

${(\mathbf{O2_{s,k}})}~{}~{}x+s.x+\overline{s}^{(k)}(\mathit{yes}+\mathit{no})=x+\overline{s}^{(k)}(\mathit{yes}+\mathit{no})~{}.$

We extend our finite axiom set $\mathcal{E}_{v}^{\prime}$ for open terms to
the infinite $\mathcal{E}_{v}^{\prime}\cup\mathcal{O}$, which we will call
$\mathcal{E}_{\textit{v,f}}^{\prime}$. The subscript $f$ in the naming scheme
states that the action set for which the axiom system is complete is finite.
When the action set is a singleton, we will replace it with the subscript $1$.
If the cardinality of the action set is not important, or if it is infinite,
then we use no subscript. Based on the naming scheme we have defined, the name
of the axiom set $\mathcal{E}_{\textit{v,f}}^{\prime}$ denotes that we are
studying verdict equivalence (v), over open terms (′) and for a finite set of
actions (f).

######  Lemma 12.

$\mathcal{E}_{\textit{v,f}}^{\prime}$ is sound. That is, if
$\mathcal{E}_{\textit{v,f}}^{\prime}\vdash m=n$ then $m\simeq n$, for all
$m,n\in$$Mon_{F}$.

###### Proof.

We have to prove soundness only for the new family of equations $\mathcal{O}$
as the other equations are sound by Theorem 1.

First of all, note that
$\sigma(x+s.x+\overline{s}^{(k)}(\mathit{yes}+\mathit{no}))$ accepts every
trace accepted by $\sigma(x+\overline{s}^{(k)}(\mathit{yes}+\mathit{no}))$,
and rejects every trace rejected by
$\sigma(x+\overline{s}^{(k)}(\mathit{yes}+\mathit{no}))$. We are therefore
left to show that

  * •

if $\sigma(s.x)$ accepts some trace then so does
$\sigma(x+\overline{s}^{(k)}(\mathit{yes}+\mathit{no}))$, and

  * •

if $\sigma(s.x)$ rejects some trace then so does
$\sigma(x+\overline{s}^{(k)}(\mathit{yes}+\mathit{no}))$.

We only detail the proof for the latter claim, as that of the former one is
similar. To this end, assume that $\sigma(s.x)$ rejects some trace
$s^{\prime}$. Then $s^{\prime}=ss^{\prime\prime}$ for some $s^{\prime\prime}$
that is rejected by $\sigma(s.x)$. If $s^{\prime\prime}$ is a prefix of
$s^{k}$, then it is not hard to see that $\sigma(x)$ rejects $s^{\prime}$ too,
and thus so does $\sigma(x+\overline{s}^{(k)}(\mathit{yes}+\mathit{no}))$. On
the other hand, if $s^{\prime\prime}$ is not a prefix of $s^{k}$, then
$s^{\prime}=ss^{\prime\prime}$ is not a prefix of $s^{k}$ either. Therefore,
$\sigma(\overline{s}^{(k)}(\mathit{yes}+\mathit{no}))$ rejects $s^{\prime}$.
It follows that $\sigma(x+\overline{s}^{(k)}(\mathit{yes}+\mathit{no}))$
rejects $s^{\prime}$, and we are done. ∎

We provide here some examples of how to use the above to derive some simpler
and more intuitive sound equations.

######  Lemma 13.

The following equations are derivable from $\mathcal{O}$ for each
$s,s_{1}\in\mathit{Act}^{*}$:

  1. 1.

$x+s.x+s.\overline{s_{0}}(\mathit{yes}+\mathit{no})=x+s.\overline{s_{0}}(\mathit{yes}+\mathit{no})$,
with $s_{0}$ a prefix of $s$,

  2. 2.

$\mathit{yes}+x+s_{1}.\overline{s_{2}}(\mathit{no})=\mathit{yes}+x+s_{1}.\overline{s_{2}}(\mathit{no})+s_{1}.x$,
where $s_{2}$ is any prefix of $s_{1}$,

  3. 3.

$\mathit{no}+x+s_{1}.\overline{s_{2}}(\mathit{yes})=\mathit{no}+x+s_{1}.\overline{s_{2}}(\mathit{yes})+s_{1}.x$,
where $s_{2}$ is any prefix of $s_{1}$,

  4. 4.

$x+s.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{no}+\mathit{yes})=x+s.(x+\sum_{a\in\mathit{Act}}a.(\mathit{no}+\mathit{yes}))$.

###### Proof.

We first show how to derive the first equation and then we derive the rest
from it. We start by picking the equation $O2_{s,1}$ i.e.

$x+s.x+s.\overline{s}^{\leq}(\mathit{yes}+\mathit{no})+s.s.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})=$
$x+s.\overline{s}^{\leq}(\mathit{yes}+\mathit{no})+s.s.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})~{}.$

In addition we have the tautology

$s.s_{0}.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})=s.s_{0}.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})~{},$

for the specific prefix $s_{0}$ of $s$. On the two valid above equations we
apply the congruence rule for $+$ and have:

$x+s.x+s.\overline{s}^{\leq}(\mathit{yes}+\mathit{no})+s.s.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})+s.s_{0}.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})$
$=x+s.\overline{s}^{\leq}(\mathit{yes}+\mathit{no})+s.s.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})+s.s_{0}.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})~{}.$

The first simplification that we perform now is by observing that the summand
$s.s_{0}.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})$
accepts and rejects a prefix of the whole summand
$s.s.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})$ and
therefore we can eliminate the latter from the summation:

$x+s.x+s.\overline{s}^{\leq}(\mathit{yes}+\mathit{no})+s.s_{0}.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})$
$=x+s.\overline{s}^{\leq}(\mathit{yes}+\mathit{no})+s.s_{0}.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})~{}.$

In addition the term $s.\overline{s}^{\leq}$ can be rewritten as
$s.\overline{s_{0}}^{\leq}(\mathit{yes}+\mathit{no})+s.s_{0}.\overline{s_{1}}(\mathit{yes}+\mathit{no})$
with $s=s_{0}.s_{1}$. To see this, consider that the traces up to length $|s|$
that do not cause a rejection of the trace $s$ are the ones that do not cause
a rejection of its prefix $s_{0}$ and the ones that start with $s_{0}$ but do
not cause the rejection of its continuation $s_{1}$. Thus we have:

$x+s.x+s.\overline{s_{0}}^{\leq}(\mathit{yes}+\mathit{no})+s.s_{0}.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})+s.s_{0}.\overline{s_{1}}(\mathit{yes}+\mathit{no})$
$=x+s.\overline{s_{0}}^{\leq}(\mathit{yes}+\mathit{no})+s.s_{0}.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})+s.s_{0}.\overline{s_{1}}(\mathit{yes}+\mathit{no})~{}.$

Now we have again that the summand
$s.s_{0}.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})$
accepts and rejects a prefix of the whole summand
$s.s_{0}.\overline{s_{1}}(\mathit{yes}+\mathit{no})$ and therefore we can omit
the latter. This gives us the equation:

$x+s.x+s.\overline{s_{0}}^{\leq}(\mathit{yes}+\mathit{no})+s.s_{0}.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})=$
$x+s.\overline{s_{0}}^{\leq}(\mathit{yes}+\mathit{no})+s.s_{0}.\displaystyle\sum_{a\in\mathit{Act}}a.(\mathit{yes}+\mathit{no})~{},$

which can be rewritten using our notation as

$x+s.x+s.\overline{s_{0}}(\mathit{yes}+\mathit{no})=x+s.\overline{s_{0}}(\mathit{yes}+\mathit{no})~{},$

giving us the target equation.

Having presented the proof for the first family of equations in detail we give
a short description for the rest. For the equations $(2)$ and $(3)$ it
suffices to use the congruence rule for $+$ with the equations
$\mathit{yes}=\mathit{yes}$ and $\mathit{no}=\mathit{no}$ respectively and
then simplify the equations by using the distribution axiom for $+$. For the
latter equation $(4)$ it is enough to instantiate the prefix $s_{0}$ in the
the family of equations $(1)$ as the empty string $\varepsilon$. This is, of
course, allowed since the empty string is a prefix of any string. ∎

Now that we have discussed the family of axioms $\mathcal{O}$, we proceed to
use them in defining a notion of reduced normal form that is suitable for
monitors over a finite action set.

######  Definition 9.

A finite-action-set reduced normal form is a term

$m=\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in
I}x_{i}~{}[+\mathit{yes}]~{}[+\mathit{no}]$

where each $m_{a}$ is different from $\mathit{end}$ and if
$v\in\\{\mathit{yes},\mathit{no}\\}$ is a summand of m then each $m_{a}$ is
$v$-free, and in reduced normal form. If both $\mathit{yes}$ and $\mathit{no}$
are summands of $m$ then $m$ is equal to $\mathit{yes}+\mathit{no}$. In
addition for every trace $s$, if there exists a $k$ such that for all the
traces $s_{0}$

$\overline{s}^{(k)}(\mathit{yes}+\mathit{no})\xrightarrow[\text{}]{s_{0}}\mathit{yes}+\mathit{no},~{}\text{implies:}~{}m\xRightarrow[\text{}]{s_{0}}\mathit{yes}~{}\text{and}~{}m\xRightarrow[\text{}]{s_{0}}\mathit{no}$

then $m\not\xrightarrow[\text{}]{s}x_{i}+m^{\prime}$ for all $i\in I$ and
$m^{\prime}$.

In order to use the above form of the monitors in $Mon_{F}$ we need to prove
that any term can be rewritten in a reduced normal form using the axioms in
$\mathcal{E}_{\textit{v,f}}^{\prime}$. Before doing so we will prove the
following useful lemma, which only uses axioms form $\mathcal{E}_{v}$.

######  Lemma 14.

For a monitor $m\in$ $Mon_{F}$:

  * •

if $m\xRightarrow[\text{}]{s}\mathit{yes}$ then $\mathcal{E}_{v}\vdash
m=m+s.\mathit{yes}$ and

  * •

if $m\xRightarrow[\text{}]{s}\mathit{no}$ then $\mathcal{E}_{v}\vdash
m=m+s.\mathit{no}$.

###### Proof.

We prove both statements by induction on the length of the trace $s$ and limit
ourselves to presenting the proof for the first one.

  * •

If $s$ is the empty trace, then $m$ accepts the empty trace. Therefore it must
contain a $\mathit{yes}$ syntactic summand and we are done.

  * •

Assume now that $s=a.s^{\prime}$. Then
$m\xrightarrow[]{a}m_{a}\xrightarrow[]{s^{\prime}}\mathit{yes}$ for some
$m_{a}$. By induction $\mathcal{E}_{\textit{v,f}}^{\prime}\vdash
m_{a}=m_{a}+s^{\prime}.\mathit{yes}$.

Now,

$\displaystyle\mathcal{E}_{\textit{v,f}}^{\prime}\vdash m$
$\displaystyle=m+a.m_{a}=m+a.(m_{a}+s^{\prime}.\mathit{yes})=m+a.m_{a}+a.s^{\prime}.\mathit{yes}$
$\displaystyle=m+a.s^{\prime}.\mathit{yes}$ ∎

We will also need a similar result, this time involving syntactic summands
that contain occurrences of variables.

######  Lemma 15.

For a monitor $m\in$ $Mon_{F}$, where $m$ is in normal form for open terms, if
$m\xrightarrow[\text{}]{s}x+m_{s}$ then $\mathcal{E}_{v}\vdash
m=m^{\prime}+s.x$ where
$m^{\prime}\not\xrightarrow[\text{}]{s}x+m^{\prime\prime}$ for every
$m^{\prime\prime}$.

###### Proof.

We prove the claim by induction on the length of the trace $s$.

  * •

If $s$ is the empty trace then $m\xrightarrow[\text{}]{\varepsilon}x+m_{s}=m$.
This means that $x$ is a summand of $m$. Since $m$ is in normal form, $m_{s}$
does not have $x$ as a summand and we are done.

  * •

Assume now that $s=a.s^{\prime}$. Since m is in normal form and
$m\xrightarrow[]{a.s^{\prime}}s+m^{\prime}$, we have that
$m=m^{\prime}+a.m_{a}$ for some $m^{\prime}\not\xrightarrow[]{a}$ and $m_{a}$
in formal form such that $m_{a}\xrightarrow[]{s^{\prime}}x+m^{\prime}$. By the
induction hypothesis, $\mathcal{E}_{v}\vdash
m_{a}=m_{a}^{\prime}+s^{\prime}.x$ where
$m_{a}^{\prime}\not\xrightarrow[]{s^{\prime}}x+m_{s^{\prime}}^{\prime}$ for
every $m_{s^{\prime}}^{\prime}$.

Therefore we have:

$m=m^{\prime}+a.m_{a}=m+a.(m_{a}^{\prime}+s^{\prime}.x)=m^{\prime}+a.m_{a}^{\prime}+a.s^{\prime}.x~{},~{}~{}$

and since
$m_{a}^{\prime}\not\xrightarrow[]{s^{\prime}}x+m_{s^{\prime}}^{\prime}$ for
every $m_{s^{\prime}}^{\prime}$ and $m^{\prime}\not\xrightarrow[]{a}$ we have
that $m=s.x+m_{rest}$ with $m_{rest}\not\xrightarrow[]{s}x+m^{\prime\prime}$
for every $m^{\prime\prime}$ and we are done. ∎

######  Lemma 16.

Each open monitor $m\in$ $Mon_{F}$, is provably equal to a reduced normal form
using $\mathcal{E}_{\textit{v,f}}^{\prime}$.

###### Proof.

From Lemma 8 we can start from a monitor $m$ already in open normal form, as
given in Definition 6. Therefore we have the following cases:

  * •

$m=\mathit{yes}+\mathit{no}$.

  * •

$m=\mathit{yes}+\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in I}x_{i}$, where
each $m_{a}$ is $\mathit{yes}$-free.

  * •

$m=\mathit{no}+\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in I}x_{i}$, where
each $m_{a}$ is $\mathit{no}$-free.

  * •

$m=\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in I}x_{i}$.

We begin our analysis from the second case. A similar analysis can be applied
to the third one and the fourth one follows by a simpler version of the same
inductive argument. We have therefore a monitor
$m=\mathit{yes}+\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in I}x_{i}$. The
extra claim for these reduced normal forms is that if for some trace $s$, and
a $k_{0}$, for all traces $s_{0}$,

$\overline{s}^{(k_{0})}(\mathit{yes}+\mathit{no})\xrightarrow[\text{}]{s_{0}}\mathit{yes}+\mathit{no},~{}\text{implies:}~{}m\xRightarrow[\text{}]{s_{0}}\mathit{yes}~{}\text{and}~{}m\xRightarrow[\text{}]{s_{0}}\mathit{no}$

then $m\not\xrightarrow[\text{}]{s}x_{i}+m_{x}$ for all $i\in I$ and $m_{x}$.
In order to prove this extra constraint we assume the premise is true. We will
show that we can reduce $m$ to $m_{red}$ with $\mathcal{E}_{fin}\vdash
m=m_{red}$ and $m_{red}\not\xrightarrow[\text{}]{s}x_{i}+m_{x}$ for every
$i\in I$ and every $m_{x}$.

Since $m$ accepts and rejects all the traces that
$\overline{s}^{(k_{0})}(\mathit{yes}+\mathit{no})$ accepts and rejects, we
have that $m\simeq m+m^{\prime}$ and that
$m^{\prime}\xrightarrow[\text{}]{s_{0}}\mathit{yes}+\mathit{no}$ for all of
the traces $s_{0}$ that
$\overline{s}^{(k_{0})}(\mathit{yes}+\mathit{no})\xrightarrow[\text{}]{s_{0}}\mathit{yes}+\mathit{no}$.
We call this set of traces $\mathcal{S}$ which is finite since $k_{0}$ is
fixed. Therefore by Lemma 14 we have that
$\mathcal{E}_{\textit{v,f}}^{\prime}\vdash
m=m+\displaystyle\sum_{s_{0}\in\mathcal{S}}s_{0}.(\mathit{yes}+\mathit{no})$.
Since the term
$\displaystyle\sum_{s_{0}\in\mathcal{S}}s_{0}.(\mathit{yes}+\mathit{no})$ is
verdict equivalent to $\overline{s}^{(k_{0})}(\mathit{yes}+\mathit{no})$ and
both terms are closed, we have that by Theorem 2,
$\mathcal{E}_{v}\vdash\displaystyle\sum_{s_{0}\in\mathcal{S}}s_{0}.(\mathit{yes}+\mathit{no})=\overline{s}^{(k_{0})}(\mathit{yes}+\mathit{no})$.
Therefore $\mathcal{E}_{\textit{v,f}}^{\prime}\vdash
m=m+\overline{s}^{(k_{0})}(\mathit{yes}+\mathit{no})$, which means

$\mathcal{E}_{\textit{v,f}}^{\prime}\vdash
m=\mathit{yes}+\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in
I}x_{i}+\overline{s}^{(k_{0})}(\mathit{yes}+\mathit{no}).$

For the same monitor $m$ we now want to argue that if
$m\xrightarrow[\text{}]{s}x_{i}$ for one of the variables in $\\{x_{i}\mid
i\in I\\}$ then we can eliminate this occurrence.

Since $m$ is in reduced normal form we have by Lemma 15 that
$m=m^{\prime}+s.x_{i}$ where $m^{\prime}\not\xrightarrow[]{s}x_{i}$.
Additionally we have shown that
$m=m+\overline{s}^{(k_{0})}(\mathit{yes}+\mathit{no})$ which implies
$m=m^{\prime}+s.x_{i}+\overline{s}^{(k_{0})}(\mathit{yes}+\mathit{no})$ with
$m^{\prime}\not\xrightarrow[\text{}]{s}x_{i}$. Since $x_{i}$ is one of the
variables that appear as summands of $m$ we can successfully apply the axiom
$O2_{s,k_{0}}$ for each variable and we have the that indeed $m$ reduces to a
monitor $m_{red}$ such that
$m_{red}\not\xrightarrow[\text{}]{s}x_{i}+m_{x_{i}}$ for every $i\in I$ and
every $m_{x_{i}}$. ∎

######  Lemma 17.

If monitor $m\in$ $Mon_{F}$, with $|\mathit{Act}|\geq 2$ is in reduced normal
form and contains an $x$ summand and $m\xrightarrow[\text{}]{s}x+m^{\prime}$
for some $m^{\prime}$ then there is at least one trace $s_{bad}$ such that for
every $k$,

$\overline{s}^{(k)}(\mathit{yes}+\mathit{no})\xRightarrow[\text{}]{s_{bad}}\mathit{yes}~{}\text{and}~{}\overline{s}^{(k)}(\mathit{yes}+\mathit{no})\xRightarrow[\text{}]{s_{bad}}\mathit{no}$

but

$m\not\xRightarrow[\text{}]{s_{bad}}\mathit{yes}~{}\text{or}~{}m\not\xRightarrow[\text{}]{s_{bad}}\mathit{no}.$

###### Proof.

We can easily show that for each $k$ there exists an $s_{k}$ such that
$\overline{s}^{(k)}(\mathit{yes}+\mathit{no})\xrightarrow[\text{}]{s_{k}}\mathit{yes}+\mathit{no}$
but $m\not\xRightarrow[\text{}]{s_{k}}\mathit{yes}$ or
$m\not\xRightarrow[\text{}]{s_{k}}\mathit{no}$. This follows since if this
were not the case then for some $k_{0}$, no such trace $s_{k_{0}}$ exists.
Thus the monitor would contain a summand
$m^{\prime}\simeq\overline{s}^{(k_{0})}(\mathit{yes}+\mathit{no})$ for this
$k_{0}$ and still it would be able to perform the transition
$m\xrightarrow[\text{}]{s}x+m^{\prime}$ which contradicts the assumption that
$m$ is in reduced normal form.

We will now show that one trace $s_{bad}$ suffices for all $k$. To that end,
consider the term $\overline{s}^{(1)}(\mathit{yes}+\mathit{no})$. If there is
an $s_{1}$, which is not a prefix of $ss$ and
$m\not\xRightarrow[\text{}]{s_{1}}\mathit{yes}$ or
$m\not\xRightarrow[\text{}]{s_{1}}\mathit{no}$ then for $s_{bad}=s_{1}$ we
have that for all $k$,
$\overline{s}^{(k)}(\mathit{yes}+\mathit{no})\xRightarrow[\text{}]{s_{bad}}\mathit{yes}~{}\text{and}~{}\overline{s}^{(k)}(\mathit{yes}+\mathit{no})\xRightarrow[\text{}]{s_{bad}}\mathit{no}$
and we are done. If this is not the case and since the trace $s_{1}$ is
guaranteed to exist (by the previous paragraph) then it must be an extension
of $ss$. Again if $s_{1}$ is not prefix of $sss$ then again for
$s_{bad}=s_{1}$ we have the necessary conclusion.

Otherwise $m\not\xRightarrow[\text{}]{s_{1}}\mathit{yes}$ or
$m\not\xRightarrow[\text{}]{s_{1}}\mathit{no}$ for the trace $s_{1}=ssa$,
where $a$ is the first action of $s$. Therefore by the definition of
$\overline{s}^{(k)}(\mathit{yes}+\mathit{no})$ we have that for all $s_{b}$
such that
$\overline{s}^{(k)}(\mathit{yes}+\mathit{no})\xrightarrow[\text{}]{s_{b}}\mathit{yes}+\mathit{no}$
and $k>1$ we have that $m\not\xRightarrow[\text{}]{s_{b}}\mathit{yes}$ or
$m\not\xRightarrow[\text{}]{s_{b}}\mathit{no}$. This allows us to look for an
$s_{bad}$ which will also cover the case $k=1$ in larger terms.

We then apply the same reasoning for $k=2,\ldots$ up to a certain $k_{b}$. If
at any point in the process we encounter a trace $s_{i}$ which fulfills our
premise then we can stop. We are just left to show that this process will
eventually terminate.

This can be shown as follows. Recall that every monitor $m$ has a finite depth
$0pt(m)$ (see Def. 2). We now take a $k_{b}$ large enough so that
$s^{k_{b}}>0pt(m)$. If the iterative procedure described above reaches this
$k_{b}$ we have that $m\not\xRightarrow[\text{}]{s_{bad}}\mathit{yes}$ or
$m\not\xRightarrow[\text{}]{s_{bad}}\mathit{no}$ for the trace $s^{k_{b}+1}a$
where $a$ is the first action of $s$. However since the depth of the monitor
$m$ is smaller that the length of this trace we also have that the monitor
cannot accept or reject any of its extensions.

Therefore for the extension $s_{bad}=s^{k_{b}+1}ac$ where $c$ is not the
second action of $s$ we have that for all $k>k_{b}$,
$\overline{s}^{(k)}(\mathit{yes}+\mathit{no})\xRightarrow[\text{}]{s_{bad}}\mathit{yes}~{}\text{and}~{}\overline{s}^{(k)}(\mathit{yes}+\mathit{no})\xRightarrow[\text{}]{s_{bad}}\mathit{no}$
while $m\\\ not\xRightarrow[\text{}]{s_{bad}}\mathit{yes}$ or
$m\not\xRightarrow[\text{}]{s_{bad}}\mathit{no}$. Additionally since the
iterative procedure we described above reached this $k_{b}$ we have that for
all $i\leq j\leq k_{b}$, it is true that
$\overline{s}^{(k)}(\mathit{yes}+\mathit{no})\xRightarrow[\text{}]{s_{j}}\mathit{yes}~{}\text{and}~{}\overline{s}^{(k)}(\mathit{yes}+\mathit{no})\xRightarrow[\text{}]{s_{j}}\mathit{no}$,
which concludes the proof. ∎

The two lemmata above play a key role in the completeness proof we will
present now.

We distinguish two cases separately, namely when $|\mathit{Act}|\geq 2$ and
when $\mathit{Act}$ is a singleton. This is necessary because equations such
as $x=x+a.x$ are only sound when $\mathit{Act}=\\{a\\}$. For the proof when
$|\mathit{Act}|\geq 2$ it is necessary to utilize at least two actions
$a,b\in\mathit{Act}$, which is the reason why when only one action is
available new cases arise.

##### Action set with at least two actions

We have already shown the soundness of the axiom system
$\mathcal{E}_{\textit{v,f}}^{\prime}$. We now proceed to show completeness.

For each such completeness theorem we follow a similar general strategy in
order to prove that two arbitrary verdict equivalent monitors have identical
reduced normal forms. To that end, we prove that they have identical variables
as summands, that the sets of initial actions that each one can perform are
equal and that after a common action they reach monitors that are also verdict
equivalent. Unfortunately, for a finite set of actions, we were not able to
define a substitution that would cover all the three above-mentioned steps
like we did when the set of actions was infinite. We therefore adopted a proof
strategy that focuses on each part of the proof separately.

######  Theorem 5.

$\mathcal{E}_{\textit{v,f}}^{\prime}$ is complete for open terms for finite
Act with $|\mathit{Act}|\geq 2$. That is, if $m\simeq n$ then
$\mathcal{E}_{\textit{v,f}}^{\prime}\vdash m=n$.

###### Proof.

By Lemma 16 we may assume that $m$ and $m$ are in reduced normal form. We
prove the claim by induction on the sum of the sizes of $m$ and $n$, and
proceed with a case analysis on the form $m$ may have.

In the case where $m$ contains both a $\mathit{yes}$ and a $\mathit{no}$
summand then both $m$ and $n$ must be equal to $\mathit{yes}+\mathit{no}$ as
they are in reduced normal form.

Assume now that

$m=\mathit{yes}+\displaystyle\sum_{a\in A}a.m_{a}+\sum_{i\in I}x_{i}~{},$

where $\\{x_{i}\mid i\in I\\}$ is the set of variables occurring as summands
of $m$ and each $m_{a}$ is $\mathit{yes}$-free and different from
$\mathit{end}$ (as a reduced normal form). Since $\sigma(m)$ accepts
$\varepsilon$ for each $\sigma$ and $m\simeq n$, monitor $n$ is bound to have
a similar form since it must contain the verdict $\mathit{yes}$ as a summand
(but not a $\mathit{no}$ one). Therefore:

$n=\mathit{yes}+\displaystyle\sum_{b\in B}b.n_{b}+\sum_{j\in J}y_{j}$

and we need to show that there is a way to apply our axioms to show that
monitor $n$ is provably equal to $m$.

We start by proving that $\\{x_{i}\mid i\in I\\}=\\{y_{j}\mid j\in J\\}$. By
symmetry, it suffices to show that $\\{x_{i}\mid i\in
I\\}\subseteq\\{y_{j}\mid j\in J\\}$. To this end, assume $x\in\\{x_{i}\mid
i\in I\\}$. Consider the substitution $\sigma$ mapping $x$ to $\mathit{no}$
and every other variable to $\mathit{end}$, i.e:

$\sigma(y)=\begin{cases}\mathit{no},&\textit{if}~{}y=x\\\
\mathit{end},&\textit{otherwise}.\end{cases}$

Then, $\sigma(m)$ rejects the empty trace $\varepsilon$. Since
$\sigma(m)\simeq\sigma(n)$, we have that $\sigma(n)$ must also reject
$\varepsilon$. By the form of $n$ and the definition of $\sigma$, this is only
possible if $n$ has $x$ as a summand, and we are done. Therefore the set of
variables of $m$ is a subset of the variables of $n$.

Next, we prove that the action sets $A,B$ are identical. Assume that $a\in A$.
Since $\mathit{Act}$ contains at least two actions, there is some action
$b\neq a$. Consider the substitution $\sigma_{1}$ defined by
$\sigma_{1}(x)=b.\mathit{no}$ for each $x\in\mathit{Var}$. Since $a\in A$ and
$m_{a}$ is $\mathit{yes}$-free and different from $\mathit{end}$, it is easy
to see that there exists an $s\in\mathit{Act}^{*}$ such that $as\in
L_{r}(\sigma_{1}(m))$. Since $m\simeq n$ we have that
$\sigma_{1}(m)\simeq\sigma_{1}(n)$ and therefore $\sigma_{1}(n)$ must also
reject $as$. By the form of $n$ and the definition of $\sigma$, this is only
possible if $n\xrightarrow[]{a}n_{a}$ for some $n_{a}$ and therefore $a\in B$.
Hence, $A\subseteq B$ and the claim follows by symmetry.

For the final part of the proof we must show that $m_{a}\simeq n_{a}$ for each
$a\in A$, which is enough to complete the proof, by the induction hypothesis.
Towards a contradiction we will assume that the two monitors $m_{a},n_{a}$ are
not verdict equivalent. Therefore there exists a substitution $\sigma_{0}$
that separates them, that is without loss of generality, there is a trace
$s_{0}$ such that $s_{0}\in L_{r}(\sigma_{0}(m_{a})),s_{0}\not\in
L_{r}(\sigma_{0}(n_{a}))$ or there is some $s_{0}\in
L_{a}(\sigma_{0}(m_{a})),s_{0}\not\in L_{a}(\sigma_{0}(n_{a}))$ .

We will analyze first the case of rejection of the string $s_{0}$. The
substitution $\sigma_{0}$ must be a closed one for $m_{a},n_{a}$ i.e. it must
map to a closed monitor all variables in $(Var(m_{a})\cup Var(n_{a}))$. We
will use this substitution to create a new one $\sigma_{bad}$ that would also
separate the original monitors $m,n$.

The first step towards this is:

$\sigma_{bad}(x)=\begin{cases}\mathit{end},~{}\text{if}~{}x\in
Var(m)\setminus(Var(m_{a})\cup Var(n_{a})),\\\ \sigma_{0}(x),~{}otherwise.\\\
\end{cases}$

Now since $s_{0}\in L_{r}(\sigma_{0}(m_{a}))$ and
$\sigma_{bad}(m_{a})=\sigma_{0}(m_{a})$ we also know that $a.s_{0}\in
L_{r}(\sigma_{bad}(a.m_{a}))$. Our aim is to show that $a.s_{0}\not\in
L_{r}(\sigma_{bad}(n))$. Following the definition
$\sigma_{bad}(n_{a})=\sigma_{0}(n_{a})$ and therefore $s_{0}\not\in
L_{r}(\sigma_{bad}(n_{a}))$.

Hence, the only way for $\sigma_{bad}(n)$ to reject $a.s_{0}$, like
$\sigma_{bad}(m)$ does, is if it was rejected by the mapping of one the
variables contained in the set $\\{x_{i}\mid i\in I\\}$.

It is useful to make here apparent that in order for $\sigma_{bad}(n)$ to
reject $a.s_{0}$, it must do so completely independently of the summand
$\sigma_{bad}(a.n_{a})$, since the latter cannot reject any of the prefixes of
$a.s_{0}$ as well. Even in the case where $s_{0}$ starts with $a$, and
$\sigma_{0}(n_{a})$ rejects some $a.s_{1}.s_{2}.\ldots s_{n-i}$ it would still
be impossible for $\sigma_{0}(n_{0})$ to reject $a.s_{0}$ since the assumption
that $a.s_{0}=a.a.s_{1}.s_{2}.\ldots s_{n-1}$ would automatically imply that
$\sigma_{0}(n_{a})$ rejects some prefix of $s_{0}$ which is a contradiction.

$\sigma_{bad}(m)$$\mathit{no}$$s^{\prime\prime}$$\sigma_{bad}(m_{a})$$\sigma_{bad}(m_{s}+x)$$\mathit{no}$$s^{\prime\prime}$$s^{\prime}$$a$
Figure 1: Transitions the monitor $\sigma_{bad}(m)$ can perform

By the definition of $\sigma_{bad}$, the variables that did not appear at all
in $n_{a}$ or $m_{a}$ were mapped to $\mathit{end}$ and therefore cannot
reject any string. Therefore the only way for $n$ to reject $a.s_{0}$ is for
one of the variables appearing in $Var(n_{a})\cup Var(m_{a})$ to have been
mapped to a closed term that can reject $a.s_{0}$. (Note that this does not
contradict the fact that $\sigma_{bad}(n_{a})$ does not reject $s_{0}$).
Therefore there is at least one $x_{0}\in Var(m_{a})\cup Var(n_{a})$ and
$x_{0}\in\\{x_{i}\mid i\in I\\}$ such that $as_{0}\in
L_{r}(\sigma_{bad}(x_{0}))$.

This leads to the case were $m,n$ reject a prefix of $as_{0}$ because of the
mapping of $x_{0}$. However this implies that we have the following situation:

$m=\mathit{yes}+x_{0}+a.m_{a}+\displaystyle\sum_{b\in
A\setminus\\{a\\}}b.m_{b}+\sum_{i\in I\setminus\\{0\\}}x_{i}\simeq$

$\mathit{yes}+x_{0}+a.n_{a}+\displaystyle\sum_{b\in
A\setminus\\{a\\}}b.n_{b}+\sum_{i\in I\setminus\\{0\\}}x_{i}=n$

and that the monitor $m_{a}$ can perform the transitions:
$m_{a}\xrightarrow[\text{}]{s^{\prime}}m_{a}^{\prime}+x_{0}$ and the monitor
$\sigma_{0}(x_{0})=\sigma_{bad}(x_{0})$ respectively can perform the
transitions:
$\sigma_{bad}(x_{0})\xrightarrow[\text{}]{s^{\prime\prime}}\mathit{no}~{},$
where $s^{\prime}$ is a prefix of $s_{0}$ (i.e.
$s_{0}=s^{\prime}.s^{\prime\prime}$) and in addition
$n_{a}\not\xrightarrow[]{s^{\prime}}x+n^{\prime}$ for any $n^{\prime}$. This
means respectively that $m\xrightarrow[]{as^{\prime}}m_{a}^{\prime}+x_{0}$ and
$\sigma_{bad}(m_{a}^{\prime}+x_{0})\xrightarrow[\text{}]{s^{\prime\prime}}\mathit{no}~{}.$

By Lemma 17 we have that there exists at least one trace $s_{b}$ such that
$m\not\xRightarrow[\text{}]{s_{b}}\mathit{yes}$ or
$m\not\xRightarrow[\text{}]{s_{b}}\mathit{no}$ but $s_{b}\in
L_{r}(\overline{as^{\prime}}^{(k)}(\mathit{yes}+\mathit{no}))$ for all $k\geq
0$. Since $m$ contains a $\mathit{yes}$ summand we have that it must be the
case that $m\not\xRightarrow[\text{}]{s_{b}}\mathit{no}$. We now, further
modify $\sigma_{bad}$ to map the variable $x_{0}$ to $s_{b}.\mathit{no}$ and
any other variable $y\neq x_{0}$ to $\mathit{end}$. We have then that $s_{b}$
and $as^{\prime}.s_{b}\in L_{r}(\sigma_{bad}(m))$. In addition $s_{b}\in
L_{r}(\sigma_{bad}(n))$. However the traces that are rejected by the term
$\overline{as^{\prime}}^{(k)}$, by definition, are exactly the traces such
that their rejection does not cause a rejection of the $as^{\prime}$ trace.
This means that under the modified substitution $\sigma_{bad}$, monitor $n$
_cannot_ reject the trace $as^{\prime}.s_{b}$. This deems the monitors $m,n$
not verdict equivalent, which contradicts our assumption. We conclude then
that the rejection set of $m_{a}$ is equal to the rejection set of $n_{a}$ for
each $a\in A$.

It remains to show that $m_{a}$ and $n_{a}$ also have identical acceptance
sets. Towards a contradiction, assume they do not and take a trace $s$ that
under some substitution $\sigma_{0}$ separates them, i.e. $s\in
L_{a}(\sigma_{0}(m_{a}))$ and $s\not\in L_{a}(\sigma_{0}(n_{a}))$. In
addition, assume that $s$ is of minimum length, meaning that no prefix of $s$
(under any substitution) has the property of separating the acceptance sets of
$m_{a}$ and $n_{a}$. This fact in addition to $m_{a}$ and $n_{a}$ being
$\mathit{yes}$-free (as a result of $m$ and $n$ being in reduced normal form)
means that the acceptance of $s$ by $m_{a}$ is the result of a variable $x$
occurring in $m_{a}$ as $m_{a}\xrightarrow[\text{}]{s}x+m^{\prime}$ for some
$m^{\prime}$. Since however the assumption is that $s\not\in
L_{a}(\sigma_{0}(n_{a}))$ we have that
$n_{a}\not\xrightarrow[\text{}]{s}x+n^{\prime}$ for any $n^{\prime}$. We know
that this is exactly the case since if the variable $x$ occurred earlier in
$m_{a}$ then by mapping it to $\mathit{yes}$ we would have a shorter trace
being accepted by $\sigma_{0}(m_{a})$ but not $\sigma_{0}(n_{a})$.

We are sure now that monitor $\sigma_{0}(n_{a})$ cannot perform the transition
$\sigma_{0}(n_{a})\xRightarrow[\text{}]{~{}s~{}}\mathit{yes}$, which means
that not only it does not arrive at the variable $x$ after reading the trace
$s$, but also does not arrive to the $\mathit{yes}$ verdict for any of its
prefixes (say $s^{\prime}$) as that would imply that it can reach the
$\mathit{yes}$ verdict for $s$ as well.

Finally, by $n$ being in reduced normal form, and by $m_{a}$ not arriving at a
$\mathit{no}$ verdict for any of the prefixes $s^{\prime}$ of $s$ (as this
would mean that if becomes a $\mathit{no}$ and therefore cannot perform the
transitions $m_{a}\xrightarrow[\text{}]{~{}s~{}}x$ ) we know that $n_{a}$ does
not arrive to the $\mathit{no}$ verdict after reading the trace $s$ or any of
its prefixes either.

Given all of the above we can now construct the substitution $\sigma_{bad}$
that would separate the rejection sets of $n_{a},m_{a}$ which is enough to
prove the contradiction as the case where such a substitution exists and
separates the rejection sets of the two sub-monitors has already been covered.
The situation we have at hand is as follows:

Monitor $\sigma_{0}(m_{a})$ can arrive to the verdict $\mathit{yes}$ after
reading the trace $s$ while $\sigma_{0}(n_{a})$ cannot and also neither
$n_{a}$ nor $m_{a}$ can produce a $\mathit{no}$ verdict for the trace $s$.
Therefore if we switch the mapping of $x$ to $\mathit{no}$ in
$\sigma^{\prime}$ and the verdicts of all other variables that where mapped to
a $\mathit{no}$ verdict to $\mathit{end}$ we have produced a substitution that
causes $s$ to be rejected by $\sigma^{\prime}(m_{a})$ but not from
$\sigma^{\prime}(n_{a})$. By utilizing our previous construction there exists
another one that separates the monitors $n,m$ as well which is a
contradiction.

We have concluded then that the $L_{a}(m_{a})=L_{a}(n_{a})$ and
$L_{r}(m_{a})=L_{r}(n_{a})$ which means that they are verdict equivalent.
Therefore we can apply the inductive hypothesis and have that
$\mathcal{E}_{\textit{v,f}}^{\prime}\vdash m_{a}=n_{a}$. Using now congruence
rules we have that $\mathcal{E}_{\textit{v,f}}^{\prime}\vdash m=n$. All other
possible forms of monitors $m,n$ are sub-cases that the relative analysis can
be applied symmetrically and therefore they are omitted. ∎

##### Singleton Action Set

We proceed now with the analysis of the completeness result when
$\mathit{Act}=\\{a\\}$.

As we mentioned earlier, when $a$ is the only action, the equation

$(V_{1})\quad x=x+a.x$

is sound, but cannot be proved from the equations in
$\mathcal{E}_{\textit{v,f}}^{\prime}$ over $\\{a\\}$. Indeed, unlike $V_{1}$,
all the equations in $E_{v}$ are sound regardless of the cardinality of the
action set and those in the family $\mathcal{O}$ introduce subterms of the
form $\mathit{yes}+\mathit{no}$, which can never be removed in equational
derivations.

######  Theorem 6.

The finite axiom system
$\mathcal{E}_{v,1}^{\prime}=\mathcal{E}_{v}^{\prime}\cup\\{V_{1}\\}$ is
complete for verdict equivalence over open monitors when
$\mathit{Act}=\\{a\\}$. That is, if $m\simeq n$ then
$\mathcal{E}_{v,1}^{\prime}\vdash m=n$. Hence, verdict equivalence is finitely
based when $\mathit{Act}=\\{a\\}$.

###### Proof.

Before we start the main proof we note that the new axiom $V_{1}$ can prove
the equation $x=a^{n}.x+x$ for each $n\geq 0$. This is done as follows: if
$n=0$ then this is the axiom $A3$. Assume we can prove that equation for $n$.
Then we can show it for $n+1$ thus:

$x\overset{\mathrm{V_{1}}}{=}x+a.x\overset{\mathrm{I.H.}}{=}x+a.(a^{n}.x+x)\overset{\mathrm{D_{a}}}{=}x+a.x+a^{n+1}.x\overset{\mathrm{V_{1}}}{=}x+a^{n+1}.x~{}~{}.$

Note here that this means that $\mathcal{E}_{v}^{\prime}\cup\\{V_{1}\\}$
proves all the equations in $\mathcal{O}$ over $\\{a\\}$, which means that
even though $\mathcal{E}_{v}^{\prime}\cup\\{V_{1}\\}$ is finite, it can prove
the infinite family $\mathcal{E}_{\textit{v,f}}^{\prime}$ over $\\{a\\}$.

Let $m\simeq n$. By Lemma 16, we can assume that $m$ and $n$ are in reduced
normal form. We will present the argument only for the case where
$m=\mathit{yes}+a.m_{a}+\displaystyle\sum_{i\in I}x_{i}$, where each $m_{a}$
is $\mathit{yes}$-free, as every other case is either trivial or a sub-case of
this one.

By following the reasoning of previous proofs, we have that
$n=\mathit{yes}~{}[+a.n_{a}]+\displaystyle\sum_{i\in I}x_{i}$.

Let us first consider the case that $a.n_{a}$ is not a summand of $n$. (Note
that this is possible, as witnessed by axiom $V_{1}$.) That is

$m=\mathit{yes}+a.m_{a}+\displaystyle\sum_{i\in
I}x_{i}\simeq\mathit{yes}+\displaystyle\sum_{i\in I}x_{i}=n\enspace.$

Observe that, for each $s\in\mathit{Act}^{*}$, we have
$m_{a}\not\xRightarrow{s}\mathit{no}$. Indeed,
$m_{a}\xRightarrow{s}\mathit{no}$ would imply that $m$ and $n$ are not verdict
equivalent under the substitution $\sigma_{\mathit{end}}(x)=\mathit{end}$ for
all $x$. This means that $m_{a}$ is both $\mathit{yes}$\- and
$\mathit{no}$-free. Moreover, note that the set of variables occurring in
$m_{a}$ is included in $\\{x_{i}\mid i\in I\\}$. To see this, assume that $x$
occurs in $m_{a}$, but is not contained in $\\{x_{i}\mid i\in I\\}$. Consider
the substitution that maps $x$ to $\mathit{no}$ and all the other variables to
$\mathit{end}$. Again, we have that $m$ rejects some trace starting with $a$
while $n$ cannot reject any trace, which contradicts our assumption that
$m\simeq n$.

For each monitor $m^{\prime}$, we define $\mathcal{V}(m^{\prime})$ as the set
of pairs $(s,x)$ such that $m^{\prime}\xrightarrow[]{s}x+m^{\prime\prime}$ for
some $m^{\prime\prime}$. By structural induction on $m^{\prime}$ and Lemma 15,
one can easily prove that, when $m^{\prime}$ is $\mathit{yes}$\- and
$\mathit{no}$-free, $\mathcal{E}_{v}$ proves
$m^{\prime}=\displaystyle\sum_{(s,x)\in\mathcal{V}(m^{\prime})}{s.x}$.

Therefore
$m=\mathit{yes}+a.\displaystyle\sum_{(s,x)\in\mathcal{V}(m_{a})}s.x+\displaystyle\sum_{i\in
I}x_{i}$. Since the only available action in $\mathit{Act}$ is $a$ and the
variables occurring in $m_{a}$ also occur in $\\{x_{i}\mid i\in I\\}$, we have
that by applying the equations we proved earlier by using axiom $V_{1}$ we can
prove $m=\mathit{yes}+\displaystyle\sum_{i\in I}x_{i}=n$, and we are done.

Assume now that $a.n_{a}$ is a summand of $n$. We proceed to prove that that
$m_{a}\simeq n_{a}$. In this case we have

$m_{a}=\displaystyle\sum_{(s,x)\in\mathcal{V}(m_{a})}{s.x}~{}[+a^{h}.\mathit{no}]~{}\text{and}~{}n_{a}=\sum_{(s,x)\in\mathcal{V}(n_{a})}{s.x}~{}[+a^{k}.\mathit{no}]~{},$

for some $h,k$.

By mapping all variables to $\mathit{end}$ we can see that $h=k$.
Additionally, for each variable $s$ and by using the axiom $V_{1}$ we can
reduce both of the above summations so that only the shortest $s$ leading to
$x$ is kept. By Lemma 10, we have that, for each variable, this $s$ is
identical for both sides of the equality $m\simeq n$ and we are done. ∎

####  4.2.2 Completeness of $\omega$-verdict equivalence

This section presents a complete axiomatization for $\omega$-verdict
equivalence over $Mon_{F}$. We have already presented the necessary axioms
that capture $\omega$-verdict equivalence over closed terms, as well as the
necessary ones to capture equivalence of terms that include variables. We will
show here that the combination of the two axiom systems is enough for
completeness of $\omega$-verdict equivalence over open terms and there is no
need for extra axioms to be added. First we look at the case for a singleton
action set, i.e. $\mathit{Act}=\\{a\\}$. In this case, the equation

$(\mathbf{V1_{\omega}})~{}x=a.x$

is sound and we therefore we can shrink the axiom system to:

$\mathcal{E}_{\omega,1}^{\prime}=\\{A1-A4\\}\cup\\{V1_{\omega}\\}\cup\\{O1\\},$

for which we prove:

######  Theorem 7.

$\mathcal{E}_{\omega,1}^{\prime}$ is complete for $\omega$-verdict equivalence
for open terms for a finite $\mathit{Act}$, with $|\mathit{Act}|=1$. That is,
if $m\simeq_{\omega}n$ then $\mathcal{E}_{\omega,1}^{\prime}\vdash m=n$.

###### Proof.

The proof of the above follows easily since, by using those equations, every
term can be proved equal to one of the form $\displaystyle\sum_{i\in
I}x_{i}~{}[+\mathit{yes}]~{}[+\mathit{no}]$, where $I$ is empty if both
$\mathit{yes}$ and $\mathit{no}$ are summands, and two terms of that form are
$\omega$-verdict equivalent iff they are equal modulo $A1-A4$. Note that, in
this case, there are only four congruence classes of terms, namely the ones
asymptotically equivalent to subsets of $\mathit{yes}$ and $\mathit{no}$, so
the quotient algebra is very small and equationally well behaved. ∎

In the case where there the action set contains more than one action but is
still finite we have a more interesting situation. We therefore define:

$\mathcal{E}_{\omega,f}^{\prime}=\mathcal{E}_{\omega}\cup\mathcal{E}_{\textit{v,f}}^{\prime}~{},$

for which we prove:

######  Theorem 8.

$\mathcal{E}_{\omega,f}^{\prime}$ is complete for $\omega$-verdict equivalence
over open terms when $\mathit{Act}$ is finite and $|\mathit{Act}|\geq 2$. That
is, if $m\simeq_{\omega}n$ then $\mathcal{E}_{\omega,f}^{\prime}\vdash m=n$.

The rest of this section is devoted to the proof of the above theorem. We
start by showing a lemma that tells us that if two monitors are
$\omega$-verdict equivalent then they can only disagree on finitely many
finite traces.

######  Lemma 18.

For two monitors in $Mon_{F}$, we have that $m\simeq_{\omega}n$ if and only
if, for any substitution $\sigma$, the set

$\displaystyle\mathcal{S}_{m,n,\sigma}=\left(L_{a}(\sigma(m))\setminus
L_{a}(\sigma(n))\right)\cup(L_{r}(\sigma(m))\setminus L_{r}(\sigma(n)))$
$\displaystyle\cup\left(L_{a}(\sigma(n))\setminus
L_{a}(\sigma(m))\right)\cup(L_{r}(\sigma(n))\setminus L_{r}(\sigma(m)))$

is finite.

###### Proof.

We prove both implications separately by establishing their contrapositive
statements. For the implication from left to right, assume that
$\mathcal{S}_{m,n,\sigma}$ is infinite. It follows that there are some
$\sigma$ and trace $s$ such that $s\in\mathcal{S}_{m,n,\sigma}$ with

$|s|>max\\{0pt(\sigma(m)),0pt(\sigma(n))\\}.$

Assume, without loss of generality, that $\sigma(m)$ accepts $s$, but
$\sigma(n)$ does not. Let $a\in\mathit{Act}$. Then $sa^{\omega}$ is in
$L_{a}(\sigma(m))\cdot\mathit{Act}^{\omega}$. We claim that $sa^{\omega}$ is
not in $L_{a}(\sigma(n))\cdot\mathit{Act}^{\omega}$. Indeed, $\sigma(n)$ does
not accept any prefix of $s$, since it does not accept $s$ itself, and it does
not accept $sa^{i}$ for any $i\geq 0$ because $|s|>0pt(\sigma(n))$. For the
implication from right to left, assume, without loss of generality, that there
are some substitution sigma and some $t\in\mathit{Act}^{\\{}omega$ such that
$t$ is in $L_{a}(\sigma(m))\cdot\mathit{Act}^{\omega}$, but not in
$L_{a}(\sigma(n))\cdot\mathit{Act}^{\omega}$. Since $t$ is in
$L_{a}(\sigma(m))\cdot\mathit{Act}^{\omega}$, we have that there are some
$s\in L_{a}(\sigma(m))$ and $u$ in $\mathit{Act}^{\omega}$ such that $t=su$.
It follows that $ss^{\prime}\in L_{a}(\sigma(m))$ for each finite prefix
$s^{\prime}$ of $u$, but none of the $ss^{\prime}$ is contained in