11institutetext:  University of Turin, Italy 22institutetext: University of
Genoa, Italy

# Ain’t No Stoppin’ Us Monitoring Now

Luca Ciccone 11 0000-0001-9515-5280 Francesco Dagnino 22 0000-0003-3599-3535
Angelo Ferrando 22 0000-0002-8711-4670

###### Abstract

Not all properties are monitorable. This is a well-known fact, and it means
there exist properties that cannot be fully verified at runtime. However,
given a non-monitorable property, a monitor can still be synthesised, but it
could end up in a state where no verdict will ever be concluded on the
satisfaction (resp., violation) of the property. For this reason, non-
monitorable properties are usually discarded. In this paper, we carry out an
in-depth analysis on monitorability, and how non-monitorable properties can
still be partially verified. We present our theoretical results at a semantic
level, without focusing on a specific formalism. Then, we show how our theory
can be applied to achieve partial runtime verification of Linear Temporal
Logic (LTL).

###### Keywords:

Monitorability Safety properties Runtime Verification

##  1 Introduction

Runtime Verification (RV) [8, 9, 21] is a well-established approach, whose aim
is to achieve the formal verification of software (resp., hardware) systems at
runtime. This means that, differently from other formal verification
techniques, such as Model Checking [10], RV focuses on the analysis of actual
system executions, rather than on a model (_i.e._ abstraction) of it. More
precisely, given a formal property, which can be expressed in various
formalisms [25, 17, 5, 20, 22], a _monitor_ is synthesised and used to verify
the property against system executions. A monitor can be seen abstractly as a
function that, given a _finite observation_ of a system execution (_e.g._ a
finite sequence, a.k.a. trace, of events generated by the system), returns a
verdict stating whether it satisfies or violates the property. Intuitively,
what the monitor does is checking whether the current observation of the
system execution carries enough information to conclude the satisfaction
(resp., violation) of the property under analysis, that is, it does not need
to observe more to determine the verdict.

Unfortunately, for some properties, the monitor could end up in scenarios
where, no matter what it observes, it would never be able to conclude a
verdict. Such cases are problematic since the monitor keeps on observing the
system, thus consuming resources, even though it has no hope to determine the
satisfaction (resp., violation) of the property. This has lead to the notion
of _monitorability_ [19, 2, 8, 27]. Roughly, a property is said to be
_monitorable_ if we can synthesise a monitor which has always the possibility
of eventually verifying it, that is, the above situation cannot happen.
Actually, this is just one out of many different flavours of monitorability
that exist in the literature [19, 2, 1, 3]. Nevertheless, we focus on this one
as it does not only require the existence of a correct monitor, but the latter
to be well behaved as well, _i.e._ it has not to run uselessly.

Since monitors of non-monitorable properties may eventually be unable to
conclude anything about the system, RV approaches usually rule such properties
out, restricting themselves to monitorable ones. However, even though a non-
monitorable property is in some cases ill-behaved, it may still be relevant to
analyse, especially when there are fragments of it where a verdict can be
reached.

In this paper, we take seriously this idea, providing first steps towards
_partial_ runtime verification. Specifically, we present an abstract semantic
approach to partially monitor any given property, which makes our framework
independent from specific formalisms used to describe properties and monitors.
We build on the abstract setting for monitorability proposed in [28]. First of
all, we observe that any property admits best safety and cosafety
approximations, which turn out to be monitorable, like all safety and cosafety
properties, under mild assumptions111In the standard linear time setting,
safety and cosafety properties are known to be always monitorable [4, 27],
but, as we will observe, this is no longer true in our abstract setting which
covers also branching time properties.. Then, we show how to combine the
verdicts of the (standard) monitors of these approximations to build a
generalised monitor, which is able to partially verify the initial property,
even though it may be non-monitorable in general. Roughly, a generalised
monitor is not only able to determine the satisfaction or violation of the
property, but also when to safely give up on the verification, since it will
never be able to conclude anything. In a sense, we move also the
monitorability check at runtime with the usual advantages: we do not discard a
property only because we statically detect that in some cases it may not be
verified, but rather we synthesise a monitor that, when such cases happen,
stops running and, otherwise, keeps on verifying the property. We dub this
approach partial RV, since the monitor may determine neither the satisfaction
nor the violation of the property, but we are guaranteed that it keeps on
running only if it has the possibility of concluding something on the
property.

To test the effectiveness of the proposed framework, we instantiate it
describing two approaches to achieve partial RV of properties in the linear
time setting. In the first one, we focus on properties expressed in Linear
Temporal Logic (LTL) [25]. In particular, we show how to extend the standard
synthesis procedure of monitors for LTL formulas, to build a generalised
monitor. In the second one, instead, we focus on the Linear Time
$\nu$-calculus (a purely coinductive fragment of the Linear Time
$\mu$-calculus [6, 30]). This calculus is much less expressive then other
formalisms, such as LTL or the full Linear Time $\mu$-calculus, since, as we
show, it can express only safety, thus monitorable, properties. We briefly
discuss how one can directly use an $LT\nu$-term as a monitor, thus avoiding
the synthesis procedure which is usually very computationally expensive, and
then we show how to combine two $LT\nu$-terms to specify a generalised
monitor. Finally, we prove that in this way we can describe generalised
monitors of all LTL formulas. For both approaches we provide prototype
implementations with some empirical evaluations of their performances.

#### Outline

Section 2 revisits basic notions about monitorability in the abstract. Using
this framework, Section 3 presents (co)safety completions of properties,
showing how they can be used to build generalised monitors. Sections 4.1 and
4.2 describe two instantiation of the general framework to concretely specify
generalised monitors for linear time properties. Finally, Section 5 discusses
related work and Section 6 concludes the paper.

##  2 Preliminaries on monitorability

In this section, we recall well-known notions about monitorability, phrasing
them in an abstract, purely semantic setting, following [28]. We need this
abstract setting to develop our results independently from specific choices of
system models and specification languages.

Assume a set $\mathcal{B}$ of _(system) behaviours_ $\alpha,\beta,\gamma$.
These can be whatever one needs, e.g., traces of events, trees, states, etc.
Then, a _property_ is a subset of behaviours $P\subseteq\mathcal{B}$.
Intuitively, one cannot directly access and manipulate system behaviours as a
whole, because they may have an infinite nature; instead we can analyse the
system through _observations_ , which are intuitively finite approximations of
system behaviours.

######  Definition 1 (Observation system)

An _observation structure_ over $\mathcal{B}$ consists of a preordered set
$\langle\mathcal{O},\triangleleft\rangle$ of _observations_ together with a
binary relation $\triangleleft_{b}\subseteq\mathcal{O}\times\mathcal{B}$ such
that the following properties hold:

  * •

$o\triangleleft p$ and $p\triangleleft_{b}\alpha$ implies
$o\triangleleft_{b}\alpha$

  * •

for all $o\in\mathcal{O}$ there is $\alpha\in\mathcal{B}$ such that
$o\triangleleft_{b}\alpha$

Let us set $\mathcal{B}(o)=\\{\alpha\in\mathcal{B}\mid
o\triangleleft_{b}\alpha\\}$ and $\mathcal{O}(\alpha)=\\{o\in\mathcal{O}\mid
o\triangleleft_{b}\alpha\\}$. Intuitively, the preorder on observations models
a refinement between them: $o\triangleleft p$ means that $p$ is a finer
observation w.r.t. $o$. The relation $\triangleleft_{b}$ relates observations
to behaviours: $o\triangleleft_{b}\alpha$ means that $o$ approximates the
behaviour $\alpha$.

######  Example 1 (Linear Time)

Assume a set of events $\mathcal{E}$. In the standard setting of runtime
verification, we are interested in monitoring properties of single executions
of a system. Hence, in this setting, we can take as set of behaviours either
the set $\mathcal{E}^{\omega}$ of infinite traces or the set
$\mathcal{E}^{\infty}$ of finite or infinite traces. Then, the set of
observations can be the set $\mathcal{E}^{\star}$ of finite traces and both
relations $\triangleleft$ and $\triangleleft_{b}$ are given by prefixing.

######  Example 2 (Hyperproperties)

Assume again a set of events $\mathcal{E}$. In some cases, we may be
interested in monitoring properties on multiple executions of a system. In
this case, we can consider as set of behaviours the set
$\wp(\mathcal{E}^{\omega})$ (resp. $\wp(\mathcal{E}^{\infty})$) of sets of
infinite (resp. finite or infinite) traces of events. Here, the set of
observation can be $\wp_{F}(\mathcal{E}^{\star})$ consisting of finite sets of
finite traces of events, where the refinement order is given by
$X\triangleleft Y$ iff for all $u\in X$ there is $v\in Y$ such that $u$ is a
prefix of $v$. Finally, the relation $\triangleleft_{b}$ relating observations
and behaviours will be given by $X\triangleleft_{b}T$ iff for all $u\in X$
there is $\sigma\in T$ such that $u$ is a prefix of $\sigma$. Note that, a
property in this setting is what is usually called _hyperproperty_ [11].

######  Example 3 (Branching Time)

Assume again a set of events $\mathcal{E}$. In a branching time setting, we
can take as set of behaviours the set $\mathsf{Tr}^{\infty}(\mathcal{E})$ of
finite and infinite trees with edges labelled by events in $\mathcal{E}$. We
illustrate two possible observation structures. A first choice for
observations can be the set of finite traces $\mathcal{E}^{\star}$ with the
prefixing ordering. The approximation relation is given by
$u\triangleleft_{b}t$ iff $t$ contains a path starting from the root labelled
by $u$. Another choice for observations can be the set
$\wp_{F}(\mathcal{E}^{\star})$ with the structure of Example 2. The
approximation relation is given by $X\triangleleft_{b}t$ iff for all $u\in X$
there is a path in $t$ starting from the root labelled by $u$.

In the following, let us fix an observation structure
$\langle\mathcal{O},\triangleleft,\triangleleft_{b}\rangle$ over
$\mathcal{B}$. Monitoring a property means trying to establish whether the
system satisfies or violates it just relying on a (finite) observation of it.
Formally, a monitor is a function $M:\mathcal{O}\rightarrow\mathcal{V}_{3}$
where $\mathcal{V}_{3}$ is the set of _verdicts_
$\\{\mathsf{yes},\mathsf{no},\mathsf{?}\\}$. This means that a monitor, given
an observation, can either accept it (verdict $\mathsf{yes}$), or reject it
(verdict $\mathsf{no}$), or be inconclusive (verdict $\mathsf{?}$). On
$\mathcal{V}_{3}$ it is clearly defined an _information order_ $\preceq$ given
by $\mathsf{?}\preceq\mathsf{yes}$ and $\mathsf{?}\preceq\mathsf{no}$. A
monitor $M$ is _impartial_ [14] if it is monotone, that is, $o\triangleleft p$
implies $M(o)\preceq M(p)$, for all $op\in\mathcal{O}$. This means that it
cannot retract conclusive verdicts when considering finer observations.

Given a property $P$, we define the _abstract monitor_ of $P$ to be a function
$\mathcal{M}_{P}:\mathcal{O}\rightarrow\mathcal{V}_{3}$ given as follows:

$\mathcal{M}_{P}(o)=\begin{cases}\mathsf{yes}&\mathcal{B}(o)\subseteq P\\\
\mathsf{no}&\mathcal{B}(o)\cap P=\emptyset\\\
\mathsf{?}&\text{otherwise}\end{cases}$

In other words, $\mathcal{M}_{P}(o)=\mathsf{yes}$ when all behaviours
approximated by $o$ _satisfy_ $P$, in which case we say that $o$ _positively
determines $P$_, $\mathcal{M}_{P}(u)=\mathsf{no}$ when all behaviours
approximated by $o$ _violate_ $P$, in which case we say that $o$ _negatively
determines $P$_, and $\mathcal{M}_{P}(o)=\mathsf{?}$ when no conclusive
verdict can be emitted yet. We say that $o$ _determines $P$_ when
$\mathcal{M}_{P}(o)\neq\mathsf{?}$. It is easy to check that the abstract
monitor is impartial.

###### Proposition 1

Let $P$ be a property on $\mathcal{B}$. Then, for all $o,p\in\mathcal{O}$,
$o\triangleleft p$ implies $\mathcal{M}_{P}(o)\preceq\mathcal{M}_{P}(p)$.

We say that an impartial monitor $M$ is _sound_ for a property $P$ if, for all
$o\in\mathcal{O}$, $M(o)\preceq\mathcal{M}_{P}(o)$, that is, it cannot
contraddict the abstract monitor of $P$. Moreover, we say that $M$ is _almost
complete_ if, for all $o\in\mathcal{O}$, there exists $p\in\mathcal{O}$ such
that $o\triangleleft p$ and $M(p)=\mathcal{M}_{P}(o)$. In other words, $M$ is
almost complete when it can always eventually meet the verdict of the abstract
monitor of $P$.

The following lemmas relate the abstract monitor with set inclusion and
complementation; where the following holds:
$\overline{\mathsf{yes}}=\mathsf{no}$, $\overline{\mathsf{no}}=\mathsf{yes}$
and $\overline{\mathsf{?}}=\mathsf{?}$.

###### Lemma 1

Let $P,Q$ be properties on $\mathcal{B}$ such that $P\subseteq Q$ and
$o\in\mathcal{O}$ be an observation. Then, $\mathcal{M}_{P}(o)=\mathsf{yes}$
implies $\mathcal{M}_{Q}(o)=\mathsf{yes}$ and $\mathcal{M}_{Q}(o)=\mathsf{no}$
implies $\mathcal{M}_{P}(o)=\mathsf{no}$.

###### Lemma 2

Let $P$ be a property on $\mathcal{B}$ and $o\in\mathcal{O}$ be an
observation. Then, $\mathcal{M}_{\mathcal{B}\setminus
P}(o)=\overline{\mathcal{M}_{P}(o)}$.

Using the abstract monitor, we define when a property $P$ is _monitorable_
(w.r.t. the notion of $\forall$-monitorable [27]). This happens when the
abstract monitor has always the possibility of emitting a positive or negative
verdict.

###### Definition 2

A property $P$ on $\mathcal{B}$ is _monitorable_ if, for every observation
$o\in\mathcal{O}$, there exists $p\in\mathcal{O}$ such that $o\triangleleft p$
and $\mathcal{M}_{P}(p)\neq\mathsf{?}$.

Thus, every observation has a refinement that determines the property. Another
feature of monitorable properties is that they are closed under
complementation.

###### Proposition 2

Let $P$ be a monitorable property on $\mathcal{B}$. Then,
$\mathcal{B}\setminus P$ is monitorable.

###### Example 4

We give some examples of non-monitorable properties.

  1. 1.

Let us consider the observation structure in Example 1. For the sake of
clarity we refer to the usual syntax and semantics of LTL (see [26]). We write
$\llbracket\phi\rrbracket$ for the semantics of the LTL formula $\phi$. Let
$\mathcal{E}=\\{a,b,c,d\\}$ and consider the formula
$\phi=(a\land\mathop{\Diamond}b)\lor(c\land\mathop{\square}\mathop{\Diamond}d)$.
The property $\llbracket\phi\rrbracket\subseteq\mathcal{E}^{\omega}$ is
clearly non-monitorable since all the traces $cu\in\mathcal{E}^{\star}$ have
no finite extensions determining it.

  2. 2.

Let us consider the first setting of Example 3 where
$\mathcal{E}=\\{a,b,c\\}$. Consider the property $P$ satisfied by all those
trees not containing a path starting from the root with an event $a$. This
property is not monitorable as, for instance, the trace $bb$ cannot be
extended to reach a conclusive verdict.

##  3 Partial monitoring via (co)safety completions

When we want to monitor a property $P$, usually we first check whether it is
monitorable, to ensure that the monitor will not run forever even when it will
never reach any conclusive verdict. In this section, we propose a different
approach, describing its semantic foundations: instead of ruling out non-
monitorable properties, we show it is always possible to find monitorable
(over/under) approximations preserving either negative or positive verdicts.
Moreover, combining such approximations, we define a generalised abstract
monitor which detects when it will not be able to provide any conclusive
verdict.

To develop our approximations, we rely on standard lattice-theoretic notions
for which we refer to [12]. In particular, the set of all properties over
$\mathcal{B}$, that is, the powerset $\wp(\mathcal{B})$, is a complete lattice
w.r.t. subset inclusion. Then, the key idea is to look for approximations of
properties in the classes of safety and cosafety properties, which are well-
behaved subsets of $\wp(\mathcal{B})$.

Let us start with safety properties. Informally, a safety property is a
property for which we can always finitely determine whether a behaviour
violates it.

######  Definition 3 (Safety property)

A property $P$ on $\mathcal{B}$ is a _safety property_ if for every
$\alpha\notin P$ there is an observation $o\triangleleft_{b}\alpha$ that
negatively determines it.

###### Proposition 3

$P$ is a safety property on $\mathcal{B}$ if and only if for every
$\alpha\in\mathcal{B}$, $\mathcal{B}(o)\cap P\neq\emptyset$ for each
observation $o\triangleleft_{b}\alpha$ implies $\alpha\in P$.

This notion is pretty standard [27] and usually safety properties come with a
crucial feature: they are always monitorable. However, in our abstract
setting, this is not true in general. For instance, Example 4 (2) shows a
safety property which is not monitorable. The issue with this example is that
observations do not have enough structure to support monitorability of safety
properties. Indeed, if we consider the same property in the second observation
structure of Example 3, it is monitorable. Intuitively, the problem is that,
if we use finite traces to monitor branching time properties, the monitor can
fall into a branch where there is no hope to reach a conclusive verdict.
Hence, to recover monitorability of safety properties, we need to assume a
richer structure on observations (see below).

###### Definition 4

An observation structure
$\langle\mathcal{O},\triangleleft,\triangleleft_{b}\rangle$ over $\mathcal{B}$
is _directed_ if, for all $o,p\in\mathcal{O}$ and $\alpha\in\mathcal{B}$,
$o\triangleleft_{b}\alpha$ and $p\triangleleft_{b}\alpha$ imply that there is
$q\in\mathcal{O}$ such that $q\triangleleft_{b}\alpha$ and $o\triangleleft q$
and $p\triangleleft q$.

In other words, the set $\mathcal{O}(\alpha)$ is a directed set w.r.t.
$\triangleleft$ for every $\alpha\in\mathcal{B}$. Note that, all the examples
of observation structures we have seen are directed except for the first one
in Example 3. Now, for directed observation structures, we can prove that
safety properties are monitorable.

###### Proposition 4

Let $\langle\mathcal{O},\triangleleft,\triangleleft_{b}\rangle$ be a directed
observation structure on $\mathcal{B}$. Then, every safety property is
monitorable.

From now on let us assume a directed observation structure
$\langle\mathcal{O},\triangleleft,\triangleleft_{b}\rangle$ over
$\mathcal{B}$. Denote by $\mathbb{S}$ the set of all safety properties over
$\mathcal{B}$. Then, the set $\mathbb{S}$ is a suborder of $\wp(\mathcal{B})$
and the following lemma shows it is a closure system, that is, it is closed
under arbitrary intersections.

###### Lemma 3

$\mathbb{S}$ is a closure system.

Like any closure system, $\mathbb{S}$ induces a closure operator on
$\wp(\mathcal{B})$:

$\Gamma_{\mathbb{S}}(P)=\bigcap\\{Q\in\mathbb{S}\mid P\subseteq Q\\}$

Being a closure operator, $\Gamma_{\mathbb{S}}$ is a monotone function on
$\wp(\mathcal{B})$ w.r.t. subset inclusion and has the following two
properties for any $P\subseteq\mathcal{B}$: $P\subseteq\Gamma_{\mathbb{S}}(P)$
and
$\Gamma_{\mathbb{S}}(\Gamma_{\mathbb{S}}(P))\subseteq\Gamma_{\mathbb{S}}(P)$.
In other words, $\Gamma_{\mathbb{S}}(P)$ is _the best safety
(over)approximation of $P$_ and we call it the _safety completion of $P$_.

We now give an alternative characterisation of $\Gamma_{\mathbb{S}}$. Let $P$
be a property on $\mathcal{B}$. Define the set $\mathsf{NR}(P)$ of _$P$
-unrefutable_ behaviours as follows:

$\mathsf{NR}(P)=\\{\alpha\in\mathcal{B}\mid\mathcal{B}(o)\cap
P\neq\emptyset\text{ for all }o\triangleleft_{b}\alpha\\}$

###### Proposition 5

$\mathsf{NR}$ is a closure operator.

Note that, by Proposition 3, $P$ is a safety property if and only if
$\mathsf{NR}(P)\subseteq P$ if and only if $P$ is a fixpoint of $\mathsf{NR}$,
as $\mathsf{NR}$ is a closure operator. Then, we get the following result.

###### Corollary 1

$\Gamma_{\mathbb{S}}(P)=\mathsf{NR}(P)$, for all $P\subseteq\mathcal{B}$.

The key property of the safety completion of $P$ is that it exactly preserves
all negative verdicts of $P$ as proved by the following theorem.

###### Theorem 3.1

Let $P$ be a property on $\mathcal{B}$ and $o\in\mathcal{O}$. Then,
$\mathcal{M}_{P}(o)=\mathsf{no}$ if and only if
$\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}(o)=\mathsf{no}$.

Therefore, if we are interested in detecting just violations of $P$, we can
monitor its safety completion, which is necessarily monitorable and emits all
and only negative verdicts of $P$. Moreover, when
$\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}(o)=\mathsf{yes}$, we are sure that
$\mathcal{M}_{P}(o)\neq\mathsf{no}$ and, since an abstract monitor is
impartial, we can safely stop the execution, as we will never receive a
negative verdict.

We now dualise everything considering cosafety properties. Informally, a
cosafety property is a property for which we can always finitely determine
whether a behaviour satisfies it.

######  Definition 5 (Cosafety property)

A property $P$ on $\mathcal{B}$ is a _cosafety property_ if for every
$\alpha\in P$, there exists an observation $o\triangleleft_{b}\alpha$
positively determining $P$.

###### Proposition 6

$P$ is a cosafety property if and only if $\mathcal{B}\setminus P$ is a safety
property.

This proposition allows us to dualise all results obtained for safety
properties. Denote by ${\mathsf{co}\mathbb{S}}$ the set of all cosafety
properties on $\mathcal{B}$. From Propositions 2 and 4 we get that cosafety
properties are monitorable and from Lemma 3 we get that
${\mathsf{co}\mathbb{S}}$, as a suborder of $\wp(\mathcal{B})$, is an interior
system, that is, it is closed under arbitrary unions. Therefore, we get an
interior operator on $\wp(\mathcal{B})$:

$\Delta_{{\mathsf{co}\mathbb{S}}}(P)=\bigcup\\{Q\in{\mathsf{co}\mathbb{S}}\mid
Q\subseteq P\\}$

Being an interior operator, $\Delta_{{\mathsf{co}\mathbb{S}}}$ is a monotone
function on $\wp(\mathcal{B})$ with respect to set inclusion and has the
following two properties for any $P\subseteq\mathcal{B}$
$\Delta_{{\mathsf{co}\mathbb{S}}}(P)\subseteq P$ and
$\Delta_{{\mathsf{co}\mathbb{S}}}(P)\subseteq\Delta_{{\mathsf{co}\mathbb{S}}}(\Delta_{{\mathsf{co}\mathbb{S}}}(P))$.
In other words, $\Delta_{{\mathsf{co}\mathbb{S}}}(P)$ is _the best cosafety
(under)approximation of $P$_ and we call it the _cosafety completion of $P$_.

It is easy to see that
$\mathcal{B}\setminus\Gamma_{\mathbb{S}}(P)=\Delta_{{\mathsf{co}\mathbb{S}}}(\mathcal{B}\setminus
P)$. Hence, the cosafety completion of $P$ exactly preserves positive verdicts
of $P$, as proved below.

###### Corollary 2

Let $P$ be a property on $\mathcal{B}$ and $o\in\mathcal{O}$. Then,
$\mathcal{M}_{P}(o)=\mathsf{yes}$ if and only if
$\mathcal{M}_{\Delta_{{\mathsf{co}\mathbb{S}}}(P)}(o)=\mathsf{yes}$.

Therefore, if we are interested in detecting just satisfaction of $P$, we can
monitor its cosafety completion, which is necessarily monitorable and emits
all and only positive verdicts of $P$. Moreover, when
$\mathcal{M}_{\Delta_{{\mathsf{co}\mathbb{S}}}(P)}(u)=\mathsf{no}$, we are
sure that $\mathcal{M}_{P}(u)\neq\mathsf{yes}$ and, since an abstract monitor
is impartial, we can safely stop the execution as we will never receive a
positive verdict.

In summary, for any property $P$ on $\mathcal{B}$, there are two monitorable
properties $\Delta_{{\mathsf{co}\mathbb{S}}}(P)\subseteq
P\subseteq\Gamma_{\mathbb{S}}(P)$, where the former captures exactly positive
verdicts of $P$ and the latter captures exactly negative verdicts of $P$.
However, combining the two completions, we get even more information: we can
characterise the so called _ugly_ observations, that is, those observations
after which it is not possible to emit any conclusive verdict. These are
precisely those observations that the monitorability constraint rules out,
but, if they can be detected, there is no need to restrict ourselves to
monitorable properties.

###### Proposition 7

Let $P$ be a property on $\mathcal{B}$ and $o\in\mathcal{O}$ an observation.
Then, $\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}(o)=\mathsf{yes}$ and
$\mathcal{M}_{\Delta_{{\mathsf{co}\mathbb{S}}}(P)}(o)=\mathsf{no}$ if and only
if, for every $p\in\mathcal{O}$ such that $o\triangleleft p$,
$\mathcal{M}_{P}(p)=\mathsf{?}$.

Relying on these results, we define a notion of generalised monitor as a
function $\widehat{M}:\mathcal{O}\rightarrow\mathcal{V}_{6}$, where
$\mathcal{V}_{6}$ is a set of verdicts consisting of six elements:
$\mathsf{yes}$, $\mathsf{no}$ and $\mathsf{?}$ as before and
$\mathsf{?}_{\mathsf{yes}}$, when no negative verdict can be reached,
$\mathsf{?}_{\mathsf{no}}$, when no positive verdict can be reached, and
$\mathsf{\chi}$, informally called _giveup_ , when no verdict at all can be
reached. The information order $\preceq$ on $\mathcal{V}_{6}$ is depicted in
Figure 1.

---
$\textstyle{\mathsf{yes}}$$\textstyle{\mathsf{\chi}}$$\textstyle{\mathsf{no}}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mathsf{?}_{\mathsf{yes}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mathsf{?}_{\mathsf{no}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mathsf{?}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

Figure 1: The information order on
$\mathcal{V}_{6}=\\{\mathsf{yes},\mathsf{no},\mathsf{?},\mathsf{?}_{\mathsf{yes}},\mathsf{?}_{\mathsf{no}},\mathsf{\chi}\\}$.

Then, for any property $P$, we can define a _generalised abstract monitor_ to
be a function
$\widehat{\mathcal{M}}_{P}:\mathcal{O}\rightarrow\mathcal{V}_{6}$ given as
follows:

$\widehat{\mathcal{M}}_{P}(o)=\begin{cases}\mathsf{yes}&\mathcal{M}_{\Delta_{{\mathsf{co}\mathbb{S}}}(P)}(o)=\mathsf{yes}\\\
\mathsf{no}&\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}(o)=\mathsf{no}\\\
\mathsf{\chi}&\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}(o)=\mathsf{yes}\text{ and
}\mathcal{M}_{\Delta_{{\mathsf{co}\mathbb{S}}}(P)}(o)=\mathsf{no}\\\
\mathsf{?}_{\mathsf{yes}}&\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}(o)=\mathsf{yes}\text{
and }\mathcal{M}_{\Delta_{{\mathsf{co}\mathbb{S}}}(P)}(o)=\mathsf{?}\\\
\mathsf{?}_{\mathsf{no}}&\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}(o)=\mathsf{?}\text{
and }\mathcal{M}_{\Delta_{{\mathsf{co}\mathbb{S}}}(P)}(o)=\mathsf{no}\\\
\mathsf{?}&\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}(o)=\mathsf{?}\text{ and
}\mathcal{M}_{\Delta_{{\mathsf{co}\mathbb{S}}}(P)}(o)=\mathsf{?}\end{cases}$

Note that cases not mentioned above are impossible due to Lemma 1. It is also
easy to see that the generalised abstract monitor is impartial, meaning that
$\widehat{\mathcal{M}}_{P}(o)\preceq\widehat{\mathcal{M}}_{P}(p)$, for all
$o,p\in\mathcal{O}$ such that $o\triangleleft p$. Moreover, it can always
eventually reach a conclusive verdict as proved by the following theorem.

###### Theorem 3.2

Let $P$ be a property on $\mathcal{B}$. Then, for every $o\in\mathcal{O}$,
there is $p\in\mathcal{O}$ such that $o\triangleleft p$ and
$\widehat{\mathcal{M}}_{P}(p)\in\\{\mathsf{yes},\mathsf{no},\mathsf{\chi}\\}$.

In conclusion, to produce all verdicts of the generalised abstract monitor of
a property $P$, we have just to look at two monitorable properties: its safety
and cosafety completions. But we can go further: since the complement of a
cosafety property is a safety property (Proposition 6), we can restrict our
attention to just safety properties, by monitoring $\Gamma_{\mathbb{S}}(P)$
and
$\mathcal{B}\setminus\Delta_{{\mathsf{co}\mathbb{S}}}(P)=\Gamma_{\mathbb{S}}(\mathcal{B}\setminus
P)$, and appropriately inverting verdicts. This is the strategy adopted in the
following sections where we instantiate this technique in different monitoring
settings.

###### Example 5

Consider the property
$\phi=(a\land\mathop{\Diamond}b)\lor(c\land\mathop{\square}\mathop{\Diamond}d)$
from Example 4 (1). Its safety completion is given by $\phi_{1}=a\lor c$,
while its cosafety completion by $\phi_{2}=a\land\mathop{\Diamond}b$. We
report below some verdicts of the generalised abstract monitor of $\phi$
obtained combining $\phi_{1}$ and $\phi_{2}$.

$\begin{array}[]{cccc}u&\quad\mathcal{M}_{\llbracket\phi_{1}\rrbracket}(u)&\quad\mathcal{M}_{\llbracket\phi_{2}\rrbracket}(u)&\quad\widehat{\mathcal{M}}_{\llbracket\phi\rrbracket}(u)\\\
\hline\cr c\dots&\mathsf{yes}&\mathsf{no}&\mathsf{\chi}\\\
a&\mathsf{yes}&\mathsf{?}&\mathsf{?}_{\mathsf{yes}}\\\
b\dots&\mathsf{no}&\mathsf{?}&\mathsf{no}\\\ a\dots
b\dots&\mathsf{yes}&\mathsf{yes}&\mathsf{yes}\end{array}$

######  Remark 1 (Never Gonna Give You Up)

Note that, the generalised abstract monitor allows us to recognise non-
monitorable properties. Indeed, by Proposition 7, a property $P$ is
monitorable if and only if $\widehat{\mathcal{M}}_{P}(o)\neq\mathsf{\chi}$ for
every $o\in\mathcal{O}$.

##  4 Partial Monitoring of Linear Time Properties

In this section we present two ways of applying the general framework
introduced in Section 3. First, we consider Temporal Logic, which is one of
the most used formalism in RV, showing how we can synthesise a generalised
monitor for them. Then, we focus on a formalism where only safety properties
can be expressed, the Linear Time $\nu$-calculus, showing how it can be used
to describe generalised monitors and proving it suffices to express those of
all LTL properties.

###  4.1 Linear Temporal Logic

LTL is a commonly used specification language in RV. We use $\phi,\psi$ to
range over LTL formulas and denote by $\llbracket\phi\rrbracket$ the semantics
of $\phi$, namely the set of infinite traces satisfying $\phi$. We refer to
the literature [25] for formal definitions (we report them in Section 0.A.6
for reader’s convenience). Given $\phi$, Figure 2 shows the canonical
procedure for synthesising its monitor [9].

$\textstyle{{Input}}$$\textstyle{{Formula}}$$\textstyle{{NBA}}$$\textstyle{{NFA}}$$\textstyle{{DFA}}$Moore
machine$\textstyle{{\phi}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathcal{A}_{\phi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\lceil\mathcal{A}_{\phi}\rceil}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\hat{\mathcal{A}}_{\phi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\tilde{\mathcal{A}}_{\phi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\phi}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{M_{\phi}}}$$\textstyle{{\lnot\phi}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathcal{A}_{\lnot\phi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\lceil\mathcal{A}_{\lnot\phi}\rceil}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\hat{\mathcal{A}}_{\lnot\phi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\tilde{\mathcal{A}}_{\lnot\phi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

Figure 2:  NBA is Non-deterministic Büchi Automaton, NFA is Non-deterministic
Finite Automaton and DFA is Deterministic Finite Automaton.

Informally, we start from $\phi$ and first we synthesize the equivalent non
deterministic Büchi automaton (NBA) $\mathcal{A}_{\phi}$. Then, we set as
_final_ all states whose accepted language is not empty (_i.e._ the states
that can reach infinitely often a final one), obtaining the NBA
$\lceil\mathcal{A}_{\phi}\rceil$. After that, we treat such automaton as a NFA
and we _determinise_ it. We do the same process for $\neg\phi$ and, finally,
we combine the DFAs $\tilde{\mathcal{A}}_{\phi}$ and
$\tilde{\mathcal{A}}_{\lnot\phi}$ to obtain the monitor.

$\textstyle{{Input}}$$\textstyle{{NBA}}$$\textstyle{{NFA}}$$\textstyle{{DFA}}$$\textstyle{{\bf
Completions}}$$\textstyle{{\bf
Gen.Mon.}}$$\textstyle{{\phi}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathcal{A}_{\phi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\lceil\mathcal{A}_{\phi}\rceil}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\hat{\mathcal{A}}_{\phi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\tilde{\mathcal{A}}_{\phi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{M_{\Gamma_{\mathbb{S}}(\phi)}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\phi}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\widehat{M}_{\phi}}}$$\textstyle{{\lnot\phi}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\mathcal{A}_{\lnot\phi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\lceil\mathcal{A}_{\lnot\phi}\rceil}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\hat{\mathcal{A}}_{\lnot\phi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{\tilde{\mathcal{A}}_{\lnot\phi}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{{M_{\Gamma_{\mathbb{S}}(\neg\phi)}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

Figure 3: Steps required to generate a generalized monitor for a LTL property
$\phi$.

Figure 3 shows how we can refine the steps in Figure 2 to build a generalized
monitor for $\phi$. Notably, the difference with respect to Figure 2 lies in
the last steps. Indeed, we transform the DFA $\tilde{\mathcal{A}}_{\phi}$ into
a monitor $M_{\tilde{\mathcal{A}}_{\phi}}$, assigning the verdict
$\mathsf{yes}$ to those states that can reach _only_ final states. Denote by
$\mathcal{L}(\mathcal{A})$ the language accepted by an automaton
$\mathcal{A}$. It is easy to check that $M_{\tilde{\mathcal{A}}_{\phi}}$
coincides with the abstract monitor of
$\mathcal{L}(\lceil\mathcal{A}_{\phi}\rceil)$, as proved below.

###### Lemma 4

For every formula $\phi$ and finite trace $u$,
$M_{\tilde{\mathcal{A}}_{\phi}}(u)=\mathcal{M}_{\mathcal{L}(\lceil\mathcal{A}_{\phi}\rceil)}(u)$.

Then, we observe that the third step in Figure 3 corresponds to a safety
completion.

###### Lemma 5

Let $\mathcal{A}$ be a NBA. Then
$\mathcal{L}(\lceil\mathcal{A}\rceil)=\Gamma_{\mathbb{S}}(\mathcal{L}(\mathcal{A}))$.

This shows we have constructed the abstract monitors for the safety
completions $\Gamma_{\mathbb{S}}(\llbracket\phi\rrbracket)$ and
$\Gamma_{\mathbb{S}}(\llbracket\neg\phi\rrbracket)$, thus combining them, as
described at the end of Section 3, we obtain the generalised abstract monitor
of $\phi$.

###### Theorem 4.1

For every formula $\phi$ and finite trace $u$,
$\widehat{M}_{\phi}(u)=\widehat{\mathcal{M}}_{\llbracket\phi\rrbracket}(u)$.

#### Implementation and Experiments.

A prototype implementing the LTL instantiation of our general framework is
available as supplementary material. In more detail, the tool is implemented
in Python exploiting the Spot library222https://spot.lrde.epita.fr/ [15], to
handle the translation from LTL to Büchi Automata, and the Automata
library333https://github.com/caleb531/automata, to handle the subsequent
transformations (to NFA and DFA). We tested our tool on the example properties
presented in this paper; then, we carried out experiments to validate it and
analyse its performance. The results are reported in Figures 6, 6 and 6.

Figure 4: Monitor synthesis.

Figure 5: Verification.

Figure 6: Verification (event).

Figure 6 reports the time required to synthesise a monitor given an LTL
formula. As in the standard LTL generation, the complexity is exponential
w.r.t. the size of the formula. However, more importantly for runtime
verification, the execution time required for the actual verification is still
linear (Figure 6). Indeed, the per event verification is constant444This is
good from an overhead perspective assuming the monitor is used incrementally
to analyse the system while the latter is running and stabilises around
$0.001$ [ms]. Note that, the experiments have been carried out on a large set
of randomly generated LTL formulas and traces of events (more than 100000
formulas).

###  4.2 Generalised Monitoring via Linear Time $\nu$-calculus

As we have seen at the end of Section 3, safety properties suffices to
describe generalised monitors. Following this idea, in this section we
consider a language where only safety properties can be expressed, the Linear
Time $\nu$-calculus, showing how it can be used to describe generalised
monitors and proving it can express those of all LTL properties. That is, this
language is enough to specify monitors of a much more expressive logic.

Let us assume a countable set $AP$ of _atomic propositions_ ranged over by
$p,q$, together with an interpretation function
$\langle\\!\langle-\rangle\\!\rangle:AP\rightarrow\wp(\mathcal{E})$,
interpreting each atomic proposition as a set of events. Let
$w\in\mathcal{E}^{\omega}$, we denote by $w_{i}$ the $i$-th element of $w$ and
by $w_{\geq i}$ the trace starting from the $i$-th element of $w$. Figure 7
shows syntax and semantics of such a calculus, a purely coinductive (_i.e._
without $\mu$ operator) fragment of the Linear Time $\mu$-calculus [6, 30, 13]
that we dub LT$\nu$. Notably, the syntax is inductively defined while the
semantics coinductively. We set
$\llbracket\mathsf{t}\rrbracket=\\{w\in\mathcal{E}^{\omega}\mid
w\mathrel{\models}_{C}\mathsf{t}\\}$.

$\displaystyle\mathsf{t},\mathsf{s}\Coloneqq\top\mid\bot\mid p\mid
p^{\bot}\mid\mathsf{t}\land\mathsf{s}\mid\mathsf{t}\lor\mathsf{s}\mid\mathop{\circ}\mathsf{t}\mid
X\mid\nu X.\mathsf{t}\penalty-10000\hskip 20.00003pt plus 0.5fil minus
5.0pt\penalty-10000\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{c-top}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
13.55452pt\vbox{\vbox{}\hbox{\hskip-13.55452pt\hbox{\hbox{$\displaystyle\displaystyle
w\mathrel{\models}_{C}\top$}}}}}}$}}}\penalty 50\hskip 20.00003pt plus 0.5fil
minus
5.0pt{\vbox{\hbox{\hbox{\small\small{c-prop}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
12.18124pt\vbox{\vbox{}\hbox{\hskip-12.18124pt\hbox{\hbox{$\displaystyle\displaystyle
w\mathrel{\models}_{C}p$}}}}}}$}}}~{}w_{0}\in\langle\\!\langle
p\rangle\\!\rangle\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{c-coprop}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
14.35902pt\vbox{\vbox{}\hbox{\hskip-14.35902pt\hbox{\hbox{$\displaystyle\displaystyle
w\mathrel{\models}_{C}p^{\bot}$}}}}}}$}}}~{}w_{0}\not\in\langle\\!\langle
p\rangle\\!\rangle\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{c-next}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
15.18785pt\vbox{\hbox{\hskip-15.18785pt\hbox{\hbox{$\displaystyle\displaystyle
w_{\geq 1}\mathrel{\models}_{C}\mathsf{t}$}}}\vbox{}}}\over\hbox{\hskip
14.11008pt\vbox{\vbox{}\hbox{\hskip-14.11008pt\hbox{\hbox{$\displaystyle\displaystyle
w\mathrel{\models}_{C}\mathop{\circ}\mathsf{t}$}}}}}}$}}}\penalty-10000\hskip
20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{c-or-l}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
11.61008pt\vbox{\hbox{\hskip-11.61006pt\hbox{\hbox{$\displaystyle\displaystyle
w\mathrel{\models}_{C}\mathsf{t}$}}}\vbox{}}}\over\hbox{\hskip
16.91563pt\vbox{\vbox{}\hbox{\hskip-16.91563pt\hbox{\hbox{$\displaystyle\displaystyle
w\mathrel{\models}_{C}\mathsf{t}\lor\mathsf{s}$}}}}}}$}}}\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{c-or-r}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
11.63785pt\vbox{\hbox{\hskip-11.63783pt\hbox{\hbox{$\displaystyle\displaystyle
w\mathrel{\models}_{C}\mathsf{s}$}}}\vbox{}}}\over\hbox{\hskip
16.91563pt\vbox{\vbox{}\hbox{\hskip-16.91563pt\hbox{\hbox{$\displaystyle\displaystyle
w\mathrel{\models}_{C}\mathsf{t}\lor\mathsf{s}$}}}}}}$}}}\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{c-and}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
33.24792pt\vbox{\hbox{\hskip-33.24792pt\hbox{\hbox{$\displaystyle\displaystyle
w\mathrel{\models}_{C}\mathsf{t}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
w\mathrel{\models}_{C}\mathsf{s}$}}}}\vbox{}}}\over\hbox{\hskip
16.91563pt\vbox{\vbox{}\hbox{\hskip-16.91563pt\hbox{\hbox{$\displaystyle\displaystyle
w\mathrel{\models}_{C}\mathsf{t}\land\mathsf{s}$}}}}}}$}}}\penalty 50\hskip
20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{c-rec}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
34.81609pt\vbox{\hbox{\hskip-34.81607pt\hbox{\hbox{$\displaystyle\displaystyle
w\mathrel{\models}_{C}\mathsf{t}\\{\nu
X.\mathsf{t}/X\\}$}}}\vbox{}}}\over\hbox{\hskip
19.72581pt\vbox{\vbox{}\hbox{\hskip-19.7258pt\hbox{\hbox{$\displaystyle\displaystyle
w\mathrel{\models}_{C}\nu X.\mathsf{t}$}}}}}}$}}}$

Figure 7: Syntax and Semantics of Linear Time $\nu$-calculus.

###### Example 6

We fix $\mathcal{E}=\wp_{F}^{*}(AP)$, the set of non-empty subsets of $AP$.
Then, $\langle\\!\langle p\rangle\\!\rangle=\\{\alpha\mid p\in\alpha\\}$. Let
$\mathsf{t}=\nu\mathsf{X}.p\land\mathop{\circ}\mathsf{X}$. Then,
$\llbracket\mathsf{t}\rrbracket=\\{w\mid\forall i.p\in w_{i}\\}$.

Without loss of generality, we assume that terms are _contractive_ , i.e.,
variables occur guarded by a next operator. Indeed, for every LT$\nu$ term,
there is an equivalent contractive one [13]. The next theorem states that the
semantics of a term is a safety property.

###### Proposition 8

Let $\mathsf{t}$ be a LT$\nu$ term. Then $\llbracket\mathsf{t}\rrbracket$ is a
safety property.

The proof of Proposition 8 relies on Definition 3 which requires the
characterization of a relation $w\not\mathrel{\models}_{C}\mathsf{t}$, meaning
that $w\not\in\llbracket\mathsf{t}\rrbracket$, which, being the dual of
$\mathrel{\models}_{C}$, is defined inductively.

As usual, we can use LT$\nu$ terms as monitors, by inductively defining a
labeled transition system $\mathsf{t}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{s}$ (see Section 0.A.2), meaning that $\mathsf{t}$
reduces to $\mathsf{s}$ when the event $e$ occurs. We write
$\mathsf{t}\not\rightarrow$ when there are no $e,\mathsf{s}$ such that
$\mathsf{t}\stackrel{{\scriptstyle e}}{{\rightarrow}}\mathsf{s}$. Let
$\stackrel{{\scriptstyle}}{{\Rightarrow}}_{*}$ be the reflexive transitive
closure of $\stackrel{{\scriptstyle}}{{\rightarrow}}$ and
$\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\omega}$ be the coinductive
predicate obtained by applying infinitely many times
$\stackrel{{\scriptstyle}}{{\rightarrow}}$ (_i.e._
$\mathsf{t}\stackrel{{\scriptstyle w}}{{\Rightarrow}}_{\omega}$ means that
$\mathsf{t}$ reduces infinitely many times using $w$).

######  Proposition 9 (Correctness of
$\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\omega}$)

Let $w\in\mathcal{E}^{\omega}$ and $\mathsf{t}$ an LT$\nu$ term. Then
$w\mathrel{\models}_{C}\mathsf{t}$ iff $\mathsf{t}\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$.

Given a LT$\nu$ term $\mathsf{t}$ we can build a monitor
$M_{\mathsf{t}}:\mathcal{E}^{\star}\rightarrow\mathcal{V}_{3}$ as follows:

$M_{\mathsf{t}}(u)=\begin{cases}\mathsf{yes}&\mathsf{t}\stackrel{{\scriptstyle
u}}{{\Rightarrow}}_{*}\mathsf{s}$ \text{ and } $\vdash\mathsf{s}\\\
\mathsf{no}&\mathsf{t}\stackrel{{\scriptstyle
u}}{{\Rightarrow}}_{*}\mathsf{s}\text{ implies }\mathsf{s}\not\rightarrow\\\
\mathsf{?}&\text{otherwise}\end{cases}$

The monitor returns $\mathsf{no}$ when it gets stuck, while it returns
$\mathsf{yes}$ when it reaches a term whose semantics is
$\mathcal{E}^{\omega}$. To check this, we rely on a coinductive proof system
(see Section 0.A.2), which is a minimal variation of the one in [13] for the
Linear Time $\mu$-calculus, satisfying
$\llbracket\mathsf{t}\rrbracket=\mathcal{E}^{\omega}$ iff $\vdash\mathsf{t}$,
for every LT$\nu$ term $\mathsf{t}$.

According to Section 3, in order to monitor an arbitrary property $P$, we have
to describe the monitors of its (co)safety completions. This can be done by
specifying two safety properties $P_{\mathbb{S}}$ and
$P_{\mathsf{co}\mathbb{S}}$ such that $P_{\mathbb{S}}\cup
P_{\mathsf{co}\mathbb{S}}=\mathcal{E}^{\omega}$, as this is equivalent to
$\mathcal{E}^{\omega}\setminus P_{\mathsf{co}\mathbb{S}}\subseteq
P_{\mathbb{S}}$ and $\mathcal{E}^{\omega}\setminus P_{\mathsf{co}\mathbb{S}}$
is a cosafety property. Therefore, given a pair of LT$\nu$ terms
$\mathsf{t}_{\mathbb{S}},\mathsf{t}_{{\mathsf{co}\mathbb{S}}}$ such that
$\llbracket\mathsf{t}_{\mathbb{S}}\rrbracket\cup\llbracket\mathsf{t}_{\mathsf{co}\mathbb{S}}\rrbracket=\mathcal{E}^{\omega}$,
which can be checked looking for a derivation of
$\vdash\mathsf{t}_{\mathbb{S}}\lor\mathsf{t}_{\mathsf{co}\mathbb{S}}$,
describing, respectively, the safety completion and the complement of the
cosafety completion of some property, we obtain a generalised monitor for $P$
by combining verdicts of $M_{\mathsf{t}_{\mathbb{S}}}$ and
$M_{\mathsf{t}_{\mathsf{co}\mathbb{S}}}$.

###### Example 7

Let $\mathcal{E}=AP=\\{a,b,c,d\\}$ and $\langle\\!\langle
p\rangle\\!\rangle=\\{p\\}$. Consider again the LTL property
$\phi=(a\land\mathop{\Diamond}b)\lor(c\land\mathop{\square}\mathop{\Diamond}d)$
from Example 4. It requires to reject all traces not starting with $a$ or $c$
and to accept all traces starting with $a$ and containing some $b$. This can
be specified by the following two LT$\nu$ terms:
$\mathsf{t}_{\mathbb{S}}=a\lor c$ and
$\mathsf{t}_{{\mathsf{co}\mathbb{S}}}=a^{\bot}\lor(\nu\mathsf{X}.b^{\bot}\land\mathop{\circ}\mathsf{X})$,
remembering that accepted traces are those rejected by
$\mathsf{t}_{\mathsf{co}\mathbb{S}}$. It is easy to see that
$\llbracket\mathsf{t}_{\mathbb{S}}\lor\mathsf{t}_{{\mathsf{co}\mathbb{S}}}\rrbracket=\mathcal{E}^{\omega}$.

Finally, the next theorem shows that by LT$\nu$ we can specify monitors for
all LTL formulas.

######  Theorem 4.2 (Expressiveness w.r.t. LTL)

Let $\phi$ be a LTL formula. Then there exists $\mathsf{t}_{\mathbb{S}}$ such
that
$\Gamma_{\mathbb{S}}(\llbracket\phi\rrbracket)=\llbracket\mathsf{t}_{\mathbb{S}}\rrbracket$.

The proof of Theorem 4.2 is based on an algorithmic encoding of Büchi automata
as LT$\nu$ terms, computing the safety completion of the language accepted by
the automaton. Such encoding can be applied to all those automata obtained
from LTL formulae.

#### Implementation and Experiments.

A prototype implementing the Linear Time $\nu$-calculus instantiation of our
general framework is available supplementary material. In more detail, the
tool is implemented in SWI-Prolog. We chose SWI-Prolog due to its native
support for coinduction and cyclic terms. Thanks to these features, the
implementation of LT$\nu$ terms syntax and transition system is
straightforward. As for the LTL prototype, we carried out experiments to
validate our tool and analyse its performance as well. The obtained results
are reported in Figures 9 and 9.

Figure 8: Verification.

Figure 9: Verification (event).

Since we directly start from the LT$\nu$ terms, there is no synthesis step.
Figure 9 reports the execution time required to verify a given trace of
events. As before, such execution is still performed in linear time w.r.t. the
length of the analysed trace. Moreover, the incremental verification is still
applicable as well, since the execution time per single event is maintained
constant and stabilises around 0.15 [ms] (Figure 9). As before, the
experiments have been carried out on a large set of randomly generated
properties (LT$\nu$ terms in this case) and traces of events (more than 100000
randomly generated terms have been tested).

##  5 Related Work

The present work can be seen as a foundational counterpart of [16], where the
authors present the idea of detecting ugly prefixes of LTL properties at
runtime from a practical perspective. Indeed, they focus only on
implementation aspects and no study on the theory behind it is done
whatsoever. To provide such a foundation in a very general setting, covering
both linear and branching time, we build on the framework in [28]. They
consider also gray-box monitoring and a concrete instantiation on
hyperproperties, which we do not address, but they are both interesting
directions for further work.

In this paper, we consider the notion of monitorability introduced by Pnueli
and Zaks [27] and Peled and Havelund [24], which generalises the first
proposal [19]. This is one of the most commonly adopted in the literature and
it has a more operational nature. That is, it focuses on the fact that a
monitor should not run uselessly rather than on the verdicts it can produce.

Other notions of monitorability are considered, for instance, by Aceto et al.
[1]. Their completely monitorable properties corresponds to properties that
are both safety and cosafety, while partially monitorable properties
correspond to either safety or cosafety properties, depending on whether one
focuses on satisfaction or violation. Hence, in the linear-time these notions
are stronger than the one we consider, while in branching-time they are
incomparable, since, as we have noticed, depending on the observation
structure, (co)safety properties may not be monitorable in our setting.

Aceto et al. [3] introduce the notion of _best monitorable consequence_ ,
which can be seen as an instance of our best safety approximation of a
property, at least when no additional condition on monitors is imposed. They
also provide a syntactic construction to compute the best monitorable
consequence of recHML formulas, which could be a good starting point to obtain
an instance of generalised monitors in a branching-time setting.555The
observation structure they use is not directed (Definition 4), hence we will
need to adjust it, for instance considering hyperproperties.

On a more general side, different works can be found on the monitorability of
LTL properties. In [29], an extension of LTL called robust LTL (rLTL) is
presented. With respect to LTL, rLTL semantics allows for distinguishing
various “degrees” to which a trace violates a property. This is obtained
through five different verdicts (instead of the standard three), which
quantitatively denote how much the property has been violated. It is important
to note that in rLTL, all properties become monitorable [23]; simply because
the resulting monitor does not look for the complete satisfaction (resp.,
violation) of the property, but it settles for a certain degree of
satisfaction (resp., violation) of the latter.

In [7], a two-step approach to address monitorability of LTL properties is
proposed. Specifically, the satisfaction (resp., violation) of the LTL
property is given by taking into consideration a prediction over the future of
the analysed trace. Differently from other works [31], such prediction is only
based upon past experience, i.e., by only looking at how the trace behaved in
the past. According to such prediction, the LTL property is evaluated
considering how far the trace is supposed to be from satisfying or violating
the property. Moreover, such distance is evaluated considering the safety and
cosafety aspects of the property.

In [18], an approach to extend the set of monitorable LTL properties through
assumptions over the system is presented. Thanks to the additional information
on the system, not all possible future continuations, given a prefix, are
considered, but only a certain subset of them. Consequently, properties that
are considered non-monitorable in general, can be monitored when such subset
of traces reduces to only satisfying (resp., violating) traces.

With respect to the previously listed works, our contribution moves forward
towards the concept of partial RV. Instead of focusing on extending LTL
semantics, or presenting a predictive version of the latter, we present a
general-purpose approach to partially monitor formal properties. Since we
tackle this problem at a semantic level, our theoretical contribution is not
limited to LTL; even though we present a possible instantiation exploiting
LTL. Moreover, works in literature are more focused on estimating fully non-
monitorable properties666Where with “fully” non-monitorable, we mean
properties for which there are no prefixes that determine them neither
positively, nor negatively., while we care for properties that are indeed non-
monitorable in general, but can be monitored in some scenarios (_i.e._ some
prefixes can still determine the property at runtime). In fact, we present a
solution that can be used both for monitoring the monitorable parts of a given
property, and at the same time, to safely recognise when to stop the
verification; since no final verdict will ever be concluded.

##  6 Conclusions and Future Work

This paper introduces partial RV, studying its semantic foundations. We show
how to build monitors capable to recognise when they will not be able to reach
any conclusive verdict, and then to stop their execution. In this way, we can
_partially_ monitor any property, avoiding issues related to non-
monitorability, that is, having monitors running forever even though they will
never be able to reach any conclusive verdict. We show that this can be
achieved by combining safety and cosafety completions, which are well-behaved
monitorable over/under approximations of any property. These results are
developed independently from specific setups, covering both branching and
linear time settings. Then, we present concrete instantiations of the
framework for linear time properties, using LTL and Linear Time $\nu$-calculus
as concrete languages. In both cases, we developed prototypes, available as
supplementary material, with an empirical evaluation of their performances.

As future work, we are planning to further test our prototypes on a set of
well-known properties (a starting point could be the ones listed in [9]). On a
more theoretical perspective, we are considering to further explore the
branching time scenario, and its implications in our monitoring setting.

## References

  * [1] Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: Adventures in monitorability: from branching to linear time and back again. Proc. ACM Program. Lang. 3(POPL), 52:1–52:29 (2019). https://doi.org/10.1145/3290365, https://doi.org/10.1145/3290365
  * [2] Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: An operational guide to monitorability. In: Ölveczky, P.C., Salaün, G. (eds.) Software Engineering and Formal Methods - 17th International Conference, SEFM 2019, Oslo, Norway, September 18-20, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11724, pp. 433–453. Springer (2019). https://doi.org/10.1007/978-3-030-30446-1_23
  * [3] Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: The best a monitor can do. In: Baier, C., Goubault-Larrecq, J. (eds.) 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference). LIPIcs, vol. 183, pp. 7:1–7:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.CSL.2021.7, https://doi.org/10.4230/LIPIcs.CSL.2021.7
  * [4] Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distributed Comput. 2(3), 117–126 (1987). https://doi.org/10.1007/BF01782772
  * [5] Ancona, D., Franceschini, L., Ferrando, A., Mascardi, V.: RML: theory and practice of a domain specific language for runtime verification. Sci. Comput. Program. 205, 102610 (2021). https://doi.org/10.1016/j.scico.2021.102610
  * [6] Barringer, H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. In: Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, St. Petersburg Beach, Florida, USA, January 1986. pp. 173–183. ACM Press (1986). https://doi.org/10.1145/512644.512660
  * [7] Bartocci, E., Bloem, R., Nickovic, D., Röck, F.: A counting semantics for monitoring LTL specifications over finite traces. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, pp. 547–564. Springer (2018). https://doi.org/10.1007/978-3-319-96145-3_29, https://doi.org/10.1007/978-3-319-96145-3_29
  * [8] Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification - Introductory and Advanced Topics, Lecture Notes in Computer Science, vol. 10457, pp. 1–33. Springer (2018). https://doi.org/10.1007/978-3-319-75632-5_1
  * [9] Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for ltl and tltl. ACM Trans. Softw. Eng. Methodol. 20(4) (Sep 2011). https://doi.org/10.1145/2000799.2000800
  * [10] Clarke, E.M.: Model checking. In: International Conference on Foundations of Software Technology and Theoretical Computer Science. pp. 54–56. Springer (1997)
  * [11] Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, USA, 23-25 June 2008. pp. 51–65. IEEE Computer Society (2008). https://doi.org/10.1109/CSF.2008.7, https://doi.org/10.1109/CSF.2008.7
  * [12] Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, 2 edn. (2002). https://doi.org/10.1017/CBO9780511809088
  * [13] Dax, C., Hofmann, M., Lange, M.: A proof system for the linear time $\mathrm{\mu}$-calculus. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings. Lecture Notes in Computer Science, vol. 4337, pp. 273–284. Springer (2006), https://doi.org/10.1007/11944836_26
  * [14] Dong, W., Leucker, M., Schallhart, C.: Impartial anticipation in runtime-verification. In: Cha, S.D., Choi, J., Kim, M., Lee, I., Viswanathan, M. (eds.) Automated Technology for Verification and Analysis, 6th International Symposium, ATVA 2008, Seoul, Korea, October 20-23, 2008. Proceedings. Lecture Notes in Computer Science, vol. 5311, pp. 386–396. Springer (2008). https://doi.org/10.1007/978-3-540-88387-6_33
  * [15] Duret-Lutz, A., Poitrenaud, D.: SPOT: an extensible model checking library using transition-based generalized büchi automata. In: DeGroot, D., Harrison, P.G., Wijshoff, H.A.G., Segall, Z. (eds.) 12th International Workshop on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS 2004), 4-8 October 2004, Vollendam, The Netherlands. pp. 76–83. IEEE Computer Society (2004). https://doi.org/10.1109/MASCOT.2004.1348184, https://doi.org/10.1109/MASCOT.2004.1348184
  * [16] Ferrando, A., Cardoso, R.C.: Towards partial monitoring: It is always too soon to give up. In: Farrell, M., Luckcuck, M. (eds.) Proceedings Third Workshop on Formal Methods for Autonomous Systems, FMAS 2021, Virtual, 21st-22nd of October 2021. EPTCS, vol. 348, pp. 38–53 (2021). https://doi.org/10.4204/EPTCS.348.3, https://doi.org/10.4204/EPTCS.348.3
  * [17] Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985). https://doi.org/10.1145/2455.2460, https://doi.org/10.1145/2455.2460
  * [18] Henzinger, T.A., Saraç, N.E.: Monitorability under assumptions. In: Deshmukh, J., Nickovic, D. (eds.) Runtime Verification - 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6-9, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12399, pp. 3–18. Springer (2020). https://doi.org/10.1007/978-3-030-60508-7_1
  * [19] Kim, M., Kannan, S., Lee, I., Sokolsky, O., Viswanathan, M.: Computational analysis of run-time monitoring - fundamentals of java-mac. Electron. Notes Theor. Comput. Sci. 70(4), 80–94 (2002). https://doi.org/10.1016/S1571-0661(04)80578-4
  * [20] Koymans, R.: Specifying real-time properties with metric temporal logic. Real Time Syst. 2(4), 255–299 (1990). https://doi.org/10.1007/BF01995674
  * [21] Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebraic Methods Program. 78(5), 293–303 (2009). https://doi.org/10.1016/j.jlap.2008.08.004
  * [22] Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004, Proceedings. Lecture Notes in Computer Science, vol. 3253, pp. 152–166. Springer (2004). https://doi.org/10.1007/978-3-540-30206-3_12
  * [23] Mascle, C., Neider, D., Schwenger, M., Tabuada, P., Weinert, A., Zimmermann, M.: From LTL to rltl monitoring: improved monitorability through robust semantics. In: Ames, A.D., Seshia, S.A., Deshmukh, J. (eds.) HSCC ’20: 23rd ACM International Conference on Hybrid Systems: Computation and Control, Sydney, New South Wales, Australia, April 21-24, 2020. pp. 7:1–7:12. ACM (2020). https://doi.org/10.1145/3365365.3382197, https://doi.org/10.1145/3365365.3382197
  * [24] Peled, D., Havelund, K.: Refining the safety-liveness classification of temporal properties according to monitorability. In: Margaria, T., Graf, S., Larsen, K.G. (eds.) Models, Mindsets, Meta: The What, the How, and the Why Not? - Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 11200, pp. 218–234. Springer (2018). https://doi.org/10.1007/978-3-030-22348-9_14, https://doi.org/10.1007/978-3-030-22348-9_14
  * [25] Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977. pp. 46–57. IEEE Computer Society (1977). https://doi.org/10.1109/SFCS.1977.32
  * [26] Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977. pp. 46–57. IEEE Computer Society (1977). https://doi.org/10.1109/SFCS.1977.32
  * [27] Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006, Proceedings. Lecture Notes in Computer Science, vol. 4085, pp. 573–586. Springer (2006). https://doi.org/10.1007/11813040_38
  * [28] Stucki, S., Sánchez, C., Schneider, G., Bonakdarpour, B.: Gray-box monitoring of hyperproperties. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11800, pp. 406–424. Springer (2019). https://doi.org/10.1007/978-3-030-30942-8_25, https://doi.org/10.1007/978-3-030-30942-8_25
  * [29] Tabuada, P., Neider, D.: Robust linear temporal logic. In: Talbot, J., Regnier, L. (eds.) 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France. LIPIcs, vol. 62, pp. 10:1–10:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016). https://doi.org/10.4230/LIPIcs.CSL.2016.10, https://doi.org/10.4230/LIPIcs.CSL.2016.10
  * [30] Vardi, M.Y.: A temporal fixpoint calculus. In: Ferrante, J., Mager, P. (eds.) Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, January 10-13, 1988. pp. 250–259. ACM Press (1988). https://doi.org/10.1145/73560.73582, https://doi.org/10.1145/73560.73582
  * [31] Zhang, X., Leucker, M., Dong, W.: Runtime Verification with Predictive Semantics. In: NASA Formal Methods. LNCS, vol. 7226, pp. 418–432. Springer (2012). https://doi.org/10.1007/978-3-642-28891-3_37

##  Appendix 0.A Appendix

We detail the proofs of all the results.

###  0.A.1 Supplement to Section 3

###### Proposition 10

Let $\langle\mathcal{O},\triangleleft,\triangleleft_{b}\rangle$ be a directed
observation structure on $\mathcal{B}$. Then, every safety property is
monitorable.

###### Proof

Let $P\subseteq\mathcal{B}$ be a safety property and $o\in\mathcal{O}$ an
observation. We distinguish two cases. If $\mathcal{B}(o)\subseteq P$, then
$\mathcal{M}_{P}(o)=\mathsf{yes}$, as needed. Otherwise, there is
$\alpha\in\mathcal{B}(o)$ such that $\alpha\notin P$. Since $P$ is safety, by
definition, there is $p\triangleleft_{b}\alpha$ such that
$\mathcal{M}_{P}(p)=\mathsf{no}$. Since
$\langle\mathcal{O},\triangleleft,\triangleleft_{b}\rangle$ is directed, there
is $q\in\mathcal{O}$ such that $q\triangleleft_{b}\alpha$ and $o\triangleleft
q$ and $p\triangleleft q$. By impartiality of the abstract monitor, we get
$\mathcal{M}_{P}(q)=\mathsf{no}$ as needed.

###### Lemma 6

$\mathbb{S}$ is a closure system.

###### Proof

Let $X\subseteq\mathbb{S}$ be a set of safety properties. We have to show that
$\bigcap X\in\mathbb{S}$. Consider $\alpha\notin\bigcap X$, then by definition
of intersection, there is a property $P\in X$ such that $\alpha\notin P$.
Since $X\subseteq\mathbb{S}$, we have that $P$ is a safety property, hence, by
definition, there is an observation $o\triangleleft_{b}\alpha$ such that
$\mathcal{B}(o)\cap P=\emptyset$. Then, because $P\in X$, we have $\bigcap
X\subseteq P$ and so $\mathcal{B}(o)\cap\left(\bigcap
X\right)\subseteq\mathcal{B}(o)\cap P=\emptyset$, hence
$\mathcal{B}(o)\cap\left(\bigcap X\right)=\emptyset$, that is, $o$ negatively
determines $\bigcap X$. This proves that $\bigcap X$ is a safety property, as
needed.

###### Proposition 11

$\mathsf{NR}$ is a closure operator.

###### Proof

It is easy to see that $NR$ is monotone ($P\subseteq Q$ implies
$\mathsf{NR}(P)\subseteq\mathsf{NR}(Q)$) and extensive
($P\subseteq\mathsf{NR}(P)$). Hence, we have only to check that
$\mathsf{NR}(\mathsf{NR}(P))\subseteq\mathsf{NR}(P)$. Let
$\alpha\in\mathsf{NR}(\mathsf{NR}(P))$, hence, for every observation
$o\triangleleft_{b}\alpha$, there is $\beta\in\\\ NR(P)$ such that
$o\triangleleft_{b}\beta$. Thus, for every observation
$p\triangleleft_{b}\beta$, there is $\gamma\in P$ such that
$p\triangleleft_{b}\gamma$. In particular, we get that, for every observation
$o\triangleleft_{b}\alpha$, there exists $\gamma\in P$ such that
$o\triangleleft_{b}\gamma$, hence $\alpha\in\mathsf{NR}(P)$, as needed.

###### Corollary 3

$\Gamma_{\mathbb{S}}(P)=\mathsf{NR}(P)$, for all $P\subseteq\mathcal{B}$.

###### Proof

It is straightforward as two closure operators with the same set of fixpoints
are equal.

###### Theorem 0.A.1

Let $P$ be a property on $\mathcal{B}$ and $o\in\mathcal{O}$. Then,
$\mathcal{M}_{P}(o)=\mathsf{no}$ if and only if
$\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}(o)=\mathsf{no}$.

###### Proof

The right-to-left implication follows from Lemma 1 as
$P\subseteq\Gamma_{\mathbb{S}}(P)$. Towards a proof of the other implication,
assume $\mathcal{B}(o)\cap P=\emptyset$ and consider
$\alpha\in\mathcal{B}(o)\cap\Gamma_{\mathbb{S}}(P)$. Then,
$o\triangleleft_{b}\alpha$ and $\alpha\in\Gamma_{\mathbb{S}}(P)$. By Corollary
1, we have $\Gamma_{\mathbb{S}}(P)=\mathsf{NR}(P)$, hence we get that, for
every observation $p\triangleleft_{b}\alpha$, $\mathcal{B}(p)\cap
P\neq\emptyset$. Hence, in particular, since $o\triangleleft_{b}\alpha$, we
get $\mathcal{B}(o)\cap P\neq\emptyset$, which is a contradiction. As a
consequence, we have $\mathcal{B}(o)\cap\Gamma_{\mathbb{S}}(P)=\emptyset$, as
needed.

###### Corollary 4

Let $P$ be a property on $\mathcal{B}$ and $o\in\mathcal{O}$. Then,
$\mathcal{M}_{P}(o)=\mathsf{yes}$ if and only if
$\mathcal{M}_{\Delta_{{\mathsf{co}\mathbb{S}}}(P)}(o)=\mathsf{yes}$.

###### Proof

We have $o$ positively determines $P$ iff $o$ negatively determines
$\mathcal{B}\setminus P$ iff $o$ negatively determines
$\Gamma_{\mathbb{S}}(\mathcal{B}\setminus P)$ iff $o$ positively determines
$\mathcal{B}\setminus\Gamma_{\mathbb{S}}(\mathcal{B}\setminus P)$. Then, the
thesis follows by the following equalities

$\mathcal{B}\setminus\Gamma_{\mathbb{S}}(\mathcal{B}\setminus
P)=\Delta_{{\mathsf{co}\mathbb{S}}}(\mathcal{B}\setminus(\mathcal{B}\setminus
P))=\Delta_{{\mathsf{co}\mathbb{S}}}(P)$

###### Proposition 12

Let $P$ be a property on $\mathcal{B}$ and $o\in\mathcal{O}$ an observation.
Then, $\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}(o)=\mathsf{yes}$ and
$\mathcal{M}_{\Delta_{{\mathsf{co}\mathbb{S}}}(P)}(o)=\mathsf{no}$ if and only
if, for every $p\in\mathcal{O}$ such that $o\triangleleft p$,
$\mathcal{M}_{P}(p)=\mathsf{?}$.

###### Proof

Let us first prove the left-to-right implication. Since abstract monitors are
impartial, we have that, for every $p\in\mathcal{O}$ such that $p\triangleleft
p$ $\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}(p)=\mathsf{yes}$ and
$\mathcal{M}_{\Delta_{{\mathsf{co}\mathbb{S}}}(P)}(p)=\mathsf{no}$. Moreover,
by Theorems 3.1 and 2, we have that
$\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}(p)=\mathsf{yes}$ implies
$\mathcal{M}_{P}(p)\neq\mathsf{no}$ and
$\mathcal{M}_{\Delta_{{\mathsf{co}\mathbb{S}}}(P)}(p)=\mathsf{no}$ implies
$\mathcal{M}_{P}(p)\neq\mathsf{yes}$. Therefore, we get
$\mathcal{M}_{P}(p)=\mathsf{?}$, as needed.

Towards a proof of the other direction, observe that, for every
$p\in\mathcal{O}$ such that $o\triangleleft p$, since
$\mathcal{M}_{P}(p)=\mathsf{?}$, there are
$\alpha_{1},\alpha_{2}\in\mathcal{B}(p)$ such that $\alpha_{1}\in P$ and
$\alpha_{2}\notin P$. Therefore, for every $\alpha\in\mathcal{B}(o)$ and every
observation $p\triangleleft_{b}\alpha$, since the observation structure is
directed, there is $q\triangleleft_{b}\alpha$ such that $o\triangleleft q$ and
$p\triangleleft q$, and, from what we observed above, there are
$\alpha_{1},\alpha_{2}\in\mathcal{B}(q)$ such that $\alpha_{1}\in P$ and
$\alpha_{2}\notin P$, and, since $o\triangleleft q$, we have
$\alpha_{1},\alpha_{2}\in\mathcal{B}(p)$. By Proposition 3 (and its dual),
this implies that $\alpha\in\Gamma_{\mathbb{S}}(P)$ and
$\alpha\notin\Delta{\mathsf{co}\mathbb{S}}](P)$, for every
$\alpha\in\mathcal{B}(o)$. Hence, we get
$\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}(o)=\mathsf{yes}$ and
$\mathcal{M}_{\Delta_{{\mathsf{co}\mathbb{S}}}(P)}(o)=\mathsf{no}$, as needed.

###### Theorem 0.A.2

Let $P$ be a property on $\mathcal{B}$. Then, for every $o\in\mathcal{O}$,
there is $p\in\mathcal{O}$ such that $o\triangleleft p$ and
$\widehat{\mathcal{M}}_{P}(p)\in\\{\mathsf{yes},\mathsf{no},\mathsf{\chi}\\}$.

###### Proof

Since $\Gamma_{\mathbb{S}}(P)$ is monitorable (Proposition 4), there is
$p\in\mathcal{O}$ such that $o\triangleleft p$ and
$\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}(p)\neq\mathsf{?}$. Moreover, since
$\Delta_{{\mathsf{co}\mathbb{S}}}(P)$ is monitorable (Propositions 6, 4 and
2), there is $q\in\mathcal{O}$ such that $p\triangleleft q$ and
$\mathcal{M}_{\Delta_{{\mathsf{co}\mathbb{S}}}(P)}(q)\neq\mathsf{?}$. Then,
since $\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}$ is impartial, we have
$\mathcal{M}_{\Gamma_{\mathbb{S}}(P)}(q)\neq\mathsf{?}$. Therefore, we get the
thesis by definition of $\mathcal{M}_{P}$.

###  0.A.2 Linear Time $\nu$-Calculus

######  Definition 6 (Proof System)

The coinductive interpretation of the following inference system describes the
proof system for LT$\nu$ terms using judgments of the form $\vdash\mathsf{t}$
for a term $\mathsf{t}$. We use $\Gamma,\Delta$ to range over sets of LT$\nu$
terms.

$\displaystyle{\vbox{\hbox{\hbox{\small\small{p-ax}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
47.29024pt\vbox{\vbox{}\hbox{\hskip-47.29022pt\hbox{\hbox{$\displaystyle\displaystyle\vdash
p_{1},\dots,p_{n},p^{\bot}_{n+1},\dots,p^{\bot}_{m},\Gamma$}}}}}}$}}}~{}\bigcup_{i=1}^{n}\langle\\!\langle
p_{i}\rangle\\!\rangle\cup\bigcup_{i=n+1}^{m}(\mathcal{E}^{\omega}\setminus\langle\\!\langle
p_{i}\rangle\\!\rangle)=\mathcal{E}^{\omega}\penalty 50\hskip 20.00003pt plus
0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{p-top}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
13.68053pt\vbox{\vbox{}\hbox{\hskip-13.68053pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\top,\Gamma$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{p-and}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
33.49994pt\vbox{\hbox{\hskip-33.49994pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\mathsf{t},\Gamma$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\mathsf{s},\Gamma$}}}}\vbox{}}}\over\hbox{\hskip
17.04164pt\vbox{\vbox{}\hbox{\hskip-17.04164pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\mathsf{t}\land\mathsf{s},\Gamma$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{p-or}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
15.0972pt\vbox{\hbox{\hskip-15.09718pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\mathsf{t},\mathsf{s},\Gamma$}}}\vbox{}}}\over\hbox{\hskip
17.04164pt\vbox{\vbox{}\hbox{\hskip-17.04164pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\mathsf{t}\lor\mathsf{s},\Gamma$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{p-rec}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
32.53937pt\vbox{\hbox{\hskip-32.53937pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\mathsf{t}\\{\nu\mathsf{X}.\mathsf{t}/\mathsf{X}\\},\Gamma$}}}\vbox{}}}\over\hbox{\hskip
20.73375pt\vbox{\vbox{}\hbox{\hskip-20.73373pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\nu\mathsf{X}.\mathsf{t},\Gamma$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{p-next}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
8.95828pt\vbox{\hbox{\hskip-8.95827pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\Gamma$}}}\vbox{}}}\over\hbox{\hskip
15.90276pt\vbox{\vbox{}\hbox{\hskip-15.90276pt\hbox{\hbox{$\displaystyle\displaystyle\vdash\mathop{\circ}\Gamma,\Delta$}}}}}}$}}}$

Where we write $\mathop{\circ}\Gamma$ for a set of LT$\nu$ terms of the form
$\mathop{\circ}\mathsf{t}_{1},\dots,\mathop{\circ}\mathsf{t}_{n}$. Note that
the proof system is the same of that presented in[13] for cut-free
derivations.

######  Definition 7 (LTS)

The following inductive inference system defines the labeled transition system
for LT$\nu$ terms.

$\displaystyle{\vbox{\hbox{\hbox{\small\small{r-top}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
14.40744pt\vbox{\vbox{}\hbox{\hskip-14.40744pt\hbox{\hbox{$\displaystyle\displaystyle\top\stackrel{{\scriptstyle
e}}{{\rightarrow}}\top$}}}}}}$}}}\penalty 50\hskip 20.00003pt plus 0.5fil
minus
5.0pt{\vbox{\hbox{\hbox{\small\small{r-prop}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
11.92308pt\vbox{\vbox{}\hbox{\hskip-11.92308pt\hbox{\hbox{$\displaystyle\displaystyle
p\stackrel{{\scriptstyle
e}}{{\rightarrow}}\top$}}}}}}$}}}~{}e\in\langle\\!\langle
p\rangle\\!\rangle\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{r-coprop}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
14.10086pt\vbox{\vbox{}\hbox{\hskip-14.10086pt\hbox{\hbox{$\displaystyle\displaystyle
p^{\bot}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\top$}}}}}}$}}}~{}e\not\in\langle\\!\langle
p\rangle\\!\rangle\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{r-next}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
11.90747pt\vbox{\vbox{}\hbox{\hskip-11.90746pt\hbox{\hbox{$\displaystyle\displaystyle\mathop{\circ}\mathsf{t}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{t}$}}}}}}$}}}\penalty-10000\hskip 20.00003pt plus
0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{r-and}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
30.41046pt\vbox{\hbox{\hskip-30.41046pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{t}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{t}^{\prime}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{s}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{s}^{\prime}$}}}}\vbox{}}}\over\hbox{\hskip
21.55858pt\vbox{\vbox{}\hbox{\hskip-21.55858pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{t}\land\mathsf{s}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{t}^{\prime}\land\mathsf{s}^{\prime}$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{r-or-l}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
10.17746pt\vbox{\hbox{\hskip-10.17744pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{t}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{t}^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
15.48302pt\vbox{\vbox{}\hbox{\hskip-15.48302pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{t}\lor\mathsf{s}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{t}^{\prime}$}}}}}}$}}}\penalty 50\hskip 20.00003pt
plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{r-or-r}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
10.233pt\vbox{\hbox{\hskip-10.23299pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{s}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{s}^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
15.51079pt\vbox{\vbox{}\hbox{\hskip-15.51079pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{t}\lor\mathsf{s}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{s}^{\prime}$}}}}}}$}}}\penalty 50\hskip 20.00003pt
plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{r-rec}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
33.38347pt\vbox{\hbox{\hskip-33.38345pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{t}\\{\nu
X.\mathsf{t}/X\\}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{t}^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
18.2932pt\vbox{\vbox{}\hbox{\hskip-18.29318pt\hbox{\hbox{$\displaystyle\displaystyle\nu
X.\mathsf{t}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{t}^{\prime}$}}}}}}$}}}$

Note that the LTS is inductively defined since we assumed that terms are
_contractive_.

###### Definition 8

We define the predicate $\mathsf{t}\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$ meaning that the term $\mathsf{t}$ reduces
infinitely many times according to $w\in\mathcal{E}^{\omega}$. We
coinductively interpret the following rule

${\hbox{$\displaystyle\displaystyle{\hbox{\hskip
12.70384pt\vbox{\hbox{\hskip-12.70384pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{s}\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$}}}\vbox{}}}\over\hbox{\hskip
14.30577pt\vbox{\vbox{}\hbox{\hskip-14.30576pt\hbox{\hbox{$\displaystyle\displaystyle\mathsf{t}\stackrel{{\scriptstyle
ew}}{{\Rightarrow}}_{\omega}$}}}}}}$}}~{}\mathsf{t}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{s}$

###### Theorem 0.A.1

Let $w\in\mathcal{E}^{\omega}$ and $\mathsf{t}$ a LT$\nu$ term. Then
$w\mathrel{\models}_{C}\mathsf{t}\iff\mathsf{t}\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$.

The proof of Theorem 0.A.1 is in Section 0.A.4. The proof of the iff part of
Theorem 0.A.1 is by coinduction. Additionally we have to prove that if
$w\mathrel{\models}_{C}\mathsf{t}$, then there exists $\mathsf{s}$ such that
$\mathsf{t}\stackrel{{\scriptstyle w_{0}}}{{\rightarrow}}\mathsf{s}$ and
$w_{\geq 1}\mathrel{\models}_{C}\mathsf{s}$ (see Lemma 8).

###### Example 8

Consider the LT$\nu$ term $\mathsf{t}=\nu\mathsf{X}.(p\lor
p^{\bot})\land\mathop{\circ}\mathsf{X}$. $\mathsf{t}\neq\top$ but it is easy
to see that $\llbracket\mathsf{t}\rrbracket=\mathcal{E}^{\omega}$. Hence, we
provide a derivation inside the proof system.

${tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
15.2645pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=30.52899pt\hbox{\kern
3.00003pt$\hyperlink{rule:p-ax}{\textup{{\small[p-ax]}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash p,p^{\bot}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=131.93665pt\hbox{\kern
3.00003pt$\hyperlink{rule:p-or}{\textup{{\small[p-or]}}}$}}}\hbox{\kern
47.37051pt\hbox{$\displaystyle\vdash p\lor p^{\bot}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\hskip 5.0pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip
0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
2.63885pt\hbox{$\displaystyle\penalty 1\vdots$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=12.77771pt\hbox{\kern
3.00003pt$\hyperlink{rule:p-rec}{\textup{{\small[p-rec]}}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\vdash\mathsf{t}$}}}}\hskip 5.0pt plus 1.0fil\penalty
2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=119.23238pt\hbox{\kern
3.00003pt$\hyperlink{rule:p-next}{\textup{{\small[p-next]}}}$}}}\hbox{\kern
50.72731pt\hbox{$\displaystyle\vdash\mathop{\circ}\mathsf{t}$}}}}\hskip 5.0pt
plus 1.0fil\penalty 2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern
0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=463.3786pt\hbox{\kern
3.00003pt$\hyperlink{rule:p-and}{\textup{{\small[p-and]}}}$}}}\hbox{\kern
200.3137pt\hbox{$\displaystyle\vdash(p\lor
p^{\bot})\land\mathop{\circ}\mathsf{t}$}}}}\hskip 5.0pt plus 1.0fil\penalty
2$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=492.59743pt\hbox{\kern
3.00003pt$\hyperlink{rule:p-rec}{\textup{{\small[p-rec]}}}$}}}\hbox{\kern
204.67543pt\hbox{$\displaystyle\vdash\nu\mathsf{X}.(p\lor
p^{\bot})\land\mathop{\circ}\mathsf{X}$}}}}$

Since the proof system is correct, we deduce
$\llbracket\mathsf{t}\rrbracket=\mathcal{E}^{\omega}$. Thus,
$M_{\mathsf{t}}(u)=\mathsf{yes}$ for any $u\in\mathcal{E}^{\star}$.

###  0.A.3 Proof of Proposition 8

######  Definition 9 (Neg Semantics)

Let $w\in\mathcal{E}^{\omega}$. The negative semantics of a term is
inductively defined by the following inference system.

$\displaystyle{\vbox{\hbox{\hbox{\small\small{nc-
bot}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
17.30452pt\vbox{\vbox{}\hbox{\hskip-17.30452pt\hbox{\hbox{$\displaystyle\displaystyle
w\not\mathrel{\models}_{C}\bot$}}}}}}$}}}\penalty 50\hskip 20.00003pt plus
0.5fil minus 5.0pt{\vbox{\hbox{\hbox{\small\small{nc-
prop}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
15.93124pt\vbox{\vbox{}\hbox{\hskip-15.93124pt\hbox{\hbox{$\displaystyle\displaystyle
w\not\mathrel{\models}_{C}p$}}}}}}$}}}~{}w_{0}\not\in\langle\\!\langle
p\rangle\\!\rangle\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{nc-
coprop}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
18.10902pt\vbox{\vbox{}\hbox{\hskip-18.10902pt\hbox{\hbox{$\displaystyle\displaystyle
w\not\mathrel{\models}_{C}p^{\bot}$}}}}}}$}}}~{}w_{0}\in\langle\\!\langle
p\rangle\\!\rangle\penalty 50\hskip 20.00003pt plus 0.5fil minus
5.0pt{\vbox{\hbox{\hbox{\small\small{nc-
or}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
40.74792pt\vbox{\hbox{\hskip-40.74792pt\hbox{\hbox{$\displaystyle\displaystyle
w\not\mathrel{\models}_{C}\mathsf{t}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle
w\not\mathrel{\models}_{C}\mathsf{s}$}}}}\vbox{}}}\over\hbox{\hskip
20.66563pt\vbox{\vbox{}\hbox{\hskip-20.66563pt\hbox{\hbox{$\displaystyle\displaystyle
w\not\mathrel{\models}_{C}\mathsf{t}\lor\mathsf{s}$}}}}}}$}}}\penalty-10000\hskip
20.00003pt plus 0.5fil minus 5.0pt{\vbox{\hbox{\hbox{\small\small{nc-
and-l}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
15.36008pt\vbox{\hbox{\hskip-15.36006pt\hbox{\hbox{$\displaystyle\displaystyle
w\not\mathrel{\models}_{C}\mathsf{t}$}}}\vbox{}}}\over\hbox{\hskip
20.66563pt\vbox{\vbox{}\hbox{\hskip-20.66563pt\hbox{\hbox{$\displaystyle\displaystyle
w\not\mathrel{\models}_{C}\mathsf{t}\land\mathsf{s}$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt{\vbox{\hbox{\hbox{\small\small{nc-
and-r}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
15.38785pt\vbox{\hbox{\hskip-15.38783pt\hbox{\hbox{$\displaystyle\displaystyle
w\not\mathrel{\models}_{C}\mathsf{s}$}}}\vbox{}}}\over\hbox{\hskip
20.66563pt\vbox{\vbox{}\hbox{\hskip-20.66563pt\hbox{\hbox{$\displaystyle\displaystyle
w\not\mathrel{\models}_{C}\mathsf{t}\land\mathsf{s}$}}}}}}$}}}\penalty
50\hskip 20.00003pt plus 0.5fil minus 5.0pt{\vbox{\hbox{\hbox{\small\small{nc-
next}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
18.93785pt\vbox{\hbox{\hskip-18.93785pt\hbox{\hbox{$\displaystyle\displaystyle
w_{\geq 1}\not\mathrel{\models}_{C}\mathsf{t}$}}}\vbox{}}}\over\hbox{\hskip
17.86008pt\vbox{\vbox{}\hbox{\hskip-17.86008pt\hbox{\hbox{$\displaystyle\displaystyle
w\not\mathrel{\models}_{C}\mathop{\circ}\mathsf{t}$}}}}}}$}}}\penalty 50\hskip
20.00003pt plus 0.5fil minus 5.0pt{\vbox{\hbox{\hbox{\small\small{nc-
rec}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
38.56609pt\vbox{\hbox{\hskip-38.56607pt\hbox{\hbox{$\displaystyle\displaystyle
w\not\mathrel{\models}_{C}\mathsf{t}\\{\nu
X.\mathsf{t}/X\\}$}}}\vbox{}}}\over\hbox{\hskip
23.47581pt\vbox{\vbox{}\hbox{\hskip-23.4758pt\hbox{\hbox{$\displaystyle\displaystyle
w\not\mathrel{\models}_{C}\nu X.\mathsf{t}$}}}}}}$}}}$

###### Theorem 0.A.2

Let $\mathsf{t}$ be a term of the calculus. Then
$\llbracket\mathsf{t}\rrbracket\in\mathbb{S}$.

###### Proof

By Definition 3 we have to prove that for each $w\in\mathcal{E}^{\omega}$ such
that $w\not\mathrel{\models}_{C}\mathsf{t}$ there exists $u\triangleleft
w\in\mathcal{E}^{\star}$ such that for all $w^{\prime}\in\mathcal{E}^{\omega}$
$uw^{\prime}\not\mathrel{\models}_{C}\mathsf{t}$. We reason by induction on
the judgment $w\not\mathrel{\models}_{C}\mathsf{t}$.

Case [nc-bot]. Then $\mathsf{t}=\bot$. We conclude taking any prefix $u$ and
by applying [nc-bot].

Case [nc-prop]. Then $\mathsf{t}=p$ and $w_{0}\not\in\langle\\!\langle
p\rangle\\!\rangle$. We conclude taking
$u\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}w_{0}$ and applying [nc-
prop].

Case [nc-coprop]. Then $\mathsf{t}=p^{\bot}$ and $w_{0}\in\langle\\!\langle
p\rangle\\!\rangle$. We conclude taking
$u\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}w_{0}$ and applying [nc-
coprop].

Case [nc-or]. Then $\mathsf{t}=\mathsf{t}^{\prime}\lor\mathsf{s}$,
$w\not\mathrel{\models}_{C}\mathsf{t}^{\prime}$ and
$w\not\mathrel{\models}_{C}\mathsf{s}$. Using the induction hypotheses we
deduce that there exist $u_{\mathsf{t}^{\prime}}\triangleleft w$ and
$u_{\mathsf{s}}\triangleleft w$ that negatively determine
$\mathsf{t}^{\prime}$ and $\mathsf{s}$ respectively. It must be the case that
either $u_{\mathsf{t}^{\prime}}\triangleleft u_{\mathsf{s}}$ or
$u_{\mathsf{s}}\triangleleft u_{\mathsf{t}^{\prime}}$. In the former case we
take $u\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}u_{\mathsf{s}}$ while
in the second $u\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}u_{\mathsf{t}^{\prime}}$. We conclude applying [nc-or].

Case [nc-and-l]. Then $\mathsf{t}=\mathsf{t}^{\prime}\land\mathsf{s}$ and
$w\not\mathrel{\models}_{C}\mathsf{t}^{\prime}$. Using the induction
hypothesis we deduce that there exists $u_{\mathsf{t}^{\prime}}\triangleleft
w$ that negatively determines $\mathsf{t}^{\prime}$. We conclude taking
$u\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}u_{\mathsf{t}^{\prime}}$
and applying [nc-and-l].

Case [nc-and-r]. Analogous to the previous case.

Case [nc-next]. Then $\mathsf{t}=\mathop{\circ}\mathsf{s}$ and $w_{\geq
1}\not\mathrel{\models}_{C}\mathsf{s}$. Using the induction hypothesis we
deduce that there exists $u_{\mathsf{s}}\triangleleft w_{\geq 1}$ that
negatively determines $\mathsf{s}$. We conclude taking
$u\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}w_{0}u_{\mathsf{s}}$ and
applying [nc-next].

Case [nc-rec]. Then $\mathsf{t}=\nu X.\mathsf{s}$ and
$w\not\mathrel{\models}_{C}\mathsf{s}\\{\nu X.\mathsf{s}/X\\}$. Using the
induction hypothesis we deduce that there exists $u_{\mathsf{s}}$ that
negatively determines $\mathsf{s}\\{\nu X.\mathsf{s}/X\\}$. We conclude taking
$u\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}u_{\mathsf{s}}$ and
applying [nc-rec].

###  0.A.4 Proof of Proposition 9

######  Definition 10 (Rank of a term)

Let $\mathsf{t}$ be a LT$\nu$ term. The function $\mathcal{R}(\mathsf{t})$
computes the _rank_ of $\mathsf{t}$.

$\begin{array}[]{lcllcl}\mathcal{R}(\top)&=&0&\qquad\mathcal{R}(\bot)&=&0\\\
\mathcal{R}(p)&=&0&\qquad\mathcal{R}(p^{\bot})&=&0\\\
\mathcal{R}(\mathsf{t}\land\mathsf{s})&=&1+\max\\{\mathcal{R}(\mathsf{t}),\mathcal{R}(\mathsf{s})\\}&\qquad\mathcal{R}(\mathsf{t}\lor\mathsf{s})&=&1+\max\\{\mathcal{R}(\mathsf{t}),\mathcal{R}(\mathsf{s})\\}\\\
\mathcal{R}(\nu\mathsf{X}.\mathsf{t})&=&1+\mathcal{R}(\mathsf{t})&\qquad\mathcal{R}(\mathop{\circ}\mathsf{t})&=&0\end{array}$

Intuitively, $\mathcal{R}(\mathsf{t})$ measures the distance from $\mathsf{t}$
to the first subformula with shape $\top,\bot,p,p^{\bot}$ or
$\mathop{\circ}\mathsf{s}$. Note that the case $\mathcal{R}(\mathsf{X})$ is
ruled out by the _contractivity_ assumption on terms.

###### Lemma 7

Let $\mathsf{t}$ be a LT$\nu$ term. Then
$\mathcal{R}(\mathsf{t})=\mathcal{R}(\mathsf{t}\\{\mathsf{s}/\mathsf{X}\\})$
for any $\mathsf{s}$.

###### Proof

By induction on $\mathsf{t}$ and by cases on its shape.

Case $\mathsf{t}=\bot$, $\mathsf{t}=\top$, $\mathsf{t}=p$,
$\mathsf{t}=p^{\bot}$. We conclude
$\mathcal{R}(\mathsf{t})=\mathcal{R}(\mathsf{t}\\{\mathsf{s}/\mathsf{X}\\})=0$
since $\mathsf{X}\not\in fn(\mathsf{t})$.

Case $\mathsf{t}=\mathsf{t}_{1}\land\mathsf{t}_{2}$. Using the induction
hypotheses we deduce

  * •

$\mathcal{R}(\mathsf{t}_{1})=\mathcal{R}({\mathsf{t}_{1}}\\{\mathsf{s}/\mathsf{X}\\})$

  * •

$\mathcal{R}(\mathsf{t}_{2})=\mathcal{R}({\mathsf{t}_{2}}\\{\mathsf{s}/\mathsf{X}\\})$

Hence we deduce

$\max\\{\mathcal{R}(\mathsf{t}_{1}),\mathcal{R}(\mathsf{t}_{2})\\}=\max\\{\mathcal{R}({\mathsf{t}_{1}}\\{\mathsf{s}/\mathsf{X}\\}),\mathcal{R}({\mathsf{t}_{2}}\\{\mathsf{s}/\mathsf{X}\\})\\}$

We conclude
$\mathcal{R}(\mathsf{t})=\mathcal{R}(\mathsf{t}\\{\mathsf{s}/\mathsf{X}\\})$.

Case $\mathsf{t}=\mathsf{t}_{1}\lor\mathsf{t}_{2}$. Analogous to the previous
case.

Case $\mathsf{t}=\nu\mathsf{Y}.\mathsf{t}^{\prime}$ and
$\mathsf{X}\neq\mathsf{Y}$. Using the induction hypothesis we deduce
$\mathcal{R}(\mathsf{t}^{\prime})=\mathcal{R}({\mathsf{t}^{\prime}}\\{\mathsf{s}/\mathsf{X}\\})$.
We conclude
$\mathcal{R}(\mathsf{t})=\mathcal{R}(\mathsf{t}\\{\mathsf{s}/\mathsf{X}\\})$.

Case $\mathsf{t}=\mathop{\circ}\mathsf{s}$. We conclude
$\mathcal{R}(\mathsf{t})=\mathcal{R}(\mathsf{t}\\{\mathsf{s}/\mathsf{X}\\})=0$
by definition of $\mathcal{R}(\mathsf{t})$.

###### Lemma 8

Let $e\in\mathcal{E},w\in\mathcal{E}^{\omega}$ and $\mathsf{t}$ a LT$\nu$
term. Then $ew\mathrel{\models}_{C}\mathsf{t}$ implies
$\mathsf{t}\stackrel{{\scriptstyle e}}{{\rightarrow}}\mathsf{s}$ for some
$\mathsf{s}$ and $w\mathrel{\models}_{C}\mathsf{s}$.

###### Proof

By complete arithmetic induction on $\mathcal{R}(\mathsf{t})$ and by cases on
$ew\mathrel{\models}_{C}\mathsf{t}$.

Case $\mathcal{R}(\mathsf{t})=0$. Then it must be the case that
$ew\mathrel{\models}_{C}\mathsf{t}$ is the consequence of [c-top] or [c-prop]
or [c-coprop] or [c-next].

Case [c-top], [c-prop], [c-coprop]. Then we take
$\mathsf{s}\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}\top$ noting that
$\mathsf{t}\stackrel{{\scriptstyle e}}{{\rightarrow}}\top$ by either [r-top]
or [r-prop] or [r-coprop]. We conclude with one application of [c-top].

Case [c-next]. Then
$\mathsf{t}=\mathop{\circ}\mathsf{s}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{s}$ by [r-next] and
$w\mathrel{\models}_{C}\mathsf{s}$. There is nothing left to prove.

Case $\mathcal{R}(\mathsf{t})>0$. Then it must be the case that
$ew\mathrel{\models}_{C}\mathsf{t}$ is the consequence of [c-and] or [c-or-l]
or [c-or-r] or [c-rec].

Case [c-and]. Then
$\mathsf{t}=\mathsf{t}_{1}\land\mathsf{t}_{2},ew\mathrel{\models}_{C}\mathsf{t}_{1}$
and $ew\mathrel{\models}_{C}\mathsf{t}_{2}$. Note that
$\mathcal{R}(\mathsf{t}_{1})<\mathcal{R}(\mathsf{t})$ and
$\mathcal{R}(\mathsf{t}_{2})<\mathcal{R}(\mathsf{t})$. Using the induction
hypotheses we deduce that there exist $\mathsf{s}_{1},\mathsf{s}_{2}$ such
that

  * •

$\mathsf{t}_{1}\stackrel{{\scriptstyle e}}{{\rightarrow}}\mathsf{s}_{1}$ and
$w\mathrel{\models}_{C}\mathsf{s}_{1}$

  * •

$\mathsf{t}_{2}\stackrel{{\scriptstyle e}}{{\rightarrow}}\mathsf{s}_{2}$ and
$w\mathrel{\models}_{C}\mathsf{s}_{2}$

We conclude taking $\mathsf{s}\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\mathsf{s}_{1}\land\mathsf{s}_{2}$ and applying [r-and] and
[c-and].

Case [c-or-l]. Then $\mathsf{t}=\mathsf{t}_{1}\lor\mathsf{t}_{2}$ and
$ew\mathrel{\models}_{C}\mathsf{t}_{1}$. Note that
$\mathcal{R}(\mathsf{t}_{1})<\mathcal{R}(\mathsf{t})$. Using the induction
hypothesis we deduce that there exists $\mathsf{s}_{1}$ such that
$\mathsf{t}_{1}\stackrel{{\scriptstyle e}}{{\rightarrow}}\mathsf{s}_{1}$ and
$w\mathrel{\models}_{C}\mathsf{s}_{1}$. We conclude taking
$\mathsf{s}\stackrel{{\scriptstyle\text{\tiny\sf def}}}{{=}}\mathsf{s}_{1}$
and applying [r-or-l].

Case [c-or-r]. Analogous to the previous case.

Case [c-rec]. Then $\mathsf{t}=\nu\mathsf{X}.\mathsf{t}^{\prime}$ and
$ew\mathrel{\models}_{C}\mathsf{t}^{\prime}\\{\nu\mathsf{X}.\mathsf{t}^{\prime}/\mathsf{X}\\}$.
Note that $\mathcal{R}(\mathsf{t}^{\prime})<\mathcal{R}(\mathsf{t})$. From
Lemma 7 we deduce
$\mathcal{R}(\mathsf{t}^{\prime})=\mathcal{R}(\mathsf{t}^{\prime}\\{\nu\mathsf{X}.\mathsf{t}^{\prime}/\mathsf{X}\\})<\mathcal{R}(\mathsf{t})$.
Using the induction hypothesis we deduce that there exists
$\mathsf{s}^{\prime}$ such that
$\mathsf{t}^{\prime}\\{\nu\mathsf{X}.\mathsf{t}^{\prime}/\mathsf{X}\\}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{s}^{\prime}$ and
$w\mathrel{\models}_{C}\mathsf{s}^{\prime}$. We conclude taking
$\mathsf{s}\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}\mathsf{s}^{\prime}$ and applying [r-rec].

###### Theorem 0.A.3

Let $w\in\mathcal{E}^{\omega}$ and $\mathsf{t}$ a LT$\nu$ term. Then
$w\mathrel{\models}_{C}\mathsf{t}$ implies $\mathsf{t}\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$.

###### Proof

The proof is by coinduction. Let $S=\\{(ew,\mathsf{t})\mid
ew\mathrel{\models}_{C}\mathsf{t}\\}$, we prove that $S$ is _consistent_ with
respect to $\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\omega}$. In particular,
if $ew\mathrel{\models}_{C}\mathsf{t}$ we have to prove that there exists
$\mathsf{s}$ such that $\mathsf{t}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{s}$ and $w\mathrel{\models}_{C}\mathsf{s}$. We
conclude applying Lemma 8.

###### Lemma 9

Let $w\in\mathcal{E}^{\omega}$ and $\mathsf{t},\mathsf{s}$ LT$\nu$ terms. Then
$\mathsf{t}\land\mathsf{s}\stackrel{{\scriptstyle w}}{{\Rightarrow}}_{\omega}$
implies, $\mathsf{t}\stackrel{{\scriptstyle w}}{{\Rightarrow}}_{\omega}$ and
$\mathsf{s}\stackrel{{\scriptstyle w}}{{\Rightarrow}}_{\omega}$.

###### Proof

We prove that $\mathsf{t}\land\mathsf{s}\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$ implies $\mathsf{t}\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$. The other proof is analogous. The proof is by
coinduction. Let
$S=\\{(\mathsf{t},ew)\mid\exists\mathsf{s}.\mathsf{t}\land\mathsf{s}\stackrel{{\scriptstyle
ew}}{{\Rightarrow}}_{\omega}\\}$. We prove that $S$ is _consistent_ with
respect to $\stackrel{{\scriptstyle}}{{\Rightarrow}}_{\omega}$.

From [r-and] we deduce that there exist
$\mathsf{t}^{\prime},\mathsf{s}^{\prime}$ such that

  * •

$\mathsf{t}\land\mathsf{s}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{t}^{\prime}\land\mathsf{s}^{\prime}$

  * •

$\mathsf{t}\stackrel{{\scriptstyle e}}{{\rightarrow}}\mathsf{t}^{\prime}$ and
$\mathsf{s}\stackrel{{\scriptstyle e}}{{\rightarrow}}\mathsf{s}^{\prime}$

  * •

$\mathsf{t}^{\prime}\land\mathsf{s}^{\prime}\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$

We have to prove $(\mathsf{t}^{\prime},w)\in S$. We conclude by observing that
there exists $\mathsf{s}^{\prime}$ such that
$\mathsf{t}^{\prime}\land\mathsf{s}^{\prime}\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$.

###### Theorem 0.A.4

Let $w\in\mathcal{E}^{\omega}$ and $\mathsf{t}$ a LT$\nu$ term. Then
$\mathsf{t}\stackrel{{\scriptstyle w}}{{\Rightarrow}}_{\omega}$ implies
$w\mathrel{\models}_{C}\mathsf{t}$.

###### Proof

The proof is by coinduction. Let
$S=\\{(ew,\mathsf{t})\mid\mathsf{t}\stackrel{{\scriptstyle
ew}}{{\Rightarrow}}_{\omega}\\}$, we prove that $S$ is _consistent_ with
respect to $\mathrel{\models}_{C}$. We proceed by cases on $\mathsf{t}$.

Case $\mathsf{t}=\top$. Then $ew\mathrel{\models}_{C}\top$ by [c-top].

Case $\mathsf{t}=p$. From [r-prop] we deduce $p\stackrel{{\scriptstyle
e}}{{\rightarrow}}\top$ and $e\in\langle\\!\langle p\rangle\\!\rangle$. Then
$ew\mathrel{\models}_{C}p$ is the consequence of [c-prop].

Case $\mathsf{t}=p^{\bot}$. From [r-coprop] we deduce
$p^{\bot}\stackrel{{\scriptstyle e}}{{\rightarrow}}\top$ and
$e\not\in\langle\\!\langle p\rangle\\!\rangle$. Then
$ew\mathrel{\models}_{C}p^{\bot}$ is the consequence of [c-coprop].

Case $\mathsf{t}=\mathsf{t}_{1}\land\mathsf{t}_{2}$. From [r-and] we deduce
that there exist $\mathsf{s}_{1},\mathsf{s}_{2}$ such that

  * •

$\mathsf{t}_{1}\land\mathsf{t}_{2}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{s}_{1}\land\mathsf{s}_{2}$

  * •

$\mathsf{t}_{1}\stackrel{{\scriptstyle e}}{{\rightarrow}}\mathsf{s}_{1}$ and
$\mathsf{t}_{2}\stackrel{{\scriptstyle e}}{{\rightarrow}}\mathsf{s}_{2}$

  * •

$\mathsf{s}_{1}\land\mathsf{s}_{2}\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$

Then $ew\mathrel{\models}_{C}\mathsf{t}_{1}\land\mathsf{t}_{2}$ is the
consequence of [c-and]. We have to prove
$\mathsf{t}_{1}\stackrel{{\scriptstyle ew}}{{\Rightarrow}}_{\omega}$ and
$\mathsf{t}_{1}\stackrel{{\scriptstyle ew}}{{\Rightarrow}}_{\omega}$. Using
Lemma 9 we deduce $\mathsf{s}_{1}\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$ and $\mathsf{s}_{2}\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$. We conclude observing that
$\mathsf{t}_{1}\stackrel{{\scriptstyle e}}{{\rightarrow}}\mathsf{s}_{1}$ and
$\mathsf{t}_{2}\stackrel{{\scriptstyle e}}{{\rightarrow}}\mathsf{s}_{2}$.

Case $\mathsf{t}=\mathsf{t}_{1}\lor\mathsf{t}_{2}$. Note that
$\mathsf{t}_{1}\lor\mathsf{t}_{2}$ can reduce with either [r-or-l] of
[r-or-r]. We consider the case in which [r-or-l] is used, the other one is
symmetric. From [r-or-l] we deduce that there exists $\mathsf{t}_{1}^{\prime}$
such that

  * •

$\mathsf{t}_{1}\lor\mathsf{t}_{2}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{t}_{1}^{\prime}$

  * •

$\mathsf{t}_{1}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{t}_{1}^{\prime}$

  * •

$\mathsf{t}_{1}^{\prime}\stackrel{{\scriptstyle w}}{{\Rightarrow}}_{\omega}$

Then it must be the case that
$ew\mathrel{\models}_{C}\mathsf{t}_{1}\lor\mathsf{t}_{2}$ is the consequence
of[c-or-l]. We have to prove that $\mathsf{t}_{1}\stackrel{{\scriptstyle
ew}}{{\Rightarrow}}_{\omega}$. The proof is straightforward since
$\mathsf{t}_{1}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{t}_{1}^{\prime}$ and
$\mathsf{t}_{1}^{\prime}\stackrel{{\scriptstyle w}}{{\Rightarrow}}_{\omega}$.

Case $\mathsf{t}=\nu\mathsf{X}.\mathsf{s}$. From [c-rec] we deduce that

  * •

$\nu\mathsf{X}.\mathsf{s}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{t}^{\prime}$

  * •

$\mathsf{s}\\{\nu\mathsf{X}.\mathsf{s}/\mathsf{X}\\}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{t}^{\prime}$

  * •

$\mathsf{t}^{\prime}\stackrel{{\scriptstyle w}}{{\Rightarrow}}_{\omega}$

Then $ew\mathrel{\models}_{C}\nu\mathsf{X}.\mathsf{s}$ is the consequence of
[c-rec]. We have to prove
$\mathsf{s}\\{\nu\mathsf{X}.\mathsf{s}/\mathsf{X}\\}\stackrel{{\scriptstyle
ew}}{{\Rightarrow}}_{\omega}$ The proof is straightforward since
$\mathsf{s}\\{\nu\mathsf{X}.\mathsf{s}/\mathsf{X}\\}\stackrel{{\scriptstyle
e}}{{\rightarrow}}\mathsf{t}^{\prime}$ and
$\mathsf{t}^{\prime}\stackrel{{\scriptstyle w}}{{\Rightarrow}}_{\omega}$.

Case $\mathsf{t}=\mathop{\circ}\mathsf{s}$. From [r-next] we deduce
$\mathop{\circ}\mathsf{s}\stackrel{{\scriptstyle e}}{{\rightarrow}}\mathsf{s}$
and $\mathsf{s}\stackrel{{\scriptstyle w}}{{\Rightarrow}}_{\omega}$. Then
$ew\mathrel{\models}_{C}\mathop{\circ}\mathsf{s}$ is the conclusion of
[c-next]. We have to prove that $\mathsf{s}\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$. There is nothing left to prove.

###  0.A.5 Proof of Theorem 4.2

Since it is always possible to provide a Büchi automaton starting from a
linear temporal logic formula such that the accepted language coincides with
the semantics of the formula, we propose an algorithm that acts directly on
Büchi automata. First we recall the definition of a Büchi automaton.

######  Definition 11 (Büchi Automaton)

A Büchi Automaton $\mathcal{A}$ is a tuple
$<\mathcal{Q},\Sigma,\mathcal{\delta},\mathcal{Q}_{0},\mathcal{F}>$ such that

  * •

$\mathcal{Q}$ is a finite set of states

  * •

$\Sigma$ is a finite set called alphabet

  * •

$\mathcal{\delta}:\mathcal{Q}\times\Sigma\rightarrow\wp(\mathcal{Q})$ is a
transition relation

  * •

$\mathcal{Q}_{0}\subseteq\mathcal{Q}$ is the set of initial states

  * •

$\mathcal{F}\subseteq\mathcal{Q}$ is the set of final states

We use $q$ to denote an element of $\mathcal{Q}$ and we denote
$\mathcal{L}(\mathcal{A})$ the language accepted by the automaton
$\mathcal{A}$. We fix $\Sigma=\wp_{F}^{*}(AP)$ and we use $\alpha,\beta$ to
denote an element of $\Sigma$. We write
$q\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}q^{\prime}$ for
$q^{\prime}\in\mathcal{\delta}(q,\alpha)$. We write $q\stackrel{{\scriptstyle
u}}{{\Rightarrow}}_{*}q^{\prime}$ when $q$ reduces in finite steps to
$q^{\prime}$ according to $u$. We write $q\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$ when $q$ reduces infinitely many times according
to $w$ (coinductively defined as for Definition 8). $u$ and $w$ denote
respectively finite and infinite sequence of elements of $\Sigma$.
$w\in\mathcal{L}(\mathcal{A})$ if $q\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$ for some $q\in\mathcal{Q}_{0}$ and such that the
reduction passes through some final state in $\mathcal{F}$ infinitely often.

######  Property 1 (Assumptions)

We assume that input NBAs satisfy the following properties:

  * •

For each $q\in\mathcal{F}$, $q$ lies in a cycle

  * •

For all $q\in\mathcal{Q}$, $q\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{*}q^{\prime}$ implies $q^{\prime}\stackrel{{\scriptstyle
w^{\prime}}}{{\Rightarrow}}_{*}q_{f}$ for some
$q_{f}\in\mathcal{F},w,w^{\prime}$

######  Lemma 10 (Emptyness)

Let
$\mathcal{A}=<\mathcal{Q},\Sigma,\mathcal{\delta},\mathcal{Q}_{0},\mathcal{F}>$.
According to the assumption we make, we obtain
$\mathcal{L}(\mathcal{A})=\emptyset$ iff $\mathcal{Q}=\emptyset$.

###### Proof

The _if_ part is obvious. To prove that if
$\mathcal{L}(\mathcal{A})=\emptyset$ then $\mathcal{Q}=\emptyset$ it is
sufficient to observe that in such an automaton either the paths (from an
initial state) do not reach some final state or some final state in reachable
but it does not belong to a cycle. Such kind of NBAs are ruled out by Property
1.

The algorithm to encode a Büchi automaton into a LT$\nu$ term is described in
Algorithm 1. Next, we show that such encoding produces the safety
approximation of the property described by the input automaton.

Algorithm 1 Encoding

1:

2:Let
$\mathcal{A}=<\mathcal{Q},\Sigma,\mathcal{\delta},\mathcal{Q}_{0},\mathcal{F}>$

3:Assume a variable $\mathsf{X}_{q}$ for each $q\in\mathcal{Q}$

4:

5:procedure $T$($q,S$)

6: if $q\in S$ then $X_{q}$

7: else

8:
$\nu\mathsf{X}_{q}.\lor\\{$$T$($\alpha$)$\land\mathop{\circ}$$T$($q^{\prime},S\cup\\{q\\}$)$\mid\alpha\in\Sigma,q^{\prime}\in\mathcal{\delta}(q,\alpha)\\}$

9:

10:$T$($\alpha$) = $\land\\{p\mid p\in\alpha\\}\land\\{p^{\bot}\mid
p\not\in\alpha\\}$

11:$T$($\mathcal{A}$) = $\lor\\{$$T$($q,\emptyset$)$\mid
q\in\mathcal{Q}_{0}\\}$

Let $\mathcal{A}$ be a Büchi automaton satisfying Property 1. We want to prove
that

  * •

$\Gamma_{\mathbb{S}}(\mathcal{L}(\mathcal{A}))\subseteq\llbracket
T(\mathcal{A})\rrbracket$ (Theorem 0.A.5)

  * •

$\llbracket
T(\mathcal{A})\rrbracket\subseteq\Gamma_{\mathbb{S}}(\mathcal{L}(\mathcal{A}))$
(Theorem 0.A.6)

First, we define the predicate $\\_\vdash\\_\mapsto\\_$.

###### Definition 12

Let $\mathcal{A}=<\mathcal{Q},\Sigma,\mathcal{\delta},\\_,\\_>$. We consider
the inductive interpretation of the following inference system that derives
judgments of the form $S\vdash q\mapsto\mathsf{t}$ where $S$ is a set of
states, $q\in\mathcal{Q}$ and $\mathsf{t}$ a LT$\nu$ term.

$\displaystyle{\vbox{\hbox{\hbox{\small\small{drv-
var}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip 0.0pt\vbox{\hbox{\hskip
0.0pt\hbox{\hbox{$\displaystyle\displaystyle\mathstrut$}}}\vbox{}}}\over\hbox{\hskip
18.08817pt\vbox{\vbox{}\hbox{\hskip-18.08817pt\hbox{\hbox{$\displaystyle\displaystyle
S\vdash q\mapsto\mathsf{X}_{q}$}}}}}}$}}}~{}q\in S\penalty 50\hskip 20.00003pt
plus 0.5fil minus 5.0pt{\vbox{\hbox{\hbox{\small\small{drv-
rec}}}\hbox{$\displaystyle\displaystyle{\hbox{\hskip
78.55167pt\vbox{\hbox{\hskip-78.55165pt\hbox{\hbox{$\displaystyle\displaystyle\forall\alpha,q^{\prime}.\alpha\in\Sigma,q^{\prime}\in\mathcal{\delta}(q,\alpha).S\cup\\{q\\}\vdash
q^{\prime}\mapsto\mathsf{t}_{q^{\prime}}^{\alpha}$}}}\vbox{}}}\over\hbox{\hskip
101.69975pt\vbox{\vbox{}\hbox{\hskip-101.69975pt\hbox{\hbox{$\displaystyle\displaystyle
S\vdash
q\mapsto\nu\mathsf{X}_{q}.\lor\\{T(\alpha)\land\mathop{\circ}\mathsf{t}_{q^{\prime}}^{\alpha}\mid\alpha,q^{\prime}.\alpha\in\Sigma,q^{\prime}\in\mathcal{\delta}(q,\alpha)\\}$}}}}}}$}}}$

###### Lemma 11

Let $\mathcal{A}$ be a Büchi automaton, $q$ one of its states and $S$ a set of
states. Then $S\vdash q\mapsto T(q,S)$.

###### Proof

By induction over $T(\\_,\\_)$ and applying [drv-var] as soon as possible.

######  Lemma 12 (Weakening)

Let $q$ be a state of an automaton, $\mathsf{t}$ a LT$\nu$ term and
$S,S^{\prime}$ two sets of states. If $S\vdash q\mapsto\mathsf{t}$ then $S\cup
S^{\prime}\vdash q\mapsto\mathsf{t}$.

###### Proof

By induction over $S\vdash q\mapsto\mathsf{t}$.

###### Lemma 13

Let $q,q^{\prime}$ be states of an automaton, $\mathsf{t},\mathsf{t}^{\prime}$
LT$\nu$ terms and $S$ a set of states. If $S\cup\\{q\\}\vdash
q^{\prime}\mapsto\mathsf{t}^{\prime}$ and $S\vdash q\mapsto\mathsf{t}$, then
$S\vdash q^{\prime}\mapsto\mathsf{t}^{\prime}\\{\mathsf{t}/\mathsf{X}_{q}\\}$.

###### Proof

By induction on $S\cup\\{q\\}\vdash q^{\prime}\mapsto\mathsf{t}^{\prime}$ and
using Lemma 12.

Case [drv-var] and $q\in S$. Then
$\mathsf{t}^{\prime}=\mathsf{X}_{q^{\prime}}$ and $S\vdash
q^{\prime}\mapsto\mathsf{t}^{\prime}\\{\mathsf{t}/\mathsf{X}_{q}\\}$ since
$\mathsf{X}_{q}\not\in fn(\mathsf{X}_{q^{\prime}})$.

Case [drv-var] and $q=q^{\prime}$. Then $\mathsf{t}^{\prime}=\mathsf{X}_{q}$
and $\mathsf{t}^{\prime}\\{\mathsf{t}/\mathsf{X}_{q}\\}=\mathsf{t}$. There is
nothing left to prove.

Case [drv-rec]. Then

  * •

$\mathsf{t}^{\prime}=\nu\mathsf{X}_{q^{\prime}}.\lor\\{T(\alpha)\land\mathop{\circ}\mathsf{t}_{q^{\prime\prime}}^{\alpha}\mid\alpha,q^{\prime\prime}.\alpha\in\Sigma,q^{\prime\prime}\in\mathcal{\delta}(q^{\prime},\alpha)\\}$

  * •

$\forall\alpha,q^{\prime\prime}.\alpha\in\Sigma,q^{\prime\prime}\in\mathcal{\delta}(q^{\prime},\alpha).S\cup\\{q,q^{\prime}\\}\vdash
q^{\prime\prime}\mapsto\mathsf{t}_{q^{\prime\prime}}^{\alpha}$

Using Lemma 12 we deduce $S\cup\\{q^{\prime}\\}\vdash q\mapsto\mathsf{t}$.
Using the induction hypotheses we deduce
$\forall\alpha,q^{\prime\prime}.\alpha\in\Sigma,q^{\prime\prime}\in\mathcal{\delta}(q^{\prime},\alpha).S\cup\\{q^{\prime}\\}\vdash
q^{\prime\prime}\mapsto\mathsf{t}_{q^{\prime\prime}}^{\alpha}\\{\mathsf{t}/\mathsf{X}_{q}\\}$.
We conclude applying [drv-rec].

###### Lemma 14

Let $\mathcal{A}$ be a Büchi automaton, $q,q^{\prime}$ two of its states and
$\mathsf{t}$ LT$\nu$ term. If
$q\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}q^{\prime}$ for some
$\alpha\in\Sigma$ and $\emptyset\vdash q\mapsto\mathsf{t}$ then
$\mathsf{t}\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}\top\land\top\land\dots\land\top\land\mathsf{t}^{\prime}$
for some $\mathsf{t}^{\prime}$ such that $\emptyset\vdash
q^{\prime}\mapsto\mathsf{t}^{\prime}$.

###### Proof

First, we prove that, if
$q\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}q^{\prime}$ for some $\alpha$,
then there exists $\mathsf{t}^{\prime}$ such that
$\mathsf{t}\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}\top\land\top\land\dots\land\mathsf{t}^{\prime}$
such that $\\{q\\}\vdash q^{\prime}\mapsto\mathsf{t}^{\prime}$.

It must be the case that $\emptyset\vdash q\mapsto\mathsf{t}$ is the
consequence of [drv-rec]. Hence, we deduce

  * •

$\mathsf{t}=\nu\mathsf{X}_{q}.\lor\\{T(\beta)\land\mathop{\circ}\mathsf{t}_{q^{\prime}}^{\beta}\mid\beta,q^{\prime}.\beta\in\Sigma,q^{\prime}\in\mathcal{\delta}(q,\beta)\\}$

  * •

$\forall\beta,q^{\prime}.\beta\in\Sigma,q^{\prime}\in\mathcal{\delta}(q,\beta).\\{q\\}\vdash
q^{\prime}\mapsto\mathsf{t}_{q^{\prime}}^{\beta}$

It is easy to see that
$\mathsf{t}\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}\top\land\top\land\dots\land\mathsf{t}_{q^{\prime}}^{\alpha}\\{\mathsf{t}/\mathsf{X}_{q}\\}$
by applying [r-rec], [r-or-l], [r-or-r], [r-next], [r-prop] and [r-coprop].

Now we have to prove that $\emptyset\vdash
q^{\prime}\mapsto\mathsf{t}_{q^{\prime}}^{\alpha}\\{\mathsf{t}/\mathsf{X}_{q}\\}$.

We conclude using Lemma 13 and $\\{q\\}\vdash
q^{\prime}\mapsto\mathsf{t}_{q^{\prime}}^{\alpha}$.

###### Lemma 15

Let $\mathcal{A}$ be a Büchi automaton satisfying Property 1 and $q$ one of
its states and $\mathsf{t}$ a LT$\nu$ term. If $\emptyset\vdash
q\mapsto\mathsf{t}$, then
$\mathcal{L}(q)\subseteq\llbracket\mathsf{t}\rrbracket$.

###### Proof

We have to prove that if $\emptyset\vdash q\mapsto\mathsf{t}$, then for all
$w\in\mathcal{E}^{\omega}$, $w\in\mathcal{L}(q)$ implies
$w\mathrel{\models}_{C}\mathsf{t}$. By Theorem 0.A.1 this is equivalent to
prove that $\mathsf{t}\stackrel{{\scriptstyle w}}{{\Rightarrow}}_{\omega}$.
The proof is by coinduction.

Let $S=\\{(\alpha w,\mathsf{t})\mid\emptyset\vdash q\mapsto\mathsf{t},\alpha
w\in\mathcal{L}(q)\\}$. We have to prove that $S$ is _consistent_ with respect
to $\mathrel{\models}_{C}$. In particular, we have to prove that
$\mathsf{t}\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}\mathsf{s}$ for some
$\mathsf{s}$ and $(w,\mathsf{s})\in S$.

From $\alpha w\in\mathcal{L}(q)$ we deduce

  * •

$q\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}q^{\prime}\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$ for some $q^{\prime}$

  * •

$w\in\mathcal{L}(q^{\prime})$

Using Lemma 14 we deduce
$\mathsf{t}\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}\top\land\top\land\dots\land\mathsf{s}$
and $\emptyset\vdash q^{\prime}\mapsto\mathsf{s}$. We conclude observing that
$\llbracket\top\land\top\land\dots\land
T_{q}(q^{\prime},\emptyset)\rrbracket=\llbracket
T_{q}(q^{\prime},\emptyset)\rrbracket$.

###### Lemma 16

Let Let $\mathcal{A}=<\\_,\\_,\\_,\mathcal{Q}_{0},\\_>$ be a Büchi automaton
satisfying Property 1. Then $\mathcal{L}(\mathcal{A})\subseteq\llbracket
T(\mathcal{A})\rrbracket$.

###### Proof

By definition, $\mathcal{L}(\mathcal{A})=\bigcup\\{\mathcal{L}(q)\mid
q\in\mathcal{Q}_{0}\\}$ and $\llbracket
T(\mathcal{A})\rrbracket=\bigcup\\{\llbracket T(q,\emptyset)\rrbracket\mid
q\in\mathcal{Q}_{0}\\}$. It is sufficient to prove that
$\mathcal{L}(q)\subseteq T(q,\emptyset)$ for all $q\in\mathcal{Q}_{0}$. We
conclude by applying Lemma 11 and Lemma 15.

###### Theorem 0.A.5

Let $\mathcal{A}$ be a Büchi automaton satisfying Property 1.

Then $\Gamma_{\mathbb{S}}(\mathcal{L}(\mathcal{A}))\subseteq\llbracket
T(\mathcal{A})\rrbracket$.

###### Proof

By definition, $\Gamma_{\mathbb{S}}(\mathcal{L}(\mathcal{A}))$ is the
intersection of all the safety properties that include
$\mathcal{L}(\mathcal{A})$. We conclude using Lemma 16 and Proposition 8.

###### Lemma 17

Let $q$ be a state of a Büchi automaton, $w\in\mathcal{E}^{\omega}$ and
$\mathsf{t}$ a LT$\nu$ term. If $\emptyset\vdash q\mapsto\mathsf{t}$ and
$w\mathrel{\models}_{C}\mathsf{t}$, then $q\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$.

###### Proof

By coinduction considering $S=\\{(\alpha w,q)\mid\emptyset\vdash
q\mapsto\mathsf{t},\alpha w\mathrel{\models}_{C}\mathsf{t}\\}$. We have to
prove that $q\stackrel{{\scriptstyle\alpha}}{{\rightarrow}}q^{\prime}$ for
some $q^{\prime}$ and $(w,q^{\prime})\in S$.

First, it must be the case that $\emptyset\vdash q\mapsto\mathsf{t}$ is the
consequence of [drv-rec]. Hence, we deduce

  * •

$\mathsf{t}=\nu\mathsf{X}_{q}.\lor\\{T(\beta)\land\mathop{\circ}\mathsf{t}_{q^{\prime}}^{\beta}\mid\beta,q^{\prime}.\beta\in\Sigma,q^{\prime}\in\mathcal{\delta}(q,\beta)\\}$

  * •

$\forall\beta,q^{\prime}.\beta\in\Sigma,q^{\prime}\in\mathcal{\delta}(q,\beta).\\{q\\}\vdash
q^{\prime}\mapsto\mathsf{t}_{q^{\prime}}^{\beta}$

Hence $q\stackrel{{\scriptstyle\beta}}{{\rightarrow}}q_{q^{\prime}}$ for some
$\beta$.

Then from $\alpha w\mathrel{\models}_{C}\mathsf{t}$ we deduce $\alpha
w\mathrel{\models}T(\beta)\land\mathop{\circ}\mathsf{t}_{q^{\prime}}^{\beta}\\{\mathsf{t}/\mathsf{X}_{q}\\}$
since [c-rec], [c-or-l], [c-or-r] have been applied to derive $\alpha
w\mathrel{\models}_{C}\mathsf{t}$. From [c-and] and [c-next] we deduce

  * •

$\alpha w\mathrel{\models}_{C}T(\beta)$

  * •

$\alpha
w\mathrel{\models}_{C}\mathop{\circ}\mathsf{t}_{q^{\prime}}^{\beta}\\{\mathsf{t}/\mathsf{X}_{q}\\}$
and
$w\mathrel{\models}_{C}\mathsf{t}_{q^{\prime}}^{\beta}\\{\mathsf{t}/\mathsf{X}_{q}\\}$

By definition, $T(\beta)=\land\\{p\in\beta\\}\land\\{p^{\bot}\mid
p\not\in\beta\\}$. From [c-and], [c-prop] and [c-coprop] we deduce

  * •

$\alpha w\mathrel{\models}_{C}p$ for all $p\in\beta$

  * •

$\alpha w\mathrel{\models}_{C}p^{\bot}$ for all $p\not\in\beta$

Hence we deduce $\alpha=\beta$.

Finally, from $\\{q\\}\vdash q^{\prime}\mapsto\mathsf{t}_{q^{\prime}}^{\beta}$
we deduce $\emptyset\vdash
q^{\prime}\mapsto\mathsf{t}_{q^{\prime}}^{\beta}\\{\mathsf{t}/\mathsf{X}_{q}\\}$.

We conclude $(w,q^{\prime})\in S$.

###### Theorem 0.A.6

Let $\mathcal{A}$ be a Büchi automaton satisfying Property 1.

Then $\llbracket
T(\mathcal{A})\rrbracket\subseteq\Gamma_{\mathbb{S}}(\mathcal{L}(\mathcal{A}))$.

###### Proof

If $w\mathrel{\models}_{C}T(\mathcal{A})$, then by definition of $T(\\_)$ it
must be the case that $w\mathrel{\models}_{C}T(q,\emptyset)$ for some $q$
initial state of $\mathcal{A}$.

From Lemma 11 we deduce $\emptyset\vdash q\mapsto T(q,\emptyset)$.

From Lemma 17 on $\emptyset\vdash q\mapsto T(q,\emptyset)$ and
$w\mathrel{\models}_{C}T(q,\emptyset)$ we deduce $q\stackrel{{\scriptstyle
w}}{{\Rightarrow}}_{\omega}$.

Hence, by Corollary 1 we have to prove that for each $u\triangleleft
w\in\mathcal{E}^{\star}$ there exists $w^{\prime}\in\mathcal{E}^{\omega}$ such
that $uw^{\prime}\in\mathcal{L}(\mathcal{A})$. This is always possible since
$\mathcal{A}$ satisfies Property 1.

###  0.A.6 Linear Temporal Logic

The semantics of LTL formulae is specified by a satisfation relation
$w,i\mathrel{\models}_{L}\phi$ (see Definition 14), stating that an infinite
trace $w$ satisfies the formula $\phi$ starting from the index
$i\in\mathbb{N}$. We write $w\mathrel{\models}_{L}\phi$ iff
$w,0\mathrel{\models}_{L}\phi$. The semantics of a formula $\phi$ is then
defined as $\llbracket\phi\rrbracket=\\{w\in\mathcal{E}^{\omega}\mid
w\mathrel{\models}_{L}\phi\\}$.

######  Definition 13 (LTL Syntax)

The set of _negation free_ LTL formulae is inductively defined by the grammar

$\phi,\psi\Coloneqq\top\mid\bot\mid p\mid
p^{\bot}\mid\phi\land\psi\mid\phi\lor\psi\mid\phi\mathrel{\mathcal{U}}\psi\mid\phi\mathrel{\mathcal{R}}\psi\mid\mathop{\circ}\phi$

We use the following abbreviations

$\begin{array}[]{lcl}\mathop{\Diamond}\phi&\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}&\top\mathrel{\mathcal{U}}\phi\\\
\mathop{\square}\phi&\stackrel{{\scriptstyle\text{\tiny\sf
def}}}{{=}}&\neg\mathop{\Diamond}\neg\phi\end{array}$

######  Definition 14 (LTL Semantics)

$\begin{array}[]{llcl}\hypertarget{rule:l-top}{\textup{{\small[l-top]}}}&w,i\mathrel{\models}_{L}\top\\\
\hypertarget{rule:l-prop}{\textup{{\small[l-prop]}}}&w,i\mathrel{\models}_{L}p&\iff&w_{i}\in\langle\\!\langle
p\rangle\\!\rangle\\\
\hypertarget{rule:l-coprop}{\textup{{\small[l-coprop]}}}&w,i\mathrel{\models}_{L}p^{\bot}&\iff&w_{i}\not\in\langle\\!\langle
p\rangle\\!\rangle\\\
\hypertarget{rule:l-and}{\textup{{\small[l-and]}}}&w,i\mathrel{\models}_{L}\phi\land\psi&\iff&w,i\mathrel{\models}_{L}\phi$
\bf{and} $w,i\mathrel{\models}_{L}\psi\\\
\hypertarget{rule:l-or}{\textup{{\small[l-or]}}}&w,i\mathrel{\models}_{L}\phi\lor\psi&\iff&w,i\mathrel{\models}_{L}\phi$
\bf{or} $w,i\mathrel{\models}_{L}\psi\\\
\hypertarget{rule:l-until}{\textup{{\small[l-until]}}}&w,i\mathrel{\models}_{L}\phi\mathrel{\mathcal{U}}\psi&\iff&\exists
k\geq i.w,k\mathrel{\models}_{L}\psi$ \bf{and} $\forall i\leq
l<k.w,l\mathrel{\models}_{L}\phi\\\
\hypertarget{rule:l-release}{\textup{{\small[l-release]}}}&w,i\mathrel{\models}_{L}\phi\mathrel{\mathcal{R}}\psi&\iff&\forall
k\geq i.w,k\mathrel{\models}_{L}\psi$ \bf{or} $\\\ &&&\exists k\geq
i.w,k\mathrel{\models}_{L}\phi$ \bf{and} $\forall i\leq l\leq
k.w,l\mathrel{\models}_{L}\psi\\\
\hypertarget{rule:l-next}{\textup{{\small[l-next]}}}&w,i\mathrel{\models}_{L}\mathop{\circ}\phi&\iff&w,i+1\mathrel{\models}_{L}\phi\end{array}$