# Decentralized LTL Enforcement

Florian Gallay Yliès Falcone Univ. Grenoble Alpes, CNRS, Inria, Grenoble INP,
Laboratoire d’Informatique de Grenoble, 38000 Grenoble, France
<EMAIL_ADDRESS>ylies.falcone@univ-grenoble-
alpes.fr

###### Abstract

We consider the runtime enforcement of Linear-time Temporal Logic formulas on
decentralized systems. A so-called enforcer is attached to each system
component and observes its local trace. Should the global trace violate the
specification, the enforcers coordinate to correct their local traces. We
formalize the decentralized runtime enforcement problem and define the
expected properties of enforcers, namely soundness, transparency and
optimality. We present two enforcement algorithms. In the first one, the
enforcers explore all possible local modifications to find the best global
correction. Although this guarantees an optimal correction, it forces the
system to synchronize and is more costly, computation and communication wise.
In the second one, each enforcer makes a local correction before
communicating. The reduced cost of this version comes at the price of the
optimality of the enforcer corrections.

##  1 Introduction

_Runtime enforcement_ (cf. [12]) consists in using runtime _enforcers_ to
ensure that a system does not violate a formal specification. The
specification is formalized for instance as a Linear-time Temporal Logic
($\mathit{LTL}$) formula [22]. Usually, the system is seen as a black box;
only its execution is observable (not its implementation). The execution is
abstracted as a sequence of events where each event contains the set of
relevant atomic propositions that hold on the system state. In (centralized)
enforcement, the sequence of events, called trace, is fed to one (central)
enforcer which transforms it and outputs a sequence that does not violate the
property. Usually, enforcers must be _sound_ , _transparent_ and _optimal_ ,
that is, their output trace should not violate the property, they should only
alter the execution if needed (i.e. to prevent property violations), and the
alteration should be minimal, respectively.

##### Motivation and challenges.

We consider decentralized systems, that is systems with no central observation
point nor authority but which are instead composed of several components, each
producing a local trace. Decentralized systems abound (e.g., multithreaded
processors, drone swarms, decentralized finance), some of which can have
safety critical properties to be ensured. It is desirable to define
enforcement techniques for decentralized systems so as to ensure their desired
properties. In the decentralized setting, enforcers should coordinate and
modify their local traces in such a way that the global trace respects the
enforced property.

##### Approach overview.

We address the problem of enforcing $\mathit{LTL}$ formulas on decentralized
systems. We start by defining the runtime enforcement problem in the
decentralized setting. Then, we define our enforcement algorithms, which
intuitively proceed as follows. Upon each new event $\sigma$ emitted by the
system, using $\mathit{LTL}$ expansion laws [22], we transform the formula to
be enforced at the current timestamp into what we refer to as a _temporal
disjunctive normal form_ , where each disjunct is composed of a present and
future obligation formula separated. The enforcers can then evaluate the
present obligations and alter their local observation if needed, i.e. when
outputting $\sigma$ would violate it. We note that our enforcers only evaluate
the present obligations in the disjuncts. After their evaluations with the
current event, a subset of the disjuncts will have their present obligations
different from $\bot$. Only the future obligations of these disjuncts are kept
for the next timestamp. This strategy spares the rewriting of the future
obligations of the discarded disjuncts. When $\sigma$ needs to be corrected,
the enforcers keep track of possible corrections of $\sigma$ and of the
associated formulas. As the system is decentralized, each enforcer can only
observe some atomic propositions of the system. Therefore, the enforcers
update the associated formulas with their local observations. Then, they send
it to another enforcer that will, in turn, do the same until the present
obligations are entirely evaluated. In our first algorithm, the formula is
evaluated with every possible event over the set of atomic propositions of the
system. This allows the enforcers to find the best possible correction if
needed. Through communication, they will naturally build the entire set of
possible events (the update can be seen as the exploration of a tree whose
leafs represent every possible assignment of the atomic propositions). After
each local update, each enforcer garbage collects the events that cannot be
extended to a viable correction of $\sigma$. Then, once the formula has been
entirely evaluated, the output event is so that soundness, transparency and
optimality are preserved. Our second algorithm proceeds similarly: the only
difference is that, instead of exploring the entire set of possible events,
each enforcer makes a local decision before sending the function to another
enforcer. This decision consists in choosing one event from the domain (w.r.t
_soundness_ and _transparency_ as well) and only sending this one in order to
prevent the exponential growth of the domain. In both cases, the formula to be
enforced in the next timestamp is built after choosing the output event. Since
enforcers make (optimal) local decisions, optimality of the global event is
not guaranteed by the second algorithm.

##### Related work.

This paper is at the intersection of two topics, namely _decentralized
monitoring_ and _runtime enforcement_. In decentralized monitoring (cf. [15]
for a survey), a lot of work has been done on the verification of systems for
several specifications languages such as $\mathit{LTL}$ and finite-state
automata. These research efforts differ mainly in the assumptions they make on
the underlying system. Some of the existing approaches to decentralized
monitoring are based on formula rewriting [23, 5, 2] (similarly to this
paper); the specification is usually represented as an $\mathit{LTL}$ formula
or in an extension of $\mathit{LTL}$ like MTL [24] and then rewritten and
simplified until a verdict can be emitted. Other approaches focus on
monitoring distributing systems and tackle the problem of global predicate
detection [19, 20] or of fault tolerance for monitors [4], that is, reaching
consensus with monitors that are subject to faults. In [9], the focus is on
monitoring decentralized specifications that is, a system in which multiple
specifications are given for separate parts of the system whereas all the
aforementioned work does decentralized monitoring on _centralized_
specification. Hence, the above approaches focus on determining a verdict but
do not consider at all 1) what should be done when the property is violated
and 2) what can be done to prevent violations. Runtime enforcement (cf. [12])
approaches try to prevent violations of specification during the execution of
system. This topic has also seen a lot of research efforts on modelling and
synthesizing enforcement monitors from several specifications formalisms for
discrete-time [13, 10, 6] and timed properties [21, 11, 14] and even
stochastic systems [18]. To the best of our knowledge, the only enforcement
approaches for decentralized systems are [17, 16], respectively tailored to
robotic swarms and artifact documents. However, in this paper, we formally
define the decentralized runtime enforcement problem in a generic manner and
provide two generic algorithms.

##### Outline.

We define preliminary notions in Sec. 2. Sec. 3 introduces the _decentralized
runtime enforcement_ problem. Sec. 4, defines the transformation of the
formula allowing the separation between the _present_ and _future_. Sec. 5
defines the datastructure used to encode the enforcer state. In Sec. 6, we
define how the enforcers evaluate the formula. Sec. 7 and 8 present and
compare our two algorithms. Details about some formula transformations are
given in Appendix A. A complete example of an execution of both algorithms is
given in Appendix B and proofs can be found in Appendix C.

##  2 Preliminary Notions

This section introduces some preliminary notions, and states the assumptions
of our approach.

##### Decentralized systems.

A decentralized system consists of $n$ components
$C_{\\_}1,\ldots,C_{\\_}{n}$. On each component $C_{\\_}i$, $i\in[1\ldots n]$,
we assume a local set of atomic propositions of interest $\mathit{AP}_{\\_}i$.
We also assume that $\\{\mathit{AP}_{\\_}1,\ldots,\mathit{AP}_{\\_}n\\}$ forms
a partition of $\mathit{AP}$.

##### Events and traces.

An event is a set of atomic propositions describing the system state. For an
event $\sigma\in 2^{AP}$, when $p\in\sigma$, it means that atomic proposition
$p$ holds on the system. We denote the set of all events $2^{AP}$ as $\Sigma$
and we call this set the alphabet. Similarly, $\Sigma_{\\_}i=2^{AP_{\\_}i}$
denotes the set of local events to component $C_{\\_}i$. Note that
$\Sigma\neq\bigcup_{\\_}{i\in[1,n]}\Sigma_{\\_}i$.

At runtime, each component $C_{\\_}i$ emits a _local trace_ $u_{\\_}i$ of
events from its local set of atomic propositions $\mathit{AP}_{\\_}i$. At any
timestamp $t$, the local trace is of the form $u_{\\_}i(1)\cdot
u_{\\_}i(2)\dotsb u_{\\_}i(t)$ with $\forall
t^{\prime}<t,u(t^{\prime})\in\Sigma_{\\_}i$ and where $u_{\\_}i(j)$ represents
the $j$-th local event of $C_{\\_}i$. The _global trace_ represents the
sequence of events emitted by the system as a whole. At any timestamp $t$, the
global trace is of the form: $u=u(1)\cdot u(2)\dotsb u(t)$ with $\forall
t^{\prime}<t,u(t^{\prime})\in\Sigma$ and where $u(j)$ represents the $j$-th
event emitted by the system. It is possible to build the global trace from the
local traces: $u=u_{\\_}1(1)\cup\dotsb\cup u_{\\_}n(1)\cdot
u_{\\_}1(2)\cup\dotsb\cup u_{\\_}n(2)\dotsb u_{\\_}1(t)\cup\dotsb\cup
u_{\\_}n(t)$ as well as the local traces from the global trace:
$u_{\\_}i=u(1)\cap AP_{\\_}i\dotsb u(t)\cap AP_{\\_}i$. The set of all finite
traces over an alphabet $\Sigma$ is denoted as $\Sigma^{*}$ whereas the set of
all infinite traces over $\Sigma$ is denoted as $\Sigma^{\omega}$. The suffix
of a (finite or infinite) trace starting at time t is $w^{t}=w(t)\cdot
w(t+1)\dotsb$. The set of all traces is denoted as
$\Sigma^{\infty}=\Sigma^{*}\cup\Sigma^{\omega}$.

To measure the differences between two events, we use a distance function that
returns the number of atomic propositions with different value between them.

######  Definition 1 (Distance between events)

Let $\sigma,\sigma^{\prime\prime}\in\Sigma$. Function
distance$:\Sigma\times\Sigma\times 2^{AP}\rightarrow\mathbb{N}$ is defined as
follows:
$\texttt{distance}(\sigma,\sigma^{\prime\prime},AP)=\\#\\{AP\cap(\sigma\cap\overline{\sigma^{\prime\prime}}\cup\overline{\sigma}\cap\sigma^{\prime\prime})\\}$.

Note that we cannot directly use the Hamming Distance because the events are
not represented as strings composed of the atomic propositions or their
negations, instead an atomic proposition that is equal to $\bot$ is not
included in the set.

##### Linear-time temporal logic on finite traces.

The specification of the expected behaviour of the system is formalized using
Linear-time Temporal Logic ($\mathit{LTL}$) [22] over the (global) set of
atomic propositions $\mathit{AP}$. We refer to the set of syntactically
correct $\mathit{LTL}$ formulas over $\mathit{AP}$ as $\mathit{LTL}$. We
assume the reader familiar with $\mathit{LTL}$ and its operators (Globally
(G), Eventually (F), …). We denote by $\vDash$ the usual semantic relation
between traces and formulas. We say that two formulas $\varphi_{\\_}1$ and
$\varphi_{\\_}2$ are semantically equivalent if for any $w\in\Sigma^{\infty}$,
$w\vDash\varphi_{\\_}1$ iff $w\vDash\varphi_{\\_}2$ and we denote this by
$\varphi_{\\_}1\equiv\varphi_{\\_}2$. In this paper, we use a finite-trace
semantics (from [3]). A finite trace $u$ evaluates to $\top$ (resp. $\bot$)
for $\varphi$ if all its infinite extensions satisfy (resp. do not satisfy)
$\varphi$. We denote this by $u\in good(\varphi)$ (resp. $u\in bad(\varphi)$).
In monitoring and evaluating formulas, we will need to refer to the atomic
propositions that have not been evaluated yet in a formula:
$\texttt{apFormula}(\varphi)\subseteq AP$ is the set of free atomic
propositions occurring on $\varphi$.

##### Normal forms.

To use the definition of literals, monomials and normal form with Linear-time
temporal logic, we extend them to cover temporal operators: A _literal_ is an
atomic proposition or the negation of an atomic proposition. A _monomial_ is a
conjunction of literals and/or of temporal operators applied to any formulas.
A formula is in _normal form_ if it only contains the operators $\vee,\wedge$
and $\neg$ and/or temporal operators (X, G, F, U, R) and if negations that are
not below a temporal operators are only applied to atomic propositions.
Finally, a formula is in _disjunctive normal form (DNF)_ if it is a
disjunction of monomials. We say that a formula is in _temporal disjunctive
normal form (TDNF)_ if it is in DNF and each monomial is of the form
$\varphi_{\\_}1\wedge\textsc{{X}}\varphi_{\\_}2$ where $\varphi_{\\_}1$ only
contains propositional logic operators (i.e. it represents a condition on the
present).

#####  map, fold and filter

We shall make use of functions map, fold and filter. Consider two arbitrary
types/sets $A$ and $B$. Function map takes as argument a function
$f:A\rightarrow B$ and a set $S$ containing elements of some type $A$. It then
returns the set $S^{\prime}=\\{f(s)\mid s\in S\\}$. Function filter takes as
argument a predicate $p$ over elements of $A$ and a set $S$ of elements from
$A$ and returns the subset of $S$ with elements that satisfy $p$. Function
fold takes as arguments a function $f:A\times B\rightarrow B$, a set $S$
containing elements of type $A$ and an element $b$ of type $B$. It is
inductively defined: if $S\neq\emptyset$, it returns
$\texttt{fold}(f,S\setminus s,f(s,b))$ (where $s\in S$). Otherwise, it returns
$b$.

##  3 Decentralized Runtime Enforcement

Let $i_{\\_}k\in\Sigma_{\\_}k^{*}$ (with $k\in[1\ldots n]$) be the local trace
of each component $C_{\\_}k$ and $i\in\Sigma^{*}$ the global trace obtained
from the union of the local traces. For $k\in[1\ldots n]$, enforcer $M_{\\_}k$
observes local trace $i_{\\_}k$. Similarly, let $o_{\\_}k\in\Sigma_{\\_}k^{*}$
be the local output trace of each enforcer and $o\in\Sigma^{*}$ the global
output trace obtained from the union of the local outputs. Our assumptions on
the system are as follows:

  * •

The specification is not equivalent to $\bot$.

  * •

The system cannot emit a new event until the previous one has been treated by
the enforcer.

  * •

An enforcer $M_{\\_}j$ can only read atomic propositions relevant to
$AP_{\\_}j$ and modify them.

  * •

All enforcers are capable to communicate with one another by exchanging
messages.

  * •

All exchanged messages are delivered reliably, in order, and with no
alteration.

  * •

Enforcers are not malicious, i.e., they do not exchange wrong informations.

Every time a new event $\sigma$ is emitted by the system, the enforcers
compute a set of events that respect the specification using their local
observations of $\sigma$. They will then choose to emit one of these events
and modify their local observations accordingly. We denote this event by
$E(\sigma)$. At time $t$, we have $E(i)=E(i(1))\cdot E(i(2))\dotsb E(i(t))=o$
and $E(i_{\\_}k)=E(i_{\\_}k(1))\cdot E(i_{\\_}k(2))\dotsb
E(i_{\\_}k(t))=o_{\\_}k$. Let $\varphi$ be the formula representing the
specification to be enforced of the system and $AP$ the set of atomic
propositions present in $\varphi$. We want to obtain online decentralized
enforcers so that if $\sigma\in bad(\varphi)$, then $E(\sigma)\not\in
bad(\varphi)$.

We define the constraints that should be satisfied by a decentralized enforcer
$E$.

######  Definition 2 (Soundness)

$\forall i\in\Sigma^{*},\ E(i)\not\in bad(\varphi)$

An enforcer is _sound_ if its output is not a bad prefix of the specification.

######  Definition 3 (Transparency)

$\forall i\in\Sigma^{*},\forall\sigma\in\Sigma,\ E(i)\cdot\sigma\not\in
bad(\varphi)\Rightarrow E(i\cdot\sigma)=E(i)\cdot\sigma$

An enforcer is _transparent_ if its input is modified only when it leads to a
violation of the specification. We also define the notion of _optimality_.

######  Definition 4 (Optimality)

${\forall i\in\Sigma^{*}},\ {\forall\sigma\in\Sigma},\
{\exists\sigma^{\prime}\in\Sigma},\
{(E(i\cdot\sigma)=E(i)\cdot\sigma^{\prime})}\wedge(\forall\sigma^{\prime\prime}\in\Sigma,\
\texttt{distance}(\sigma,\sigma^{\prime\prime},AP)<\texttt{distance}(\sigma,\sigma^{\prime},AP)\Rightarrow
E(i)\cdot\sigma^{\prime\prime}\in bad(\varphi))$

An enforcer is _optimal_ if it outputs the closest event to the input that
respects the property.

For the remainder of this paper, we will illustrate each part of the
subsequent enforcement algorithms on formula
$\phi=\neg(\textsc{{G}}a\vee\textsc{{F}}b)$. This example system has two
components $C_{\\_}1$ and $C_{\\_}2$ and therefore uses two enforcers
$M_{\\_}1$ and $M_{\\_}2$ with $AP_{\\_}1=\\{a\\}$ and $AP_{\\_}2=\\{b\\}$.
The event emitted by the system is $\sigma=\\{a\\}$ and the enforcer
$M_{\\_}1$ is doing the initialization (this is an arbitrary choice).

Also, for the remainder of this paper, unless specified otherwise,
$\sigma\in\Sigma$ represents the global event emitted by the system,
$E(\sigma)\in\Sigma$ denotes the event outputted by the enforcers and
$\varphi\in LTL$ represents the formula to be enforced. At timestamp 1,
$\varphi$ is equal to the specification formula $\varphi_{\\_}{init}$ and
then, at timestamp $t+1$, $\varphi$ is equal to $\varphi^{t+1}$, the formula
obtained at the end of the $t$-th timestamp.

##  4 Normalizing $\mathit{LTL}$ Formulas

We transform the formula into its Temporal Disjunctive Normal Form (TDNF) to
get a disjunction of monomials. To get this, we start by separating present
and future obligations in the formula as defined in Sec. 4.1 and then use an
algorithm given in Sec. 4.2 to transform the result of the previous
transformation into its DNF. These two operations applied one after the other
on the input formula yield the TDNF, in which each monomial represents a
logical model of the formula and is the conjunction of two sub-formulas: a
state formula (i.e. the present obligation) and a conjunction of temporal
operators (i.e. the future obligation).

###  4.1 Separating Present and Future Obligations

The enforcers determine whether or not there is a violation of the set of
properties by evaluating the corresponding formula with $\sigma$. To achieve
this, we use the expansion laws (as defined in [22]) in order to separate what
$\sigma$ needs to satisfy in the current timestamp, i.e. the present
obligations, from what needs to be satisfied in the future, i.e. the future
obligations. For example, to evaluate $\textsc{{G}}a$, we first need to
rewrite it as $a\wedge\textsc{{X}}(\textsc{{G}}a)$. We can clearly see after
rewriting that $a$ needs to be hold on the current event $\sigma$ and that
$\textsc{{G}}a$ has to hold in the future.

######  Definition 5 (Expansion function (rwT))

Let $\varphi,\varphi_{\\_}1,\varphi_{\\_}2\in\mathit{LTL}$. Function
rwT$:\mathit{LTL}\rightarrow\mathit{LTL}$ is inductively defined as follows:

$\displaystyle\texttt{rwT}(p)$ $\displaystyle=p,\ \text{for p}\in AP$
$\displaystyle\texttt{rwT}(\top)$ $\displaystyle=\top$
$\displaystyle\texttt{rwT}(\varphi_{\\_}1\vee\varphi_{\\_}2)$
$\displaystyle=\texttt{rwT}(\varphi_{\\_}1)\vee\texttt{rwT}(\varphi_{\\_}2)$
$\displaystyle\texttt{rwT}(\bot)$ $\displaystyle=\bot$
$\displaystyle\texttt{rwT}(\varphi_{\\_}1\wedge\varphi_{\\_}2)$
$\displaystyle=\texttt{rwT}(\varphi_{\\_}1)\wedge\texttt{rwT}(\varphi_{\\_}2)$
$\displaystyle\texttt{rwT}(\neg\varphi)$
$\displaystyle=\neg\texttt{rwT}(\varphi)$
$\displaystyle\texttt{rwT}(\varphi_{\\_}1\Rightarrow\varphi_{\\_}2)$
$\displaystyle=\texttt{rwT}(\varphi_{\\_}1)\Rightarrow\texttt{rwT}(\varphi_{\\_}2)$
$\displaystyle\texttt{rwT}(\textsc{{X}}\varphi)$
$\displaystyle=\textsc{{X}}\varphi$
$\displaystyle\texttt{rwT}(\varphi_{\\_}1\textsc{{U}}\varphi_{\\_}2)$
$\displaystyle=\texttt{rwT}(\varphi_{\\_}2)\vee(\texttt{rwT}(\varphi_{\\_}1)\wedge\textsc{{X}}(\varphi_{\\_}1\textsc{{U}}\varphi_{\\_}2))$
$\displaystyle\texttt{rwT}(\textsc{{G}}\varphi)$
$\displaystyle=\texttt{rwT}(\varphi)\wedge\textsc{{X}}(\textsc{{G}}\varphi)$
$\displaystyle\texttt{rwT}(\varphi_{\\_}1\textsc{{R}}\varphi_{\\_}2)$
$\displaystyle=\texttt{rwT}(\varphi_{\\_}2)\wedge(\texttt{rwT}(\varphi_{\\_}1)\vee\textsc{{X}}(\varphi_{\\_}1\textsc{{R}}\varphi_{\\_}2))$
$\displaystyle\texttt{rwT}(\textsc{{F}}\varphi)$
$\displaystyle=\texttt{rwT}(\varphi)\vee\textsc{{X}}(\textsc{{F}}\varphi)$

######  Example 1 (rwT)

Recall that $\phi=\neg(\textsc{{G}}a\vee\textsc{{F}}b)$. We have rwT($\phi$) =
$\neg(a\wedge\textsc{{X}}(\textsc{{G}}a)\vee
b\vee\textsc{{X}}(\textsc{{F}}b))=\phi^{\prime}$

###### Property 1

Any formula outputted by function rwT is semantically equivalent to the input
formula, that is $\forall\varphi\in\mathit{LTL},\
\varphi\equiv\texttt{rwT}(\varphi)$

###### Property 2

Let $\varphi\in\mathit{LTL}$. In the syntactic tree of
$\texttt{rwT}(\varphi)$, any temporal operator different from X is below a X
thanks to the expansion laws.

###  4.2 Transforming to Temporal Disjunctive Normal Form

A problem that arises now is knowing which formula has to be evaluated in the
future based on the current observation. For example, with $a\textsc{{U}}b$,
the formula to evaluate in the future will be either $\top$ or
$a\textsc{{U}}b$ depending on the values of $a$ and $b$ in the current event.

Each monomial of a formula in DNF represents one of its model. The
transformation to DNF gives, for each model, a formula of the form
$\varphi_{\\_}1\wedge\textsc{{X}}\varphi_{\\_}2$ where $\varphi_{\\_}1$ is a
conjunction of literals and $\varphi_{\\_}2$ is a conjunction of temporal
operators, that is, $\varphi_{\\_}1$ (resp. $\varphi_{\\_}2$) represents the
present obligation (resp. future obligation). Intuitively, if the present
obligations of a monomial hold, then the corresponding future obligations
should hold on the trace later on and should therefore be included in the
formula that needs to be evaluated during the next timestamp.

In the following, we use a function DNF that transforms any formula in DNF.
The definition of the sub-functions used are omitted for space reasons and can
be found in Appendix A.

######  Example 2 (Transformation to DNF)

We transform $\phi^{\prime}$ into its DNF: $\texttt{DNF}(\phi^{\prime})=\neg
a\wedge\neg b\wedge\textsc{{X}}(\textsc{{G}}\neg
b)\vee\textsc{{X}}(\textsc{{F}}\neg a)\wedge\neg
b\wedge\textsc{{X}}(\textsc{{G}}\neg b)$. The detail of each step of the
transformation can also be found in Appendix A. We denote
$\texttt{DNF}(\phi^{\prime})$ by $\phi_{\\_}{DNF}$.

###### Property 3

Any formula outputted by function DNF is semantically equivalent to the input
formula, that is $\forall\varphi\in\mathit{LTL},\
\varphi\equiv\texttt{DNF}(\varphi)$

###### Property 4

Let $\varphi$ be an $\mathit{LTL}$ formula that has been rewritten by rwT. In
the syntactic tree of $\texttt{DNF}(\varphi)$, any temporal operator different
from X is below a X. Therefore, a formula that has been rewritten by rwT and
then transformed into its DNF with DNF is in TDNF.

###### Definition 6

$\mathit{LTL}_{\mathrm{p}}$ is the set of formulas representing the present
obligations. It is defined by the following grammar (where $\mathrm{p}$ is any
atomic proposition in AP): $\varphi_{\\_}p\in\mathit{LTL}_{\mathrm{p}}::=\neg
p\ |\ p\ |\ \top\ |\ \bot\ |\ \varphi_{\\_}p\wedge\varphi_{\\_}p$

###### Definition 7

$\mathit{LTL}_{\mathrm{f}}$ is the set of formulas representing the future
obligations. It is defined by the following grammar (where
$\varphi\in\mathit{\mathit{LTL}}$):
$\varphi_{\\_}f\in\mathit{LTL}_{\mathrm{f}}:=\textsc{{X}}\varphi\ |\
\varphi_{\\_}f\wedge\varphi_{\\_}f$

##  5 Temporal Enforcement Encoding

Normalization (Sec. 4) provides a clear separation between present and future
and the specification formula is in TDNF. We define in Sec. 5.1 an encoding
that associates each monomial of the formula with a pair (present, future)
where present (resp. future) is a formula that represents the present
obligations (resp. future obligations). Then, we define the partial function
representing the state of an enforcer in Sec. 5.2.

###  5.1 Encoding Present and Future: Temporal Obligation Pairs (TOP)

The enforcers are now able to rewrite and evaluate the present obligations to
determine whether or not $\sigma$ leads to a violation of the specification.
To represent the whole formula, we generate a set containing a pair for each
monomial of the formula. We call these pairs: _temporal obligation pairs_
(TOP). As the set represents a disjunction of monomials, there is a violation
iff the present obligations of every pair in the set evaluate to $\bot$.

This separation allows the enforcers to only work on the present obligations.
This is useful because, for example, at timestamp $t$, the next formula to be
enforced $\varphi^{t+1}$ contains some of the future obligations of
$\varphi^{t}$ but not necessarily all of them. Let
$\mathit{present}\wedge\mathit{future}$ be a monomial in $\varphi^{t}$. If
$E(\sigma)\vDash\mathit{present}$, then $\mathit{future}$ is included in
$\varphi^{t+1}$. Evaluating certain future obligations is useless if they are
not included in the next formula to be enforced. To illustrate this, consider
formula $a\textsc{{U}}b$, we have
$\texttt{rwT}(a\textsc{{U}}b)=b\vee(a\wedge\textsc{{X}}(a\textsc{{U}}b))$. We
can see here that if $b\in\sigma$ ($b$ holds), then the trace should satisfy
$\top$ in the future and that, if only $a$ is true, then the trace should
satisfy $a\textsc{{U}}b$ in the future. Therefore, we associate
$a\textsc{{U}}b$ with $\\{(b,\top),(a,a\textsc{{U}}b)\\}$. Furthermore,
splitting the formula to be enforced into smaller formulas reduces the cost of
the simplification because we do not need to rewrite the future obligations in
the current timestamp as stated above.

We define function encode which transforms an $\mathit{LTL}$ formula into a
set of pairs (present, future). We assume that the input formula has already
been rewritten by the expansion function and then transformed into its TDNF.
We know from Property 4 that any temporal operators is below a X. Therefore,
we do not need to define the following function for temporal operators as
there cannot be any in present obligations.

######  Definition 8 (Temporal obligation pair (TOP))

Let $\varphi,\varphi_{\\_}1,\varphi_{\\_}2\in\mathit{LTL}$. Function
$\texttt{encode}:\mathit{LTL}\rightarrow
2^{\mathit{LTL}_{\mathrm{p}}\times\mathit{LTL}_{\mathrm{f}}}$ is defined as
follows:

$\displaystyle\texttt{encode}(\varphi_{\\_}1\vee\varphi_{\\_}2)$
$\displaystyle=\texttt{encode}(\varphi_{\\_}1)\cup\texttt{encode}(\varphi_{\\_}2)$
$\displaystyle\texttt{encode}(\varphi_{\\_}1\wedge\varphi_{\\_}2)$
$\displaystyle=\\{(p_{\\_}{\varphi_{\\_}1}\wedge
p_{\\_}{\varphi_{\\_}2},f_{\\_}{\varphi_{\\_}1}\wedge
f_{\\_}{\varphi_{\\_}2})\\}\text{ where }$ $\displaystyle\texttt{encode}(\neg
p)$ $\displaystyle=\\{(\neg p,\top)\\},\text{with }p\in AP$ $\displaystyle\ \
\ \ \
\\{(p_{\\_}{\varphi_{\\_}1},f_{\\_}{\varphi_{\\_}1})\\}=\texttt{encode}(\varphi_{\\_}1)\text{
and }$ $\displaystyle\texttt{encode}(p)$
$\displaystyle=\\{(p,\top)\\},\text{with }p\in AP$ $\displaystyle\ \ \ \ \
\\{(p_{\\_}{\varphi_{\\_}2},f_{\\_}{\varphi_{\\_}2})\\}=\texttt{encode}(\varphi_{\\_}2)$
$\displaystyle\texttt{encode}(\textsc{{X}}\varphi)$
$\displaystyle=\\{(\top,\varphi)\\}$

######  Example 3 (Temporal obligation pair (TOP))

Let $\phi_{\\_}{1}=\neg a\wedge\neg b\wedge\textsc{{X}}(\textsc{{G}}\neg b)$
and $\phi_{\\_}{2}=\textsc{{X}}(\textsc{{F}}\neg a)\wedge\neg
b\wedge\textsc{{X}}(\textsc{{G}}\neg b)$, we have
$\texttt{encode}(\phi_{\\_}{1})=\\{(\neg a\wedge\neg b,\text{
}\textsc{{G}}\neg b)\\}$ and $\texttt{encode}(\phi_{\\_}{2})=\\{(\neg b,\text{
}\textsc{{F}}\neg a\wedge\textsc{{G}}\neg b)\\}$. As
$\phi_{\\_}{DNF}=\phi_{\\_}1\vee\phi_{\\_}2$, we have
$\texttt{encode}(\phi_{\\_}{DNF})=\\{(\neg a\wedge\neg b,\text{
}\textsc{{G}}\neg b),(\neg b,\textsc{{F}}\neg a\wedge\textsc{{G}}\neg b)\\}$.
We denote by $\phi_{\\_}{TOP}$ the result of
$\texttt{encode}(\phi_{\\_}{DNF})$.

###### Property 5

Let $S\in 2^{\mathit{LTL}_{\mathrm{p}}\times\mathit{LTL}_{\mathrm{f}}}$. We
have $\forall\varphi\in\mathit{LTL},\
\texttt{encode}(\varphi)=S\implies\varphi\equiv\bigvee_{\\_}{(p,f)\in
S}p\wedge f$.
Therefore, according to the semantics of $\mathit{LTL}$, we have
$\sigma\not\in bad(\varphi)$ iff
$\exists(p,f)\in\texttt{encode}(\varphi),(\sigma\not\in
bad(p))\wedge(\sigma\not\in bad(f))$.

###  5.2 Temporal Correction Log (TCL, Enforcer State)

To enforce the specification, we explore the correction events
$\sigma^{\prime}$ s.t. $\sigma^{\prime}\notin bad(\varphi)$. For this, we
define the Temporal Correction Log (TCL) which serves as a state of the
enforcer, encoding the status of the exploration. The TCL is a function that
associates events of the alphabet with a pair containing a set of temporal
obligation pairs and a natural number. We denote the set of all possible TCL
by TCL and an object from this set by tcl. When the event observed by the
enforcers is $\sigma$ and $\texttt{tcl}(\sigma^{\prime})=(S,n)$, it means that
the LTL formula that would need to be satisfied if the enforcers choose to
produce event $\sigma^{\prime}$ as output is encoded by the set of TOP $S$ and
that the distance between $\sigma$ and $\sigma^{\prime}$ is $n$. A TCL is
built incrementally: each enforcer updates the values associated with the
events using their local observations. It is a partial function
$\texttt{tcl}:\Sigma\rightarrow 2^{LTL_{\\_}p\times
LTL_{\\_}f}\times\mathbb{N}$. Initially, the state of the enforcers is
initialized such that
$\texttt{tcl}(\emptyset)=(\texttt{encode}(\texttt{DNF}(\texttt{rwT}(\varphi))),0)$.

##  6 Evaluating the Formula

After initializing their state, the enforcers have to evaluate the formula to
be able to choose the output event. To achieve this, they update their state
using their local observations and send it to other enforcers to gather
information on the global event. In Sec. 6.1, we define how the state of an
enforcer is updated using its local observation and we then give in Sec. 6.2 a
function to reduce the size of an enforcer’s state as well as defining the
communication between the enforcers.

###  6.1 Updating the Temporal Correction Log

When an enforcer receive the state of another one (i.e. a tcl), it updates its
domain by adding its local observations. Each new event is associated with an
updated pair and the old events are removed from the domain. The set of TOP is
updated by rewriting the present obligations and the distance metric is
updated using the new local observation.

We define the local function used by each enforcer for the rewriting of the
present obligations using a local observation
$\sigma^{\prime\prime}\in\Sigma_{\\_}i$. This function uses $AP_{\\_}i$ to
differentiate an atomic proposition that does not hold on
$\sigma^{\prime\prime}$ from one that has not been observed yet.

######  Definition 9 (Rewriting of the present obligations)

Let $\varphi,\varphi_{\\_}1,\varphi_{\\_}2\in\mathit{LTL}_{\mathrm{p}}$ and
$\sigma^{\prime\prime}\in 2^{AP_{\\_}i}$. Function
rwi$:\mathit{LTL}_{\mathrm{p}}\times\Sigma_{\\_}i\rightarrow\mathit{LTL}_{\mathrm{p}}$
is defined as:

$\displaystyle\texttt{rw${}_{i}$}(p\in AP,\sigma^{\prime\prime})$
$\displaystyle=\begin{cases}\top&\text{if }p\in\sigma^{\prime\prime}\\\
\bot&\text{if }p\notin\sigma^{\prime\prime}\wedge p\in AP_{\\_}i\\\
p&\text{otherwise}\end{cases}$
$\displaystyle\texttt{rw${}_{i}$}(\neg\varphi,\sigma^{\prime\prime})$
$\displaystyle=\neg\texttt{rw${}_{i}$}(\varphi,\sigma^{\prime\prime})$
$\displaystyle\texttt{rw${}_{i}$}(\varphi_{\\_}1\vee\varphi_{\\_}2,\sigma^{\prime\prime})$
$\displaystyle=\texttt{rw${}_{i}$}(\varphi_{\\_}1,\sigma^{\prime\prime})\vee\texttt{rw${}_{i}$}(\varphi_{\\_}2,\sigma^{\prime\prime})$
$\displaystyle\texttt{rw${}_{i}$}(\varphi_{\\_}1\wedge\varphi_{\\_}2,\sigma^{\prime\prime})$
$\displaystyle=\texttt{rw${}_{i}$}(\varphi_{\\_}1,\sigma^{\prime\prime})\wedge\texttt{rw${}_{i}$}(\varphi_{\\_}2,\sigma^{\prime\prime})$

Note: These cases are sufficient because we only use function rwi on present
obligations. Therefore, there is no temporal operators (nor implications or
equivalences thanks to function DNF).

We now build the set of atomic propositions that still need to be evaluated (the remaining atomic propositions in the formula). When this set is empty, every atomic proposition of the formula has been evaluated which means the evaluation phase is over and we then need to decide about the event to emit. Therefore, we define function $\texttt{apr}:\texttt{TCL}\rightarrow 2^{AP}$ which builds this set using apFormula. More precisely, apr yields the union of the result of apFormula on the present obligations of every set of TOP in the codomain of the tcl, that is, $\texttt{apr}(\texttt{tcl})=\texttt{fold}(\cup,\texttt{ map}(\texttt{apFormula},\\{p\text{ | }(p,f)\in\texttt{top}\text{ with }(\texttt{top},-)\in codom(\texttt{tcl})\\}),\ \emptyset)$.

Additionally, to prevent useless rewritings with atomic propositions that are
not in the formula, we update the tcl using each event from
$2^{AP_{\\_}i\cap\texttt{apr}(\texttt{tcl})}$ instead of $\Sigma_{\\_}i$. For
example, in formula $\textsc{{F}}a$, we have
$\texttt{apr}(\texttt{tcl})=\\{a\\}$. Now suppose an enforcer $M$ with
$AP_{\\_}i=\\{a,b\\}$ has to update that formula. $M$ can observe four events
locally: $\emptyset,\\{a\\},\\{b\\}$ and $\\{a,b\\}$. However, as $b$ is not
in the formula, $\emptyset$ and $\\{b\\}$ both yield the same result after
rewriting (likewise with $\\{a\\}$ and $\\{a,b\\}$). Therefore, we can see
that evaluating the formula using atomic propositions that are not present in
it leads to "useless" rewriting because the result is the same with at least
one other local observation. This also means that each enforcer only receives
the tcl once during the evaluation as all the atomic propositions they can
observe locally are replaced by either $\top$ or $\bot$. In the remainder of
this paper, we denote $2^{AP_{\\_}i\cap\texttt{apr}(\texttt{tcl})}$ by
$\Sigma_{\\_}i^{r}$ which represents, intuitively, the set of all local
observations of enforcer $M_{\\_}i$ containing only atomic propositions that
are present in the formula.

######  Example 4 (Rewriting of the present obligations)

Recall that $\phi_{\\_}{TOP}=\\{(\neg a\wedge\neg b,\textsc{{G}}\neg b),(\neg
b,\textsc{{F}}\neg a\wedge\textsc{{G}}\neg b)\\}$. After initialization, we
have dom(tcl) = $\\{\emptyset\\}$ and tcl($\emptyset$) = ($\phi_{\\_}{TOP}$,
0). Here, the present obligation of the first monomial contains $a$ and $b$,
the ones from the second monomial only contains $b$. Therefore,
$\texttt{apr}(\texttt{tcl})=\texttt{apFormula}(\neg a\wedge\neg
b)\cup\texttt{apFormula}(\neg b)=\\{a,b\\}$. We have $AP_{\\_}1=\\{a\\}$ so
$\Sigma_{\\_}1=\\{\emptyset,\\{a\\}\\}=\Sigma_{\\_}1^{r}$. Evaluating the
present obligations using the local observations of $M_{\\_}1$ yields the
following formulas:

$\displaystyle\texttt{rw${}_{i}$}(\neg a\wedge\neg b,\emptyset)=\neg b$
$\displaystyle\texttt{rw${}_{i}$}(\neg b,\emptyset)=\neg b$
$\displaystyle\texttt{rw${}_{i}$}(\neg a\wedge\neg b,\\{a\\})=\bot$
$\displaystyle\texttt{rw${}_{i}$}(\neg b,\\{a\\})=\neg b$

Algorithm 1 Update of the current enforcer state: updateTCL(tcl, $\sigma$,
apr(tcl))

1: for each $\sigma^{\prime}\in dom(\texttt{tcl})$ do

2: Let $(\mathit{pf},n)$ = $\texttt{tcl}(\sigma^{\prime})$

3: $dom(\texttt{tcl})=dom(\texttt{tcl})\setminus\sigma^{\prime}$

4: for each $\sigma^{\prime\prime}\in\Sigma_{\\_}i^{r}$ do

5: Let
$\mathit{pf^{\prime}}=\texttt{map}(\lambda(p,-).\texttt{rw${}_{i}$}(p,\sigma^{\prime\prime}),\
\mathit{pf})$

6:
$\texttt{tcl}=\texttt{tcl}[\sigma^{\prime\prime}\cup\sigma^{\prime}\rightarrow\
(\mathit{pf^{\prime}},\
n+\texttt{distance}(\sigma^{\prime\prime},\sigma,AP_{\\_}i\cap\texttt{apr}(\texttt{tcl})))]$

7: end for

8: end for

We now define function updateTCL $:\texttt{TCL}\times\Sigma_{\\_}i\times
AP\rightarrow\texttt{TCL}$ used by the enforcers to update their state. The
function takes three arguments: the updated enforcer’s state, its local
observation of the global event and the set of atomic propositions that have
not been evaluated yet in any present obligation. It is updated using every
$\sigma^{\prime\prime}\in\Sigma_{\\_}i^{r}$. The domain becomes the set
$\sigma^{\prime}\cup\sigma^{\prime\prime}$ (with $\sigma^{\prime}\in
dom(\texttt{tcl})$, an event of the "old" domain). Let $pr$ be some present
obligation. $pr$ is rewritten as follows: $pr$ = rwi($pr$,
$\sigma^{\prime\prime}$). The distance is updated: it is increased by 1 for
each atomic proposition $p\in\sigma^{\prime\prime}$ that has a different truth
value compared to $\sigma$, that is, if the metric was equal to $n$ before the
update, it becomes
$n+\texttt{distance}(\sigma,\sigma^{\prime\prime},AP_{\\_}i\cap\texttt{apr}(\texttt{tcl})))$.
The definition of updateTCL is given in Algorithm 1.

######  Example 5 (updateTCL)

Recall that $AP_{\\_}1=\\{a\\}$, $\texttt{apr}(\texttt{tcl})=\\{a,b\\}$ and
$\sigma=\\{a\\}$. Before $M_{\\_}1$ updates tcl, we have
$\texttt{tcl}(\emptyset)=(\phi_{\\_}{TOP},0)=(\\{(\neg a\wedge\neg b,\
\textsc{{G}}\neg b),(\neg b,\textsc{{F}}\neg a\wedge\textsc{{G}}\neg b)\\},\
0)$. After updating tcl with updateTCL, we have:

$\displaystyle\texttt{tcl}(\emptyset)=(\\{(\neg b,\textsc{{G}}\neg b),(\neg
b,\textsc{{F}}\neg a\wedge\textsc{{G}}\neg b)\\},\ 1)$
$\displaystyle\texttt{tcl}(\\{a\\})=(\\{(\bot,\textsc{{G}}\neg b),(\neg
b,\textsc{{F}}\neg a\wedge\textsc{{G}}\neg b)\\},\ 0)$

###  6.2 Reduction of the Obligations Set and Communication

Algorithm 2 Reduce the size of the domain of the TCL

1: for each $\sigma^{\prime}\in dom(\texttt{tcl})$ do

2: Let $(\mathit{pf},-)=\texttt{tcl}(\sigma^{\prime})$

3: $\mathit{pf}^{\prime}=\texttt{filter}((\lambda(p,f).(p\not\equiv\bot\wedge
f\not\equiv\bot)),\ \mathit{pf})$

4: if $\mathit{pf}^{\prime}==\emptyset$ then

5: $dom(\texttt{tcl})=dom(\texttt{tcl})\setminus\sigma^{\prime}$

6: else

7:
$\texttt{tcl}=\texttt{tcl}[\sigma^{\prime}\rightarrow(\mathit{pf}^{\prime},\
n)]$

8: end if

9: end for

An issue of Algorithm 1 is that the size of the domain of the tcl doubles for
each atomic propositions in $AP_{\\_}i\cap\texttt{apr}(\texttt{tcl})$.
Therefore, we reduce its size by removing certain elements that become useless
after rewriting. First, we reduce the size of the elements of the codomain
(the images) by removing the pairs in which either the present or the future
obligations have been evaluated to $\bot$, i.e. the monomial has been
evaluated to $\bot$. Then, we remove from the domain the events that are
associated to a pair containing an empty set of TOP as these events satisfy no
present obligations. The second reduction guarantees that any event in the
domain at the end of the evaluation does not lead to a violation of $\varphi$.
Therefore, this also guarantees that adding the emitted event to the trace
will not form a bad prefix of the formula.
For this, we define reduce$:\texttt{TCL}\rightarrow\texttt{TCL}$ which
implements the two aforementioned reductions in Algorithm 2.

######  Example 6 (reduce)

In example 5, we got $\texttt{tcl}(\\{a\\})=(\\{(\bot,\textsc{{G}}\neg
b),(\neg b,\textsc{{F}}\neg a\wedge\textsc{{G}}\neg b)\\},\ 0)$. The set of
obligations associated to this event contains a monomial in which the present
obligations have been evaluated to $\bot$. Therefore,
$\texttt{tcl}(\\{a\\})=(\\{(\neg b,\textsc{{F}}\neg a\wedge\textsc{{G}}\neg
b)\\},\ 0)$.

After this reduction, if there still is at least one atomic proposition to
evaluate, then the current enforcer communicates its state to another enforcer
that can update it, i.e. an enforcer that can locally observe one of the
remaining atomic propositions in any of the present obligations. If there are
multiple enforcers that can rewrite the formula, the one with the smallest
index is chosen. If the formula has been evaluated in its entirety, the
decision rule can be applied to choose the event to emit.

######  Example 7 (Communication)

We can see in the previous example that $b$ has not been evaluated yet so the
tcl is sent to a enforcer that can observe this atomic proposition:
$M_{\\_}2$, in that case.

##  7 Enforcement using a Decision based on Global Exploration

We now define the decision rule applied by the last enforcer in Sec. 7.1 and
the algorithm itself in Sec. 7.2. We state some properties of the algorithm in
Sec. 7.3. A detailed example is given in Appendix B.1.

###  7.1 Decision Rule

The decision rule is used by the enforcers to determine the emitted event. Let
$\texttt{tcl}_{\\_}f$ be the partial function representing the final state of
the enforcer. Once an event has been chosen, each enforcer will modify its
local observations accordingly (if needed). The last enforcer that updates the
tcl needs to send its state to all the other enforcers so that they all apply
the decision rule and choose an event in parallel.

To respect _transparency_ , we simply choose the event that has the least
number of changes compared to $\sigma$. We know (from section 6.2), that the
events $\sigma^{\prime}$ so that $u\cdot\sigma^{\prime}\in bad(\varphi)$ (with
$u\in\Sigma^{*}$ the trace up until the current timestamp and $\varphi\in LTL$
the property to enforce) have been removed from the domain of
$\texttt{tcl}_{\\_}f$. Therefore, if $u\cdot\sigma\not\in bad(\varphi)$, then
$\sigma$ is the only element of the domain with its distance equal to 0 so
$\sigma$ will be emitted. If $u\cdot\sigma\in bad(\varphi)$, it is possible to
have multiple events with the same distance. Let
$\texttt{tcl}_{\\_}{\mathrm{candidates}}$ be the set of events with the least
number of changes from $\sigma$:
$\texttt{tcl}_{\\_}{\mathrm{candidates}}=\\{\sigma^{\prime}\in\texttt{tcl}_{\\_}f\
|\ \texttt{tcl}_{\\_}f(\sigma^{\prime})=(-,n_{\\_}{\mathrm{min}})\\}$ so that
$n_{\\_}{\mathrm{min}}=min(\\{n\ |\ (-,n)\in codom(\texttt{tcl}_{\\_}f)\\})$.
If $\sigma^{\prime}$ is chosen, then the local event emitted by each enforcer
$M_{\\_}i$ is $\sigma^{\prime}\cap AP_{\\_}i$.

If we choose to emit the event $\sigma^{\prime}$, then $\varphi^{t+1}$ is the
disjunction of the future obligations associated to the emitted event and we
have $\varphi^{t+1}=\texttt{fold}(\ (\lambda x,(-,f).(x\vee f)),\
\mathit{pf},\ \bot)$) with
$(\mathit{pf},-)=\texttt{TCL}_{\\_}f(\sigma^{\prime})$. Therefore, if
$(\top,\top)$ is included in the set of TOP of any events in
$\texttt{TCL}_{\\_}{\mathrm{candidates}}$, then $\varphi^{t+1}=\top$. In this
particular situation, we can stop the enforcers (any event is a good prefix of
$\top$) so, if there exists
$\sigma^{\prime}\in\texttt{TCL}_{\\_}{\mathrm{candidates}}$ so that
$\texttt{TCL}(\sigma^{\prime})=(\mathit{pf},-)\wedge(\top,\top)\in\mathit{pf}$
then we reduce $\texttt{TCL}_{\\_}{\mathrm{candidates}}$ so that it contains
these $\sigma^{\prime}$. Finally, if we still have
$\\#\texttt{TCL}_{\\_}{\mathrm{candidates}}>1$, we choose the event to emit
from this set arbitrarily (but deterministically). Every enforcer applies the
decision rule but the choice of the verdict is deterministic so they will all
choose the same one. This implies that $\varphi^{t+1}$ is the same for all of
them which means that they all know the next formula to enforce without any
additional communication.

######  Example 8 (Decision rule)

After the update of $M_{\\_}2$, the tcl is as follows

$\displaystyle\texttt{tcl}(\emptyset)=(\\{(\top,\top),(\top,\textsc{{F}}\neg
a\wedge\textsc{{G}}\neg b)\\},\ 1)$
$\displaystyle\texttt{tcl}(\\{a\\})=(\\{(\top,\textsc{{F}}\neg
a\wedge\textsc{{G}}\neg b)\\},\ 0)$

The events $\\{a,b\\}$ and $\\{b\\}$ have been removed as they lead to a
violation of $\phi$ ($\textsc{{G}}\neg b$ evaluates to $\bot$ if $b=\top$). We
apply the decision rule to choose the event to emit. Here, $\sigma$ is chosen
because it does not lead to a violation so we do not need to modify it. The
local event emitted by $M_{\\_}1$ (resp. $M_{\\_}2$) is
$\sigma^{\prime\prime}=\\{a\\}\in\Sigma_{\\_}1$ (resp.
$\sigma^{\prime\prime}=\emptyset\in\Sigma_{\\_}2$). The formula that needs to
be monitored during the next timestamp is $\phi^{t+1}=\textsc{{F}}\neg
a\wedge\textsc{{G}}\neg b$.

###  7.2 Enforcement Algorithm

Let $\mathcal{M}=\\{M_{\\_}1,...,M_{\\_}n\\}$, the set of enforcers. Each
enforcer runs this algorithm and the enforcer $M_{\\_}1$ is chosen arbitrarily
to be the one initializing the evaluation. $M_{\\_}1$ also updates its state
immediately if it is able to, i.e. if the formula contains an atomic
propositions in $AP_{\\_}1$. All the other enforcers start by waiting to
receive a tcl. Each enforcer takes its local observation of the global event
$\sigma\in\Sigma$ emitted by the system as input. Once the computation is
over, they output their local observations of the event
$\sigma^{\prime}\in\Sigma$, that is different from $\sigma$ iff
$u\cdot\sigma\in bad(\varphi)$, where $u$ is the trace up until the current
timestamp t, $u\in\Sigma^{*}$. They also build the formula $\varphi^{t+1}$
based on the emitted event. Details are given in Algorithm 3.

Algorithm 3 Enforcement on $M_{\\_}j$ using a decision based on global
exploration

1: Initialization:  If $j==1$, tcl is initialized to:
$\texttt{tcl}(\emptyset)=(\texttt{encode}(\texttt{DNF}(\texttt{rwT}(\varphi^{t}))),0)$.
Otherwise, wait until a tcl is received from another enforcer. If
$\texttt{apr}(\texttt{tcl})=\emptyset$ in the received tcl, jump to step 5.

2: Evaluation:  Compute apr(tcl), the set of atomic propositions that have not
been evaluated yet. Update tcl using updateTCL(tcl, $\sigma$,
$AP_{\\_}j\cap\texttt{apr}(\texttt{tcl})$).

3: Reduction:  Reduce the domain of tcl by removing the monomials that
evaluate to $\bot$ and the bad prefixes of $\varphi^{t}$ using reduce(tcl).

4: Communication:  If $\texttt{apr}(\texttt{tcl})\neq\emptyset$, let
$\mathit{Ens\\_Mon}\in\mathcal{M}$ be the set of enforcer $M_{\\_}k$ so that
$AP_{\\_}k\cap\texttt{apr}(\texttt{tcl})\neq\emptyset\wedge j\neq k$. tcl is
sent to the enforcer $M_{\\_}{k_{\\_}{\mathrm{min}}}$ with
$k_{\\_}{\mathrm{min}}=min\\{k|M_{\\_}k\in\mathit{Ens\\_Mon}\\}$. Wait until a
tcl is received from another enforcer. Otherwise, send tcl to all the others
enforcers so that they can apply the decision rule.

5: Decision:  Let $\texttt{tcl}_{\\_}f$ be the final state of tcl. Apply the
decision rule to choose what event $\sigma^{\prime}$ to emit and
$\varphi^{t+1}=\texttt{fold}(\text{ }(\lambda x,(-,f).(x\vee f)),\
\mathit{pf},\ \bot)$) (with
$(\mathit{pf},-)=\texttt{tcl}_{\\_}f(\sigma^{\prime})$).

###  7.3 Properties

The number of messages sent is bounded: in the worst case scenario, that is,
if the formula contains at least one local observations of each enforcer, we
need to send the tcl to every enforcer during the evaluation and once more at
the end so that every enforcer can apply the decision rule. Therefore, if we
denote by $\delta_{\\_}{\mathrm{init}}$ the time it takes to initialize the
state of the enforcer (Algorithm 2), by $\delta_{\\_}{\mathrm{update}}$ the
time one update of the tcl takes (update with each element of
$2^{AP_{\\_}i\cap\texttt{apr}(\texttt{tcl})}$) and by
$\delta_{\\_}{\mathrm{decision}}$ the time it takes to apply the decision
rule, the delay between two events emitted by the system is, at worst,
$\\#\mathcal{M}\times\delta_{\\_}{\mathrm{update}}+\delta_{\\_}{\mathrm{init}}+\delta_{\\_}{\mathrm{decision}}$
(every enforcer executes the decision rule at the same time). The size of the
messages is also bounded: as we rewrite the obligations using every possible
events in $\Sigma$, the size of the domain doubles for each atomic proposition
that we observe. Therefore, if we denote by $n_{\\_}{AP}$ the number of atomic
propositions in the formula, the size of the domain is bounded by
$2^{n_{\\_}{AP}}$ elements and the size of the last message sent can be at
most $2^{n_{\\_}{AP}-1}$. At worst, the domain will contain $2^{\\#AP}$
elements at the end. It is worth noting that the transformation to TDNF is
costly (exponential in the size of the formula) and that, in the worst case
scenario, if reduce does not remove elements from the domain, its size grows
exponentially as well which means that, in turn,
$\delta_{\\_}{\mathrm{update}}$ gets longer every timestamp.
$\delta_{\\_}{\mathrm{decision}}$ is negligible compared to the other terms.

###### Lemma 1

Let $\varphi^{t}$ be the property to enforcer at timestamp t and
$\varphi^{t+1}$ the formula built at the end of the algorithm (that will be
monitored during timestamp t+1). If $\varphi^{t}\not\equiv\bot$, then
$\varphi^{t+1}\not\equiv\bot$.

This property implies that algorithm 3 cannot produce a formula that is
equivalent to $\bot$.

###### Property 6

Algorithm 3 is _sound_ , _transparent_ and _optimal_ (as defined in Sec. 3.).

##  8 Enforcement using a Decision based on Local Exploration

In this section, we define another enforcement algorithm where each enforcer
takes a local decision before sending its state to the next enforcer: instead
of sending the whole tcl, the current enforcer only sends a single entry with
its image. This also means that the enforcers do not need to make a decision
at the end of the enforcement round: the local emitted event corresponds to
this local decision. The receiving enforcer then initializes its state using
the received event and applies the updates to it. The point of this approach
is to prevent the exponential growth of the domain of the tcl. The local
decision rule is defined in Sec. 8.1 and the algorithm in Sec. 8.2. We compare
the two versions in Sec. 8.3 and give the properties of the second version in
Sec. 8.4. A complete example is given in Sec. 8.5.

###  8.1 Local Decision Rule

To allow the enforcers to make a local decision, we redefine the decision
rule. Let tcl be the partial function representing the state of the enforcer
after its update. apr(tcl) is recomputed after the evaluation. Two cases are
possible:
\- If $AP_{\\_}r=\emptyset$, the algorithm stops and the current enforcer decides which event to emit from a set $\texttt{tcl}_{\\_}{candidates}=\\{\sigma^{\prime}\in\texttt{tcl}_{\\_}f\ |\ \texttt{tcl}_{\\_}f(\sigma^{\prime})=(-,n_{\\_}{min})\\}$ so that $n_{\\_}{min}=min(N)$ with $N=\\{n\ |\ (-,n)\in codom(\texttt{tcl}_{\\_}f)\\}$. If there exists $\sigma^{\prime}\in\texttt{tcl}_{\\_}{candidates}$ so that $\texttt{tcl}(\sigma^{\prime})=(\mathit{pf},-)\wedge(\top,\top)\in\mathit{pf}$, then $\texttt{tcl}_{\\_}{candidates}=\\{\sigma^{\prime}\in\texttt{tcl}_{\\_}{candidates}\text{ | }\texttt{tcl}(\sigma^{\prime})=(\mathit{pf},-)\wedge(\top,\top)\in\mathit{pf}\\}$ for the same reasons as in the first algorithm: if $\varphi^{t+1}=\top$, we do not need to enforce the formula anymore as any event is a good prefix of $\top$. Finally, if there are multiple elements in $\texttt{tcl}_{\\_}{candidates}$, one is chosen arbitrarily.
\- If $AP_{\\_}r\neq\emptyset$, the current enforcer decides which element of
the domain it will send to the next enforcer (with its image). The element is
chosen from the set
$\texttt{tcl}_{\\_}c=\\{(\sigma^{\prime},(\mathit{pf},n_{\\_}{min}))\ |\
\sigma^{\prime}\in
dom(\texttt{tcl})\wedge\texttt{tcl}(\sigma^{\prime})=(\mathit{pf},n_{\\_}{min})\\}$
so that $n_{\\_}{min}=min(N)$ with $N=\\{n\ |\ (-,n)\in
codom(\texttt{tcl}_{\\_}f)\\}$, that is, it is chosen among the element that
have the smallest distance to $\sigma$. If there are several events that
respect the property mentioned above, the set is reduced to the events that
have the most models, i.e.
$\texttt{tcl}_{\\_}c=\\{(-,(\mathit{pf},-))\in\texttt{tcl}_{\\_}c\text{ $|$
}\nexists(-,(\mathit{pf}^{\prime},-))\in\texttt{tcl}_{\\_}c\text{ so that
}\mathit{pf}\neq\mathit{pf}^{\prime}\wedge|\mathit{pf}^{\prime}|>|\mathit{pf}|\\}$
(the formulas that have the highest amount of monomials). If there are still
multiple elements in $\texttt{tcl}_{\\_}c$, one is chosen arbitrarily (and
deterministically).

Just as in the first algorithm, if $\sigma^{\prime}$ is chosen, then
$M_{\\_}i$ outputs $\sigma^{\prime}\cap AP_{\\_}i$. As only the last enforcer
that applies the decision rule has sufficient informations to determine
$\varphi^{t+1}$, it needs to be sent to the other enforcers at the end of the
evaluation.

###  8.2 Enforcement Algorithm

To obtain the enforcement algorithm in the case of decision based on local
exploration, we update Algorithm 3 as follows.

In step 1, the (current) enforcer waits for a tcl or the formula to enforce in
the next timestamp. If it receives a formula, the execution of the algorithm
for the current timestamp stops.

In step 4, the enforcer always applies the local decision rule to choose an
event from the domain. It then removes all the other events from the domain
and, if $\texttt{apr}(\texttt{tcl})\neq\emptyset$, it sends tcl to the next
enforcer using the same criteria as in the first algorithm. Otherwise, it
waits for the formula to enforce in the next timestamp instead of a tcl. When
it receives the formula, the current timestamp stops (the enforcer does not go
to step 5).

In step 5, the enforcer does not apply the decision rule as it already did it
in the previous step. It only builds the formula to enforce at the next
timestamp and sends it to all the other enforcers.

###  8.3 Comparison

Despite the fact that this algorithm requires the transformation to DNF during
the initialization, it presents a significant improvement regarding the size
of the messages and of the domain (it prevents their exponential growth).
Furthermore, the size of the domain is much smaller, it only contains one
element before the update instead of, at worst, $2^{k-1}$ after $k$ updates,
which allows the enforcers to only do one update per element of
$2^{AP_{\\_}i\cap\texttt{apr}(\texttt{tcl})}$ instead of
$\\#2^{AP_{\\_}i\cap\texttt{apr}(\texttt{tcl})}*2^{k-1}$ updates (one per
local observations per element of the domain). There are a few drawbacks,
however: the decision rule has to be applied by each enforcer, although this
is not that significant considering its negligible compared to the other
operations, and this version does not guarantee _optimality_. It is worth
noting that the first version of the algorithm is better than this one in one
very specific scenario: if the domain of tcl is reduced to a single element
with reduce at the end of every update, then this version is worse because it
does not improve the size of the messages/domain but the enforcers still have
to apply the local decision rule after every update instead of once in the
first version. Even in this situation, the difference is not significant
unless there is a large number of enforcers.

###  8.4 Properties

Just as in the first version, the number of messages sent is bounded: in the
worst case, that is, if the formula contains at least one local observation of
each enforcer, one message is sent to each enforcer. An additional message is
sent to all the enforcers (except 1) at the end to communicate
$\varphi^{t+1}$. Therefore, the delay between two events emitted by the system
is, at worst,
$(\delta_{\\_}{\mathrm{update}}+\delta_{\\_}{\mathrm{decision}})\times\\#\mathcal{M}+\delta_{\\_}{\mathrm{init}}$
with $\delta_{\\_}{\mathrm{init}},\delta_{\\_}{\mathrm{update}}$ and
$\delta_{\\_}{\mathrm{decision}}$ defined as in Sec. 7.3. As we only send a
pair containing an element of the domain of tcl and its image, the size of the
message is quite small. It is not completely constant because the size of the
image may vary (although not by much). This algorithm guarantees the property
of _soundness_ and _transparency_ but (as said above) not _optimality_. As we
always send an event associated with a set of future obligations that has at
least one solution, there is always a solution, otherwise, this event would
not be in the domain. However, as we are not entirely exploring the set of all
possible events over $AP$, the event emitted at the end might not be the best
(wrt the distance from $\sigma$), hence the fact that _optimality_ is not
guaranteed.

###  8.5 Complete Example: Decentralized Traffic Lights

We consider a crossroad and its four traffic lights. We have
$AP_{\\_}i=\\{g_{\\_}i,y_{\\_}i,r_{\\_}i\\},i\in\\{1,2,3,4\\}$. The variable
$g_{\\_}i$ (resp. $y_{\\_}i$ and $r_{\\_}i$) represents whether or not the
green (resp. yellow and red) light of the i-th traffic light is on
($g_{\\_}i=\top$ means it is on). Let $\varphi$ be the property representing
the following specification: _At any time, exactly two opposed traffic lights
must be green at the same time_. We have:
$\varphi=\textsc{{G}}((g_{\\_}1\wedge g_{\\_}3\wedge\neg(g_{\\_}2\vee
g_{\\_}4))\vee(\neg(g_{\\_}1\vee g_{\\_}3)\wedge g_{\\_}2\wedge g_{\\_}4))$.
Let $M_{\\_}1,M_{\\_}2,M_{\\_}3$ and $M_{\\_}4$ be the four enforcers
associated to each traffic light (one per traffic light). Let
$\sigma\in\Sigma$ be the event emitted by the system,
$\sigma=\\{g_{\\_}1,g_{\\_}2,g_{\\_}3\\}$ which means that only the green
light of the first three traffic lights is on. All the transformations are
given in the following table, a detailed description of this example on both
version of the algorithm is given in Appendix B.1 and B.2. In the table,
shaded pairs are removed from the set through function reduce. Then, events
associated to an empty set of TOP are removed from the domain.

Present/Future | $\texttt{rwT}(\varphi)=(g_{\\_}1\wedge g_{\\_}3\wedge\neg(g_{\\_}2\vee g_{\\_}4)\vee\neg(g_{\\_}1\vee\neg g_{\\_}3)\wedge g_{\\_}2\wedge g_{\\_}4)\wedge\textsc{{X}}\varphi=\varphi_{\\_}{rwT}$
---|---
Transf. to TDNF | $\texttt{DNF}(\varphi_{\\_}{rwT})=(g_{\\_}1\wedge g_{\\_}3\wedge\neg g_{\\_}2\wedge\neg g_{\\_}4\wedge\textsc{{X}}\varphi)\vee\ (\neg g_{\\_}1\wedge\neg g_{\\_}3\wedge g_{\\_}2\wedge g_{\\_}4\wedge\textsc{{X}}\varphi)=\varphi_{\\_}{TDNF}$
Initial tcl | $[\emptyset\mapsto\texttt{encode}(\varphi_{\\_}{TDNF})=(\\{(g_{\\_}1\wedge g_{\\_}3\wedge\neg g_{\\_}2\wedge\neg g_{\\_}4,\varphi),(\neg g_{\\_}1\wedge\neg g_{\\_}3\wedge g_{\\_}2\wedge g_{\\_}4,\varphi)\\},\ 0)]$
Evaluation ($M_{\\_}1$) | $[\emptyset\mapsto(\\{{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)},(\neg g_{\\_}3\wedge g_{\\_}2\wedge g_{\\_}4,\varphi)\\},\ 1),\\{g_{\\_}1\\}\mapsto(\\{(g_{\\_}3\wedge\neg g_{\\_}2\wedge\neg g_{\\_}4,\varphi),{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)}\\},\ 0)]$
Decision ($M_{\\_}1$) | The entry corresponding to $\\{g_{\\_}1\\}$ is chosen, others are removed.
Evaluation ($M_{\\_}2$) | $[\\{g_{\\_}1\\}\mapsto\\{(g_{\\_}3\wedge\neg g_{\\_}4,\varphi)\\},\ 1),\\{g_{\\_}1,g_{\\_}2\\}\mapsto(\\{{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)}\\},\ 0)]$
Decision ($M_{\\_}2$) |  $\\{g_{\\_}1\\}$ is the only event left in the domain. It is therefore chosen by default
Evaluation ($M_{\\_}3$) | $[\\{g_{\\_}1\\}\mapsto(\\{{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)}\\},\ 2),\\{g_{\\_}1,g_{\\_}3\\}\mapsto(\\{(\neg g_{\\_}4,\varphi)\\},\ 1)]$
Decision ($M_{\\_}3$) |  $\\{g_{\\_}1,g_{\\_}3\\}$ is the only event left in the domain. It is therefore chosen by default
Evaluation ($M_{\\_}4$) | $[\\{g_{\\_}1,g_{\\_}3\\}\mapsto(\\{(\top,\varphi)\\},\ 1),\\{g_{\\_}1,g_{\\_}3,g_{\\_}4\\}\mapsto(\\{{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)}\\},\ 2)]$
Decision ($M_{\\_}4$) |  $\\{g_{\\_}1,g_{\\_}3\\}$ is the only event left in the domain. It is therefore chosen by default
Next formula | $\varphi^{2}=\varphi$

##  9 Conclusion and Future work

We define the problem of _decentralized runtime enforcement_ and give two
enforcement algorithms for LTL formulas. Both algorithms guarantee _soundness_
and _transparency_. The first also guarantees the _optimality_ of the
modifications done by the enforcer in terms of distance to the original event
emitted by the system while the second comes with a drastically reduced cost
(in both memory and time).

The natural extension of this work is its implementation to empirically
evaluate it (on LTL specification patterns [7] for example) in terms of
computational and communication costs. Then, we plan to integrate it into the
THEMIS tool [8] which currently only supports verification. Our enforcement
algorithms can also be extended in several ways. First, using LTL formula
rewriting has a few drawbacks and in particular, rewriting makes analyzing the
runtime behavior of monitors hard to predict as it depends on the
simplification function applied to LTL formulas after rewriting.
Alternatively, we consider encoding the specification using automata, for
example. Finally, we shall also consider timed properties as they are much
more expressive. There are some approaches for runtime enforcement of timed
properties (see [14] for an overview) but all are centralized.

## References

  * [1]
  * [2] Andreas Bauer & Yliès Falcone (2012): _Decentralised LTL Monitoring_.  In Dimitra Giannakopoulou & Dominique Méry, editors: FM 2012: Formal Methods, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 85–100, 10.1007/978-3-642-32759-910.  Available at https://arxiv.org/abs/1111.5133.
  * [3] Andreas Bauer, Martin Leucker & Christian Schallhart (2011): _Runtime Verification for LTL and TLTL_.  ACM Trans. Softw. Eng. Methodol. 20(4), 10.1145/2000799.2000800.  Available at https://dl.acm.org/doi/10.1145/2000799.2000800.
  * [4] Borzoo Bonakdarpour, Pierre Fraigniaud, Sergio Rajsbaum & Corentin Travers (2016): _Challenges in Fault-Tolerant Distributed Runtime Verification_.  In Tiziana Margaria & Bernhard Steffen, editors: Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, Springer International Publishing, Cham, pp. 363–370, 10.1007/978-3-319-47169-327.
  * [5] Christian Colombo & Yliès Falcone (2016): _Organising LTL monitors over distributed systems with a global clock_.  Formal Methods in System Design 49(1), pp. 109–158, 10.1007/s10703-016-0251-x.  Available at https://hal.inria.fr/hal-01315776.
  * [6] Egor Dolzhenko, Jay Ligatti & Srikar Reddy (2015): _Modeling Runtime Enforcement with Mandatory Results Automata_.  Int. J. Inf. Secur. 14(1), p. 47–60, 10.1007/s10207-014-0239-8.  Available at https://www.cse.usf.edu/~ligatti/papers/mra-full-tr.pdf.
  * [7] Matthew B. Dwyer, George S. Avrunin & James C. Corbett (1999): _Patterns in Property Specifications for Finite-State Verification_.  In: Proceedings of the 21st International Conference on Software Engineering, ICSE ’99, Association for Computing Machinery, New York, NY, USA, p. 411–420, 10.1145/302405.302672.  Available at https://ieeexplore.ieee.org/document/841031.
  * [8] Antoine El-Hokayem & Yliès Falcone (2017): _THEMIS: A Tool for Decentralized Monitoring Algorithms_.  In: ISSTA 2017, Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, Santa Barbara, United States, pp. 125–135, 10.1145/3092703.3092723.  Available at https://hal.archives-ouvertes.fr/hal-01653727.
  * [9] Antoine El-Hokayem & Yliès Falcone (2019): _On the Monitoring of Decentralized Specifications: Semantics, Properties, Analysis, and Simulation_.  ACM Transactions on Software Engineering and Methodology, pp. 1–57, 10.1145/3355181.  Available at https://hal.archives-ouvertes.fr/hal-02283429.
  * [10] Yliès Falcone, Jean-Claude Fernandez & Laurent Mounier (2012): _What can you verify and enforce at runtime?_ Int. J. Softw. Tools Technol. Transf. 14(3), pp. 349–382, 10.1007/s10009-011-0196-8.  Available at https://hal.inria.fr/hal-00627594/en.
  * [11] Yliès Falcone, Thierry Jéron, Hervé Marchand & Srinivas Pinisetty (2016): _Runtime enforcement of regular timed properties by suppressing and delaying events_.  Sci. Comput. Program. 123, pp. 2–41, 10.1016/j.scico.2016.02.008.  Available at https://hal.archives-ouvertes.fr/hal-01281727/.
  * [12] Yliès Falcone, Leonardo Mariani, Antoine Rollet & Saikat Saha (2018): _Runtime Failure Prevention and Reaction_.  In Ezio Bartocci & Yliès Falcone, editors: Lectures on Runtime Verification - Introductory and Advanced Topics, Lecture Notes in Computer Science 10457, Springer, pp. 103–134, 10.1007/978-3-319-75632-5_4.  Available at https://hal.archives-ouvertes.fr/hal-01723606.
  * [13] Yliès Falcone, Laurent Mounier, Jean-Claude Fernandez & Jean-Luc Richier (2011): _Runtime enforcement monitors: composition, synthesis, and enforcement abilities_.  Formal Methods Syst. Des. 38(3), pp. 223–262, 10.1007/s10703-011-0114-4.  Available at https://hal.archives-ouvertes.fr/hal-00576948.
  * [14] Yliès Falcone & Srinivas Pinisetty (2019): _On the Runtime Enforcement of Timed Properties_.  In Bernd Finkbeiner & Leonardo Mariani, editors: Runtime Verification - 19th International Conference, RV 2019, Porto, Portugal, October 8-11, 2019, Proceedings, Lecture Notes in Computer Science 11757, Springer, pp. 48–69, 10.1007/978-3-030-32079-9_4.  Available at https://hal.archives-ouvertes.fr/hal-02433521.
  * [15] Adrian Francalanza, Jorge A. Pérez & César Sánchez (2018): _Runtime Verification for Decentralised and Distributed Systems_.  In Ezio Bartocci & Yliès Falcone, editors: Lectures on Runtime Verification - Introductory and Advanced Topics, Lecture Notes in Computer Science 10457, Springer, pp. 176–210, 10.1007/978-3-319-75632-5_6.  Available at https://www.researchgate.net/publication/323082912_Runtime_Verification_for_Decentralised_and_Distributed_Systems.
  * [16] Sylvain Hallé, Raphaël Khoury, Quentin Betti, Antoine El-Hokayem & Yliès Falcone (2018): _Decentralized enforcement of document lifecycle constraints_.  Inf. Syst. 74(Part), pp. 117–135, 10.1016/j.is.2017.08.002.  Available at https://hal.archives-ouvertes.fr/hal-01653879.
  * [17] Chi Hu, Wei Dong, Yonghui Yang, Hao Shi & Fei Deng (2020): _Decentralized runtime enforcement for robotic swarms_.  Frontiers Inf. Technol. Electron. Eng. 21(11), pp. 1591–1606, 10.1631/FITEE.2000203.  Available at https://link.springer.com/article/10.1631/FITEE.2000203.
  * [18] Bettina Könighofer, Julian Rudolf, Alexander Palmisano, Martin Tappler & Roderick Bloem (2021): _Online Shielding for Stochastic Systems_.  In Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz & Ivan Perez, editors: NASA Formal Methods - 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021, Proceedings, Lecture Notes in Computer Science 12673, Springer, pp. 231–248, 10.1007/978-3-030-76384-8_15.  Available at https://arxiv.org/abs/2012.09539.
  * [19] Aravind Natarajan, Himanshu Chauhan, Neeraj Mittal & Vijay K. Garg (2017): _Efficient abstraction algorithms for predicate detection_.  Theoretical Computer Science 688, pp. 24–48, https://doi.org/10.1016/j.tcs.2015.12.037.  Available at https://www.sciencedirect.com/science/article/pii/S0304397515012074.  Distributed Computing and Networking.
  * [20] Vinit A. Ogale & Vijay K. Garg (2007): _Detecting Temporal Logic Predicates on Distributed Computations_.  In Andrzej Pelc, editor: Distributed Computing, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 420–434, 10.1007/978-3-540-75142-732.  Available at https://link.springer.com/chapter/10.1007/978-3-540-75142-7_32.
  * [21] Srinivas Pinisetty, Yliès Falcone, Thierry Jéron, Hervé Marchand, Antoine Rollet & Omer Nguena-Timo (2014): _Runtime enforcement of timed properties revisited_.  Formal Methods Syst. Des. 45(3), pp. 381–422, 10.1007/s10703-014-0215-y.  Available at https://hal.inria.fr/hal-01088136.
  * [22] Amir Pnueli (1977): _The temporal logic of programs_.  In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp. 46–57, 10.1109/SFCS.1977.32.  Available at https://ieeexplore.ieee.org/document/4567924.
  * [23] Grigore Roşu & Klaus Havelund (2005): _Rewriting-Based Techniques for Runtime Verification_.  Automated Software Engineering 12(2), pp. 151–197, 10.1007/s10515-005-6205-y.  Available at https://www.researchgate.net/publication/227050141_Rewriting-Based_Techniques_for_Runtime_Verification.
  * [24] Prasanna Thati & Grigore Roşu (2005): _Monitoring Algorithms for Metric Temporal Logic Specifications_.  Electronic Notes in Theoretical Computer Science 113, pp. 145–162, https://doi.org/10.1016/j.entcs.2004.01.029.  Available at https://www.sciencedirect.com/science/article/pii/S1571066104052570.  Proceedings of the Fourth Workshop on Runtime Verification (RV 2004).

##  Appendix A Transforming an
LTL formula to Disjunctive Normal Form

To translate a formula to Disjunctive Normal Form (DNF), we first need to
translate it to normal form, that is getting rid of equivalences and
implications as well as propagating the negations until they are only applied
to literals. Therefore, we define negF which transforms a formula into its
negation and then define nf that transforms any $\mathit{LTL}$ formula into
its normal form. nf rewrites implications / equivalences and uses negF to
propagate the negations. In order to transform a formula from normal form to
DNF, we only need to distribute $\wedge$ over $\vee$ until the formula is in
DNF. Therefore, we define isDNF that checks whether or not a formula is in DNF
by searching for a conjunction of disjunction or for a negation that is not
directly applied to a literal. Finally, we define distrib which applies the
distribution laws (of $\wedge$ over $\vee$). By repeating this operation until
stabilization, we get a formula in DNF. In Appendix A.5, we give the algorithm
that takes any $\mathit{LTL}$ formula as input and transforms it into its DNF.

In the following, we consider a set of atomic propositions $AP$ and we will
use formula $\phi^{\prime}=\neg(a\wedge\textsc{{X}}(\textsc{{G}}a)\vee
b\vee\textsc{{X}}(\textsc{{F}}b))$ to illustrate the definitions.

###  A.1 Negation of a formula

######  Definition 10 (negF)

Let $\varphi,\varphi_{\\_}1,\varphi_{\\_}2\in\mathit{LTL}$.
negF$:\mathit{LTL}\rightarrow\mathit{LTL}$ is inductively defined as follows:

$\displaystyle\texttt{negF}(\bot)$ $\displaystyle=\top$
$\displaystyle\texttt{negF}(\top)$ $\displaystyle=\bot$
$\displaystyle\texttt{negF}(p\in AP)$ $\displaystyle=\neg p$
$\displaystyle\texttt{negF}(\neg\varphi)$ $\displaystyle=\varphi$
$\displaystyle\texttt{negF}(\varphi_{\\_}1\Rightarrow\varphi_{\\_}2)$
$\displaystyle=\varphi_{\\_}1\wedge\texttt{negF}(\varphi_{\\_}2)$
$\displaystyle\texttt{negF}(\varphi_{\\_}1\vee\varphi_{\\_}2)$
$\displaystyle=\texttt{negF}(\varphi_{\\_}1)\wedge\texttt{negF}(\varphi_{\\_}2)$
$\displaystyle\texttt{negF}(\varphi_{\\_}1\Leftrightarrow\varphi_{\\_}2)$
$\displaystyle=(\texttt{negF}(\varphi_{\\_}1)\wedge\varphi_{\\_}2)\vee(\varphi_{\\_}1\wedge\texttt{negF}(\varphi_{\\_}2))$
$\displaystyle\texttt{negF}(\varphi_{\\_}1\wedge\varphi_{\\_}2)$
$\displaystyle=\texttt{negF}(\varphi_{\\_}1)\vee\texttt{negF}(\varphi_{\\_}2)$
$\displaystyle\texttt{negF}(\varphi_{\\_}1\textsc{{R}}\varphi_{\\_}2)$
$\displaystyle=\texttt{negF}(\varphi_{\\_}1)\textsc{{U}}\texttt{negF}(\varphi_{\\_}2)$
$\displaystyle\texttt{negF}(\textsc{{G}}\varphi)$
$\displaystyle=\textsc{{F}}(\texttt{negF}(\varphi))$
$\displaystyle\texttt{negF}(\varphi_{\\_}1\textsc{{U}}\varphi_{\\_}2)$
$\displaystyle=\texttt{negF}(\varphi_{\\_}1)\textsc{{R}}\texttt{negF}(\varphi_{\\_}2)$
$\displaystyle\texttt{negF}(\textsc{{F}}\varphi)$
$\displaystyle=\textsc{{G}}(\texttt{negF}(\varphi))$
$\displaystyle\texttt{negF}(\textsc{{X}}\varphi)$
$\displaystyle=\textsc{{X}}(\texttt{negF}(\varphi))$

######  Example 9 (Negation of a formula)

Let $\varphi,\varphi_{\\_}1,\varphi_{\\_}2\in\mathit{LTL}$.

  * •

negF($\varphi_{\\_}1\vee\varphi_{\\_}2$) =
$\neg\varphi_{\\_}1\wedge\neg\varphi_{\\_}2$

  * •

negF($\textsc{{G}}\varphi_{\\_}1\wedge\textsc{{F}}\varphi_{\\_}2$) =
$\textsc{{F}}\neg\varphi_{\\_}1\vee\textsc{{G}}\neg\varphi_{\\_}2$

  * •

negF($\neg\varphi$) = $\varphi$

###  A.2 Transformation to normal form

######  Definition 11 (nf)

Let $\varphi,\varphi_{\\_}1,\varphi_{\\_}2\in\mathit{LTL}$. Function
nf$:\mathit{LTL}\rightarrow\mathit{LTL}$ is inductively defined as follows:

$\displaystyle\texttt{nf}(\top)$ $\displaystyle=\top$
$\displaystyle\texttt{nf}(\bot)$ $\displaystyle=\bot$
$\displaystyle\texttt{nf}(p\in AP)$ $\displaystyle=p$
$\displaystyle\texttt{nf}(\neg\varphi)$ $\displaystyle=\begin{cases}\neg
p&\text{if }\varphi=p\in AP,\\\
\texttt{nf}(\texttt{negF}(\varphi))&otherwise\end{cases}$
$\displaystyle\texttt{nf}(\varphi_{\\_}1\Rightarrow\varphi_{\\_}2)$
$\displaystyle=\texttt{nf}(\neg\varphi_{\\_}1)\vee\texttt{nf}(\varphi_{\\_}2)$
$\displaystyle\texttt{nf}(\varphi_{\\_}1\vee\varphi_{\\_}2)$
$\displaystyle=\texttt{nf}(\varphi_{\\_}1)\vee\texttt{nf}(\varphi_{\\_}2)$
$\displaystyle\texttt{nf}(\varphi_{\\_}1\Leftrightarrow\varphi_{\\_}2)$
$\displaystyle=\texttt{nf}(\varphi_{\\_}1)\wedge\texttt{nf}(\varphi_{\\_}2)\vee\texttt{nf}(\neg\varphi_{\\_}1)\wedge\texttt{nf}(\neg\varphi_{\\_}2)$
$\displaystyle\texttt{nf}(\varphi_{\\_}1\wedge\varphi_{\\_}2)$
$\displaystyle=\texttt{nf}(\varphi_{\\_}1)\wedge\texttt{nf}(\varphi_{\\_}2)$
$\displaystyle\texttt{nf}(\varphi_{\\_}1\textsc{{U}}\varphi_{\\_}2)$
$\displaystyle=\varphi_{\\_}1\textsc{{U}}\varphi_{\\_}2$
$\displaystyle\texttt{nf}(\textsc{{G}}\varphi)$
$\displaystyle=\textsc{{G}}\varphi$
$\displaystyle\texttt{nf}(\varphi_{\\_}1\textsc{{R}}\varphi_{\\_}2)$
$\displaystyle=\varphi_{\\_}1\textsc{{R}}\varphi_{\\_}2$
$\displaystyle\texttt{nf}(\textsc{{F}}\varphi)$
$\displaystyle=\textsc{{F}}\varphi$
$\displaystyle\texttt{nf}(\textsc{{X}}\varphi)$
$\displaystyle=\textsc{{X}}\varphi$

######  Example 10 (nf)

We recall that $\phi^{\prime}=\neg(a\wedge\textsc{{X}}(\textsc{{G}}a)\vee
b\vee\textsc{{X}}(\textsc{{F}}b))$. We have nf($\phi^{\prime}$) = $\neg
a\vee\textsc{{X}}(\textsc{{F}}\neg a)\wedge\neg
b\wedge\textsc{{X}}(\textsc{{G}}\neg b)$.

###  A.3 DNF Test

######  Definition 12 (isDNF)

Let $\varphi,\varphi_{\\_}1,\varphi_{\\_}2\in\mathit{LTL}$. Function
isDNF$:\mathit{LTL}\times\mathbb{B}\rightarrow\mathbb{B}$ is inductively
defined as follows:

$\displaystyle\texttt{isDNF}(\varphi_{\\_}1\vee\varphi_{\\_}2,\bot)$
$\displaystyle=\texttt{isDNF}(\varphi_{\\_}1,\bot)\wedge\texttt{isDNF}(\varphi_{\\_}2,\bot)$
$\displaystyle\texttt{isDNF}(\varphi_{\\_}1\vee\varphi_{\\_}2,\top)$
$\displaystyle=\bot$
$\displaystyle\texttt{isDNF}(\varphi_{\\_}1\wedge\varphi_{\\_}2,\\_)$
$\displaystyle=\texttt{isDNF}(\varphi_{\\_}1,\top)\wedge\texttt{isDNF}(\varphi_{\\_}2,\top)$
$\displaystyle\texttt{isDNF}(\textsc{{X}}\varphi,\\_)$ $\displaystyle=\top$
$\displaystyle\texttt{isDNF}(p\in AP,\\_)$ $\displaystyle=\top$
$\displaystyle\texttt{isDNF}(\neg\varphi,\\_)$
$\displaystyle=\begin{cases}\top&\text{if }\varphi\in AP\\\
\bot&\text{otherwise}\end{cases}$

The parameter _flag_ of isDNF is equal to $\top$ whenever the function is
searching within a monomial. If a disjunction is found inside of a monomial,
then the formula is not in DNF (there is a conjunction of disjunction). This
parameter is only used to differentiate both cases (disjunction outside/inside
a monomial).
These cases are sufficient because nf removed any implications/equivalences
from the formula and we know from Property 2 that any temporal operator
different from X is below a X.

######  Example 11 (isDNF)

Let $a,b,c\in AP$.

  * •

isDNF$(a\wedge b,\bot)$ = $\top$

  * •

isDNF$(a\vee(b\wedge c),\bot)$ = $\top$

  * •

isDNF$(a\vee(\textsc{{X}}\textsc{{G}}(a\vee b)\wedge c),\bot)$ = $\top$

  * •

isDNF$((a\vee b)\wedge c,\bot)$ = $\bot$

###  A.4 Distribution of $\wedge$ over $\vee$

######  Definition 13 (distrib)

Let $\varphi,\varphi_{\\_}1,\varphi_{\\_}2,\varphi_{\\_}3\in\mathit{LTL}$.
Function distrib$:\mathit{LTL}\rightarrow\mathit{LTL}$ is inductively defined
as follows:

$\displaystyle\texttt{distrib}(\varphi)$ $\displaystyle\text{ = match
}\varphi\text{ with }$ $\displaystyle\ \
|\varphi_{\\_}1\wedge(\varphi_{\\_}2\vee\varphi_{\\_}3)$
$\displaystyle\rightarrow\texttt{distrib}(\varphi_{\\_}1\wedge\varphi_{\\_}2)\vee\texttt{distrib}(\varphi_{\\_}1\wedge\varphi_{\\_}3)$
$\displaystyle\ \ |(\varphi_{\\_}2\vee\varphi_{\\_}3)\wedge\varphi_{\\_}1$
$\displaystyle\rightarrow\texttt{distrib}(\varphi_{\\_}1\wedge\varphi_{\\_}2)\vee\texttt{distrib}(\varphi_{\\_}1\wedge\varphi_{\\_}3)$
$\displaystyle\ \ |\varphi_{\\_}1\wedge\varphi_{\\_}2$
$\displaystyle\rightarrow\texttt{distrib}(\varphi_{\\_}1)\wedge\texttt{distrib}(\varphi_{\\_}2)$
$\displaystyle\ \ |\varphi_{\\_}1\vee\varphi_{\\_}2$
$\displaystyle\rightarrow\texttt{distrib}(\varphi_{\\_}1)\vee\texttt{distrib}(\varphi_{\\_}1)$
$\displaystyle\ \ |\\_$ $\displaystyle\rightarrow\varphi$

######  Example 12 (Distribution of $\wedge$ over $\vee$)

Let $a,b,c\in AP$.

  * •

distrib$(a\wedge(b\vee c))$ = $(a\wedge b)\vee(a\wedge c)$

  * •

distrib$((a\wedge b)\vee c)$ = $(a\wedge b)\vee c$

  * •

distrib$((a\vee b)\wedge\textsc{{X}}\textsc{{G}}(a\vee b))$ =
$(a\wedge\textsc{{X}}\textsc{{G}}(a\vee
b))\vee(b\wedge\textsc{{X}}\textsc{{G}}(a\vee b))$

###  A.5 Transformation to DNF

Algorithm 4 Compute $\texttt{DNF}(\varphi)$

1: $\varphi=\texttt{nf}(\varphi)$

2: while $\texttt{isDNF}(\varphi,\bot)=\bot$ do

3: $\varphi=\texttt{distrib}(\varphi)$

4: end while

Algorithm 5 gives the full transformation of any formula in $\mathit{LTL}$ to
DNF. This algorithm terminates for the following reasons:

  * •

We apply nf so the formula is in normal form. In particular, its negations are
only applied to literals.

  * •

The function distrib moves the occurrences of operator $\vee$ up in the
syntactic tree of the input formula (by distributing $\wedge$ over $\vee$). A
formula in DNF is so that there is no $\vee$ in the subtree below a $\wedge$.
Therefore, if we apply this function repeatedly until there is no $\vee$ in
the subtree below a $\wedge$, we will necessarily get a DNF.

##  Appendix B Complete examples: Traffic lights (decentralized)

We consider a crossroad and its four traffic lights. We have
$AP_{\\_}i=\\{g_{\\_}i,y_{\\_}i,r_{\\_}i\\},i\in\\{1,2,3,4\\}$. The variable
$g_{\\_}i$ (resp. $y_{\\_}i$ and $r_{\\_}i$) represents whether or not the
green (resp. yellow and red) light of the i-th traffic light is on
($g_{\\_}i=\top$ means it is on). Let $\varphi$ be the property representing
the following specification: _At any time, exactly two opposed traffic lights
must be green at the same time_. We have:

$\varphi=\textsc{{G}}((g_{\\_}1\wedge g_{\\_}3\wedge\neg(g_{\\_}2\vee
g_{\\_}4))\vee(\neg(g_{\\_}1\vee g_{\\_}3)\wedge g_{\\_}2\wedge g_{\\_}4))$

Let $M_{\\_}1,M_{\\_}2,M_{\\_}3$ and $M_{\\_}4$ be the four enforcers
associated to each traffic light (one per traffic light). Let
$\sigma\in\Sigma$ be the event emitted by the system,
$\sigma=\\{g_{\\_}1,g_{\\_}2,g_{\\_}3\\}$ which means that only the green
light of the first three traffic lights is on.

###  B.1 Enforcement using a Decision based on Global Exploration

We describe in detail an example of the behaviour of the first algorithm.

#### Rewriting the temporal operators

We start by using rwT in order to rewrite the temporal operators and to start
separating the present and future obligations.

$\displaystyle\texttt{rwT}(\varphi)$
$\displaystyle=\texttt{rwT}(\textsc{{G}}((g_{\\_}1\wedge
g_{\\_}3\wedge\neg(g_{\\_}2\vee g_{\\_}4))\vee(\neg(g_{\\_}1\vee
g_{\\_}3)\wedge g_{\\_}2\wedge g_{\\_}4)))$
$\displaystyle=\texttt{rwT}(g_{\\_}1\wedge g_{\\_}3\wedge\neg(g_{\\_}2\vee
g_{\\_}4))\vee(\neg(g_{\\_}1\vee g_{\\_}3)\wedge g_{\\_}2\wedge
g_{\\_}4)\wedge\textsc{{X}}\varphi$
$\displaystyle=(\texttt{rwT}(g_{\\_}1\wedge g_{\\_}3\wedge\neg(g_{\\_}2\vee
g_{\\_}4))\vee$ $\displaystyle\indent\ \texttt{rwT}(\neg(g_{\\_}1\vee
g_{\\_}3)\wedge g_{\\_}2\wedge g_{\\_}4)\wedge\textsc{{X}}\varphi$
$\displaystyle=(\texttt{rwT}(g_{\\_}1)\wedge\texttt{rwT}(g_{\\_}3)\wedge\texttt{rwT}(\neg(g_{\\_}2\vee
g_{\\_}4))\vee$ $\displaystyle\indent\ \texttt{rwT}(\neg(g_{\\_}1\vee
g_{\\_}3))\wedge\texttt{rwT}(g_{\\_}2)\wedge\texttt{rwT}(g_{\\_}4))\wedge\textsc{{X}}\varphi$
$\displaystyle=(g_{\\_}1\wedge v_{\\_}{3}\wedge\neg\texttt{rwT}(g_{\\_}2\vee
g_{\\_}4)\vee$ $\displaystyle\indent\ \neg\texttt{rwT}(g_{\\_}1\vee
g_{\\_}3)\wedge g_{\\_}2\wedge g_{\\_}4))\wedge\textsc{{X}}\varphi$
$\displaystyle=(g_{\\_}1\wedge
v_{\\_}{3}\wedge\neg(\texttt{rwT}(g_{\\_}2)\vee\texttt{rwT}(g_{\\_}4))\vee$
$\displaystyle\indent\
\neg(\texttt{rwT}(g_{\\_}1)\vee\texttt{rwT}(g_{\\_}3))\wedge g_{\\_}2\wedge
g_{\\_}4))\wedge\textsc{{X}}\varphi$ $\displaystyle=(g_{\\_}1\wedge
g_{\\_}3\wedge\neg(g_{\\_}2\vee g_{\\_}4)\vee\neg(g_{\\_}1\vee\neg
g_{\\_}3)\wedge g_{\\_}2\wedge g_{\\_}4)\wedge\textsc{{X}}\varphi$

We denote the result of this rewriting by $\varphi_{\\_}{rwT}$.

#### Transformation to TDNF

Applying function DNF (see Sec. A.5) on $\varphi_{\\_}{rwT}$ transforms the
formula into its normal form:

$((g_{\\_}1\wedge g_{\\_}3\wedge\neg g_{\\_}2\wedge\neg g_{\\_}4)\vee(\neg
g_{\\_}1\wedge\neg g_{\\_}3\wedge g_{\\_}2\wedge
g_{\\_}4))\wedge\textsc{{X}}\varphi$

Then, it distributes the conjunctions over disjunctions until stabilization to
reach the TDNF:

$(g_{\\_}1\wedge g_{\\_}3\wedge\neg g_{\\_}2\wedge\neg
g_{\\_}4\wedge\textsc{{X}}\varphi)\vee(\neg g_{\\_}1\wedge\neg g_{\\_}3\wedge
g_{\\_}2\wedge g_{\\_}4\wedge\textsc{{X}}\varphi)$

We call this result $\varphi_{\\_}{DNF}$.

#### Initialization of the enforcer state

We separate the present and the future obligations to create a set of Temporal
Obligation Pairs (TOP):

$\texttt{encode}(\varphi_{\\_}{DNF})=\\{(g_{\\_}1\wedge g_{\\_}3\wedge\neg
g_{\\_}2\wedge\neg g_{\\_}4,\varphi),(\neg g_{\\_}1\wedge\neg g_{\\_}3\wedge
g_{\\_}2\wedge g_{\\_}4,\varphi)\\}$

We denote encode($\varphi_{\\_}{DNF}$) by $\varphi_{\\_}{TOP}$. The first
element of each pair represents the present obligations that needs to be
satisfied by the current event $\sigma$ in the current timestamp. The second
element represents the future obligations that will need to be satisfied by
the trace in the future (only if the corresponding present obligations are
satisfied in the current timestamp).

The state of the current enforcer is initialized to:
$\texttt{tcl}(\emptyset)=(\varphi_{\\_}{TOP},0)$, where tcl is the partial
function representing the state of the enforcer.

#### Evaluation ($M_{\\_}1$)

If $M_{\\_}1$, which did the previous transformations, can rewrite the formula
(meaning it contains one of the enforcer’s local observations), then it
updates the domain of the tcl. The enforcer starts by computing the set
containing the atomic propositions that still need to be evaluated. We get
$\texttt{apr}(\texttt{tcl})=\\{g_{\\_}1,g_{\\_}2,g_{\\_}3,g_{\\_}4\\}$. We can
see here that $AP_{\\_}1$ contains atomic propositions that are not in the
formula ($\\{y_{\\_}1$ and $r_{\\_}1\\}$). Therefore, the rewriting using the
event $\\{g_{\\_}1,y_{\\_}1\\}$ yields the same result as the one using
$\\{g_{\\_}1\\}$. To avoid these useless rewritings, the domain is updated
using the events from $\Sigma_{\\_}1^{r}$ instead of $\Sigma_{\\_}1$, i.e.
using events containing only atomic propositions that have not been evaluated
yet and that can be observed locally by the current enforcer. Here,
$AP_{\\_}1\cap\texttt{apr}(\texttt{tcl})=\\{g_{\\_}1\\}$ so $M_{\\_}1$ can
update tcl (because the set is not empty).

Function updateTCL is used to update the obligations. For each element of
$\Sigma_{\\_}i^{r}$, the domain of tcl is updated (as well as the
corresponding images). Here, we have
$\Sigma_{\\_}i^{r}=\\{\emptyset,\\{g_{\\_}1\\}\\}$ and we recall that,
currently, tcl is only defined on $\emptyset$ so that
$\texttt{tcl}(\emptyset)=(\varphi_{\\_}{TOP},0)$. After the update, tcl is
such that:

$\displaystyle\texttt{tcl}(\emptyset\cup\emptyset)$
$\displaystyle=(\texttt{rw}_{\\_}1(\varphi_{\\_}{TOP},\emptyset),\text{
}0+\texttt{distance}(\sigma,\emptyset,AP_{\\_}1\cap\texttt{apr}(\texttt{tcl}))),$
$\displaystyle\texttt{tcl}(\emptyset\cup\\{g_{\\_}1\\})$
$\displaystyle=(\texttt{rw}_{\\_}1(\varphi_{\\_}{TOP},\\{g_{\\_}1\\}),\text{
}0+\texttt{distance}(\sigma,\\{g_{\\_}1\\},AP_{\\_}1\cap\texttt{apr}(\texttt{tcl})))$

Henceforth:

$\displaystyle\texttt{tcl}(\emptyset)$
$\displaystyle=(\\{{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)},(\neg
g_{\\_}3\wedge g_{\\_}2\wedge g_{\\_}4,\varphi)\\},\text{ }1),$
$\displaystyle\texttt{tcl}(\\{g_{\\_}1\\})$
$\displaystyle=(\\{(g_{\\_}3\wedge\neg g_{\\_}2\wedge\neg
g_{\\_}4,\varphi),{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)}\\},\text{
}0)$

#### Reduction of the domain ($M_{\\_}1$)

The monomials in which the present obligations have been evaluated to $\bot$
are removed. In the example above, the removed pairs are the shaded ones.

#### Transmission of the tcl($M_{\\_}1$)

Finally,
$\texttt{apr}(\texttt{tcl})=\\{g_{\\_}1,g_{\\_}2,g_{\\_}3,g_{\\_}4\\}\setminus\\{g_{\\_}1\\}=\\{g_{\\_}2,g_{\\_}3,g_{\\_}4\\}$.
As $\texttt{apr}(\texttt{tcl})\neq\emptyset$, $M_{\\_}1$ sends communicates
its state (tcl) to another enforcer that can evaluate at least one atomic
proposition in $\texttt{apr}(\texttt{tcl})$, i.e. a enforcer $M_{\\_}j$ so
that $AP_{\\_}j\cap\texttt{apr}(\texttt{tcl})\neq\emptyset$. In this example,
$M_{\\_}2$, $M_{\\_}3$ and $M_{\\_}4$ can evaluate one of the remaining atomic
propositions so $M_{\\_}2$ is chosen (because $2$ is the smallest $j$
satisfying the previous requirement).

#### Update ($M_{\\_}{2}$)

$M_{\\_}2$ receives the partial function (tcl) representing the state of
$M_{\\_}1$ and does the same update as before. Here, we have $2^{AP_{\\_}2\cap
AP_{\\_}r}=\\{\emptyset,\\{g_{\\_}2\\}\\}$. After calling updateTCL(tcl,
$\sigma$), the partial function is defined as follows:

$\displaystyle\texttt{tcl}(\emptyset)$
$\displaystyle=(\\{{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)}\\},\text{
}2),$ $\displaystyle\texttt{tcl}(\\{g_{\\_}1\\})$
$\displaystyle=(\\{(g_{\\_}3\wedge\neg g_{\\_}4,\varphi)\\},\text{ }1),$
$\displaystyle\texttt{tcl}(\\{g_{\\_}2\\}$ $\displaystyle=(\\{(\neg
g_{\\_}3\wedge g_{\\_}4,\varphi)\\},\text{ }1),$
$\displaystyle\texttt{tcl}(\\{g_{\\_}1,g_{\\_}2\\})$
$\displaystyle=(\\{{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)}\\},\text{
}0)$

Function reduce removes the two shaded pairs above and then removes the events
$\emptyset$ and $\\{g_{\\_}1\\}$ from the domain as they lead to a violation
of $\varphi$ (the set of TOP associated to these event is empty). $M_{\\_}3$
and $M_{\\_}4$ can evaluate one of the remaining atomic propositions
$M_{\\_}2$ sends tcl to $M_{\\_}3$ (because $3<4$).

#### Update ($M_{\\_}{3}$)

$M_{\\_}3$ receives tcl and updates it using updateTCL. We get:

$\displaystyle\texttt{tcl}(\\{g_{\\_}1\\})$
$\displaystyle=(\\{{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)}\\},\text{
}2),$ $\displaystyle\texttt{tcl}(\\{g_{\\_}2\\})$
$\displaystyle=(\\{(g_{\\_}4,\varphi)\\},\text{ }2),$
$\displaystyle\texttt{tcl}(\\{g_{\\_}1,g_{\\_}3\\})$ $\displaystyle=(\\{(\neg
g_{\\_}4,\varphi)\\},\text{ }1),$
$\displaystyle\texttt{tcl}(\\{g_{\\_}2,g_{\\_}3\\})$
$\displaystyle=(\\{{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)}\\},\text{
}1)$

After having removed the monomials evaluated to $\bot$ and then removed the
events associated with an empty set of TOP from the domain,tcl is sent to
$M_{\\_}4$ in order to evaluate $g_{\\_}4$.

#### Update ($M_{\\_}{4}$)

$M_{\\_}4$ receives tcl and updates it using updateTCL. We get:

$\displaystyle\texttt{tcl}(\\{g_{\\_}2\\})$
$\displaystyle=(\\{{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)}\\},\text{
}2),$ $\displaystyle\texttt{tcl}(\\{g_{\\_}1,g_{\\_}3\\})$
$\displaystyle=(\\{(\top,\varphi)\\},\text{ }1),$
$\displaystyle\texttt{tcl}(\\{g_{\\_}2,g_{\\_}4\\})$
$\displaystyle=(\\{(\top,\varphi)\\},\text{ }3),$
$\displaystyle\texttt{tcl}(\\{g_{\\_}1,g_{\\_}3,g_{\\_}4\\}$
$\displaystyle=(\\{{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)}\\},\text{
}2)$

The two monomials evaluated to $\bot$ are removed (as well as the event
leading to a violation of $\varphi$) using reduce and, as every atomic
proposition of the formula has been evaluated, the decision rule is applied to
choose which event to emit.

#### Decision

The event $\sigma$ is not in the domain of tcl anymore which means that
$\sigma$ leads to a violation of $\varphi$, therefore, the enforcer has to
choose an event with the smallest distance to $\sigma$. Here, there is only
one event with a minimal distance (of 1) so
$\sigma^{\prime}=\\{g_{\\_}1,g_{\\_}3\\}$ is chosen and $M_{\\_}2$ modifies
its local observation (in which $g_{\\_}2=\top$) accordingly in order to
enforce the specification. The formula that will need to be monitored during
the next timestamp is $\varphi^{2}=\varphi$.

###  B.2 Enforcement using a Decision based on Local Exploration

We describe in detail the execution of the second version on the same example
as in appendix B.1. We are using the same enforcers (each of them have the
same $AP_{\\_}i$), same properties and same event in order to show the
differences between the two.

As the initialization of the enforcer and the first update is the same as
before, we skip these parts and start when the first enforcer applies the
local decision rule.

#### Local decision rule and communication ($M_{\\_}1$)

At this point, the enforcer has reduced the domain of the tcl using reduce.
Currently, function tcl is such that:

$\displaystyle\texttt{tcl}(\emptyset)$ $\displaystyle=(\\{(\neg g_{\\_}3\wedge
g_{\\_}2\wedge g_{\\_}4,\varphi)\\},\text{ }1),$
$\displaystyle\texttt{tcl}(\\{g_{\\_}1\\})$
$\displaystyle=(\\{(g_{\\_}3\wedge\neg g_{\\_}2\wedge\neg
g_{\\_}4,\varphi)\\},\text{ }0)$

The local decision rule is now applied in order to determine the pair that
will be sent to the next enforcer ($\texttt{apr}(\texttt{tcl})\neq\emptyset$).
There is one event in the domain of tcl that is associated to a metric of 0
($\\{g_{\\_}1\\}$). Therefore, the pair
$(\\{g_{\\_}1\\},(\\{(g_{\\_}3\wedge\neg g_{\\_}2\wedge\neg
g_{\\_}4,\varphi)\\},\text{ }0))$ is sent to the next enforcer: $M_{\\_}2$.

#### Update ($M_{\\_}{2}$)

After receiving the pair, the state of $M_{\\_}2$ is represented by the
partial function only defined for $\\{g_{\\_}1\\}$ as follows:
$\texttt{tcl}(\\{g_{\\_}1\\})=(\\{(g_{\\_}3\wedge\neg g_{\\_}2\wedge\neg
g_{\\_}4,\varphi)\\},\text{ }0)$. This function is updated with every element
from
$2^{AP_{\\_}2\cap\texttt{apr}(\texttt{tcl})}=\\{\emptyset,\\{g_{\\_}2\\}\\}$
which gives:

$\displaystyle\texttt{tcl}(\\{g_{\\_}1\\})$
$\displaystyle=\\{(g_{\\_}3\wedge\neg g_{\\_}4,\varphi)\\},\text{ }1),$
$\displaystyle\texttt{tcl}(\\{g_{\\_}1,g_{\\_}2\\})$
$\displaystyle=(\\{{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)}\\},\text{
}0)$

After reducing the size of the domain, it only contains a single element
($\\{g_{\\_}1\\}$) so the pair containing this element and its image is sent
to the next enforcer ($\texttt{apr}(\texttt{tcl})\neq\emptyset$): $M_{\\_}3$.

#### Update ($M_{\\_}{3}$)

$M_{\\_}3$ receives the pair $(\\{g_{\\_}1\\},(\\{(g_{\\_}3\wedge\neg
g_{\\_}4,\varphi)\\},\text{ }1)$ and its state is initialized as follows:
$\texttt{tcl}(\\{g_{\\_}1\\})=(\\{(g_{\\_}3\wedge\neg
g_{\\_}4,\varphi)\\},\text{ }1)$. It is then updated using updateTCL which
gives:

$\displaystyle\texttt{tcl}(\\{g_{\\_}1\\})$
$\displaystyle=(\\{{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)}\\},\text{
}2),$ $\displaystyle\texttt{tcl}(\\{g_{\\_}1,g_{\\_}3\\})$
$\displaystyle=(\\{(\neg g_{\\_}4,\varphi)\\},\text{ }1)$

After reducing the size of the domain with reduce, there is only one element
left. $\texttt{apr}(\texttt{tcl})\neq\emptyset$ so it is sent to the next
enforcer ($M_{\\_}4$).

#### Update ($M_{\\_}{4}$) and Final Decision

$M_{\\_}4$ initializes its state as follows:
$\texttt{tcl}(\\{g_{\\_}1,g_{\\_}3\\})=(\\{(\neg g_{\\_}4,\varphi)\\},\text{
}1)$. After updating it, we have:

$\displaystyle\texttt{tcl}(\\{g_{\\_}1,g_{\\_}3\\})$
$\displaystyle=(\\{(\top,\varphi)\\},\text{ }1),$
$\displaystyle\texttt{tcl}(\\{g_{\\_}1,g_{\\_}3,g_{\\_}4\\})$
$\displaystyle=(\\{{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}\pgfsys@color@gray@stroke{0.5}\pgfsys@color@gray@fill{0.5}(\bot,\varphi)}\\},\text{
}2)$

Again, the domain of tcl is reduced to a single element and, as there is no
atomic propositions that needs to be evaluated in the formula, $M_{\\_}4$
decides which event to emit. There is only one event that can be chosen:
$\sigma^{\prime}=\\{g_{\\_}1,g_{\\_}3\\}$. $M_{\\_}2$ enforces the property by
modifying its local observation ($g_{\\_}2$ has to be equal to $\bot$ instead
of $\top$). The formula to evaluate during the next timestamp is
$\varphi^{2}=\varphi$.

##  Appendix C Proofs

######  Proof 1 (Property 1)

Any formula rewritten by rwT is semantically equivalent to its input formula
because we are only applying expansion laws, i.e. transforming a formula into
another equivalent formula [22].

######  Proof 2 (Property 2)

The fact that every temporal operators (apart from X) is preceded by X also is
a direct consequence of using the expansion laws.

######  Proof 3 (Property 3)

Any formula transformed into its DNF by DNF is semantically equivalent to the
input formula. In negF, we are only propagating negations until they are
applied to atomic propositions. We use the standard equivalences on operators
from propositional logic and equivalences given in [22] for temporal
operators. Function nf only transforms implications and equivalences into an
equivalent formula also using the standard equivalences of propositional
logic. Function isDNF does not modify the formula and, finally, function
distrib uses the distributive law from propositional logic. Therefore, as all
these operations yield a semantically equivalent formula, so does DNF that
only uses these four functions.

######  Proof 4 (Property 4)

Let us show that, after transforming a formula that has been rewritten by rwT
into its DNF, every temporal operators (apart from X) is preceded by X.

According to Property 2, every temporal operators in a formula rewritten by
rwT is preceded by X (apart from X). Function DNF uses two functions that
modify the input formula: nf and distrib. Function nf uses function negF and
removes equivalences/implications from the input formula.

Removing equivalences/implications and distributing $\wedge$ over $\vee$
simply moves the sub formulas of the form X$\varphi$ without modifying them
and does not introduce any new temporal operators. Function negF applies
negations on sub formulas which means that it does not introduce any new
temporal operators nor move them (it only changes them into their dual).

Therefore, a formula that has been rewritten by rwT and then transformed into
its DNF does have all of its temporal operators (except X) preceded by X.

######  Proof 5 (Property 5)

Let us show that $u\cdot\sigma\not\in bad(\varphi^{t})$ iff there exists
$(p,f)\in\texttt{encode}(\varphi^{t})$ so that $u\cdot\sigma\vDash p$ and
$u\cdot\sigma\not\in bad(f)$.

This result comes directly from the definition of encode. As the formula is in
DNF, if a single monomial evaluates to $\top$ then the whole formula is as
well. Therefore, if there is a pair $(p,f)$ (which represents a monomial that
is equal to $p\wedge f$) in the result of encode($\varphi$) that evaluates to
$\top$, then the whole formula does as well.

######  Proof 6 (Lemma 1)

Let us show that, in both algorithms, $\forall t\in\mathbb{N},\
\varphi^{t}\not\equiv\bot\Rightarrow\varphi^{t+1}\not\equiv\bot$.

We recall that $\varphi^{t}$ represents the formula that is being monitored
during the $t$-th timestamp. $\varphi^{t+1}$ is equal to the disjunction of
the future obligations associated with the event that has been emitted.
Assuming we apply a simplification on the input formula before the
initialization in order to simplify any sub formula that is equivalent to
$\bot$, any monomial in which the future obligations are equivalent to $\bot$
will be removed (through reduce). Therefore, it is impossible to have a
formula $\varphi^{t+1}$ so that every monomial composing it is equivalent to
$\bot$. In fact, no monomial in this formula can be equivalent to $\bot$).

######  Proof 7 (Soundness)

Let us show that $\forall u\in\Sigma^{*},\ E(u)\not\in
bad(\varphi_{\\_}{init})$ by induction on the size of the trace.

Let $u\in\Sigma^{*}$ be a trace of size 1 so that $u=\sigma$ and
$\varphi^{1}=\varphi_{\\_}{init}$ the formula that is being monitored (at the
first timestamp). Function reduce ensures that any monomial evaluated to
$\bot$ is removed from its set of TOP and that any event associated to an
empty set of TOP (i.e. bad prefix of the property) is removed from the domain
of the TCL. This means that at the end of the algorithm, the events that are
still in the domain are not bad prefixes of $\varphi^{1}$ and, as
$\varphi^{1}\not\equiv\bot$, there is at least one event that does not lead to
a violation of $\varphi^{1}$ (which means that the domain is never empty). As
the event emitted by the last monitor is chosen from the domain, by
construction, it cannot lead to a violation of $\varphi^{1}$. Therefore, we
have $E(u)=E(\sigma)=\sigma^{\prime}$ so that $E(u)\not\in bad(\varphi^{1})$.
Therefore, the property holds for a trace of size 1 (assuming
$\varphi_{\\_}{init}\not\equiv\bot$).

Let us now assume that the property holds for a trace of size
$n\in\mathbb{N^{*}}$, that is $\forall u\in\Sigma^{*},|u|=n\ \Rightarrow
E(u)\not\in bad(\varphi_{\\_}{init})$. Let us show that it also holds for a
trace of size $n+1$.

Let $u^{\prime}=a(0)\dotsb a(n)\in\Sigma^{*},|u^{\prime}|=n+1$. $u^{\prime}$
is of the form $u\cdot\sigma$ with $u\in\Sigma^{*},|u|=n$ and
$\sigma\in\Sigma$. We need to show that $E(u^{\prime})\not\in bad(\varphi)$,
which is equivalent to showing that $E(u)\cdot E(\sigma)\not\in bad(\varphi)$.
According to Lemma 1, if $\varphi^{t}\not\equiv\bot$, then
$\varphi^{t+1}\not\equiv\bot$. Therefore, since
$\varphi_{\\_}{init}=\varphi^{1}\not\equiv\bot$, then
$\varphi^{n}\not\equiv\bot$ ($\varphi^{n}$ is the formula monitored at the
n+1-th timestamp). As explained above, reduce ensures that $E(\sigma)$ (the
event emitted at the end) is not a bad prefix of $\varphi^{n}$. Therefore, as
$E(u)\not\in bad(\varphi_{\\_}{init})$ (given by the induction hypothesis), we
have $(E(u)\cdot E(\sigma)\not\in bad(\varphi)$.

######  Proof 8 (Optimality)

Let us show that $\forall i\in\Sigma^{*},\ \forall\sigma\in\Sigma,\
\exists\sigma^{\prime}\in\Sigma,\
E(i\cdot\sigma)=E(i)\cdot\sigma^{\prime}\wedge(\forall\sigma^{\prime\prime}\in\Sigma,\
\texttt{distance}(\sigma,\sigma^{\prime\prime},AP)<\texttt{distance}(\sigma,\sigma^{\prime},AP)\Rightarrow
E(i)\cdot\sigma^{\prime\prime}\in bad(\varphi))$

Function reduce removes the bad prefixes of $\varphi$ from the domain (which
means that the event emitted at the end is not a bad prefix either). The first
criteria used (in the first algorithm) to decide which event $\sigma^{\prime}$
to emit is to choose it so that distance($\sigma$, $\sigma^{\prime}$, AP) is
minimal. This means that, if $\sigma$ is not a bad prefix of $\varphi$, then
it will be the only event with a distance of 0 from $\sigma$. If not, then we
know by construction that the emitted event will be chosen from the set of
good prefixes of $\varphi$ and that have the smallest distance from $\sigma$
(among the events that are in the domain).

Therefore, the first algorithm does guarantee _Optimality_ as no bad prefixes
can be emitted.

######  Proof 9 (Transparency)

The proof is identical to the one above (for _Optimality_) because, if
$\sigma$ does not lead to a violation of $\varphi$ then it is the only event
with a distance of 0 from $\sigma$.