Antoine El-Hokayem
email: antoine.el-hokayem@univ-grenoble-alpes.fr

Yliès Falcone
email: ylies.falcone@univ-grenoble-alpes.fr

Monitoring Decentralized Specifications

Keywords: Runtime Verification, Monitoring, Decentralized Specification, Monitorability, Eventual Consistency

published or not. The documents may come

INTRODUCTION

Runtime Verification (RV) [2, [START_REF] Falcone | A Tutorial on Runtime Verification[END_REF][START_REF] Leucker | A brief account of runtime verification[END_REF]] is a lightweight formal method which consists in verifying that a run of a system is correct wrt a specification. The specification formalizes the behavior of the system typically in logics (such as variants of Linear-Time Temporal Logic, LTL) or finite-state machines. Typically the system is considered as a blackbox that feeds events to a monitor. An event usually consists of a set of atomic propositions that describe some abstract operations or states in the system. The sequence of events transmitted to the monitor is referred to as the trace. Based on the received events, the monitor emits verdicts in a truth domain that indicate the compliance of the system to the specification. RV techniques have been used for instance in the context of decentralized automotive [START_REF] Sylvain Cotard | A Data Flow Monitoring Service Based on Runtime Verification for AUTOSAR[END_REF] and medical [START_REF] Leucker | Runtime Verification for Interconnected Medical Devices[END_REF] systems. In both cases, RV is used to verify correct communication patterns between the various components and their adherence to the architecture and their formal specifications. While RV comprehensively deals with monolithic systems, multiple challenges are presented when scaling existing approaches to decentralized systems, that is, systems with multiple components with no central observation point.

Challenges. Several algorithms have been designed [START_REF] Bauer | Decentralised LTL Monitoring[END_REF][START_REF] Bonakdarpour | Challenges in Fault-Tolerant Distributed Runtime Verification[END_REF][START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF][START_REF] Falcone | Efficient and Generalized Decentralized Monitoring of Regular Languages[END_REF] and used [START_REF] Bartocci | Sampling-based Decentralized Monitoring for Networked Embedded Systems[END_REF] to monitor decentralized systems. Algorithms are primarily designed to address one issue at a time and are typically experimentally evaluated by considering runtime and memory overheads. However, such algorithms are difficult to compare as they may combine multiple approaches at once. For example, algorithms that use LTL rewriting [START_REF] Bauer | Decentralised LTL Monitoring[END_REF][START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF][START_REF] Rosu | Rewriting-Based Techniques for Runtime Verification[END_REF] not only exhibit variable runtime behavior due to the rewriting, but also incorporate different monitor synthesis approaches that separate the specification into multiple smaller specifications depending on the monitor. In this case, we would like to split the problem of generating equivalent decentralized specifications from a centralized one (synthesis) from the problem of monitoring. In addition, works on characterizing what one can monitor (i.e., monitorability [START_REF] Falcone | What can you verify and enforce at runtime?[END_REF][START_REF] Kim | Formally specified monitoring of temporal properties[END_REF][START_REF] Pnueli | PSL Model Checking and Run-Time Verification Via Testers[END_REF]) for centralized specifications exist [START_REF] Bauer | Runtime Verification for LTL and TLTL[END_REF][START_REF] Diekert | Topology, monitorable properties and runtime verification[END_REF][START_REF] Falcone | What can you verify and enforce at runtime?[END_REF], but do not extend to decentralized specifications. For example by splitting an LTL formula ad-hoc, it is possible to obtain a non-monitorable subformula 1 which interferes with the completeness of a monitoring algorithm.

Contributions. In this paper, we tackle the presented challenges using two complementary approaches. We first lay out the basic blocks, by introducing our basic data structure, and the basic notions of monitoring with expressions in Sec. [START_REF] Basin | Failure-aware Runtime Verification of Distributed Systems[END_REF]. Then, we present our first approach, a middle ground between rewriting and automata evaluation by introducing the Execution History Encoding (EHE) data structure in Sec. [START_REF] Bauer | Runtime Verification for LTL and TLTL[END_REF]. We restrict the rewriting to boolean expressions, determine the parameters and their respective effect on the size of expressions, and fix upper bounds. In addition, EHE is designed to be particularly flexible in processing, storing and communicating the information in the system. EHE operates on an encoding of atomic propositions and guarantees strong-eventual consistency [START_REF] Shapiro | Conflict-Free Replicated Data Types[END_REF]. In Sec. 5, we shift the focus on studying decentralized specifications and their properties, we define their semantics, interdependencies and study their monitorability. We aim at abstracting the high-level steps of decentralized monitoring. By identifying these steps, we elaborate a general decentralized monitoring algorithm. We view a decentralized system as a set of components C. We associate n monitors to these components with the possibility of two or more monitors being associated to a component. We see a decentralized specification as a set of n finite-state automata with specific properties. Each automaton is associated with a monitor. Therefore, we generalize monitoring algorithms to multiple monitors. Therefore, we present a general decentralized monitoring algorithm that uses two high level steps: setup and monitor. Monitoring a centralized system can be seen as a special case with one component, one specification, and one monitor. Additionally, the two high level operations help decompose monitoring into different subproblems and define them independently. For example, the problem of generating a decentralized specification from a centralized specification is separated from checking the monitorability of a specification, and also separated from the computation and communication performed by the monitor. In Sec. 6, we use our analysis of EHE to study the behavior of three existing algorithms and discuss the situations that advantage certain algorithms over others. In Sec. 7, we present THEMIS, a JAVA tool that implements the concepts in this paper; and show how it can be used to design and analyze new algorithms. In Sec. 8, we use THEMIS to create new metrics related to load-balancing and our data structures, and to experimentally verify our analysis. Finally, we conclude and present future work in Sec. 9. An extended version of this paper (with full proofs) is available at [START_REF] El | THEMIS Website[END_REF].

RELATED WORK

Several approaches have been taken to handle decentralized monitoring focusing on different aspects of the problem. The first class of approaches consists in monitoring by LTL formula rewriting [START_REF] Bauer | Decentralised LTL Monitoring[END_REF][START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF][START_REF] Rosu | Rewriting-Based Techniques for Runtime Verification[END_REF]. Given an LTL formula specifying the system, a monitor will rewrite the formula based on information it has observed or received from other monitors. Typically a formula is rewritten and simplified until it is equivalent to ⊤ (true) or ⊥ (false) at which point the algorithm terminates. Another approach [START_REF] Thati | Monitoring Algorithms for Metric Temporal Logic Specifications[END_REF] extends rewriting to focus on real-time systems. They use Metric Temporal Logic (MTL), which is an extension to LTL with temporal operators. This approach also covers lower bound analysis on monitoring MTL formulae. While these techniques are simple and elegant, rewriting varies significantly during runtime based on observations, thus analyzing the runtime behavior could prove difficult if not unpredictable. For example, when excluding specific syntactic simplification rules, G(⊤) could be rewritten ⊤∧G(⊤) and will keep growing in function of the number of timestamps. To tackle the unpredictability of rewriting LTL formulae, another approach [START_REF] Falcone | Efficient and Generalized Decentralized Monitoring of Regular Languages[END_REF] uses automata for monitoring regular languages, and therefore (i) can express richer specifications, and (ii) has predictable runtime behavior. This approach focuses on a centralized specification.

Another class of research focuses on handling a different problem that arises in distributed systems. In [START_REF] Bonakdarpour | Challenges in Fault-Tolerant Distributed Runtime Verification[END_REF], monitors are subject to many faults such as failing to receive correct observations or communicate state with other monitors. Therefore, the problem handled is that of reaching consensus with fault-tolerance, and is solved by determining the necessary verdict domain needed to be able to reach a consensus. To remain general, we do not impose the restriction that all monitors must reach the verdict when it is known, as we allow different specifications per monitor. Since we have heterogeneous monitors, we are not particularly interested in consensus. However for monitors that monitor the same specification, we are interested in strong eventual consistency. We maintain the 3-valued verdict domain, and tackle the problem from a different angle by considering eventual delivery of messages. Similar work [START_REF] Basin | Failure-aware Runtime Verification of Distributed Systems[END_REF] extends the MTL approach to deal with failures by modeling knowledge gaps and working on resolving these gaps.

We also highlight that the mentioned approaches [START_REF] Basin | Failure-aware Runtime Verification of Distributed Systems[END_REF][START_REF] Bauer | Decentralised LTL Monitoring[END_REF][START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF], and other works [START_REF] Diekert | On Distributed Monitoring of Asynchronous Systems[END_REF][START_REF] Scheffel | Three-valued asynchronous distributed runtime verification[END_REF][START_REF] Sen | Efficient Decentralized Monitoring of Safety in Distributed Systems[END_REF] do in effect introduce a decentralized specification. These approaches define separate monitors with different specifications, typically consisting of splitting the formula into subformulae. Then, they describe the collaboration between such monitors. However, they primarily focus on presenting one global formula of the system from which they derive multiple specifications. In our approach, we generalize the notions from a centralized to a decentralized specification, and separate the problem of generating multiple specifications equivalent to a centralized specification from the monitoring of a decentralized specification.

COMMON NOTIONS

We begin by introducing the dict data structure used to build more complex data structures in Sec. 3.1. Then, we introduce the basic concepts for decentralized monitoring in Sec. 3.2.

The dict Data Structure

In monitoring decentralized systems, monitors typically have a state, and attempt to merge other monitor states with theirs to maintain a consistent view of the running system, that is, at no point in the execution, should two monitors receive updates that conflict with one another. We would like in addition, that any two monitors receiving the same information be in equivalent states. Therefore, we are interested in designing data structures that can replicate their state under strong eventual consistency (SEC) [START_REF] Shapiro | Conflict-Free Replicated Data Types[END_REF], they are known as state-based convergent replicated data-types (CvRDTs). We use a dictionary data structure dict as our basic building block that maps a key to a value. dict supports two operations: query and merge. The merge operation is the only operation that modifies dict. The modifications never remove entries, the state of dict is then monotonically increasing. By ensuring that merge is idempotent, commutative, and associative we fulfill the necessary conditions for our data structure to be a CvRDT. Proposition 3.1. Data structure dict with operations query and merge is a CvRDT.

We model dict as a partial function f. The keys are the domain of f, i.e., dom(f) and values are mapped to each entry of the domain. The query operation checks if a key k ∈ dom(f) and returns f(k). If k dom(f), then it is undef. The merge operation of a dict f with another dict д, is modeled as function composition. Two partial functions f and g are composed using operator † op where op :

(dom(f ) × dom(д)) → (codom(f ) ∪ codom(д)) is a binary function. f † op g(x) : dom(f) ∪ dom(g) → codom(f) ∪ codom(g) =            op(f(x), g(x)) if x ∈ dom(f) ∩ dom(g) g(x) if x ∈ dom(g) \ dom(f) f(x) if x ∈ dom(f) \ dom(g) undef otherwise
On sets of functions, † op applies pairwise: op {f 1 , . . .

f n } = ((f 1 † op f 2 ) . . . f n )
The following two operators are used in the rest of the paper: † 2 and † ∨ . We define both of these operators to be commutative, idempotent, and associative to ensure SEC.

† 2 (x, x ′ ) = x ′ if x ≺ x ′ x otherwise † ∨ (x, x ′ ) = x ∨ x ′
Operator † 2 acts as a replace function with the addition of a total order (≺) between the elements, so that it always chooses the highest element to guarantee idempotence, while † ∨ is simply the logical or operator. Respectively, we denote the pairwise set operators as2 and ∨ .

Basic Monitoring Concepts

We recall the basic building blocks of monitoring. We consider the set of verdicts B 3 = {⊤, ⊥, ?} to denote the verdicts true, false, not reached (or inconclusive) respectively. A verdict from B 2 = {⊤, ⊥} is a final verdict. Given a set of atomic propositions AP, we define an encoding of the atomic propositions as Atoms, this encoding is left to the monitoring algorithm to specify. Example 3.3 (Event). The event {⟨a, ⊤⟩, ⟨b, ⊥⟩} over AP = {a, b} indicates that the proposition a has been observed to be true, while b has been observed to be false.

Definition 3.4 (Memory).

A memory is a dict, and is modeled as a partial function M : Atoms → B 3 that associates an atom to a verdict. The set of all memories is defined as Mem.

Events are commonly stored in a monitor memory with some encoding (e.g., adding a timestamp). An event can be converted to a memory by encoding the atomic propositions to atoms, and associating their truth value: memc : 2 AP×B 2 × (Expr AP → Expr Atoms ) → Mem. Example 3.5 (Memory). Let e = {⟨a, ⊤⟩, ⟨b, ⊥⟩} be an event at t = 1, the resulting memories using our encoders are: memc(e, idt)

= [a → ⊤, b → ⊥], memc(e, ts 1 ) = [⟨1, a⟩ → ⊤, ⟨1, b⟩ → ⊥].
If we impose that Atoms be a totally ordered set, then two memories M 1 and M 2 can be merged by applying operator † 2 . The total ordering is needed for the operator † 2 . This ensures that the operation is idempotent, associative and commutative. Monitors that exchange their memories and merge them have a consistent snapshot of the memory, regardless of the ordering. Since memory is a dict and † 2 is idempotent, associative, and commutative, it follows from Prop. 3.1 that it is a CvRDT. Corollary 3.6. A memory with operation † 2 is a CvRDT.

In this paper, we perform monitoring by manipulating expressions in Expr. The first operation we provide is rw, which rewrites the expression to attempt to eliminate Atoms. Using information from a memory M, the expression is rewritten by replacing atoms with a final verdict (a truth value in B 2 ) in M when possible. Atoms that are not associated with a final verdict are kept in the expression. The operation rw yields a smaller formula to work with and repeatedly evaluate. Since c is associated with ? B 2 then it will not be replaced. The resulting expression is rw(e, M) = (⊤ ∨ ⊥) ∧ c.

We eliminate additional atoms using boolean logic. We denote by simplify(expr) the simplification of formula expr 2 . Example 3.9 (Simplification). Consider M = [a → ⊤] and e = (a ∧ b) ∨ (a ∧ ¬b). We have e ′ = rw(e, M) = (b ∨ ¬b). Atoms can be eliminated with simplify(e ′ ). We finally get ⊤.

We combine both rewriting and simplification in the eval function which determines a verdict from an expression expr. Definition 3.10 (Evaluating an expression). The evaluation of an boolean expression expr ∈ Expr using a memory M yields a verdict. eval :

Expr × Mem → B 3 : eval(expr, M) =        ⊤ if e ′ ⇔ ⊤ ⊥ if e ′ ⇔ ⊥ ?
otherwise with e ′ = simplify(rw(expr, M))

Function eval returns the ⊤ (resp. ⊥) verdict if the simplification after rewriting is (boolean) equivalent to ⊤ (resp. ⊥), otherwise it returns the verdict ?. A decentralized system is as set of components C, we associate a sequence of events to each component using a decentralized trace function.

Definition 3.12 (Decentralized trace). A decentralized trace is a function tr

: N × C → 2 AP×B 2 .
Function tr assigns an event to a component for a given timestamp. We additionally define function lu : AP → C to associate an observation to a component 3

. lu(ap) = c s.t. ∃t ∈ N, ∃v ∈ B 2 : ⟨ap, v⟩ ∈ tr(t, c).
We consider timestamp 0 to be associated with the initial state, therefore our traces start at 1. Thus, a finite trace of length n is a function tr with a domain [1, n]. An empty trace has length 0 and is denoted by ∅. While tr gives us a view of what components can locally see, we reconstruct the global trace to reason about all observations. Definition 3.13 (Reconstructing a global trace). Given a decentralized trace tr of length n, the global trace ρ(tr

) = e 1 • . . . • e n is s.t. ∀i ∈ [1, n] : e i = c ∈ C tr(i, c).
For each timestamp i ∈ [1, n] we take all observations of all components and union them to get a global event. Consequently, an empty trace yields an empty global trace, ρ(∅) = ∅.

CENTRALIZED SPECIFICATIONS

We now focus on a decentralized system specified by one global automaton. The automaton is similar to automata defined for monitoring LTL 3 . This has been the topic of a lot of the Runtime Verification literature, we focus on adapting the approach to use a new data structure called Execution History Encoding (EHE). Typically, monitoring is done by labeling an automaton with events, then playing the trace on the automaton and determining the verdict based on the reached state. We present EHE, a data structure that encodes the necessary information from an execution of the automaton, and ensures strong eventual consistency. We begin by defining the specification automaton used for monitoring in Sec. 4.1, then we present the EHE data structure, illustrate how it can be used for monitoring in Sec. 4.2, and describe its use when partial observations are available in Sec. 4.3.

Preliminaries

Specifications are similar to the Moore automata generated by [START_REF] Bauer | Runtime Verification for LTL and TLTL[END_REF]. We modify labels to be boolean expressions over atomic propositions (in Expr AP ). Definition 4.1 (Specification). The specification is a deterministic Moore automaton ⟨Q, q 0 ∈ Q, δ, ver⟩ where δ : Q × Expr AP → Q is the transition function and ver : Q → B 3 is the labeling function.

We choose to label the transitions with boolean expressions as opposed to events, to keep a homogeneous representation 4 . The labeling function associates a verdict with each state. The specification is a complete automaton, only one label will be equivalent to ⊤, and for a given state q ∈ Q if we disjunct the labels of all outgoing transitions, the expression should be equivalent to ⊤. When using multiple automata we use the subscript notation to separate them, A i = ⟨Q i , q i 0 , δ i , ver i ⟩. The semantics of the specification are given by a function ∆5 .

q 0 q 1 a ∨ b ⊤ ¬a ∧ ¬b Figure 1: Representing F(a ∨ b)
Definition 4.2 (Semantics of the specification). Given A i , a state q ∈ Q i , and an event e, we build the memory M = memc(e, idt). We have:

∆ i (q, e) = q ′ | ∃q ′ ∈ Q i : go(q, q ′ , M) if e ∅ q otherwise go(q, q ′ , M) ⇔ ∃e ∈ Expr AP : δ (q, e) = q ′ ∧ eval(e, M) = ⊤
Using M we evaluate each label of an outgoing transition, and determine if a transition can be taken on e. In the case of an empty event (e = ∅), we return the same state. To handle a trace, we extend ∆ i to its reflexive and transitive closure in the usual way, and note it ∆ * i .

Example 4.3 (Monitoring using expressions). We consider Atoms = AP = {a, b} and the specifiction in Fig. 1, we seek to monitor F(a ∨b). The automaton consists of two states: q 0 and q 1 associated respectively with the verdicts ? and ⊤. We consider at t = 1 the event e = {⟨a, ⊤⟩, ⟨b, ⊥⟩}. The resulting memory is M = [a → ⊤, b → ⊥] (see Ex. 3.5). The transition from q 0 to q 1 is taken since eval(a ∨ b, M) = ⊤. Thus we have ∆(q 0 , e) = q 1 with verdict ver(q 1 ) = ⊤.

Execution History Encoding

The execution of the specification automaton, is in fact, the process of monitoring, upon running the trace, the reached state determines the verdict. An execution of the specification automaton can be seen as a sequence of states q 0 • q 1 • . . . q t • q t +1 . . .. It indicates that for each timestamp t ∈ [0, ∞[ the automaton is in the state q t . In a decentralized system, a component receives only local observations and does not necessarily have enough information to determine the state at a given timestamp. Typically, when sufficient information is shared between various components, it is possible to know the state q t that is reached in the automaton at t (we say that the state q t has been found, in such a case). The main motivation behind designing the EHE encoding is to ensure strong eventual consistency in determining the state q t of the execution of an automaton. That is, after two different monitors share their EHE, they should both be able to find q t for t (if there exists enough information to infer the global state), or if not enough information is available, they both find no state at all.

Definition 4.4 (Execution History Encoding -EHE). An Execution History Encoding (EHE) of the execution of an automaton

A i is a partial function I i : N × Q → Expr.
For a given execution, we encode the conditions to be in a state at a given timestamp as an expression in Expr. I i (t, q) = e indicates that the automaton is in state q at t if eval(e, M) is ⊤ given a memory M. Since we are encoding deterministic automata, we assume that when a state q is reachable at t, no other state is reachable at t (i.e., ∃q

∈ Q i : eval(I i (t, q)) = ⊤ =⇒ ∀q ′ ∈ Q i : q ′ q =⇒ eval(I i (t, q ′ )) ⊤).
To compute I i for a timestamp range, we will next define some (partial) functions: sel i , verAt i , next i , to i , and mov i . The purpose

Table 1: A tabular representation of I 2 t q expr 0 q 0 ⊤ 1 q 0 ¬ ⟨1, a ⟩ ∧ ¬ ⟨1, b ⟩ 1 q 1 ⟨1, a ⟩ ∨ ⟨1, b ⟩ 2 q 0 (¬ ⟨1, a ⟩ ∧ ¬ ⟨1, b ⟩) ∧ (¬ ⟨2, a ⟩ ∧ ¬ ⟨2, b ⟩) 2 q 1 ( ⟨1, a ⟩ ∨ ⟨1, b ⟩) ∨ ((¬ ⟨1, a ⟩ ∧ ¬ ⟨1, b ⟩) ∧ ( ⟨2, a ⟩ ∨ ⟨2, b ⟩))
of these functions is to extract information from I i at a given timestamp, which we can use to recursively build I i for future timestamps. Given a memory M which stores atoms, the function sel i determines if a state is reached at a timestamp t. If the memory does not contain enough information to evaluate the expressions, then the state is undef. The state q at timestamp t with a memory M is determined by:

sel i (I i , M, t) =        q if ∃q ∈ Q i : eval(I i (t, q), M) = ⊤ undef otherwise
Function verAt i is a short-hand to retrieve the verdict at t:

verAt i (I i , M, t) =        ver i (q) if ∃q ∈ Q i : q = sel i (I i , M, t) ? otherwise
The automaton is in the first state at t = 0. We start building up I i with the initial state and associating it with expression ⊤:

I i = [0 → q 0 → ⊤].
Then, we check the next possible states in the automaton; for timestamp t, we look at the states in I i (t) and check for the possible states at t + 1 using δ i .

next i (I i , t) = {q ′ | ∃q ∈ I i (t, q), ∃e : δ i (q, e) = q ′ } We now build the necessary expression to reach q ′ from multiple states q by disjoining the transition labels. Since the label consists of expressions in Expr AP we use an encoder to get an expression in Expr Atoms To get to the state q ′ at t + 1 from q we conjunct the condition to reach q at t.

to i (I i , t, q ′ , f ) = { ⟨q,e ′ ⟩ | δ (q,e ′ )=q ′ } (I i (t, q) ∧ enc(e ′ ))
By considering the disjunction, we cover all possible paths to reach a given state. Updating the conditions for the same state on the same timestamp is done by disjoining the conditions.

mov i (I i , t s , t e ) = mov i (I ′ i , t s + 1, t e ) if t s < t e I i otherwise
with:

I ′ i = I i † ∨ ∨ q ′ ∈next A (I i ,t s ) {t s + 1 → q ′ → to i (I i , t s , q ′ , ts t s +1 )}.
Finally, I ′ i is obtained by considering the next states and merging all their expressions to I i . We omit the A subscript when we have one automaton, and denote the encoding up to a timestamp t as I t .

Example 4.5 (Monitoring with EHE). We encode the execution of the automaton presented in Ex. 4.3. We have

I 0 = [0 → q 0 → ⊤].
From q 0 , it is possible to go to q 0 or q 1 , therefore next(I 0 , 0) = {q 0 , q 1 }. To move to q 1 at t = 1, we must be at q 0 at t = 0. The following condition must hold: to(I 0 , 0, q 1 , ts 1 ) = I 0 (0, q 0 ) ∧ (⟨1, a⟩ ∨ ⟨1, b⟩) = ⟨1, a⟩ ∨ ⟨1, b⟩. The encoding up to timestamp t = 2 is obtained with I 2 = mov(I 0 , 0, 2) and is shown in Table 1. We consider the same event as in Ex. 3.5 at t = 1, e = {⟨a, ⊤⟩, ⟨b, ⊥⟩}. Let M = memc(e, ts 1 ) = [⟨1, a⟩ → ⊤, ⟨1, b⟩ → ⊥]. It is possible to infer the state of the automaton after computing only I 1 = mov(I 0 , 0, 1) by using sel(I 1 , M, 1), we evaluate:

eval(I 1 (1, q 0 ), M) = ¬⟨1, a⟩ ∧ ¬⟨1, b⟩ = ⊥ eval(I 1 (1, q 1 ), M) = ⟨1, a⟩ ∨ ⟨1, b⟩ = ⊤
We find that q 1 is the selected state, with verdict ver(q 1 ) = ⊤.

Proposition 4.6 (Soundness). Given a decentralized trace tr of length n, we reconstruct the global trace e = ρ(tr) = e 0 • . . . • e n , we have: ∆ * (q 0 , e) = sel(I n , M n , n), with:

I n = mov([0 → q 0 → ⊤], 0, n), and
M n = 2 t ∈[1,n]
{memc(e t , ts t )}. EHE is sound wrt the specification automaton; both will indicate the same state reached with a given trace. Thus, the verdict is the same as it would be in the automaton. The proof is by induction on the reconstructed global trace. We first establish that both the EHE and the automaton memories evaluate two similar expressions modulo encoding with the same result. Then, starting from the same state at lenghth n, we build the expression (for each encoding) to reach the state at n + 1. Then we show that the expression (for each encoding) is the only expression that evaluates to ⊤.

Reconciling Execution History

We also note that EHE provides interesting properties for decentralized monitoring. Merging two EHEs of the same automaton with † ∨ allows us to aggregate information from two partial histories. For the same execution of the automaton and a timestamp t, if we have two encodings I(t, q) = e and I ′ (t, q) = e ′ , then we know that the automaton is in q at t iff either e or e ′ evaluates to ⊤ (Def. 4.4). Therefore, the new expression e ′′ = e ∨ e ′ can be an effective way to reconcile information from two encodings. The memory M can be embedded in an expression e by simply using rw(e, M) (Def. 3.7). Thus, by rewriting expressions and combining EHEs, it is possible to reconcile multiple partial observations of an execution. 2 shows the EHEs at t = 1. Constructing the EHE follows similarly from Ex. 4.5. We show the rewriting for both I 0 and I 1 respectively in the next two columns. Then, we show the result of combining the rewrites using † ∨ . We notice initially that since b is ⊥, m 1 could evaluate ¬⟨1, a⟩ ∨ ⊤ = ⊤ and know that the automaton is in state q 0 . However, for m 0 , this is not possible until the expressions are combined. By evaluating the combination (⊥ ∨ ¬⟨1, b⟩) ∨ ⊤ = ⊤, m 0 determines that the automaton is in state q 0 . In this case, we are only looking for expressions that evaluate to ⊤. We notice that the monitor m 1 can determine that q 1 is not reachable (since ⟨1, a⟩ ∧ ⊥ = ⊥) while m 0 cannot (⟨1, b⟩). This does not affect the outcome, as we are only looking for one expression that evaluates to ⊤, since both I 0 and I 1 are encoding the same execution.

q 0 q 1 a ∧ b ⊤ ¬a ∨ ¬b Figure 2: Representing F(a ∧ b) Table 2: Reconciling information t q I 0 I 1 † ∨ 0 q 0 ⊤ ⊤ ⊤ 1 q 0 ⊥ ∨ ¬ ⟨1, b ⟩ ¬ ⟨1, a ⟩ ∨ ⊤ ⊤ 1 q 1 ⊤ ∧ ⟨1, b ⟩ ⟨1, a ⟩ ∧ ⊥ ⟨1, b ⟩ q 00 q 01 ¬m 1 ∧ a 0 m 1 ∧ a 0 m 1 ∧ ¬a 0 ¬m 1 ∧ ¬a 0 ⊤ q 10 q 11 q 12 b 0 ¬b 0 ⊤ ⊤ Figure 3: Representing F(a 0 ∨ b 0 ) (decentralized)
Since EHE is a dict mapping a pair in N × Q to an expression in Expr, and since the combination is done using † ∨ , which is idempotent, commutative and associative, it follows from Prop. 3.1 that EHE is a CvRDT. Two components receiving the same EHE and merging them will be able to infer the same execution history of the automaton. Corollary 4.8. An EHE with operation † ∨ is a CvRDT.

DECENTRALIZED SPECIFICATIONS

In this section, we shift the focus to a specification that is decentralized. A set of automata represent various requirements for different components of a system. In Sec. 5.1, we define the notion of a decentralized specification and its semantics, and in Sec. 5.2, we tackle the monitorability of such specification. The dep function finds all monitors which the expression e references by syntactically traversing it.

Decentralizing the Specification

Example 5.2 (Decentralized specification). Figure 3 shows a decentralized specification corresponding to the specification in Ex. 4.3. It consists of 2 monitors m 0 and m 1 , with automata A 0 and A 1 respectively. We consider two atomic propositions a 0 and b 0 which can be observed by component c 0 and c 1 respectively. Monitor m 0 (resp. m 1 ) is attached to component c 0 (resp. c 1 ). A 0 depends on the verdict from m 1 and only observations local to c 0 , while A 1 is only labeled with observations local to c 1 . Given e = m 1 ∧ a 0 , we have dep(e) = {m 1 }.

Semantics of the decentralized specification. The transition function of the decentralized specification is similar to the centralized automaton with the exception of monitor ids. Definition 5.3 (Semantics of the decentralized specification automaton). Consider the monitor id m k , with the specification automaton A k , a state q ∈ Q k , a decentralized trace tr of length t with i ∈ [0, t].

∆ ′ * k (q, tr, i, t) = ∆ ′ * k (∆ ′ k (q, tr, i), i + 1, t) if i < t ∆ ′ k (q, tr, i) otherwise ∆ ′ k (q, tr, i) =        q ′ | ∃e : δ k (q, e) = q ′ ∧ eval(e, M) = ⊤ if tr(i, c k ) ∅ q otherwise M = memc(tr(i, c k ), idt) † 2 2 m j ∈dep(e) {[m j → ver j (q j f )]} q j f = ∆ ′ * j (q j 0 , tr, i, t)
For a monitor m k , we determine the new state of the automaton starting at q ∈ Q k , and running the trace tr from timestamp i to timestamp t by applying ∆ ′ * k (q, tr, i, t). To do so, we evaluate one transition at a time using ∆ ′ k as would ∆ * k with ∆ k (see Def. 4.2). To evaluate ∆ ′ k at any state q ′ ∈ Q k , we need to evaluate the expressions so as to determine the next state q ′′ . The expressions contain atomic propositions and monitor ids. For atomic propositions, the memory is constructed using memc(tr(i, c k ), idt) which is based on the event with observations local to c k . However, for monitor ids, the memory represents the verdicts of the monitors. To evaluate an id m j , the remainder of the trace starting from the current event timestamp i is evaluated recursively on the automaton A j from the initial state q j 0 ∈ A j . Then, the verdict of the monitor is associated with m j in the memory.

Example 5.4 (Monitoring the decentralized specification). Consider monitors m 0 and m 1 associated to components c 0 and c 1 respectively and the trace tr

= [1 → c 0 → {⟨a, ⊥⟩}, 1 → c 1 → {⟨b, ⊥⟩}, 2 → c 0 → {⟨a, ⊥⟩}, 2 → c 1 → {⟨b, ⊤⟩}].
To evaluate tr on A 0 (from Fig. 3), we use ∆ ′ * 0 (q 0 0 , tr, 1, 2). To do so, we first evaluate ∆ ′ 0 (q 0 0 , tr, 1). We notice that the expressions depend on m 1 , therefore we need to evaluate ∆ ′ * 1 (q 1 0 , tr, 1, 2). All expressions have no monitor labels, thus we construct M 1 1 = memc(⟨b, ⊥⟩, idt) = [b → ⊥], and notice that eval(¬b, M 1 1 ) = ⊤ and therefore it can move to state q 1 2 associated with verdict ⊥. Notice that ∆ ′ 1 ( ∆ ′ 1 (q 1 0 , tr, 1), tr, 2) = q 1 2 with ver 1 (q 1 2 ) = ⊥. We can construct

M 1 0 = memc(⟨a, ⊥⟩, idt) † 2 [m 1 → ⊥] = [a → ⊥, m 1 → ⊥].
We then have eval(¬m 1 ∧ ¬a 0 , Mem 1 0 ) = ⊤) and A 0 is in state (m 0 , q 0 ). By doing the same for t = 2, we obtain Mem 2 0 = [a → ⊥, m 1 → ⊤], we then evaluate eval(m 1 ∧ ¬a 0 ) = ⊤. This indicates that ∆ ′ 0 (∆ ′ 0 (q 0 0 , tr, 1), tr, 2) = q 0 1 and the final verdict is ⊤. Remark 1 (Compliance/Violation). Importantly, we do not define a global verdict for the system. We do not impose that a main monitor be present, or that the monitors be organized in a tree or list topology. We leave the choice of the topology and dependencies to the algorithm in question.

Decentralized Monitorability

We next consider the monitorability of decentralized specifications by introducing the notion of path expression.

Path expression. A path from a state q s to a state q e is expressed as an expression over atoms. We define paths(q s , q e ) to return all possible paths from q s to q e . Definition 5.5 (Path expressions). paths(q s , q e ) = expr ∃t ∈ N, ∃expr : I t (t, q e ) = expr

∧ I t = mov([0 → q s → ⊤], 0, t)
The expression is derived similarly as would an execution in the EHE (Def. 4.4). Instead of executing from the initial state q 0 , we start from state q s and use a logical timestamp starting at 0 incrementing it by 1 for the next reachable state.

Decentralized monitorability. Decentralized monitorability for a given automaton A k is determined by looking at the paths that reach a state associated with a final verdict. However, since paths depend on other monitors, then it must also extend recursively to those monitors.

Definition 5.6 (Decentralized monitorability). A spec

A k is mon- itorable, noted monitorable(A k ), iff ∀q ∈ Q A k ∃q f ∈ Q A k ∃e f ∈ paths(q, q f ), such that (1) e f is satisfiable; (2) ver k (simplify(q f )) ∈ B 2 ; (3) ∀m j ∈ dep(e f ): monitorable(A j ).
The first condition ensures that the path can be taken (i.e., there exists a trace that satisfies it) 6 . The second condition ensures that the state is labeled with a final verdict. And the third condition ensures that the atomic propositions that depend on other monitors can be evaluated. Additionally, q is said to be a monitorable state, and if ver k (q f ) = ⊥ (resp. ⊤), then we say that q can be negatively (resp. positively) determined. An automaton is monitorable iff we can from any state reach a state that can output a final verdict.

Remark 2 (Monitoring Completeness). Verdicts must be eventually reported, so that they can be included in the memory to evaluate the expressions with monitor ids. A memory with a missing verdict generates the verdict ?, this could cause an expression to never evaluate (see Def. 3.10). Monitorability guarantees that a path expression to a final verdict can be evaluated. This however can require a timestamp t much higher than the length of the current trace and it ensures that at least one monitor will terminate. Therefore, ∆ * k may not terminate.

ANALYSIS

We compare decentralized monitoring algorithms in terms of computation, communication and memory overhead. We first consider the parameters and the cost for the basic functions of the EHE. Then, we adapt the existing algorithms to use EHE and analyze their behavior. We use s e to denote the size necessary to encode e. For example, s AP is the size needed to encode AP.

Data Structure Costs

Storing partial functions. Since memory and EHE are partial functions, to assess their required memory storage and iterations, we consider only the elements defined in the function. The size of a partial function f , denoted | f |, is the size to encode each f (x) = y mapping. We denote | dom(f )| the number of entries in f . The size of each entry f (x) = y is the sum of the sizes |x | + |y|. Therefore

| f | = x ∈dom(f ) |x | + | f (x)|.
Merging. Merging two memories or two EHEs, is linear in the size of both structures in both time and space. In fact to construct f ′ = f † op д, we first iterate over each x ∈ dom(f ), check if x ∈ dom(д), and if so assign f ′ (x) = op(f (x), д(x)), otherwise assign f ′ (x) = f (x). Finally we assign f ′ (y) = д(y) ∀y ∈ dom(д) :

y dom(f ). This results in | dom(f ′ )| = | dom(f ) ∪ dom(д)| which is at most | dom(f )| + | dom(д)|.
Information delay. EHE associates an expression with a state for any given timestmap. When an expression expr associated with a state q kn for some timestamp t kn is ⊤, we know that the automaton is in q kn at t kn . We call q kn a 'known' (or stable) state. Since we know the automaton is in q kn , prior information is no longer necessary, therefore it is possible to discard all t < t kn in I. We parametrize the number of timestamps needed to reach a new known state from an existing known state as the information delay δ t . This can be seen as a garbage collection strategy [START_REF] Shapiro | Conflict-Free Replicated Data Types[END_REF][START_REF] Gene | Efficient Solutions to the Replicated Log and Dictionary Problems[END_REF] for the memory and EHE. EHE encoding. For the EHE data structure we are interested in three functions: mov, eval, and sel 7 . Function mov depends on the topology of the automaton, we quantify it using the maximum size of the expression that labels a transition L, the maximum size of outbound transitions from a state that share the same destination state P, and the number of states in the automaton |Q |. From a known state each mov considers all possible transitions and states that can be respectively taken and reached, for each outbound transition, the label itself is added. Therefore, the rule is expanded by L for each P for each move beyond t kn . For each timestamp, we need for each state an expression, the maximum size of the EHE is therefore:

|I δ t | = δ t |Q | δ t 1 LP = δ 2 t |Q |LP .
For a given expression expr, we use |expr| to denote the size of expr, i.e., the number of atoms in expr. Given a memory M, the complexity of function eval(expr, M) is the cost of simplify( rw(expr, M)). Function rw(expr, M) looks up each atom in expr in M and attempts to replace it by its truth-value. The cost of a memory lookup is Θ(1), and the replacement is linear in the number of atoms in expr. It effectively takes one pass to syntactically replace all atoms by their values, therefore the cost of rw is θ (|expr|). However, simplify() requires solving the Minimum Equivalent Expression problem which is Σ p 2 -complete [START_REF] Buchfuhrer | The Complexity of Boolean Formula Minimization[END_REF], it is exponential in the size of the expression, making it the most costly function. |expr| is bounded by δ t LP. Function sel() requires evaluating every expression in the EHE. For each timestamp we need at most |Q | expressions, and the number of timestamps is bounded by δ t .

Memory. The memory required to store M depends on the trace, namely the amount of observations per component. We note that once a state is known, observations can be removed, the number of timestamps is bounded by δ t . The size of the memory is then:

i+δ t t =i |tr(c, t)| × (s N × s AP × s B 2 ).

Analyzing Existing Algorithms

Overview. A decentralized monitoring algorithm consists of two steps: setting up the monitoring network, and monitoring. In the first step, an algorithm initializes the monitors, defines their connections, and attaches them to the components. We represent the connections between the various monitors using a directed graph ⟨Mons, E⟩ where E = 2 Mons ×Mons defines the edges describing the sender-receiver relationship between monitors. For example, the network ⟨{m 0 , m 1 }, {⟨m 1 , m 0 ⟩}⟩ describes a network consisting of two monitors m 0 and m 1 where m 1 sends information to m 0 . In the second step, an algorithm proceeds with monitoring, wherein each monitor processes observations and communicates with other monitors.

We consider the existing three algorithms: Orchestration, Migration and Choreography [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF] adapted to use EHE. We note that these algorithms operate over a global clock, therefore the sequence of steps can be directly mapped to the timestamp. We choose an appropriate encoding of Atoms to consist of a timestamp and the atomic proposition (Atoms = N × AP). These algorithms are originally presented using an LTL specification instead of automata, however, it is possible to obtain an equivalent Moore automaton as described in [START_REF] Bauer | Runtime Verification for LTL and TLTL[END_REF].

Approach. A decentralized monitoring algorithm consists of one or more monitors that use the EHE and memory data structures to encode, store, and share information. By studying δ t , we derive the size of the EHE and the memory a monitor would use. Knowing the sizes, we determine the computation overhead of a monitor, since we know the bound on the number of simplifications a monitor needs to make (δ t |Q |), and we know the bounds on the size of the expression to simplify (δ t LP). Once the cost per monitor is established, the total cost for the algorithm can be determined by aggregating the costs per monitors. This can be done by summing to compute total cost or by taking the maximum cost in the case of concurrency following the Bulk Synchronous Parallel (BSP) [START_REF] Valiant | A Bridging Model for Parallel Computation[END_REF] approach.

Orchestration. The orchestration algorithm (Orch) consists in setting up a main monitor which will be in charge of monitoring the entire specification. However since that monitor cannot access all observations on all components, orchestration introduces one monitor per component to forward the observations to the main monitor. Therefore for our setup, we consider the case of a main monitor m 0 placed on component c 0 which monitors the specification and |C| -1 forwarding monitors that only send observations to m 0 (labeled m k with k ∈ [1, |C|]). We consider that the reception of a message takes at most d rounds. The information delay δ t is then constant, δ t = d. The number of messages sent at each round is |C| -1, i.e., the number of forwarding monitors sending their observations. The size of the message is linear in the number of observations for the component, for a forwarding monitor k, the size of the message is

MS k = |tr(t, c k )| × (s N × s AP × s B 2 ).
Migration. The migration algorithm (Migr) initially consists in rewriting a formula and migrating from one or more component to other components to fill in missing observations. We call the monitor rewriting the formula the active monitor. Our EHE encoding guarantees that two monitors receiving the same information are in the same state. Therefore, monitoring with Migration amounts to rewriting the EHE and migrating it across components. Since all monitors can send the EHE to any other monitor, the monitor network is a strongly-connected graph. In Migr, the delay depends on the choice of a choose function, which determines which component to migrate to next upon evaluation. By using a simple choose which causes a migration to the component with the atom with the smallest timestamp, it is possible to view the worst case as an expression where for each timestamp we depend on information from all components, therefore |C| -1 rounds are necessary to get all the information for a timestamp (δ t = |C| -1). We parametrize Migration by the number of active monitors at a timestamp m. The presented choose in [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF], chooses at most one other component to migrate to. Therefore, after the initial choice of m, subsequent rounds can have at most m active monitors. The initial choice of active monitors is bounded by m ≤ |C|. Since at most m -1 other monitors can be running, there can be (m -1) merges. The size of the resulting EHE is m × |I δ t | = m(|C| -1) 2 |Q |LP. In the worst case, the upper bound on the size of EHE is (|C| -1) 3 |Q |LP. The number of messages is bounded by the number of active monitors m. The size of each message is however the size of the EHE, since Migr requires the entire EHE to be sent.

Choreography. Choreography (Chor) presented in [START_REF] Bauer | Decentralised LTL Monitoring[END_REF][START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF] splits the initial LTL formula into subformulae and delegates each subformula to a component. Thus Chor can illustrate how it is possible to monitor decentralized specifications. Once the subformulae are determined by splitting the main formula, we adapt the algorithm to generate an automaton per subformula to monitor it. To account for the verdicts from other monitors, the set of possible atoms is extended to include the verdict of a monitor identified by its id. Therefore, Atoms = (N × AP) ∪ (Mons × N). Monitoring is done by replacing the subformula by the id of the monitor associated with it. Therefore, monitors are organized in a tree, the leafs consisting of monitors without any dependencies, and dependencies building up throughout the tree to reach the main monitor that outputs the verdict. The information delay for a monitor is thus dependent on its depth in the network tree. A monitor that is not monitorable will never emit a verdict, therefore its depth is ∞. A leaf monitor has no dependencies, its depth is 1. In terms of communication, the number of monitors generated determines the number of messages that are exchanged. By using the naive splitting function (presented in [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF]), the number of monitors depends on the size of the LTL formula. Therefore, we expect the number of messages to grow with the number of atomic propositions in the formula. By denoting |E| the number of edges between monitors, we can say that the number of messages is linear in |E|. The size of the messages is constant, it is the size needed to encode a timestamp, id and a verdict in the case

( | C |) O (AP c ) Migration O ( | C |) O (m) O (m | C | 2 ) Choreography O (depth(0)) Θ( |E |) Θ(1)
of msg ver , or only the size needed to encode an id in the case of msg kill .

Discussion. We summarize the main parameters that affect the algorithms in Table 3. This comparison could serve as a guide to choose which algorithm to run based on the environment (architectures, networks etc). For example, on the one hand, if the network only tolerates short message sizes but can support a large number of messages, then Orch or Chor is preferred over Migr. On the other hand, if we have heterogeneous nodes, as is the case in the client-server model, we might want to offload the computation to one major node, in this scenario Orch would be preferable as the forwarding monitor require no computation. This choice can be further impacted by the network topology. In a ring topology for instance, one might want to consider using Migration (with m = 1), as using Orch might impose further delay in practice to relay all information, while in a star topology, using Orch might be preferable. In a more hierarchical network, Chor can adapt its monitor tree to the hierarchy of the network.

THE THEMIS FRAMEWORK

THEMIS is a tool to facilitate the design, development, and analysis of decentralized monitoring algorithms; developed using Java and As-pectJ [START_REF] Kiczales | An Overview of AspectJ[END_REF] (∼5700 LOC). 8 It consists of a library and command-line tools. The library provides all necessary building blocks to develop, simulate, and instrument decentralized monitoring algorithms. The command-line tools provide basic functionality to generate traces, execute a monitoring run and execute a full experiment (multiple parametrized runs).

The purpose of THEMIS is to minimize the overhead of designing and assessing decentralized monitoring algorithms. THEMIS provides an API for monitoring and necessary data structures to load, encode, store, exchange, and process observations, as well as manipulate specifications and traces. These basic building blocks can be reused or extended to modify existing algorithms or design new more intricate algorithms. To assess the behavior of an algorithm, THEMIS provides a base set of metrics (such as messages exchanged and their size, along with computations performed), but also allows for the definition of new metrics by using the API or by writing custom AspectJ instrumentation. These metrics can be used to assess existing algorithms as well as newly developed ones. Once algorithms and metrics are developed, it is possible to use existing tools to perform monitoring runs or full experiments. Experiments are used to define sets of parameters, traces and specifications. An experiment is effectively a folder containing all other necessary files. By bundling everything in one folder, it is possible to share and reproduce the experiment. After running a single run or an experiment, the metrics are stored in a database for postmortem 8 The THEMIS framework is further described and demonstrated in the companion tool-demonstration paper [START_REF] El | THEMIS: A Tool for Decentralized Monitoring Algorithms[END_REF] and on its Website [START_REF] El | THEMIS Website[END_REF].

analysis. These can be queried, merged or plotted easily using thirdparty tools. After completing the analysis, algorithms and metrics can be tuned so as to refine the design as necessary.

EVALUATION AND DISCUSSION

We use THEMIS to compare adapted existing algorithms (Orch, Migr, and Chor -Sec. 6) and validate the behavior of the EHE data structure. We additionally consider a round-robin variant of Migr, Migrr and use that for analyzing the behavior of the migration family of algorithms as it has a predictable choose. We conduct a study to confirm the analysis in Sec. 6 and explore the situations that best suit the algorithms.

Experimental setup. We generate the specifications as random LTL formulas using randltl from Spot [START_REF] Duret-Lutz | Manipulating LTL formulas using Spot 1.0[END_REF] then converting the LTL formulae to automata using ltl2mon [START_REF] Bauer | Runtime Verification for LTL and TLTL[END_REF]. We generate traces by using the GeneratorTrace tool in THEMIS which generates synthetic traces by creating random events using a normal probability distribution. For all algorithms we considered the communication delay to be 1 timestamp. That is, messages sent at t are available to be received on t + 1. In the case of both Migration variants, we set the active monitors to 1 (m = 1). For our experiment 200 traces of 100 events per component, we associate with each component 2 observations. We vary the number of components between 3 and 5, and ensure that for each number we have at least 1,000 formulae that references all components. We were not able to effectively use a larger number of components since the formula becomes sufficiently large that generating an automaton from it becomes unfeasible. The generated formulae were fully constructed of atomic propositions, there were no terms containing ⊤ or ⊥. 9When computing sizes, we use a normalized unit to separate the encoding from actual implementation strategies, our assumptions on the sizes is similar to the number of bytes needed to encode data (for example: 1 byte for a character, 4 for an integer). We normalized our metrics using the length of the run, that is, the number of rounds taken to reach the final verdict (if applicable) or timeout, as different algorithms take different number of rounds to reach a verdict.

Monitoring metrics. The first considered metric is that of information delay δ t . δ t impacts the size of the EHE and therefore the computation, communication costs to send an EHE structure, and also the memory required to store it. By considering our analysis in Sec. 6, we split our metrics into two main categories: communication and computation. We consider communication using two metrics: number of messages and data communicated. The number of messages is the total messages sent by all monitors throughout the entire run. The data communicated consists of the total size of messages sent by all monitors throughout the entire run. Both number of messages and the data transferred are normalized using the run length. The EHE structure requires the evaluation and simplification of a boolean expression which is costly (see Sec. 4.2). Thus, we count the number of simplifier calls as a measure of computation required by the monitor. Alternatively, it can be seen as the number of formula evaluations conducted by the monitor. We measure simplifications per round as a normalized value, by taking the total number of simplifications performed by all monitors throughout the run and dividing by the run length. The simplifications per round describes the total computations done by all monitors. We introduce this metric to measure concurrency. Since monitors can execute in parallel, we are interested in the monitor with the most amount of simplifications to perform in a given round, since it acts as a bottleneck for concurrency. In addition, to capture load balancing, we introduce convergence where:

convergence = 1 n n t =1 c ∈ C s t c s t - 1 |C| 2 , with s t = c ∈ C s t c
At a round t, we consider all simplifications performed on all components s t and for a given component s t c . Then, we consider the ideal scenario where computations have been spread evenly across all components. Thus, the ideal ratio is 1 | C | . We compute the ratio for each component ( s t c s t ), then its distance to the ideal ratio. Distances are added for all components across all rounds then normalized by the number of rounds. The higher the convergence the further away we are from having all computations spread evenly across components.

Results. We present the results in Table 4, we show the algorithm followed by the number of components, and an average of our metrics across all runs. The column #S denotes the normalized number of simplifications while #S/Mon denotes the normalized number of simplifications per monitor. We notice that Orch maintains the lowest delay, followed by Migrr and Chor. In addition, we notice that Migrr has an average δ t that increases with |C|. We note that Migrr data transfer is an estimation of the size of the EHE, as we have one active monitor sending the EHE per round. This gives us a good estimate of the growth the size of EHE with |C| for Migr. The size of EHE determines the computation required, we see that for higher δ t , #S increases. Since Chor is the only algorithm running multiple monitors we can see that it effectively spreads the computation across components, making its slowest monitor (#S/Mon) perform a bit worse than Orch, but with reasonable scalability wrt |C|. On the one hand, Migrr sends a small and balanced #Msgs that does not depend on |C|, in exchange, its data transfer is much bigger as it has to send the entire EHE. On the other hand, we observe that both Orch and Chor maintain a smaller number of data than Migrr but a higher #Msgs. We notice that in terms of data, Chor outperforms Orch. This is consistent with the observation that the size of messages for Chor is constant while, in the case of Orch, it scales with the number of observations per component.

Discussion. The observed behavior of the simulation confirms the initial analysis described in Sec. 6. We observe that the EHE presents predictable behavior in terms of size and computation. The delay presented for each algorithm indeed depends on the listed parameters in the analysis. With the presented bounds on EHE, we can determine and compare the algorithms that use it. Therefore, we can theoretically estimate the situations where algorithms might be (dis)advantaged.

CONCLUSIONS AND FUTURE WORK

We present a general approach to monitoring decentralized specifications. A specification is a set of automata associated with monitors that are attached to various components. We provide a general decentralized monitoring algorithm defining the major steps needed to monitor such specifications. In addition, we present the EHE data structure which allows us to (i) aggregate monitor states with strong eventual consistency, (ii) remain sound wrt the execution of the monitor, and (iii) characterize the behavior of the algorithm at runtime. We then map three existing algorithms: Orchestration, Migration and Choreography to our approach using our data structures. We develop and use THEMIS to implement algorithms and analyze their behavior by designing new metrics.

We can now explore new directions of decentralized monitoring. One is to study algorithms that generate from a centralized specification, an equivalent decentralized one. Another direction is the design of new algorithms for combining monitors for specific parts of the systems. One can now separate the problem of the topology and dependencies of the monitors from the monitoring procedure. That is, one can generate a decentralized specification that balances computation to suit the system architecture, or optimize specific algorithms for specific layouts of decentralized systems (as discussed in Sec. 6). Moreover, one could consider creating new metrics for THEMIS to analyze more aspects of decentralized monitoring algorithms. New metrics would be automatically instrumented on all existing algorithms and experiments could be easily replicated to compare them. Finally, we shall consider new settings for runtime enforcement [START_REF] Falcone | You Should Better Enforce Than Verify[END_REF]: (i) decentralized runtime enforcement of centralized specifications and (ii) (decentralized) runtime enforcement of decentralized specifications.

Definition 3 . 7 (

 37 Rewriting). An expression expr is rewritten with a memory M using rw(expr, M) defined as follows: rw : Expr × Mem → Expr rw(expr, M) = match expr with | a ∈ Atoms → M(a) if a ∈ dom(M) a otherwise | ¬e → ¬rw(e, M) | e 1 ∧ e 2 → rw(e 1 , M) ∧ rw(e 2 , M) | e 1 ∨ e 2 → rw(e 1 , M) ∨ rw(e 2 , M)

Example 3 . 8 (

 38 Rewriting). We consider M = [a → ⊤, b → ⊥]; and e = (a ∨ b) ∧ c. We have M(a) = ⊤, M(b) = ⊥, M(c) = ?.

Example 3 . 11 (

 311 Evaluating expressions). Consider M = [a → ⊤, b → ⊥] and e = (a ∨ b) ∧ c. Ãź We have simplify(rw(e, M)) = simplify((⊤ ∨ ⊥) ∧ c) = c, and eval(e, M) = ? which depends on c: we cannot emit a final verdict before observing c.

Example 4 . 7 (

 47 Reconciling information). We consider the specification F(a ∧ b) (Fig. 2), and two components: c 0 and c 1 monitored by m 0 and m 1 respectively. The monitors can observe the propositions a and b respectively and use one EHE each: I 0 and I 1 respectively. Their memories are respectively M 0 = [⟨1, a⟩ → ⊤] and M 1 = [⟨1, b⟩ → ⊥]. Table

  To decentralize the specification, we consider a set of monitor labels Mons = {m 0 , . . . , m n-1 }. Each monitor label m k is associated with a specification automaton A k (Definition 4.1) and a componentc k ∈ C (with k ∈ [0, n -1]).However, the transition labels of the automaton is restricted to either observations local to c k or references to other monitors. Transitions are labeled over Atoms k = Mons \ {m k } ∪ {ap ∈ AP | lu(ap) = c k }. This ensures that the automaton is labeled with observations it can locally observe or depends on other monitors. Definition 5.1 (Monitor dependency). The set of monitor ids in an expression e is denoted by dep(e). dep(e) = match e with: | id ∈ Mons → {id} | e 1 ∧ e 2 → dep(e 1 ) ∪ dep(e 2 ) | ¬e → dep(e) | e 1 ∨ e 2 → dep(e 1 ) ∪ dep(e 2 )

Table 3 :

 3 Scalability of Existing Algorithms.

	Algorithm	δ t	# Msg	|Msg|
	Orchestration	Θ(1)	Θ

Table 4 :

 4 Decentralized Monitoring Metrics

	Alg.	| C |	δ t	#Msgs	Data	#S #S/Mon Conv
		3	2.37	2.02	18.05 15.27	6.63	0.18
	Chor	4	2.49	2.54	22.62 18.22	6.79	0.20
		5	2.37	3.08	27.18 21.29	6.95	0.22
		3	1.02	0.36	49.46	4.80	4.80	1.00
	Migr	4	1.38	0.41 128.26	5.67	5.67	1.00
		5	2.28	0.57 646.86	9.40	9.40	1.00
		3	1.09	0.86	58.02	5.00	5.00	1.00
	Migrr	4	1.49	0.85 144.62	5.91	5.91	1.00
		5	2.32	0.83 684.81	9.60	9.60	1.00
		3	0.63	1.68	21.01	4.13	4.13	1.00
	Orch	4	0.65	2.43	30.42	4.11	4.11	1.00
		5	0.81	3.04	38.51	5.55	5.55	1.00

July 14, 2017July 14, © 2017 Copyright held by the owner/author(s).

We use the example from[START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF]: GF(a) ∧ ¬(GF(a)) is monitorable, but its subformulae are both non-monitorable.

This is also known as The Minimum Equivalent Expression problem[START_REF] Buchfuhrer | The Complexity of Boolean Formula Minimization[END_REF].

We assume that[START_REF] Bartocci | Sampling-based Decentralized Monitoring for Networked Embedded Systems[END_REF] no two components can observe the same atomic propositions, and (2) a component has at least one observation at all times (a component with no observations to monitor, can be simply considered excluded from the system under monitoring).

Indeed, an event can be converted to an expression by the conjunction of all observations, negating the terms that are associated with the verdict ⊥.

[START_REF] Bauer | Decentralised LTL Monitoring[END_REF] We note that in this case, we are not using any encoding (Atoms = AP).

This is ensured if the automaton is generated from LTL[START_REF] Bauer | Runtime Verification for LTL and TLTL[END_REF].

verAt is simply a sel followed by a O (1) lookup

To generate formulae with basic operators, string false=0,true=0,xor=0, M=0,W=0,equiv=0,implies=0,ap=6,X=2,R=0 is passed to randltl.


Antoine El-Hokayem
email: antoine.el-hokayem@univ-grenoble-alpes.fr

Yliès Falcone
email: ylies.falcone@univ-grenoble-alpes.fr

THEMIS: A Tool for Decentralized Monitoring Algorithms

Keywords: Runtime Verification, Monitoring, Tool, Java, AspectJ

come   L'archive ouverte pluridisciplinaire

INTRODUCTION

Runtime Verification. Runtime Verification (RV) [START_REF] Bartocci | First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV 2014[END_REF][START_REF] Falcone | A Tutorial on Runtime Verification[END_REF][START_REF] Leucker | A brief account of runtime verification[END_REF]] is a lightweight formal method which consists in verifying that a run of a system is correct with respect to a user-provided specification. The specification formalizes the expected behavior of the system. Typically, the system is considered as a blackbox that feeds events to a monitor. An event usually consists of a set of atomic propositions describing abstract operations or states in the system. A sequence of such events is referred to as a trace. When receiving a trace, the monitor will emit verdicts in a truth domain that indicate the compliance of the system to the specification. We focus on methods to monitor decentralized systems, that is, systems with multiple components having no central observation point. In decentralized systems, the monitors have a partial view of the system and need to account for communication [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF] in addition to computation.

Existing Approaches. Several algorithms have been designed to monitor decentralized systems, they are detailed in [START_REF] El | Monitoring Decentralized Specifications[END_REF]. They can be summarized into two different approaches. The first approach consists in monitoring by formula rewriting such as rewriting Linear Temporal Logic (LTL) [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF][START_REF] Rosu | Rewriting-Based Techniques for Runtime Verification[END_REF]. Typically a formula is rewritten and simplified until it is equivalent to ⊤ (true) or ⊥ (false) at which point the algorithm terminates. The second approach [START_REF] Bonakdarpour | Decentralized Asynchronous Crash-Resilient Runtime Verification[END_REF] is concerned with consensus on the verdict with fault-tolerance. Monitors may fail to receive correct observations or communicate state with other monitors. This approach determines the necessary verdict domain needed to be able to reach a consensus. Algorithms are primarily designed to address one issue at a time and are typically experimentally evaluated by considering runtime and memory overheads. However, such algorithms are difficult to compare as they may combine multiple approaches at once. For example, algorithms that use rewriting not only exhibit variable runtime behavior due to the rewriting, but also incorporate different monitor synthesis approaches that separate the specification into multiple smaller specifications depending on the monitor. DecentMon [START_REF] Bauer | Decentralised LTL monitoring[END_REF][START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF] was developed and extended to study the behavior of three decentralized monitoring algorithms that rely on LTL rewriting. DecentMon uses various measures to assess the algorithms both on computation and communication overhead. The measures presented are related to the delay, representing an extra time imposed by communication to generate the verdict, number and size of messages transferred across the system components and the number of progressions, representing the rewrites done to the formula. DecentMon runs the benchmarks on the three algorithms, generates the necessary synthetic traces and reports the measures. However it does not easily allow for flexibility to tune the existing algorithms, experiment with different measures, develop new variants, and it only supports LTL specifications.

THE THEMIS APPROACH

Methodology. THEMIS [START_REF] El | THEMIS Website[END_REF] is written in Java, uses AspectJ [START_REF] Kiczales | An Overview of AspectJ[END_REF] and is provided as a library with a set of command-line tools. The primary goal of THEMIS is to design and analyze decentralized monitoring algorithms. It is addressed mostly for researchers to experiment, tune, and compare decentralized monitoring algorithms. To assess the behavior of an algorithm, we identify four phases (Figure 1): design, instrument, execute, and analyze. The design phase consists in elaborating a monitoring algorithm. THEMIS generalizes the monitoring steps and provides an API to describe the operations. These operations are used as building-blocks to assemble an algorithm. The instrument phase consists in the definition of measures. Measures are instrumented into THEMIS and the algorithms at run-time and operate on the API and data structures. The execute phase consists in using the THEMIS set of tools to run simulations of the monitoring algorithms and record the measures. The analyze phase consists in using the recorded measures to study, compare, and refine the algorithm. In this paper, simulations are executed on synthetic traces of programs. An instrumented program feeds THEMIS a stream of events (by implementing the interface Trace).

Design Goals. The main design goal of THEMIS is to provide a general API for decentralized monitoring. That is, to provide an environment that accounts for changes at all levels: traces, specification, monitoring logic. By doing so, we allow for new approaches implementing the API to benefit from all existing metrics and analysis. Additionally, this allows metrics to be assessed at the abstract level, for example the metric messages sent could be simply reused if new algorithms exchange messages. Following this goal, we also aimed that our measures be stored per run in a database. This allows for analysis and benchmarking to be reduced to querying and analysis of the database. This effectively separates the analysis from the monitoring. Third-party tools can be used to explore and analyze the data. Another important design goal is reproducibility. We wanted to minimize the effort of re-running older simulations or comparing new approaches with older ones. This is reflected with the Experiment command-line tool which, in short, allows users to bundle all traces, specifications and algorithms. Since metrics are designed to work at the API level and data structures, any algorithm using the same building blocks can be measured similarly without added effort. This allows for new algorithms or variants of older algorithms to be easily compared against older ones with the same data and measures. By accomplishing these two primary goals, we minimize the overhead needed to design new algorithms and study them, and let researchers focus on the algorithm and the monitoring itself. Finally, THEMIS is designed to introduce decentralized specifications [START_REF] El | Monitoring Decentralized Specifications[END_REF]. That is, having different specifications for different components in the system. While some approaches [START_REF] Basin | Failure-aware Runtime Verification of Distributed Systems[END_REF][START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF] do in effect introduce a decentralized specification, they primarily focus on presenting one global formula of the system from which they derive multiple specifications. THEMIS encompasses [START_REF] Basin | Failure-aware Runtime Verification of Distributed Systems[END_REF][START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF] and in addition supports any decentralized specification.

THE THEMIS FRAMEWORK

Monitoring. We begin by explaining the basic layout of a generalized decentralized monitoring algorithm. A monitoring algorithm has two phases: setup and monitor. In the first phase, the algorithm creates and initializes the monitors, connects them to each other so they can communicate, and attaches them to components so they receive the observations generated by components. In the second phase, each monitor receives observations at a timestamp based on the component it is attached to. The monitor can then perform some computation, communicate with other monitors, abort monitoring or report a verdict. To accomplish this we use the two interfaces MonitoringAlgorithm and Monitor. In the basic use case, MonitoringAlgorithm is expected to provide the setup() method, which does the setup phase of the algorithm, and returns a map specifying monitors and their ids. A monitor has to implement the monitor() method for the monitoring logic, and the reset() method to reset its state when executing multiple runs. The method monitor() provides the monitor with a timestamp and a memory of observations at that timestamp based on the monitored component. The provided flow of the base MonitoringAlgorithm is similar to the Bulk Synchronous Parallel (BSP) [START_REF] Valiant | A Bridging Model for Parallel Computation[END_REF] model. In the BSP model, all processes execute a computation phase, then, they communicate and finally synchronize. The timestamp is associated with the round number. The monitoring phase begins by setting up the monitor network. Then, for each timestamp, the observations are gathered from the trace, then all monitors execute their monitor() method. Measuring. THEMIS uses AspectJ to record measures of a metric for a given algorithm. Writing a metric for an algorithm consists in using AspectJ's aspects to intercept the points in the execution. To simplify the task, THEMIS provides the base aspect Instrumentation and the classes Measure and MeasureFunction. The Instrumentation aspect already defines basic pointcuts and triggers simple methods upon reaching them, they are shown in Listing 1. When running THEMIS tools to execute the monitoring algorithms, metrics are instrumented into the code at load-time using AspectJ's Load-Time Weaving (LTW) configuration. This is found in aop.xml, the file configures the AspectJ agent that weaves the aspects during load-time. Thus, by pre-loading aop.xml measures can be enabled or disabled for a specific run.

Traces. The provided tools and algorithms use a simple format to represent components and the traces of events they receive. The components are named alphabetically starting with a (for example: a, b, c). The observations bound to the components are prefixed by the component and followed with a number starting from 0 (for example: a0, a1, a2, b0, b1). The trace consists of multiple files, prefixed by the trace ID and suffixed by the component name. A trace for two components a and b consists of two files: 1-a.trace and 1-b.trace. Each line in the file consists of an event.

Specifications. A top level specification is by default a decentralized specification. A decentralized specification is a collection of specifications. Specifications are passed to a monitoring algorithm as a Map, where each specification is identified by a key. Each specification must provide two attributes: an id and a class name. The id is a string name for the specification, it is used by the algorithm during the setup phase. The provided algorithms use the id root to denote the main specification. The class name is a string representing a full class name of the specification class. Listing 2 shows an example of LTL specification. It is given the name root and is loaded by the class SpecLTL. THEMIS will instantiate a SpecLTL object and invoke the setLTL(String) method with the LTL formula passed as string. THEMIS currently handles both LTL and Automata specifications and supports loading from dot files similar to those exported by ltl2mon [START_REF] Bauer | Runtime Verification for LTL and TLTL[END_REF].

Execution History Encoding (EHE). For the demonstration, we focus on specifications formalized using automata. The execution of the specification automaton, is in fact, the process of monitoring, upon running the trace, the reached state determines the verdict. In a decentralized system, a component receives only local observations, it generally does not have enough information to determine the state at a given timestamp. Typically, when sufficient information is shared between various components, it is possible to know the state reached in the automaton. The EHE is a data structure that encodes the execution of the automaton using boolean expressions and ensures strong eventual consistency in determining the state reached in the execution. Formal details are in [START_REF] El | Monitoring Decentralized Specifications[END_REF].

Command-line Tools. The THEMIS framework is bundled with several tools to execute monitoring. The Run tool takes as input the name of a monitoring algorithm class, a specification file, the number of components, the length of a trace (in order to timeout), a traces directory, and one or more traces to read and simulate the run of the algorithm on the given trace and specification. Upon finishing the execution, the measures will be printed. The Experiment tool is designed to execute a set of runs packaged as an experiment. Experiments are used to define sets of parameters, traces and specifications. An experiment is effectively a folder containing all necessary files. After running a single run or an experiment, the measures are stored in a database for postmortem analysis. These can be queried, merged, or plotted easily using third-party tools.

THE MIGRATION ALGORITHM

The migration algorithm is a decentralized monitoring algorithm where information is passed throughout the components to eventually verify the specification. In our setup, the migration algorithm will assign a monitor per component. These monitors are strongly connected; each monitor is connected to all other monitors. The monitors are either active or inactive. Active monitors are monitors that seek to find a verdict while inactive monitors are idle, waiting for other monitors to send them their EHE. Both active and inactive monitors store the observations they receive in their memory. However, only active monitors will update the expressions in their EHE. After expressions are updated, active monitors will determine which other monitors should be sent the EHE to continue monitoring using a method getNext. In this demonstration, we use two different implementations of getNext. The first chooses the next monitor by cycling through all monitors in a round-robin fashion. The second chooses the monitor based on the earliest observation missing to evaluate the EHE [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF].

Setup. Listing 3 shows the setup phase. We first make sure to convert the main specification (identified by root) to an automaton specification (line 2-3). Next, we create the monitors map, and generate as many monitors as components, giving them ids starting from zero. Each monitor is then attached to a component (line 8) to receive observations on that component. We note that in the default implementation of communication, all monitors are connected to each other, therefore there is no need to connect monitors to each other. Monitor. The monitoring logic of the monitor is shown in Listing 4. First, the monitor updates its memory by adding the new observations (line 3). Then, the monitor checks if it received anything and merges the received EHE. If the monitor receives anything then they become active. Upon receiving observations the monitor then updates its EHE and checks for a verdict. If a verdict has changed (line 9) and the verdict reached is a final verdict (line 11), then we report it and remove unnecessary entries in the EHE (line 13). We then determine the id of the new monitor to send the EHE to (line 15). The two implementations of the method getNext() determine the variants of Migration. If it is a different monitor id, then we must migrate, the EHE is sent to the next monitor (line 18) and the current monitor is rendered inactive (line 19). Measures. To evaluate the behavior of the migration algorithm we use the communication as an example metric. We measure the number of messages sent and the size of the messages. The number of messages indicates the number of migrations performed, while the size of the messages indicates how big the EHE is. The number of messages is shown in Listing 5. We begin by adding the measure and initializing with zero (line 2). We intercept the message sending using AspectJ (line 4) and update our measure (line 5). Analyze. We aim to compare the communication patterns of the two variants. To do so, we execute 2,934,400 runs to generate a database of the measures. We use 200 traces of 100 events per component, we associate with each component 2 observations. We vary the number of components between 3 and 5, and ensure that for each number we have at least 1,000 formulae that reference all components. Specifications are generated as random LTL formulae using randltl from Spot [START_REF] Duret-Lutz | Manipulating LTL formulas using Spot 1.0[END_REF], then converted to automata using ltl2mon [START_REF] Bauer | Runtime Verification for LTL and TLTL[END_REF]. Figure 2 displays our example query on the database to retrieve the communication measures, where column alg (resp. comps, avg(msg_num), avg(msg_data), count) indicates the algorithm (resp. number of components, average number of messages, average size of messages, the number of runs). MigrationRR stands for Migration with round robin. We can see that the naive roundrobin variant has both a higher number of messages and more communication. The smaller number of messages indicates that less migrations are performed overall.

Listing 3 Migration Setup Phase

Listing 4 Migration Monitor

CONCLUSION

We present THEMIS, a tool for designing and decentralized monitoring algorithms. THEMIS is an extensible framework for analyzing current algorithms, designing new ones, and experimenting with variants of existing algorithms. In addition, THEMIS provides common metrics for communication and computation overheads. THEMIS allows for re-use of both algorithms and measures so as to allow for easier comparison between algorithms. We provide an example of the methodology by applying it to the migration algorithm.

Finally, it is possible to check the tool, more examples, usage tutorial, technical documentation, and the (reproducible) experiments conducted with THEMIS on its website [START_REF] El | THEMIS Website[END_REF].

Figure 1 :

 1 Figure 1: Using the THEMIS Framework

Listing 2

 2 An LTL Specification <specifications> <specification id="root" class="uga.corse.themis.monitoring.SpecLTL"> <setLTL><![CDATA[XXXX(!a0 | (b1 U G(a0 & b0 & c0)))]]></setLTL> </specification> </specifications>

1 protected 5 Integer

 15 Map<Integer, ? extends Monitor> setup() { 2 config.getSpec().put("root", 3 Convert.makeAutomataSpec(config.getSpec().get("root"))); 4 Map<Integer, Monitor> mons = new HashMap<Integer, Monitor>();

1 public

 1 void monitor(int t, Memory<Atom> observations)

Listing 5 3 } 4 after( 6 }Figure 2 :

 53462 Figure 2: Example Database Querying

  Listing 1 Main Instrumentation Methods

	public void setupRun(MonitoringAlgorithm alg);
	protected void runBegin();
	protected void stepBegin(int t);
	protected void stepEnd(int t);
	protected void stepReport(int t, ReportVerdict rep);
	protected void runEnd();

July 2017 © 2017 Copyright held by the owner/author(s).