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

On the Monitoring of Decentralized Specifications: Semantics, Properties, Analysis, and Simulation

Keywords: CCS Concepts:, Software and its engineering → Software verification, • Theory of computation → Formal languages and automata theory, Data structures design and analysis, • Computing methodologies → Simulation tools, Runtime Verification, Monitoring, Simulation, Decentralized Monitoring, Automata, Eventual Consistency

We introduce two complementary approaches to monitor decentralized systems. The first approach relies on systems with a centralized specification, i.e., when the specification is written for the behavior of the entire system. To do so, our approach introduces a data structure that (i) keeps track of the execution of an automaton (ii) has predictable parameters and size and (iii) guarantees strong eventual consistency. The second approach defines decentralized specifications wherein multiple specifications are provided for separate parts of the system. We study two properties of decentralized specifications pertaining to monitorability and compatibility between specification and architecture. We also present a general algorithm for monitoring decentralized specifications. We map three existing algorithms to our approaches and provide a framework for analyzing their behavior. Furthermore, we present THEMIS, a framework for designing such decentralized algorithms and simulating their behavior. We demonstrate the usage of THEMIS to compare multiple algorithms and validate the trends predicted by the analysis in two scenarios: a synthetic benchmark and the Chiron user interface.

INTRODUCTION

Runtime Verification (RV) [START_REF] Bartocci | First international Competition on Runtime Verification: rules, benchmarks, tools, and final results of CRV[END_REF][START_REF] Falcone | A Tutorial on Runtime Verification[END_REF][START_REF] Falcone | A Taxonomy for Classifying Runtime Verification Tools[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 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 black box 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 whether or not the run complies with the specification. A typical truth domain is the set {⊤, ⊥, ?} where verdicts ⊤ and ⊥ indicate respectively that a program complies or violates the specification, and verdict ? indicates that no final verdict could be reached yet. Truth domains can also include additional verdicts such as currently true and currently false, to indicate a finer grained truth value. 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 :2 Antoine El-Hokayem and Yliès Falcone q 0 q 1 q 2 ¬s s ¬s s ∧ ℓ s ∧ ¬ℓ ⊤ 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. These challenges are inherent to the nature of decentralization; the monitors have a partial view of the system and need to account for communication and consensus. Our assumptions on the system are as follows: No monitors are malicious, i.e., messages do not contain wrong information; No messages are lost, they are eventually delivered in their entirety but possibly out-of-order; All components share one logical discrete time marked by round numbers indicating relevant transitions in the system specification.

Example 1.1 (Switch triggers bulb). Consider a system that contains two components: a light switch and a light bulb. The possible states of the switch and bulb can be on or off. Let us associate the states of the switch and bulb with the atomic propositions s and ℓ, respectively. Using the atomic propositions, we can encode the observations about the system. For example, the observation ⟨s, ⊥⟩ indicates that the switch is in the state off. An event is simply a set of observations. The event {⟨s, ⊤⟩, ⟨ℓ, ⊥⟩} indicates that the switch is on, and the light is off. We next define (informally) a property of the system: "The light bulb must be on one timestamp after the switch is on, until the switch is turned off". The property is used to synthesize a monitor that checks it (for example, the monitor in Figure 1, introduced in Example 2.1). Now let us consider two traces: tr 0 def = {⟨s, ⊥⟩, ⟨ℓ, ⊥⟩} • {⟨s, ⊤⟩, ⟨ℓ, ⊥⟩} • {⟨s, ⊤⟩, ⟨ℓ, ⊤⟩} • {⟨s, ⊥⟩, ⟨ℓ, ⊥⟩} and tr 1 def = {⟨s, ⊥⟩, ⟨ℓ, ⊥⟩} • {⟨s, ⊤⟩, ⟨ℓ, ⊥⟩} • {⟨s, ⊤⟩, ⟨ℓ, ⊥⟩}. We see that tr 0 complies with the specification, while tr 1 violates it as the light is not turned on after the switch is turned on. When monitoring such a system, we can construct a decentralized monitor of the property. For this, we need to decide on where to deploy the monitors, and what will each monitor check. By being able to vary monitor placement, we are able to control the resources needed to monitor on a given component of the system. Furthermore, due to the nature of decentralization, each monitor will have a partial view of the system. While the monitor on the switch can see the value of atomic proposition s, it cannot determine that of ℓ, and as such, it must communicate with other monitors to establish it.

Challenges. Several algorithms have been designed [START_REF] Bauer | Decentralised LTL monitoring[END_REF][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] 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. Such techniques start from a global specification and then synthesize local monitors with either a copy of the global specification [START_REF] Bauer | Decentralised LTL monitoring[END_REF][START_REF] Bonakdarpour | Challenges in Fault-Tolerant Distributed Runtime Verification[END_REF] or a completely different specification to monitor (typically a subformula of the original formula) [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]. In this paper, we refer to the former as a centralized specification and to the latter as a decentralized specification. These different approaches of synthesis are separate from monitoring and their evaluation is of interest. In this case, we would like to split the problem of generating equivalent On the Monitoring of Decentralized Specifications :3 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 1which interferes with the completeness of a monitoring algorithm.

Contributions. We tackle the presented challenges using two complementary approaches. The first approach consists in using the data structure Execution History Encoding (EHE) that encodes automata executions. Since by using EHE one only needs to rewrite Boolean expressions, we are able to 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]. The second approach introduces decentralized specifications. We introduce decentralized specifications, define their semantics, interdependencies and study some of their properties. 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. A decentralized specification is thus as a set of n finitestate automata with specific properties, which we call monitors. We associate n monitors to these components with the possibility of multiple monitors being associated to a component. Therefore, we generalize monitoring algorithms to multiple monitors. Monitoring a centralized system can be seen as a special case with one component, one specification, and one monitor. As such, we present a general decentralized monitoring algorithm that uses two high level steps: setup and monitor. The setup phase creates the monitors, defines their dependencies and attaches them to components. As such, the setup phase defines a topology of monitors and their dependencies. The monitor phase allows the monitors to begin monitoring and propagating information to reach a verdict when possible. Therefore, 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. We formulate and solve the problems of deciding compatibility and monitorability for decentralized specifications. Compatibility ensures that a monitor topology can be deployed on a given system, monitorability ensures that given a specification, monitors are able to eventually emit a verdict, for all possible traces. 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. We use THEMIS to create new metrics related to load-balancing and our data structures. We use two scenarios to compare four existing algorithms. The first scenario is a synthetic benchmark, using random traces and specifications, while the second scenario is a real example that uses the publish-subscribe pattern in the Chiron graphical user interface system. The synthetic scenario examines the trends of the analysis, and the Chiron scenario examines more specific differences in behavior.

This paper extends the work presented at the ACM SIGSOFT International Symposium on Software Testing and Analysis 2017 [START_REF] El | Monitoring Decentralized Specifications[END_REF], as follows:

• introducing a high-level informal overview of the approach (Section 2);

• improving on the clarity by providing a running example that tackles all introduced concepts;

• adding the property that the EHE construction guarantees its determinism (Proposition 4.8);

• elaborating and adding properties of decentralized specifications (monitorability, compatibility) as well as the algorithms for checking them (Section 6);

• improving THEMIS by optimizing the EHE performance, and adding distributed and multithreaded support (Section 8); • elaborating on the results and providing a discussion of the synthetic benchmarks (Section 9.1); • including additional insight on the effect of network delay on the EHE size (Section 9.1.7);

• evaluating the algorithms on a new use case based on the Chiron example that relies on publish subscribe and has a formalized specification (Section 9.2); • extending related work (Section 10); and • formulating additional problems for the future (Section 11).

Overview. We begin by introducing an informal view of the approaches in Section 2, by first distinguishing between centralized and decentralized for two aspects of RV: the specification and the monitoring itself. Then, we introduce a high-level view of decentralized specifications semantics, advantages, and the need to manage partial observations. We lay out the basic blocks, by introducing our basic data structure (dict), and the basic notions of monitoring with expressions in Section 3. We present our first approach, a middle ground between rewriting and automata evaluation by introducing the Execution History Encoding (EHE) data structure in Section 4. The EHE is designed to be particularly useful for handling partial observations. We shift the focus on studying decentralized specifications by defining their semantics (Section 5), and their properties (Section 6). In Section 7, 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 Section 8, we present the THEMIS tool, which we use in Section 9 to compare the algorithms presented in Section 7 under two different scenarios: a synthetic random benchmark, and an example of a publish-subscribe system. In Section 10, we present related work that covers decentralized monitoring using rewriting, global predicate detection, and streams. In Section 11, we present future work and formulate additional interesting properties for decentralized specifications. Finally, we conclude in Section 12.

METHODOLOGICAL OVERVIEW

In this section, we discuss the basic terminology referenced in the paper. We distinguish between centralized and decentralized for two aspects of RV: the specification and the monitoring itself. The distinction allows us to introduce and overview our approach to monitoring decentralized specifications.

Centralized Monitoring of a Centralized Specification

An LTL3 monitor is a typical automaton used in RV (c.f. [START_REF] Bauer | Runtime Verification for LTL and TLTL[END_REF][START_REF] Falcone | Efficient and Generalized Decentralized Monitoring of Regular Languages[END_REF]). An LTL3 monitor is a complete, minimal, and deterministic Moore automaton where states are labeled with the verdicts in the set B 3 = {⊤, ⊥, ?}, and transitions are labeled with atomic propositions, which are used to represent abstract states of the system. Verdicts ⊤ and ⊥ respectively indicate that the current execution complies and does not comply with the specification, while verdict ? indicates that the verdict has not been determined yet. Verdicts ⊤ and ⊥ are called "final", as once the monitor outputs ⊤ or ⊥ for a given trace, it cannot output a different verdict for any extension of that trace.

Example 2.1 (LTL3 monitor). We introduced in Example 1.1 the system composed of a lightbulb and a switch. The LTL 3 monitor that checks for its specification is presented in Figure 1. The automaton consists of three states: q 0 , q 1 , and q 2 associated respectively with the verdicts ?, ?, and ⊥. Upon reaching q 2 , the verdict is final as it can no longer change. The final verdict indicates that, at some point in the execution, the light was off while the switch was on.

In the case of Example 2.1, it is possible to imagine one monitor running (with or alongside) the program, and having access to the global state of the program. We refer to such a scenario On the Monitoring of Decentralized Specifications :5 as centralized monitoring of a centralized specification. There is one global specification of the system, being checked by a given monitor that has access to all the information about the atomic propositions.

Decentralized Monitoring of Centralized Specifications

Section 2.1 introduces a monitor capable of observing all of the atomic propositions. Such monitor is able to immediately take transitions upon receiving observations. However, it is not always the case that we have a central point of observation. That is, it is possible that atomic propositions are not all observable by one monitor. Such a scenario is typically called decentralized monitoring, and is the topic of many research efforts (see Section 10). The monitoring is done by various monitors communicating to determine the global state efficiently, and be able to check the property.

Example 2.2 (Decentralized monitoring). Consider the monitor presented in Example 2.1. We can see that the switch and lightbulb are two separate components, a monitor placed on the switch cannot observe any atomic proposition related to the lightbulb. In this case, the associated RV technique considers the global specification of the system, and then proceeds to create monitors and determine their communication patterns.

We note that the monitors are all monitoring one global specification. The main challenge is that monitors must deal with partial observations. We refer to such a scenario as decentralized monitoring of a centralized specification, as all monitors are verifying the same specification. Details on centralized and decentralized monitoring of a centralized specification are provided in Section 4.

Decentralized Monitoring of Decentralized Specifications

We noticed that so far, decentralized monitoring allows for several monitors that monitor the same specification. Typically, a decentralized monitoring algorithm will consider one (global) specification, and either generate necessary monitors that are tasked with monitoring a part of the specification, or allow for consensus among multiple monitors to find the global verdict 2 . In this paper, we focus on multiple monitors each having their own independent specification, of which others are normally unaware. We thus focus on decentralized monitoring of decentralized specifications3 .

Informal

Semantics. Informally, a decentralized specification considers the system as a set of components, defines a set of LTL3 monitors (see Section 2.1), additional atomic propositions that represent references to monitors, and attaches each monitor to a component. Attaching monitors to components allows a monitor specification to explicitly reference atomic propositions that are associated with the component. However, the transition labels in a monitor are restricted to only atomic propositions related to the component on which the monitor is attached, and references to other monitors.

A monitor reference is evaluated as if it were an oracle as shown in Figure 2. That is, to evaluate a monitor reference m j , in a monitor A i , at a timestamp n, the monitor referenced (A j ) is executed starting from the initial state by looking at observations in the trace starting at n. The atomic proposition m j at n takes the value of the final verdict reached by the monitor A j starting its evaluation from n. Details of the semantics are provided in Section 5. Furthermore, to evaluate reference we need the resulting oracle execution to be able to reach a final verdict, which is not always guaranteed. As such, it is important to define some of the properties of decentralized specifications such as monitorability, which indicates that a final verdict is co-reachable from any state in a given monitor (Section 6.1). We elaborate on characterizing and computing properties of decentralized specifications in Section 6.

q i0 q i q ′ i [1, n -1] ¬m j m j ⊤ A i q j0 q j [n, m -1] ⊤ A j 0 n n + 1 m n : m j → ⊥

Managing Partial

Observations. We notice that monitor references are evaluated as if we were evaluating partial observations that we receive in the future. In fact, managing partial observations is important for decentralized monitoring in general, including decentralized monitoring of centralized specifications (Section 2.2). To that end, we introduce the Execution History Encoding (EHE) data structure in Section 4.2 that allows us to monitor in the presence of partial observations. The EHE is useful for two main reasons.

First, since we deal with partial observations, it is important to keep track of potential states an automaton could be in, and manage the guesses as information is eventually known, in a uniform way, this applies for decentralized monitoring in general. This helps us compare algorithms that rely on partial observations (Sections 7, 8 and 9).

Second, since we do not deal with loss of messages in the system, monitors are always guaranteed to receive observations eventually. Therefore, we are interested in designing the EHE so that it can replicate its state under strong eventual consistency (SEC) [START_REF] Shapiro | Conflict-Free Replicated Data Types[END_REF]; any two monitors eventually exchanging EHEs should have the same view of the system. This is only useful if monitors are monitoring the same automaton, thus it is mainly useful for decentralized monitoring of centralized specifications. Section 4.3 elaborates on the usage of EHE where multiple monitors are monitoring the same specification.

Monitor Placement.

Being able to decide the specification and monitor placement is particularly useful for applications such as internet of things. Applications can be tailored to the computational resources and also to the proximity of various devices and the network itself. Recall Example 2.2, if more computing resources are given to the switch component than the lightbulb, then it is possible for the monitor on the switch to perform the monitoring computations, while the one on the lightbulb merely forwards observations. Alternatively, they can both forward the observations to another component which can then perform the monitoring computations. The decentralized specification determines what each monitor will check as well as the dependencies between the various monitors in the system.

Advantages of Using

References. We mentioned in Section 2.3.1 that references are not always guaranteed to return a final verdict, and we need specific properties to ensure so. However, references are particularly useful when synthesizing monitors from LTL as in [START_REF] Bauer | Runtime Verification for LTL and TLTL[END_REF], since the algorithm is doubly exponential in the number of atomic propositions. Offsetting parts of the subformula to other monitors allows us to have a lower number of atomic propositions in a given specification. Additionally, since references are treated as oracles, this allows specifications to be constructed in a modular way, allowing monitors to not even be aware of the subspecification.

Example 2.3 (Synthesizing check light). Recall the property in Example 2.1 responsible for verifying that a light switch does indeed turn a light bulb on until the switch is turned off. Suppose we have multiple rooms with multiple such lightbulbs and switches, the LTL formula parametrized by each pair can be expressed in LTL as follows:

sc_light(i) def = G(s i =⇒ X(ℓ i U ¬s i )).
To verify the property across all n pairs, we formulate a property sc_ok

def = i ∈[0..n] sc_light(i).
In the case of a decentralized specification the formula will reference each monitor leading to a conjunction of n atomic propositions. However, in the case of a centralized specification, the specification needs to be written as:

sc_ok cent def = i ∈[0...n] G(s i =⇒ X(ℓ i U ¬s i ))
, which is significantly more complex as a formula consisting of 4n operators (to cover the subspecification), along n conjunctions, and defined over each sensor and light bulb atomic propositions (2n). Given that monitor synthesis is doubly exponential, ltl2mon [START_REF] Bauer | Runtime Verification for LTL and TLTL[END_REF] requires significant resources and time to generate the minimal Moore automaton (in our case 4 , it was unable to generate the monitor for n = 3 after a timeout of one hour).

COMMON NOTIONS

We introduce the dict data structure (Section 3.1.) used to build more complex data structures, and define the basic concepts for decentralized monitoring (Section 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. In addition, we would like 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 (noted dict) as our basic building block that assigns a value to a given key. Data structure dict will be used to define the memory of a monitor (Section 3.2), and data structure EHE which encodes the execution of an automaton (Section 4.2).

We model dict as a partial function f. The domain of f (denoted by dom(f)) is the set of keys, while the codomain of f (denoted by codom(f)) is the set of values. dict supports two operations: query and merge. The query operation checks if a key k ∈ dom(f) and returns f(k). If k dom(f), then it is undefined. The merge operation of a dict f with another dict g, is modeled as function composition. Two partial functions f and g are composed using operator † op where op :

(dom(f) × dom(g)) → (codom(f) ∪ codom(g)) is a binary function. f † op g : dom(f) ∪ dom(g) → codom(f) ∪ codom(g) f † op g(x) =            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 based on a total order (≺) between the elements, so that it always chooses the highest element to guarantee idempotence, while † ∨ uses the logical or operator to combine elements. Respectively, we denote the associated pairwise set operators by 2 and ∨ . Data structure dict can be composed by only using operation merge. The modifications never remove entries, the state of dict is then monotonically increasing using the order provided by merge. By ensuring that merge is idempotent, commutative, and associative we fulfill the necessary conditions [START_REF] Shapiro | Conflict-Free Replicated Data Types[END_REF] for our data structure to be a CvRDT (Proposition 3.1). Proposition 3.1. Data structure dict with operations query and merge is a CvRDT.

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 in B 2 = {⊤, ⊥} is a final verdict. It indicates that the monitor has concluded its monitoring, and any further input will not change affect it. Abstract states of a system are represented as a set of atomic propositions (AP). A monitoring algorithm typically includes additional information such as a timestamp associated with the atomic propositions. We capture this information as an encoding of the atomic propositions (Atoms), this encoding is left to the monitoring algorithm to specify.

Definition 3.2 (Event

). An observation is a pair in AP × B 2 indicating whether or not a proposition has been observed. An event is a set of observations in 2 AP×B 2 .

Example 3.3 (Event). We recall the example of a light switch and bulb from Example 1.1. We have AP = {s, ℓ}. The event {⟨s, ⊤⟩, ⟨ℓ, ⊥⟩} indicates that the switch is observed to be on (i.e., the atomic proposition s is observed to be true), while the light bulb is observed to be off (i.e., the atomic proposition ℓ is observed to be false).

A decentralized monitoring algorithm requires retaining, retrieving and communicating observations. Monitoring algorithms are versatile, and may require additional information associated with atomic propositions. This information can include timestamps indicating when the atomic proposition was observed, or a component ID, to determine where the atomic proposition was observed. As such, when stored, atomic propositions are typically encoded to add this additional information by the monitoring algorithm. To abstract the additional information, and remain general, the monitors store the encoded atomic proposition (instead of the atomic proposition itself), the encoded atomic proposition is referred to as atom. Expr Atoms (resp. Expr AP ) denotes the set of Boolean expressions over Atoms (resp. AP). An encoder is a function enc : Expr AP → Expr Atoms that encodes the atomic propositions into atoms. In this paper, we use two encoders: idt which is the identity function (it does not modify the atomic proposition), and ts t which adds a timestamp t to each atomic proposition. The identity encoder is mainly used with automata as its transitions are labelled by AP, and the timestamp encoder is used when manipulating the execution history encoding introduced in Section 4.2, as it encodes information about rounds in the expressions.

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.

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). We recall from Example 3.3 the event: evt = {⟨s, ⊤⟩, ⟨ℓ, ⊥⟩}. At t = 1, the resulting memories using encoders idt and ts 1 are: memc(evt, idt) = [s → ⊤, ℓ → ⊥], memc(evt, ts 1 ) = [⟨1, s⟩ → ⊤, ⟨1, ℓ⟩ → ⊥], respectively.

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 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 a memory is a dict and † 2 is idempotent, associative, and commutative, it follows from Proposition 3.1 that a memory is a CvRDT (Corollary 3.6). Corollary 3.6. A memory with operation † 2 is a CvRDT.

In this paper, we perform monitoring by manipulating expressions in Expr Atoms . 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. Operation rw yields a smaller formula to work with. Example 3.8 (Rewriting). We extend the set of atomic propositions from Example 3.3 to include a motion sensor. We associate the motion sensor state with the atomic proposition pres, where if pres is observed to be ⊤, then the sensor is detecting motion. We have AP = {s, ℓ, pres}. We consider the memory from Example 3.5: M = [s → ⊤, ℓ → ⊥]; and an expression e = (s ∨ ℓ) ∧ pres. In this case, we want to check if the light or switch are on only when the motion detects presence. We have M(s) = ⊤, M(ℓ) = ⊥, M(pres) = ?. Since pres is associated with ? B 2 then it will not be replaced when the expression is evaluated. The resulting expression is rw(e, M) = (⊤ ∨ ⊥) ∧ pres.

We eliminate additional atoms using Boolean logic. We denote by simplify(expr) the simplification of expression expr5 . Example 3.9 (Simplification). Using the same setting as Example 3.8, we consider memory M = [s → ⊤] and expression e = (s ∧ ℓ) ∨ (s ∧ ¬ℓ). We have e ′ = rw(e, M) = (ℓ ∨ ¬ℓ). We notice that rewriting e ′ does not yield a final verdict. However, 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 e. Function eval returns the verdict ⊤ (resp. ⊥) if the simplification after rewriting is (Boolean) equivalent to ⊤ (resp. ⊥), otherwise it returns verdict ?.

Example 3.11 (Evaluating expressions). We recall from Example 3.8 memory M = [s → ⊤, ℓ → ⊥]; and expression e = (s∨ℓ)∧pres. We have simplify(rw(e, M)) = simplify((⊤∨⊥)∧pres) = pres, and eval(e, M) = ? which depends on pres. We cannot emit a final verdict before observing pres.

A decentralized system is a set of components C. We assign a sequence of events to each component using a decentralized trace function.

Definition 3.12 (Decentralized trace). A decentralized trace of length n is a total function tr :

[1, n] × C → 2 AP×B 2 (
where [1, n] denotes the interval of the n first non-zero natural numbers).

Function tr assigns an event to a component for a given timestamp. We denote by T the set of all possible decentralized traces. We additionally define function lu : AP → C to assigns an atomic proposition to a component. We assume that (1) no two components can observe the same atomic propositions 6 , and (2) at least one atomic proposition is associated with a component (a component with no atomic propositions to monitor, can be simply considered excluded from the system under monitoring). Function lu is defined as 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. The length of a trace tr is denoted by |tr|. An empty trace has length 0 and is denoted by ϵ. Monitoring using LTL or finite-state automata relies on sequencing the trace. Events must be totally ordered. A timestamp indicates simply the order of the sequence of events. As such, a timestamp represents a logical time, it can be seen as a round number. Every round consists in a transition taken on the automaton after reading a part of the word. While tr gives us a view of what components can locally see, we reconstruct the global trace to reason about all observations. A global trace of the system is therefore a sequence of events. A global trace encompasses all observations observed locally by components. While a global trace will never be used in practice, we use it for the purpose of reasoning about the global state (Section 4.1), and ensuring the correctness of our approach (Proposition 4.10).

Definition 3.13 (Reconstructing a global trace). Given a decentralized trace tr of length n, we reconstruct the global trace using function ρ :

[1, n] × C → 2 AP×B 2 → [1, n] → 2 AP×B 2 defined as ρ(tr) = evt 1 • . . . • evt n s.t. ∀i ∈ [1, n] : evt 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, ρ(ϵ) = ϵ.

Example 3.14 (Traces). Using the switch and light bulb from Example 1.1, we define multiple components. We consider a system of two components lswitch and bulb, that are associated with atomic propositions s and ℓ respectively. An example decentralized trace of the system is given by tr = [1 → lswitch → {⟨s, ⊤⟩}, 1 → bulb → {⟨ℓ, ⊤⟩}, 2 → lswitch → {⟨s, ⊤⟩}, 2 → bulb → {⟨ℓ, ⊥⟩}]. That is, component lswitch observes proposition s to be ⊤ at both timestamps 1 and 2, while bulb observes ℓ to be ⊤ at timestamp 1 and ⊥ at timestamp 2. The associated global trace is: ρ(tr) = {⟨s, ⊤⟩, ⟨ℓ, ⊤⟩} • {⟨s, ⊤⟩, ⟨ℓ, ⊥⟩}.

On the Monitoring of Decentralized Specifications :11

CENTRALIZED SPECIFICATIONS

We now focus on a decentralized system specified by one global automaton. We consider automata that emit 3-valued verdicts in the domain B 3 , similar to those in [START_REF] Bauer | Runtime Verification for LTL and TLTL[END_REF][START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF] for centralized systems. Using automata with 3-valued verdicts has been the topic of a lot of the Runtime Verification literature [START_REF] Basin | Failure-aware Runtime Verification of Distributed Systems[END_REF][START_REF] Bauer | Runtime Verification for LTL and TLTL[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][START_REF] Falcone | Efficient and Generalized Decentralized Monitoring of Regular Languages[END_REF], we focus on extending the approach for decentralized systems in [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF] 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 the EHE, a data structure that encodes the necessary information from an execution of the automaton. Monitoring using EHEs ensures strong eventual consistency. We begin by defining the specification automaton used for monitoring in Section 4.1, then we present the EHE data structure, illustrate its usage for monitoring in Section 4.2, and describe its use to reconcile partial observations in Section 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 ). We choose to label the transitions with Boolean expressions as opposed to events, to keep a homogeneous representation (with EHE)7 . Definition 4.1 (Specification). The specification is a deterministic Moore automaton ⟨Q, q 0 , δ, ver⟩ where q 0 ∈ Q is the initial state, δ : Q × Expr AP → Q is the transition function and ver : Q → B 3 is the labeling function.

The labeling function associates a verdict with each state. We assume that by construction the state with final verdicts are sink states (as synthesized in [START_REF] Bauer | Runtime Verification for LTL and TLTL[END_REF]).

When using multiple automata we use labels to separate them, A ℓ = ⟨Q ℓ , q ℓ 0 , δ ℓ , ver ℓ ⟩. We fix A to be a specification automaton for the remainder of this section. For monitoring, we are interested in events (Definition 3.2), we extend δ to events, and denote it by ∆8 . Definition 4.2 (Transition over events). Given an event evt, we build the memory M = memc(evt, idt). Then, function ∆ : Q × 2 AP×B 2 → Q is defined as follows:

∆(q, evt) = q ′ if evt ∅ ∧ ∃q ′ ∈ Q, ∃e ∈ Expr AP : δ (q, e) = q ′ ∧ eval(e, M) = ⊤, q otherwise.
A transition is taken only when an event contains observations (i.e., evt ∅). This allows the automaton to wait on observations before evaluating, as such it remains in the same state (i.e., ∆(q, ∅) = q). Upon receiving observations, we use M to evaluate each label of an outgoing transition, and determine if a transition can be taken (i.e., ∃q ′ ∈ Q, ∃e ∈ Expr AP : δ (q, e) = q ′ ∧eval(e, M) = ⊤).

To handle a trace, we extend ∆ to its reflexive and transitive closure in the usual way, and note it ∆ * . For the empty trace, the automaton makes no moves, i.e., ∆ * (q 0 , ϵ) = q 0 . Example 4.3 (Monitoring using expressions). Recall the monitor from Example 2.1 monitoring the light switch and bulb interaction. Let us consider the global trace from Example 3.14: evt 0 • evt 1 , with evt 0 = {⟨s, ⊤⟩, ⟨ℓ, ⊤⟩} and evt 1 = {⟨s, ⊤⟩, ⟨ℓ, ⊥⟩}. The resulting memory at t = 1 is M = memc(evt 0 , idt) = [s → ⊤, ℓ → ⊤] (see Example 3.5). The transition from q 0 to q 1 is taken since eval(s, M) = ⊤. Thus we have ∆(q 0 , evt 0 ) = q 1 with verdict ver(q 1 ) = ?. We continue by repeating the process for t = 2. The memory is M ′ = memc(evt 1 , idt) = [s → ⊤, ℓ → ⊥]. The transition from q 1 to q 2 is taken since eval(s ∧ ¬ℓ, M) = ⊤. Thus we have ∆(q 1 , evt 1 ) = q 2 with verdict ver(q 2 ) = ⊥. We can see that for this trace, the property is violated.

Remark 1 (Properties and normalization). We recall that the specification is a deterministic and complete automaton. Hence, there are properties on the expressions that label the transition function. For any q ∈ Q, we have: 1) ∀M ∈ Mem : (∃⟨q, e⟩ ∈ dom(δ ) : eval(e, M) = ⊤) =⇒ (∄⟨q, e ′ ⟩ ∈ dom(δ ) \ {⟨q, e⟩} :

eval(e ′ , M) = ⊤); and 2) the disjunction of the labels of all outgoing transitions results in an expression that is a tautology. The first property states that for all possible memories encoded with idt no two (or more) labels can evaluate to ⊤ at once. It results from determinism: no two (or more) transitions can be taken at once. The second property results from completeness: given any input, the automaton must be able to take a move. Furthermore, we note that for each pair of states ⟨q, q ′ ⟩ ∈ Q × Q, we can rewrite δ such that there exists at most one expression e ∈ Expr AP , such that δ (q, e) = q ′ , without loss of generality. This is because for a pair of states, we can always disjoin the expressions to form only one expression, as it suffices that only one expression needs to evaluate to ⊤ to reach q ′ . By having at most one transition between any pair of states, we simplify the topology of the automaton.

The Execution History Encoding (EHE) Data Structure

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 . . .. It indicates that, for each timestamp t ∈ N * , the automaton is in the state q t9 . 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 aim of the EHE is to construct a data structure which follows the current state of an automaton, and in case of partial information, tracks the possible states the automaton can be in. For that purpose, we need 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. Execution History Encoding (EHE) is a data structure designed to encode an execution of an automaton using boolean expressions while accounting for partial observations. Definition 4.4 (Execution History Encoding -EHE). An Execution History Encoding (EHE) of the execution of an automaton A is a partial function

I : N × Q → Expr Atoms .
Intuitively, for a given execution, an EHE encodes the conditions to be in a state at a given timestamp as an expression in Expr Atoms . I(t, q) is an expression used to track whether the data structure automaton is in state q at t, i.e., I(t, q) holds iff the automaton is in state q at timestamp t. We begin by defining the EHE at timestamp t = 0 which indicates the initial state of the execution. For a given automaton with an initial state q 0 , we know that we are indeed in the initial state at t = 0. As such, the initial EHE for the beginning of the execution is the function [0 → q 0 → ⊤]. For future timestamps, the EHE is extended inductively based on reachable states.

On the Monitoring of Decentralized Specifications :13 t q e 0 q 0 ⊤ 1 q 0 ¬⟨1, s⟩ q 1 ⟨1, s⟩ 2 q 0 (¬⟨1, s⟩ ∧ ¬⟨2, s⟩) ∨ (⟨1, s⟩ ∧ ¬⟨2, s⟩) q 1 (⟨1, s⟩ ∧ ⟨2, s⟩ ∧ ⟨2, ℓ⟩) ∨ (¬⟨1, s⟩ ∧ ⟨2, s⟩) q 2 ⟨1, s⟩ ∧ ⟨2, s⟩ ∧ ¬⟨2, ℓ⟩ Definition 4.5 (Constructing an EHE). An EHE encoding the execution till timestamp t, noted I t is constructed inductively using function mov :

(N × Q → Expr Atoms ) × N × N → (N × Q → Expr) I t def = mov([0 → q 0 → ⊤], 0, t) mov(I, t s , t e ) def = mov(I ′ , t s + 1, t e ) if t s < t e , I otherwise, with I ′ = I † ∨ ∨ q ′ ∈next(I,t s )
{t s + 1 → q ′ → to(I, t s , q ′ , ts t s +1 )}, and to(I, t, q ′ , enc) def = { ⟨q,e ′ ⟩ | δ (q,e ′ )=q ′ } (I(t, q) ∧ enc(e ′ ))

next(I, t) def = {q ′ ∈ Q | ∃⟨t, q⟩ ∈ dom(I), ∃e ∈ Expr AP : δ (q, e) = q ′ }.
The automaton is in the initial state at t = 0. We start building up I with the initial state and associating it with expression ⊤: [0 → q 0 → ⊤]. Then, for a given timestamp t, we use function next to check the next set of reachable states in the automaton (at t + 1) by looking at the outgoing transitions for all states in I at t (i.e., we find a state q ′ such that ∃⟨t, q⟩ ∈ dom(I), ∃e ∈ Expr AP : δ (q, e) = q ′ ).

We now build the necessary expression to reach a state q ′ from multiple states by disjoining the transition labels using to(I, t, q ′ , enc), as it suffices to take only one such path to reach q ′ . Since the label consists of expressions in Expr AP we use an encoder (enc) to get an expression in Expr Atoms . If an expression I(t, q) encodes the condition to reach q at t, and q ′ is reachable from q at t + 1 using the condition e ′ , then it suffices to compute the conjunction.

Finally, I ′ is obtained by considering the next states and merging all their expressions with

I: I ′ = I † ∨ ∨ q ′ ∈next(I,t s ) {t s + 1 → q ′ → to(I, t s , q ′ , ts t s +1 )}.
We recall from Section 3.1 that operator † ∨ performs the disjunction between entries, while operator ∨ on EHE adds expressions for given timestamps and states that are not present, and merges multiple EHEs row by row using disjunction when the entry exists. As such, an EHE is assembled for t + 1 by combining all expressions for reachable states at t + 1 using ∨ . The assembled EHE for t + 1 is then combined with the EHE for t (I) using † ∨ , to form the EHE that contains both (I ′ ). We use the notation rounds(I), to denote all the timestamps that the EHE encodes, i.e., rounds(I) = {t ∈ N | ⟨t, q⟩ ∈ dom(I)}. Similarly to automata notation, if multiple EHEs are present, we use a label in the subscript to identify them and their respective operations (I ℓ denotes the EHE of A ℓ ).

Example 4.6 (Constructing an EHE). We encode the execution of the automaton presented in Example 4.3. For this example, we use the encoder ts n which appends timestamp n to an atomic proposition. 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 stay at q 0 at t = 1, we must be at q 0 at t = 0, and have : to(I 0 , 0, q 0 , ts 1 ) = I 0 (0, q 0 ) ∧ ¬⟨1, s⟩. 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, s⟩ = ⟨1, s⟩. The encoding up to timestamp t = 2 is obtained with I 2 = mov(I 0 , 0, 2) and is shown in Table 1. We notice that when a state can be reached from multiple states, their expressions are disjoined. For instance, to reach q 0 at t = 2, we can either have stayed at q 0 at t = 1 and taken the loop transition or have moved to q 1 , then taken the transition back to q 0 (¬⟨2, s⟩).

Constructing an EHE with function mov is done only through merges using operator † ∨ . By creating an arbitrary order on the states (noted ≺ Q ) in the specification automaton, we can then compare any two entries of the EHE. We can enumerate the states of the EHE I as a set of tuples: {⟨t, q, e⟩ | I(t, q) = e}. We are then able to compare any such two tuples: ⟨t, q, e⟩ ≺ ⟨t ′ , q ′ , e ′ ⟩. To do so, we first check the order of timestamps (i.e. if t ≺ t ′ then ⟨t, q, e⟩ ≺ ⟨t ′ , q ′ , e ′ ⟩). When the timestamps are the same (t = t ′ ) then we use the order ≺ Q to determine the order of the tuples. When both the timestamp and the state are the same, then merging occurs. By merging with † ∨ (Section 3.1) the entries not found in both are added using set union, and entries with the same timestamp and state (t, q) are disjoined (∨), which is idempotent, associative, and commutative. As such, the EHE is a CvRDT. Corollary 4.7. An EHE constructed with mov and merged with † ∨ is a CvRDT.

By constructing the EHE, we have for each timestamp t and each state q in the EHE an expression. Using information from the execution stored in a memory M, if eval(I(t, q), M) is ⊤, then we know that the automaton is indeed in state q at timestamp t. Given a memory M which stores atoms, function sel 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, M, t) = q if ∃q ∈ Q : eval(I(t, q), M) = ⊤, undef otherwise.
We note that q such that eval(I(t, q), M) = ⊤ is unique. Since we are encoding deterministic automata, we recall from Remark 1 that when a state q is reached at a timestamp t resulting from an execution, no other state can be reached at t for the same execution. Moreover, the EHE construction using operation mov and encoder ts preserves determinism. Proposition 4.8 (Deterministic EHE). Given an EHE I constructed with operation mov using encoder ts, we have:

∀t ∈ rounds(I), ∀M ∈ Mem, ∃q ∈ Q : eval(I(t, q), M) = ⊤ =⇒ ∀q ′ ∈ Q \ {q} : eval(I(t, q ′ ), M) ⊤.
Determinism is preserved since, by using encoder ts, we only change an expression to add the timestamp. By construction, when there exists a state q s.t. eval(I(t, q), M) = ⊤, such a state is unique, since the EHE is built using a deterministic automaton. The full proof is in Appendix A.

Function verAt is a short-hand to retrieve the verdict at a given timestamp t:

verAt(I, M, t) = ver(q) if ∃q ∈ Q : q = sel(I, M, t), ? otherwise.
Example 4.9 (Monitoring with EHE). Consider the constructed EHE from Example 4.6 shown in Table 1. Let us consider the global trace from Example 3.14: evt 0 • evt 1 , with evt 0 = {⟨s, ⊤⟩, ⟨ℓ, ⊤⟩} and evt 1 = {⟨s, ⊤⟩, ⟨ℓ, ⊥⟩}. We create a memory with the events of the two timestamps. Let M = memc(evt 0 , ts 1 ) † 2 memc(evt 1 , ts 2 ) = [⟨1, s⟩ → ⊤, ⟨1, ℓ⟩ → ⊤, ⟨2, s⟩ → ⊤, ⟨2, ℓ⟩ → ⊥, ]. It is possible to infer the state of the automaton at t = 2 using I 2 = mov([0 → q 0 → ⊤], 0, 2) by using sel(I 2 , M, 2), we evaluate:

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

While the construction of an EHE preserves the determinism found in the automaton, an important property is in ensuring that the EHE encodes correctly the execution of the automaton. Proposition 4.10 (Soundness). Given a decentralized trace tr of length n, we reconstruct the global trace ρ(tr) = evt 1 • . . . • evt n , we have: ∆ * (q 0 , ρ(tr)) = sel(I n , M n , n), with:

I n = mov([0 → q 0 → ⊤], 0, n), and M n = 2 t ∈[1,n] {memc(evt t , ts t )}.
EHE is sound with respect to the specification automaton; both the automaton and EHE 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 (|ρ(tr)|).

Proof sketch. We first establish that both the EHE and the automaton memories evaluate two similar expressions modulo encoding to the same result. That is, for the given length i, the generated memories at i + 1 with encodings idt and ts i+1 yield similar evaluations for the same expression e. Then, starting from the same state q i reached at length i, we assume ∆ * (q 0 , evt 1 • . . . • evt i ) = sel(I i , M i , i) = q i holds. We prove that it holds at i + 1, by building the expression (for each encoding) to reach state q i+1 at i + 1, and showing that the generated expression is the only expression that evaluates to ⊤. As such, we determine that both evaluations point to q i+1 being the next state. The full proof is in Appendix A.

Decentralized Monitoring with EHE

EHE provides interesting properties for decentralized monitoring. Two (or more) components sharing EHEs and merging them will be able to infer the same execution history of the automaton. That is, components will be able to aggregate the information of various EHEs, and are able to determine the reached state, if possible, or that no state was reached. Merging two EHEs of the same automaton with † ∨ allows us to aggregate information from two partial histories.

However, two EHEs for the same automaton contain the same expression if constructed with mov. To incorporate the memory in an EHE, we generate a new EHE that contains the rewritten and simplified expressions for each entry. To do so we define function inc to apply to a whole EHE and a memory to generate a new EHE: inc(I, M) = 2 ⟨t ,q ⟩ ∈dom(I) {[⟨t, q⟩ → simplify(rw(I(t, q), M))]}. We note, that for a given I and M, inc(I, M) maintains the invariant of Proposition 4.8. We are simplifying expressions or rewriting atoms with their values in the memory which is what eval already does for each entry in the EHE. That is, inc(I, M) is a valid representation of the same deterministic and complete automaton as I. However, inc(I, M) incorporates information from memory M in addition. ∀⟨t, q⟩ ∈ dom(inc(I, M)) : eval(I(t, q), M) ⇔ eval(inc(I, M)(t, q), []).

Proof. Follows directly by construction of inc and the definition of eval (which uses functions simplify and rw). □ Proposition 4.11 ensures that it is possible to directly incorporate a memory in an EHE, making the memory no longer necessary. This is useful for algorithms that communicate the EHE, as they do not need to also communicate the memory.

By rewriting the expressions, the EHEs of two different monitors receiving different observations contain different expressions. However, since they still encode the same automaton, and observations do not conflict, merging with † ∨ shares useful information. Corollary 4.12. Given an EHE I constructed using function mov, and two memories M 1 and M 2 that do not observe conflicting observations10 , the two EHEs I 1 = inc(I, M 1 ) and I 2 = inc(I, M 2 ) have the following properties ∀⟨t, q⟩ ∈ dom(I ′ ):

1)

I ′ = I 1 † ∨ I 2 is deterministic (Proposition 4.8); 2) eval(I ′ (t, q), []) =⇒ eval(I(t, q), M 1 † 2 M 2 ); 3) eval(I ′ (t, q), []) = ⊤ =⇒ eval(I ′ (t, q), M 1 ) = ⊤ ∧ eval(I ′ (t, q), M 2 ) = ⊤; 4) eval(I ′ (t, q), []) = ⊤ =⇒ eval(I 1 (t, q), M 1 ) ⊥ ∧ eval(I 2 (t, q), M 2 ) ⊥.
The first property ensures that merging two EHEs that incorporate memories are still indeed representing a deterministic and complete automaton, this follows from Proposition 4.8 and Proposition 4.11. Since operation † ∨ disjoins the two expressions, and since the two expressions come from EHEs that each maintain the property, the additional disjunction will not affect the outcome of eval. The second property extends Proposition 4.11 to the merging of EHE with incorporated memories. It follows directly from Proposition 4.11, and the assumptions that the memories have no conflicts. The third property adds a stronger condition. It states that merging two EHEs with incorporated memories results in an EHE that evaluates to true, cannot evaluate to anything else with the two different memories. This follows from the second property and the fact that the memories do not have conflicting observations. Finally, the fourth property ensures that merging an EHE with an entry that evaluates to ⊥ does not result in an entry that evaluates to ⊤. That is, if an EHE has already determined that a state is not reachable, merging it with another EHE does not result in the state being reachable. This ensures the consistency when sharing information. This property follows from the merging operator † ∨ which uses ∨ to merge entries in two EHEs. We recall that an entry in ⟨t, q⟩ ∈ dom(I ′ ) is constructed as: eval(I 1 (t, q), M 1 ) ∨ eval(I 2 (t, q), M 2 ). For eval(I ′ (t, q), []) to be ⊤, either eval(I 1 (t, q), M 1 ) or eval(I 2 (t, q), M 2 ) has to be ⊤, if one is already ⊥, then the other has to be ⊤. This leads to a contradiction, since both I 1 and I 2 encode the same deterministic automaton, as such, the automaton cannot be in two states at once. Example 4.13 (Reconciling information). We consider the specification presented in Example 2.1, and the decentralized trace and two components: lswitch and bulb presented in Example 3.14. We recall the trace tr

= [1 → lswitch → {⟨s, ⊤⟩}, 1 → bulb → {⟨ℓ, ⊤⟩}, 2 → lswitch → {⟨s, ⊤⟩}, 2 → bulb → {⟨ℓ, ⊥⟩}]
. Furthermore, we associate respectively two monitors m 0 and m 1 with components lswitch and bulb. We focus on the timestamp at t = 2. The monitors can observe the propositions s and ℓ respectively and use one EHE each: I 2 0 and I 2 1 respectively. Their memories are respectively ] and [M 2 1 ], the result of performing eval on the EHE † 2 ∨ using memories M 2 0 and M 2 1 respectively. A dash (-) indicates the expression is the same as I 2 .

M 2 0 = [⟨1, s⟩ → ⊤, ⟨1, s⟩ → ⊤] and M 2 1 = [⟨1, ℓ⟩ → ⊤, ⟨2, ℓ⟩ → ⊥].
t q I 2 I 2 0 I 2 1 † 2 ∨ [M 2 0 ] [M 2 1 ] 0 q 0 ⊤ ⊤ ⊤ ⊤ ⊤ ⊤ 1 q 0 ¬ ⟨1, s⟩ ⊥ - - ⊥ ? q 1 ⟨1, s⟩ ⊤ - ⊤ ⊤ ⊤ 2 q 0 ¬ ⟨1, s⟩ ∧ ¬ ⟨2, s⟩ ∨ ⟨1, s⟩ ∧ ¬ ⟨2, s⟩ ⊥ - - ⊥ ? q 1 ⟨1, s⟩ ∧ ⟨2, s⟩ ∧ ⟨2, ℓ ⟩ ∨ ¬ ⟨1, s⟩ ∧ ⟨2, s⟩ ⟨2, ℓ ⟩ ¬ ⟨1, s⟩ ∧ ⟨2, s⟩ ⟨2, ℓ ⟩ ∨ (¬ ⟨1, s⟩ ∧ ⟨2, s⟩) ? ? q 2 ⟨1, s⟩ ∧ ⟨2, s⟩ ∧¬ ⟨2, ℓ ⟩ ¬ ⟨2, ℓ ⟩ ⟨1, s⟩ ∧ ⟨2, s⟩ ¬ ⟨2, ℓ ⟩ ∨ ( ⟨1, s⟩ ∧ ⟨2, s⟩) ⊤ ⊤
the EHEs (where I 2 denotes the non-rewritten EHE). The columns

[M 2 0 ] and [M 2 1 ]
show the result of performing eval on the EHE † 2 ∨ using memories M 2 0 and M 2 1 respectively. Constructing the EHE I 2 follows similarly from Example 4.6. We show the rewriting for both I 2 0 and I 2 1 respectively in the next two columns. Then, we show the result of combining the rewrites using † ∨ . We notice initially that since s is ⊥, m 0 could evaluate ⟨1, s⟩ = ⊤ and know that the automaton is in state q 1 . However, for m 1 , this is not possible until the expressions are combined. By evaluating the combination, m 1 determines that the automaton is in state q 0 at t = 1. We see at t = 2 for both q 1 and q 2 the expression resulting from combining the EHE is much weaker than the one present in each of the individual EHEs. After evaluating with the local memory, both monitors determine that the automaton is in state q 2 .

In this case, we are only looking for expressions that evaluate to ⊤. We notice that monitor m 0 can determine that q 0 is not reachable (since ¬⟨1, s⟩ = ⊥) while m 1 cannot, as the expression ¬⟨1, s⟩ cannot yet be evaluated to a final verdict, and thus the combination evaluates to ?. This does not affect the outcome, as we are only looking for one expression that evaluates to ⊤, since both I 2 0 and I 2 1 are encoding the same execution. In the future, we would like to also propagate the information about the non-reachable states by tweaking the combination of EHEs.

DECENTRALIZED SPECIFICATIONS

In this section, we shift the focus to a specification that is decentralized. A set of automata represent various requirements (and dependencies) for different components of a system. In this section, we define the notion of a decentralized specification and its semantics, and in Section 6, we define various properties on such specifications.

Decentralizing a Specification

We recall that a decentralized system consists of a set of components C. To decentralize the specification, instead of having one automaton, we have a set of specification automata (Definition 4.1) Mons = {A ℓ | ℓ ∈ AP mons }, where AP mons ⊆ AP is a set of monitor labels. We refer to these automata as monitors. To each monitor, we associate a component using a function L : Mons → C. However, the transition labels of a monitor mon ∈ Mons are expressions restricted to either observations local to the component the monitor is attached to (i.e., L(mon)), or references to other monitors. Transitions are labeled over AP mons \ {mon} ∪ {ap ∈ AP \ AP mons | lu(ap) = L(mon)}. This ensures that the monitor is labeled with observations it can locally observe or depend on other monitors. To evaluate a trace as one would on a centralized specification, we require one of the monitors to be a starting point, we refer to that monitor as the root monitor (rt ∈ Mons).

q 0 start q 1 q 2 s ¬s ¬s s ∧ ℓ ⊤ s ∧ ¬ℓ (a) Centralized. q 0 start q 1 q 2 s ¬s ¬s s ∧ m 1 ⊤ s ∧ ¬m 1 q ′ 0 start q ′ 1 q ′ 2 ℓ ¬ℓ ⊤ ⊤ A m0 A m1 (b) Decentralized.
Definition 5.1 (Decentralized specification). A decentralized specification is a tuple ⟨AP mons , Mons, C, L, rt⟩.

We note that a centralized specification is a special case of a decentralized specification, with one component (global system, sys), and one monitor (g) attached to the sole component, i.e. ⟨{g}, {A g }, {sys}, [A g → sys], A g ⟩.

As automata expressions now include references to monitors, we first define function dep : Expr AP → Mons, which determines monitor dependencies. Then, we define the semantics of evaluating (decentralized) specifications with references. Function dep finds all monitors referenced by expression e, by syntactically traversing it.

Example 5.3 (Decentralized specification). Figure 3b shows a decentralized light switch and bulb specification corresponding to the centralized specification in Example 2.1 (shown in Figure 3a for side-by-side comparison). We recall from Example 3.14 that the system consists of two components the light switch and bulb, labeled lswitch and bulb, respectively. We associated the components lswitch and bulb with the monitors A m 0 and A m 1 , respectively. We use A m 0 as the root monitor for the decentralized specification. We consider the two atomic propositions s and ℓ can only be observed by component lswitch and bulb respectively. A m 0 depends on the verdict from m 1 and only observations local to lswitch, while A m 1 is only labeled with observations local to bulb. Given the expression s ∧ m 1 , we have dep(s ∧ m 1 ) = {A m 1 }.

Semantics of a Decentralized Specification

The transition function of the decentralized specification is similar to the centralized automaton with the exception of monitor ids. Definition 5.4 (Semantics of a decentralized specification). Consider the root monitor A rt and a decentralized trace tr with index i ∈ [1, |tr|] representing the timestamps. Monitoring tr starting from A rt emits the verdict ver rt (∆ ′ * rt (q rt 0 , tr, 1)) where for a given monitor label ℓ:

∆ ′ * ℓ (q, tr, i) = ∆ ′ * ℓ (∆ ′ ℓ (q, tr, i), tr, i + 1) if i < |tr| ∆ ′ ℓ (q, tr, i) otherwise ∆ ′ ℓ (q, tr, i) = q ′ if tr(i, L(A ℓ )) ∅ ∧ ∃e ∈ Expr AP : δ ℓ (q, e) = q ′ ∧ eval(idt(e), M) = ⊤ q otherwise where M = memc(tr(i, L(A ℓ )), idt) † 2 2 A ℓ ′ ∈dep(e) {[ℓ ′ → ver ℓ ′ (q ℓ ′ f )]} and q ℓ ′ f = ∆ ′ * ℓ ′ (q ℓ ′ 0 , tr, i)
For a monitor A ℓ , we determine the new state of the automaton starting at q ∈ Q ℓ , and running the trace tr from timestamp i to timestamp t by applying ∆ ′ * ℓ (q, tr, i). To do so, we evaluate one transition at a time using ∆ ′ ℓ as would ∆ * ℓ with ∆ ℓ (see Definition 4.2). To evaluate ∆ ′ ℓ at any state q ′ ∈ Q ℓ , 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, L(A ℓ )), idt) which is based on the event with observations local to the component the monitor is attached to (i.e., L(A ℓ )). However, for monitor ids, the memory represents the verdicts of the monitors. To evaluate each reference ℓ ′ in the expression, the remainder of the trace starting from the current event timestamp i is evaluated recursively on the automaton A ℓ ′ from the initial state q ℓ ′ 0 ∈ A ℓ ′ . Then, the verdict of the monitor is associated with ℓ ′ in the memory. Example 5.5 (Monitoring of a decentralized specification). We consider the decentralized specification from Example 5.3. We have the monitors A m 0 (root) and A m 1 associated to components lswitch and bulb respectively. Furthermore, we consider the decentralized trace from Example 3.14: tr =

[1 → lswitch → {⟨s, ⊤⟩}, 1 → bulb → {⟨ℓ, ⊤⟩}, 2 → lswitch → {⟨s, ⊤⟩}, 2 → bulb → {⟨ℓ, ⊥⟩}].
To evaluate tr on A m 0 (from Figure 3b), we use ∆ ′ * m 0 (q 0 , tr, 1). To do so, we first evaluate ∆ ′ m 0 (q 0 , tr, 1). In this case, the expressions only depend on the atomic proposition s, which does not depend on any other monitor. We have M 1 m 0 = memc(⟨s, ⊤⟩, idt) = [s → ⊤], and eval(s, M 1 m 0 ) = ⊤. Thus, we obtain ∆ ′ m 0 (q 0 , tr, 1) = q 1 . In q 1 at t = 2, we now evaluate ∆ ′ m 0 (q 1 , tr, 2). Transitions from q 1 are labeled with expressions that depend on m 1 . Therefore, we evaluate the decentralized trace on A m 1 starting at t = 2 by evaluating ∆ ′ * m 1 (q ′ 0 , tr, 2). We start by evaluating ∆ ′ m 1 (q ′ 0 , tr, 2). We have

M 2 m 1 = memc(⟨ℓ, ⊥⟩, idt) = [ℓ → ⊥],
and eval(¬ℓ, M 2 m 1 ) = ⊤. Thus, we obtain ∆ ′ m 1 (q ′ 0 , tr, 2) = q ′ 2 labeled by the verdict ⊥. Having reached a final verdict for m 1 , we can construct the memory for m 0 . We have

M 2 m 0 = memc(⟨s, ⊤⟩, idt) † 2 [m 1 → ⊥] = [s → ⊤, m 1 → ⊥]. Knowing that eval(s ∧ ¬m 1 , M 2 m 0 ) = ⊤, we conclude that the next state is ∆ ′ m 0 (q 1 , tr, 2) = q 2 .
Since q 2 is labeled by verdict ⊥, the monitoring concludes and we detect a violation of the specification.

PROPERTIES FOR DECENTRALIZED SPECIFICATIONS

A key advantage of using decentralized specifications is to make the association of monitors with components explicit. Since monitors have been explicitly modeled as a set of automata with dependencies between each other, we can now determine properties on decentralized specifications. In this section, we revisit the concept of monitorability, characterize it for automata, define it for decentralized specifications, and describe an algorithm for deciding monitorability. Furthermore, we explore compatibility, that is the ability of a decentralized specification to be deployed on a given architecture. q 0 ⊤ Fig. 4. A trivial non-monitorable specification.

Decentralized Monitorability

An important notion to consider when dealing with runtime verification is that of monitorability [START_REF] Falcone | You Should Better Enforce Than Verify[END_REF][START_REF] Pnueli | PSL Model Checking and Run-Time Verification Via Testers[END_REF]. In brief, monitorability of a specification determines whether or not an RV technique is applicable to a specification. That is, a monitor synthesized for a non-monitorable specification is unable to check if the execution complies or violates the specification for all possible traces. Consider the automaton shown in Figure 4, one could see that there is no state labeled with a final verdict. In this case, we can trivially see that no trace allows us to reach a final verdict. We also notice similar behavior when monitoring LTL expressions with the pattern GF(p) with p is an atomic proposition. The LTL expression requires that at all times F(p) holds ⊤, while F(p) requires that p eventually holds ⊤. As such, at any given point of time, we are unable to determine a verdict, since if p is ⊥ at the current timestamp, it can still be ⊤ at a future timestamp, and thus F(p) will be ⊤ for the current timestamp. And if F(p) is ⊤ at the current timestamp, the G requires that it be ⊤ for all timestamps, so in the future there could exist a timestamp which falsifies it. Consequently, when monitoring such an expression, a monitor will always output ?, as it cannot determine a verdict for any given timestamp. In this section, we first characterize monitorability in terms of automata and EHE for both centralized and decentralized specifications. Then, we provide an effective algorithm to determine monitorability.

Characterizing Monitorability.

Centralized monitorability of properties. Monitorability in the sense of [START_REF] Pnueli | PSL Model Checking and Run-Time Verification Via Testers[END_REF] is defined on traces. A property is monitorable if for all finite traces t (a sequence of events) in the set of all (possibly infinite) traces, there exists a continuation t ′ such that monitoring t • t ′ results in a true or false verdict. Informally, it can be seen as whether or not continuing to monitor the property after reading t can still yield a final verdict. We note that this definition deals with all possible traces, it establishes monitorability to be oblivious of the input trace.

Centralized monitorability in automata. We express monitorability to reach "true" or "false" verdict to the notion of reaching a final verdict, and associate it with automata. For automata, monitorability can be analyzed in terms of reachability and states. Definition 6.1 (Monitorability of an automaton). Given a automaton A = ⟨Q, q 0 ∈ Q, δ, ver⟩, a state q ∈ Q is monitorable (noted monitorable(q)) iff ver(q ′ ) ∈ B 2 or ∃q ′ ∈ Q such that ver(q ′ ) ∈ B 2 and q ′ is reachable from q. Automaton A is said to be monitorable (noted monitorable(A)) iff ∀q ∈ Q : monitorable(q). Defining monitorability using reachability is consistent with [START_REF] Pnueli | PSL Model Checking and Run-Time Verification Via Testers[END_REF]. After reading a finite trace t and reaching q (q = ∆ * (q 0 , t)), there exists a continuation t ′ that leads the automaton to a state q ′ (q ′ = ∆ * (q, t ′ )), such that ver(q ′ ) ∈ B 2 . We note that an automaton is monitorable according to this definition iff, in the automaton, all paths from the initial state q 0 lead to a state with a final verdict. As such, it is sufficient to analyze the automaton to determine monitorability irrespective of possible traces (see Section 6.1.2) 12 . We illustrate monitorability of automata in Example 6.2. Example 6.2 (Centralized monitorability of automata.). Figure 3a illustrates the automaton that expresses the light switch and bulb specification. It is monitorable, as the states q 0 , q 1 , and q 2 are On the Monitoring of Decentralized Specifications :21 monitorable. For both q 0 and q 1 , it is possible to reach q 2 labeled with the final verdict ⊥. We note that monitorability is a necessary but not sufficient condition for termination (with a final verdict). An infinite trace consisting of repetitions of the event {¬⟨s, ⊥⟩, ⟨ℓ, ⊥⟩} never lets the automaton reach q 2 . However, monitorability guarantees the possibility of reaching a final verdict. If a state q is not monitorable, we know that it is impossible to reach a final verdict from q, and can abandon monitoring.

Centralized monitorability with EHE. Reachability in automata can be expressed as well using the EHE data structure. A path from a state q to a state q ′ is expressed as an expression over atoms. We define paths(q, q ′ ) to return all possible paths from q to q ′ . paths(q, q ′ ) = {e ∈ Expr Atoms | ∃t ∈ N :

I t (t, q ′ ) = e ∧ I t = mov([0 → q → ⊤], 0, t)}
Each expression is derived similarly as would an execution in the EHE (Definition 4.4). We start from state q and use a logical timestamp starting at 0 incrementing it by 1 for the next reachable state. A state q is monitorable iff ∃e f ∈ paths(q, q f ), such that (1) e f is satisfiable; (2) ver(simplify(e f )) ∈ B 2 . The first condition ensures that the path is able to lead to the state q f , as an unsatisfiable path will never evaluate to true. The second condition ensures that the state is labeled by a final verdict. An automaton is thus monitorable iff all its states are monitorable. We note that paths(q, q ′ ) can be infinite if the automaton contains cycles, however path expressions could be "compacted" using the pumping lemma. Using EHE we can frame monitorability as a satisfiability problem which can benefit from additional knowledge on the truth values of atomic propositions. For the scope of this paper, we focus on computing monitorability on automata in Section 6.1.2.

Decentralized monitorability. In the decentralized setting, we have a set of monitors Mons. The labels of automata include monitor ids (AP mons ). We recall that the evaluation of a reference ℓ ∈ AP mons consists in running the remainder of the trace on A ℓ starting from the initial state q ℓ 0 . As such, for any dependency on a monitor A ℓ , we know that ℓ evaluates to a final verdict iff monitorable(A ℓ ). We notice that monitorability of decentralized specification is recursive, and relies on the inter-dependencies between the various decentralized specifications. This is straightforward for EHE, since a path is an expression. For a path e f , the dependent monitors are captured in the set dep(e f ). The additional condition on the path is thus: ∀A ℓ ∈ dep(e f ) : monitorable(A ℓ ).

Computing Monitorability.

Centralized specification. We compute the monitorability of a centralized specification A, with respect to a set of final verdicts B 2 13 . We denote monitorability by monitorable(A, B 2 ). In the remainder of the thesis we always use B 2 , thus, we write monitorable(A). Computing monitorability consists in checking that all states of the automaton are co-reachable from states with final verdicts. As such, it relies on a traversal of the graph starting from the states that are labeled with final verdicts. To do so, we use a variation of the work-list algorithm. We begin by adding all states labeled by a final verdict to the work list. These states are trivially monitorable. Conversely, any state that leads to a monitorable state is monitorable. As such, for each element in the work list, we add its predecessors to the work list. We maintain a set of marked states (Mark), that is, states that have already been processed, so as to avoid adding them again. This ensures that cycles are properly handled. The algorithm stabilizes when no further states can be processed (i.e., the work list is empty). All marked states (Mark) are therefore monitorable. To check if an automaton is monitorable, we need all of its states to be monitorable. As such we verify that |Mark| = |Q |. The number of edges between any pair of states can be rewritten to be at most 1 (as explained in Section 4.1). As such, one has to traverse the graph once, the complexity being linear in the states and edges (i. ). Decentralized specifications. In the case of decentralized specifications, the evaluation of paths (using eval) in an automaton depends on other monitors (and thus other automata). To compute monitorability, we first build the monitor dependency set for a given monitor A ℓ (noted MDS(A ℓ )) associated with a monitor label ℓ.

MDS(A

ℓ ) = {e ∈Expr AP | ∃q,q ′ ∈Q ℓ : δ ℓ (q,e)=q ′ } dep(e)
The monitor dependency list for a monitor contains all the references to other monitors across all paths in the given automaton (A ℓ ), by examining all the transitions. It can be obtained by a simple traversal of the automaton.

Second, we construct the monitor dependency graph (MDG), which describes the dependencies between monitors. The monitor dependency graph for a set of monitors Mons is noted MDG(Mons) = ⟨Mons, DE⟩ where DE is the set of edges which denotes the dependency edges between the monitors, defined as:

DE = {⟨A ℓ , A ℓ ′ ⟩ ∈ Mons×Mons | A ℓ ′ ∈ MDS(A ℓ )}.
A monitor A m i depends on another monitor A m j iff m j appears in the expressions on the transitions of A m i . Proposition 6.3 (Sufficient conditions for monitorability of decentralized specifications.). A decentralized specification is monitorable if the two following conditions are met: (i) MDG(Mons) has no cycles; and (ii) ∀ℓ ∈ Mons : monitorable(A ℓ ).

The first condition ensures that no cyclical dependency exists between monitors. The second condition ensures that all monitors are individually monitorable. We note, that both conditions are decidable. Furthermore, detecting cycles in a graph can be done in linear time with respect to the sum of nodes and edges, by doing a depth-first traversal with back-edge detection, or by finding strongly connected components [START_REF] Endre | Depth-First Search and Linear Graph Algorithms[END_REF]. Thus, in worst case, it is quadratic in |Mons|. Monitorability is therefore quadratic in the number of monitors and states in the largest automaton. Example 6.4 (Decentralized monitorability of decentralized specifications.). We consider the decentralized counterpart of the light switch and bulb presented in Example 6.2. The decentralized specification is shown in Figure 3b, it introduces two monitors A m 0 and A m 1 . The set of monitors is Mons def = {A m 0 , A m 1 }. We compute the monitor dependency sets for each monitor. We have MDS(

A m 0 ) = dep(⊤) ∪ dep(s) ∪ dep(¬s) ∪ dep(s ∧ m 1 ) ∪ dep(s ∧ ¬m 1 ) = {A m 1 }, and MDS(A m 1 ) = dep(⊤) ∪ dep(ℓ) ∪ dep(¬ℓ) = ∅.
Using the monitor dependency sets, we construct the monitor dependency graph: MDG(Mons) = ⟨Mons, {⟨A m 0 , A m 1 ⟩}⟩. The monitor dependency graph has no cycles, as it contains only one edge indicating the dependency of A m 0 on A m 1 .

We now verify the monitorability of each monitor separately using centralized monitorability. Both A m 0 and A m 1 are monitorable as the states q 2 and q ′ 1 or q ′ 2 are reachable from all states. The requirement for no cycles is sufficient but not necessary, it is possible for certain cycles to exist while the decentralized specification is still able to reach a final verdict. This stems from the fact that boolean expressions may cancel out the dependency, or dependencies can be on different timestamps (i.e., future transitions in the automaton). We illustrate a monitorable decentralized specification in Fiдure 5 with two monitors that depend on each other. Regardless of the choice of the root monitor, it is possible to still avoid the dependency if one operands of the disjunction

q 0 start q 1 q ′ 0 start q ′ 1 m 1 ∨ b ¬(m 1 ∨ b) ⊤ a ∨ m 0 ¬(a ∨ m 0 ) ⊤ A m0 A m1
Fig. 5. A monitorable decentralized specification with cyclically dependent monitors. When observing ⟨a, ⊤⟩, and ⟨b, ⊤⟩, the disjunction cancels out the dependency.

holds true. That is, if we observe ⟨a, ⊤⟩ then it is no longer necessary to evaluate m 0 , and no real dependency exists.

Compatibility

A key advantage of decentralized specifications is the ability to associate monitors to components. This allows us to associate the monitor network with the actual system architecture constraints.

The monitor network is a graph N = ⟨Mons, E⟩, where Mons is the set of monitors, and E representing the communication edges between monitors. The monitor network is typically generated by a monitoring algorithm during its setup phase (See Section 7.2). For example, N could be obtained using the construction MDG(Mons) presented in Section 6.1.2. The system is represented as another graph S = ⟨C, E ′ ⟩, where C is the set of components, and E ′ is the set of communication channels between components.

Defining compatibility. We now consider checking for compatibility. Compatibility denotes whether a monitoring network can be actually deployed on the system. That is, it ensures that communication between monitors is possible when those are deployed on the components. We first consider the reachability in both the system and monitor graphs as the relations reach S : C → 2 C , and reach M : Mons → 2 Mons , respectively. Second, we recall that a monitor may depend on other monitors and also on observations local to a component. If a monitor depends on local observations, then it provides us with constraints on where it should be placed. We identify those constraints using the partial function cdep : Mons → C. We can now formally define compatibility. Compatibility is the problem of deciding whether or not there exists a compatible assignment. Definition 6.5 (Compatible assignment). A compatible assignment is a function compat : Mons → C that assigns monitors to components while preserving the following properties:

1) ∀m 1 , m 2 ∈ Mons : m 2 ∈ reach M (m 1 ) =⇒ compat(m 2 ) ∈ reach S (compat(m 1 )); 2) ∀m ∈ dom(cdep) : cdep(m) = compat(m).
The first proposition ensures that reachability is preserved. That is, it ensures that if a monitor m 1 communicates with another monitor m 2 (i.e. m 2 ∈ reach M (m 1 )), then m 2 must be placed on a component reachable from where m 1 is placed (i.e. compat(m 2 ) ∈ reach S (compat(m 1 ))). The second proposition ensures that dependencies on local observations are preserved. That is, if a monitor m depends on local observations from a component c ∈ C (i.e. cdep(m) = c), then m must be placed on c (i.e. cdep(m) = compat(m)).

Computing compatibility. We next consider the problem of finding a compatible assignment of monitors to components. Algorithm 1 finds a compatible assignment for a given monitor network (⟨Mons, E⟩), system (⟨C, E ′ ⟩), and an initial assignment of monitors to components (cdep). The algorithm can be broken into three procedures: procedure verifyCompatible verifies that a (partial) assignment of monitors to components is compatible, procedure compatibleProc takes as input a set of monitors that need to be assigned and explores the search space (by iterating over components), and finally, procedure compatible performs necessary pre-computation of reachability, verifies that the constraint is first compatible, and starts the search.

We verify that an assignment of monitors to components (s : Mons → C) is compatible using algorithm verifyCompatible (Lines 1-8). We consider each assigned monitor (m ∈ dom(s)). Then, we constrain the set of reachable monitors from m to those which have been assigned a component (M ′ = reach M (m) ∩ dom(s)). Using M ′ , we construct a new set of components using s (i.e., C ′ = {s(m ′ ) ∈ C | m ′ ∈ M ′ }). Set C ′ represents the components on which reachable monitors have been placed. Finally, we verify that the components in the set C ′ are reachable from where we placed m (i.e., C ′ ⊆ reach S (s(m))). If that is not the case, then the assignment is not compatible (Line 4). To iterate over all the search space, that is, all possible assignments of monitors to components, procedure compatibleProc (Lines 9-24) considers a set of monitors to assign (M), selects a monitor m ∈ M (Line 13), and iterates over all possible components, verifying that the assignment is compatible (Lines 14 -22). If the assignment is compatible, it iterates over the remainder of the monitors (i.e., M \ {m}), until it is empty (Line 16). If the assignment is not compatible, it discards it and proceeds with another component. For each monitor we seek to find at least one compatible assignment. One can see that the procedure eventually halts (as we exhaust all the monitors to assign), and is affected exponentially based on the number of monitors to assign |Mons \ dom(cdep)| (Line 31) with a branching factor determined by the possible values to assign (|C|, Line 14). It is important to note that the number of monitors to assign is in practice particularly small. The number of monitors to assign includes monitors that depend only on other monitors and not local observations from components, as the dependency on local observations requires that a monitor be placed on a given component (that is, it will be in dom(cdep)).

Example 6.6 (Compatibility). Figure 6 presents a simple network of 3 monitors, and a system graph of 4 components. We consider the following constraint: cdep = [m 0 → c 0 , m 2 → c 2 ]. For compatibility, we must first verify that cdep is indeed a compatible (partial) assignment, then consider placing m 1 on any of the components (i.e., both properties of Definition 6.5). Procedure compatible computes the set of reachable nodes for both the monitor network and the system. They are presented in Figure 6c and Figure 6d, respectively. We then proceed with line 28 to verify the constraint (cdep) using procedure verifyCompatible. We consider both m 0 and m 2 . For m 0 (resp. m 2 ) we generate the set (Line 3) {c 0 } (resp. {c 2 }), and verify that it is indeed a subset of reach S (c 0 ) (resp. reach S (c 2 )). This ensures that the constraint is compatible. We then proceed to place m 1 by calling compatibleProc(cdep, {m 1 }, {c 0 , c 1 , c 2 , c 3 }, reach M , reach S ). While procedure compatibleProc will attempt all components, we will consider for the example placing m 1 on c 1 . On line 15, the partial function s ′ will be cdep † 2 [m 1 → c 1 ]. We now call verifyCompatible to verify s ′ . We consider both m 0 , m 1 , and m 2 . For m 0 (resp. m 1 , m 2 ) we generate the set {c 0 , c 1 } (resp. {c 1 }, {c 2 , c 1 }). We notice that for m 0 , {c 0 , c 1 } is indeed a subset of reach S (c 0 ). This means that m 0 is able to communicate with m 1 . However, it is not the case for m 2 , the set {c 2 , c 1 } is not a subset of reach S (c 2 ) = {c 2 , c 3 }. The monitor m 2 will not be able to communicate with m 1 if m 1 is placed on c 1 . Therefore, assigning m 1 to c 1 is incompatible. Example of compatible assignments for m 1 are c 2 and c 3 as both of those components are reachable from c 2 . Procedure compatibleProc continues by checking other components, and upon reaching c 2 or c 3 stops and returns that there is at least one compatible assignment. Therefore, the monitor network (Figure 6a) is compatible with the system (Figure 6b).

ANALYSIS

We aim to compare decentralized monitoring algorithms in terms of computation, communication, and memory overhead. Since the EHE and memory datastructures are used to abstract the behavior of a monitoring algorithm. We first consider the parameters and the cost for the basic functions of the EHE and memory data structures in Section 7.1. We use s E to denote the size necessary to encode an element of the set E. For example, s AP is the size needed to encode an element of set AP. Then, in Section 7.2, we elaborate on the general phases of decentralized monitoring algorithms and illustrate the approach to analyze them by adapting algorithms from [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF] as examples.

m 1 m 0 m 2 (a) Monitor network. c 0 c 1 c 2 c 3 (b) System. m 0 {m 0 , m 1 } m 1 {m 1 } m 2 {m 2 , m 1 } (c) reach M . c 0 {c 0 , c 1 , c 2 , c 3 } c 1 {c 1 , c 2 , c 3 } c 2 {c 2 , c 3 } c 3 {c 3 } (d) reach S .

Data Structure Costs

We consider the cost of using a memory or an EHE. To do so, we first address the cost to store partial functions and merge them.

7.1.1 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 all x = f (x) mappings. We recall that | dom(f )| the number of entries in f . The size of each mapping x = f (x) is the sum of the

sizes |x | + | f (x)|. Therefore | f | = x ∈dom(f ) |x | + | f (x)|.
7.1.2 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 † op д, we first iterate over each x ∈ dom(f ), check whether x ∈ dom(д), and if so assign op(f (x), д(x)), otherwise assign f (x). Finally we assign д(x)

to any x ∈ dom(д) ∩ dom(f ). This results in | dom(f † op д)| = | dom(f ) ∪ dom(д)| which is at most | dom(f )| + | dom(д)|.

Information delay.

The main goal of the EHE data structure is to keep track of partial states of an automaton execution. Keeping track of partial states becomes unnecessary once enough information is gathered to determine which state was reached during an execution. An EHE associates an expression with a state for any given timestamp. When an expression e associated with a state q kn for some timestamp t kn is evaluated to ⊤, we know that the automaton is in q kn at t kn . We call q kn a 'known' state. The information delay δ t is the number of timestamps needed to reach a new known state from an existing known state. That is, it is the number of timestamps in the EHE storing partial information without determining a known state. Information delay is a runtime measure, as it depends on the updates done to the EHE as it evolves with time. Given an EHE at timestamp t kn such that q kn is a known state for a given memory M t kn i.e. sel(I t kn , M t kn , t kn ) = q kn . The next known timestamp is the least timestamp t newkn > t kn , such that sel(I t newkn , M t newkn , t newkn ) undef, where I t and M t at some timestamp t are used to denote respectively the changes to the EHE and memory through time in the execution 14 . The information delay for this evaluation of a state is δ t = t newkn -t kn . While information delay needs to be computed each time a known state is reached, it is often the case that it is measured for a whole execution of an algorithm, in which case we can consider an average information delay and a maximum information delay, where we aggregate the various information delays (for reaching each known state) by computing their average and maximum. Since we know the automaton is in q newkn , prior information is no longer necessary, therefore it is possible to discard all entries in I with t < t newkn . Thus, it reduces the number of expressions in the EHE. 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. We next show how the information delay parameter affects the size of the EHE.

EHE Encoding.

For the EHE data structure, we consider the three functions: mov, eval, and sel 15 (see Section 4.2). Function mov depends on the topology of the automaton. We quantify it using the maximum size of the expression that labels a transition in a normalized automaton L (see Remark 1), and the number of states in the automaton (|Q |). From a known state, each application of 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 per On the Monitoring of Decentralized Specifications :27

t → q → ⊤ δ t                                                            t + 1 → q 0 → e 10 q 1
→ e 11 . . .

q |Q |-1 → e 1(|Q |-1)                  |Q | t + 2 → q 0 → e 20 . . . q |Q |-1 → e 2(|Q |-1)          |Q | . . . t + δ t → q 0 → e δt 0 q 1 → e δt 1 . . . q |Q |-1 → e δt (|Q |-1)                |Q | Fig. 7
. Size of the EHE (worst-case) with respect to information delay.

outbound state for each move beyond t kn . We illustrate the expansion in Figure 7, where for each timestamp, we associated an expression with each state. We use S(t) to denote the size of an expression at t timestamps after a known state. As such to reach a given state, we require a previous expression (i.e., S(t -1)), and add the label of a given transition (of maximum size L). In the worst-case, the automaton is a fully connected graph, a state can be reached by all other states (including itself). Hence, we require the disjunction of |Q | such expressions. The recurrence relation is given by: S(t) = |Q | × (S(t -1) + L). S(t) is thus a geometric series of ratio strictly greater than 1. There is a unique expression at a known time stamp and the size of such expression is 1 (since the expression is ⊤). We can then deduce that the size of the expression is exponential in the number of timestamps. An EHE contains δ t × |Q | expressions. In the worst case, its total size is exponential in the number of states. For δ t ≥ 1, we have:

|I δ t | = |Q | × δ t × 1 - L 1 -|Q | × 1 -|Q | δ t 1 -|Q | + δ t × L 1 -|Q | = Θ |Q | δ t -1
For a given expression e, we use |e| to denote the size of e, i.e., the number of atoms in e. Given a memory M, the complexity of function eval(e, M) is the cost of simplify(rw(e, M)). Function rw(e, M) looks up each atom in e 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 e. It effectively takes one pass to syntactically replace all atoms by their values, therefore the cost of rw is Θ(|e|). However, applying function 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. |e| is bounded by δ t × L. 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 . 7.1.5 Memory. The memory required to store M depends on the trace, namely the amount of observations per component. Recall 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 ).
The size of the memory depends for each timestamp on the number of observations associated with the component (|tr(c, t)|), and the size of each observation. The size of an observation is the size needed to encode the timestamp (s N ), the atomic proposition (s AP ) and the verdict (s B 2 ).

Analyzing Existing Algorithms

We now shift the focus to the algorithms and their usage of the data structures. We first present an overview of the abstract phases performed by decentralized monitoring algorithms. We then elaborate on our approach to model their behavior. Finally, as an example, we present the analysis for each of the algorithms adapted from [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF]: Orchestration (Orch), Migration (Migr), and Choreography (Chor). The algorithms contain both multiple monitors monitoring the same specification (Orch, and Migr), and a decentralization algorithm which splits one global specification to multiple subspecifications distributed on monitors (Chor). We later explore the trends provided by the analysis by benchmarking in Section 9.

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 (see Section 7.1) . 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 × L). 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. 7.2.3 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 a message is linear in the number of observations for the component, for a forwarding monitor labeled with m k , the size of the message is |tr(t, c k )| × (s N × s AP × s B 2 ). 7.2.4 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 function choose, which determines which component to migrate to next upon evaluation. By using a simple function 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 Migr by the number of active monitors at a timestamp m. The presented function choose in [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF], selects at most one other component to migrate to. Therefore, after the initial choice of m, subsequent rounds can have at most m active monitors.

We illustrate Migr in Algorithm 2. The state of a migration monitor consists of a variable isActive that determines whether or not the monitor is active, and I that is an EHE encoding the same automaton shared by all monitors. At each round the monitor receives a timestamp t and a set of observations o. Line 2 displays the memory update with observations for that round. Lines 3 to 9 describe the reception of EHEs from other monitors. Upon receiving an EHE, the monitor state is set to active (Line 7). An active monitor will then update its EHE by first ensuring that it is expanded to the current timestamp using mov (Line 11), then rewriting and evaluating each entry (Lines 12-17). The number of entries in the EHE depends on δ t . If any of the entries is evaluated to a final verdict (Line 14), then the verdict is found and we terminate. While the verdict is not found, the migration algorithm first removes all unnecessary entries in the EHE (Line 18). Unnecessary entries are entries for which the state is known, the last known state is only kept, all previous timestamps are removed. After removing unnecessary entries, we determine a new monitor to continue monitoring using the function choose (Lines [START_REF] Diekert | Topology, monitorable properties and runtime verification[END_REF][START_REF] Diekert | On Distributed Monitoring of Asynchronous Systems[END_REF][START_REF] Duret-Lutz | Manipulating LTL formulas using Spot 1.0[END_REF][START_REF] Matthew | Patterns in Property Specifications for Finite-State Verification[END_REF]. 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. In the worst case, the upper bound on the size of EHE is exponential in δ t , and thus, it is exponential in the number of components. 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. 7.2.5 Choreography. Choreography (Chor) presented in [START_REF] Colombo | Organising LTL Monitors over Distributed Systems with a Global Clock[END_REF][START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF] splits the initial LTL formula into subformulas and delegates each subformula to a component. Thus Chor can illustrate how it is possible to monitor decentralized specifications. Once the subformulas are determined by splitting the main formula 16 , 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 leaves consisting of monitors without any dependencies, and dependencies building up throughout the tree to reach the main monitor that outputs the verdict. Since each monitor is in charge of evaluating a subformula, the monitors communicate the evaluation of the

23:

end if

24: end procedure formula as a verdict B 2 when it is resolved. Furthermore, monitors may instruct other monitors to stop monitoring as they are no longer necessary. The two messages are referred to as msg ver and msg kill , respectively. For each monitor labeled ℓ ∈ AP mons we determine the set coref ℓ ∈ 2 AP mons which contains the labels of monitors that send their verdicts to monitor A ℓ . The information delay for a monitor is thus dependent on its depth in the network tree. The depth of a monitor labeled ℓ that depends on the set of monitors coref ℓ , is computed recursively as follows:

depth(ℓ) =          1 if monitorable(A ℓ ) ∧ coref ℓ = ∅, 1 + max({depth(ℓ ′ ) | ℓ ′ ∈ coref ℓ }) if monitorable(A ℓ ) ∧ coref ℓ ∅, ∞ otherwise,
A monitor synthesized from a non-monitorable specification will never emit a verdict, therefore its depth is ∞. A leaf monitor has no dependencies, its depth is 1. Since the depth controls the information delay (δ t ), it is possible in the case of choreography to obtain a large EHE depending on the specification. In effect, the worst case the size of the EHE can be linear in the size of the trace δ t = |tr|, as it will be required to store the EHE until the end of the trace. As such properties of the specification such as monitorability (see Section 6.1) impact greatly the delay, and thus performance.

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 of msg ver , or only the size needed to encode an id in the case of msg kill .

7.2.6 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

Migration O(|C|) O(m) Θ(|Q | | C |-2 ) Choreography O(depth(rt) + |tr|) Θ(|E|) Θ(1)
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. Since we perform a worst-case analysis, we investigate the trends shown in Section 9 by simulating the behavior of the algorithms on a benchmark consisting of randomly generated specifications and traces. Furthermore, we use a real example in Section 9.2 to refine the comparison by looking at six different specifications.

THE THEMIS FRAMEWORK

THEMIS is a framework to facilitate the design, development, and analysis of decentralized monitoring algorithms; developed using Java and AspectJ [START_REF] Kiczales | An Overview of AspectJ[END_REF] (∼5700 LOC). 17 It consists of a library and command-line tools. The library provides all necessary building blocks to develop, simulate, instrument, and execute 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 effort required to design and assess 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 18 . After running a single run or an experiment, the metrics are stored in a database for postmortem analysis. These can be queried, merged or plotted easily using third-party tools. After completing the analysis, algorithms and metrics can be tuned so as to refine the design as necessary.

The THEMIS framework has been improved since [START_REF] El | Monitoring Decentralized Specifications[END_REF][START_REF] El | THEMIS: A Tool for Decentralized Monitoring Algorithms[END_REF] to support fully distributed and multithreaded for monitoring by adding the tool Node that acts as a runtime. One or more nodes can be deployed on a given platform. A node receives information (via commands) to deploy components, and monitors on the current platform. Each component contains one or multiple peripheries. A periphery is an input stream to the component, that generates observations. Peripheries follow a stream interface, and waits on a next() call to generate the next observations. Monitors are attached to components, and receive the observations that components receive. Thus, a node follows a publish-subscribe model. Components can be seen as topics, where a monitor registers to a topic. Peripheries produce a stream of observations for components. Peripheries can include reading traces from files, over network sockets, or be generated in a stream. Nodes can communicate with other nodes in a distributed manner, through sockets. The implementation of a node defines the high level assumptions of monitoring, for example, our round-based monitoring approach is implemented as a node. For our implementation of a node, reading peripheries to generate component observations is done in parallel. Once all peripheries have executed their next() call to read the next events on the stream, the observations are aggregated in an event that is sent to monitors associated with the component. Monitors execute in parallel, once all monitors have completed for a given round, the next round begins. This behavior could be altered to ignore rounds, and simply monitor as soon as information is available by using a different node implementation. Measures have been updated to be thread-safe and work at the node-level.

Furthermore, the simplification logic (operation eval) for the data structure EHE has been greatly improved to call the simplifier less and be more aggressive with the simplifications. This yields on average, a much smaller EHE, more details are provided in Appendix C.

COMPARING ALGORITHMS WITH THEMIS

We use THEMIS to compare the adapted versions of existing algorithms (Orch, Migr, and Chor), introduced as examples to validate the trends presented in the analysis in Section 7. Furthermore, since the analysis presented worst-case scenarios, we look at the usefulness of simulations to determine the advantages or disadvantages of certain algorithms in specific scenarios. The THEMIS tool, the data for both scenarios used in this paper, the scripts used to process the data, and the full documentation for reproducing the experiments is found at [START_REF] El | THEMIS Article Artifact[END_REF].

Overview of scenarios. 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 heuristic (function choose). We compare the algorithms under two scenarios. The first scenario explores synthetic benchmarks, that is, we consider random traces and specifications. This allows us to account for different types of behavior. The second scenario explores a specific example associated with a common pattern in programming. For that, we consider a publish-subscribe system, where multiple publishers subscribe to a channel (or topic), the channel publishes events to the subscribers. We use the Chiron user interface example [START_REF] Avrunin | Comparing Finite-State Verification Techniques for Concurrent Software[END_REF][START_REF]Chiron User Interface[END_REF], along with the specifications formalized for it [START_REF] Matthew | Patterns in Property Specifications for Finite-State Verification[END_REF].

Monitoring metrics. The first considered metric is that of information delay (δ t ) (Section 7.1). The information delay 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. To compute the average information delay (average delay), we first consider the timestamp difference when an EHE is resolved (i.e., it indicates a state). We sum these differences across the entire run and count the number of resolutions. As such, we acquire the average number of timestamps stored in an EHE. We notice that it is possible for delay to fall below 1, as some traces can cause some monitors to emit a verdict at the very first timestamp. By considering our analysis in Section 7, we split our metrics into two main categories: computation and communication. The EHE structure requires the evaluation and simplification of a Boolean expression which is costly (see Section 4.2). To measure computation, we can count the number of expressions evaluated (using memory lookup), and the number of calls to the simplifier. For this experiment we consider the calls to the simplifier. Since algorithms may have more than one monitor active, we consider for a given round the monitor with the most simplifications. We sum the maximum number of simplifications per round across all the rounds, and then normalize by the number of rounds. This allows us to determine the slowest monitor per round, as other monitors are executing in parallel. Therefore, we determine the bottleneck. We refer to this metric as critical simplifications. This can be similarly done by considering the number of expressions evaluated. Since monitors can execute in parallel, we introduce convergence as a metric to capture load balancing across a run of length n, where:

conv(n) = 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. Convergence can also be measured similarly on evaluated expressions. We consider communication using three metrics: number of messages, total data transferred, and the data transferred in a given message. The number of messages is the total messages sent by all monitors throughout the entire run. The data transferred consists of the total size of messages sent by all monitors throughout the entire run. Both the number of messages and the data transferred are normalized using the run length. Finally, we consider the data transferred in a given message to verify the message sizes. To do so, we normalize the total data transferred using the number of messages. 9.1 Synthetic Scenario 9.1.1 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 Generator tool in THEMIS which generates synthetic traces using various probability distributions (provided by COLT 19 ). For all algorithms we considered the communication delay to be 1 timestamp. That is, messages sent at t are available to be received at most at t + 1. In the case of migration, we set the active monitors to 1 (m = 1). For our experiment, we vary the number of components between 3 and 5, and ensure that for each number we have 100 formulae that reference all components. We were not able to effectively use a larger number of components since most formulae become sufficiently large that generating an automaton from them using ltl2mon fail. The generated formulae were fully constructed of atomic propositions, there were no terms containing ⊤ or ⊥20 . We use 200 traces of 60 events per component, we associate with each component 2 observations. Traces are generated using 4 probability distributions (50 traces for each probability distribution). The used distributions include normal (µ = 0.5, σ 2 = 1), binomial (n = 100, p = 0.3), and two beta distributions: beta-1 (α = 2, β = 5), and beta-2 (α = 5, β = 1). The varied distributions provide different probability to assign ⊤ and ⊥ to observations in the traces, as such we achieve varied coverage 21 . Figure 8a shows the outcome of runs for different probability distributions. We notice that by varying the distributions we obtain different distributions of verdicts across all runs for all given specifications. The trace length is chosen to be 60, based on the consideration (b) Verdicts for all runs, across all traces of all probability distributions, using all random generated formulae. that random formulae usually cause monitor verdicts to either be returned very early or timeout (Figure 8b). The percentage of runs that lasted more than 60 timestamps and returned a final verdict is less than 0.1% of total runs. When computing sizes, we use a normalized unit to separate the encoding from actual implementation strategies. Our assumptions on the sizes follow from the 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 numbers of rounds to reach a verdict. In the case of timeout, the length of the run is 65 (length of the trace, and 5 additional timestamps to timeout). 9.1.2 Comparing Algorithms. Figures 9 and 10 present the outcome of the proposed metrics for the algorithms. We inspect the behavior of information delay in Figure 9a by computing the average information delay. As expected, orchestration never exceeds a delay of 1. For migration, the delay depends on the heuristic used, as mentioned in Section 7.2, its worst case is the number of components. Migration can still have a lower delay than orchestration in some cases (as observed for |C | ≥ 4). This observation is due to the initial monitor placement, as in our case we chose the first component always to be where we place the main orchestration monitor (component A), while for migration, the heuristic function (choose) decides which monitor starts. As such, in a specification where the verdict can be resolved at the first timestamp, migration has an advantage. For Chor, the delay is at least 1, as the network depth affects the delay. Furthermore, we notice that the delay for Chor is not particularly affected with the number of components. We know that its worst-case will depend on traces in cases of non-monitorability, we inspect that further in Section 9.2. Figure 9b shows the average maximum computation done by a monitor for a given round. By looking at computation, we notice that Orch performs no simplifications. This is the case as expressions in the EHE do not become sufficiently complex to require simplification. We recall that for orchestration, the memories of all local observations are sent to the main monitor within one timestamp. And as such, by memory lookup, the expression is immediately evaluated without the need to simplify. We notice that for the average case, Migr performs a small number of simplifications, and Chor still executes a reasonable number of simplifications. Figure 9c shows the convergence for the algorithms. Since Chor is the only algorithm that performs computations at different components in a given round, we notice that the convergence is much lower.

For communication, we first consider the number of messages transferred normalized by the length of the run. We notice that for algorithms Orch and Chor the number of messages increases with the number of components. Since Chor depends on the edges that connect monitors, it scales better with the number of components than Orch (the depth of the network is usually smaller than the number of components). In contrast, we notice that for Migr and Migrr, the number of messages is independent from the number of components, as it depends on the number of active monitors. Figure 10a presents the total data transferred normalized by the run length. We notice by examining algorithm Orch that sending all observations can be costly. Algorithms Migr and Migrr are capable of sending much less data on average, but have variable behavior, and scale poorly, we notice an increase as |C| increases. Algorithm Chor performs better than Orch, and scales much better with component size. We notice that while Migr and Migrr send fewer messages than the other algorithms, and have better scaling in the number of messages transferred, they can still, in total, send more data depending on the traces and specification. We notice that the 75% quartile for Migrr still exceeds that of Orch. Since total data transferred includes both the number of messages and their sizes, we present the size of the message in Figure 10b by dividing the total data transferred by the number of messages. We observe that for Orch and Chor the size of a message is constant, not very variable and does not depend on |C|, while for Migr and Migrr we observe a significant increase as |C| increase. We recall from Section 7.2 that the migration algorithms send the EHE which expressions grow exponentialy in the size of the information delay. 9.1.3 Comparing Variants. Using the same dataset, we look at another use case of THEMIS; that of comparing variants of the same algorithm. In this case, we focus on differences between Migr and Migrr. The heuristic of Migr improves on the round-robin heuristic of Migrr by choosing to transfer the EHE to the component that can observe the atomic proposition with the earliest timestamp in the EHE (referred to as earliest obligation [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF]). Using the simple heuristic, we notice a drop in the delay starting from |C| > 4 (Figure 9a). The simple heuristic of earliest obligation seems to reduce on average the delay of the algorithm, interestingly, it maintains a mean of 1. Furthermore, we observe a drop in both messages transferred (Figure 10a) and size of messages (Figure 10b). Consequently, this constitutes a drop in the total data transferred (Figure 10a). We note that the message size is also the size of the EHE. The drop in the number of messages sent is explained by the decision not to migrate when the soonest observation can be observed by the same component, while for Migrr, the round-robin heuristic causes the EHE to always migrate. However, this does not lead to a much lower number of simplifications (Figure 9b). Using THEMIS to compare the variants shows us that the earliest obligation heuristic reduces the size of the EHE, and thus, the size of the message, but also the number of messages sent. However, it does not seem to impact computation as the number of simplifications remains similar. 9.1.4 Discussion. The observed behavior of the simulation aligns with the initial analysis described in Section 7. 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. However, both Figures 9 and10 show that for most metrics, we observe a large variance (as evidenced by the interquartile difference). As such, we caution that while the analysis presents trends where algorithms have the advantage, it is still necessary to address the specifics, hence the need for simulation. 9.1.5 Explaining earlier results. In [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF], the authors conducted experiments to compare the various algorithms. In particular, they broke down the metrics by delay, message count, message size and number of progressions (rewrites to the formula). We focus on the first three ignoring the last, since we do not monitor by rewriting. First, the authors rank the algorithms from lowest to highest as follows: Orch, Chor, and Migr. This is consistent with our analysis and our synthetic benchmark, since Orch has a constant delay, Chor a delay depending on the depth of the network, and Migr a delay depending on the number of components. However, we note that there are (small) cases where Chor will have a worst-case delay of the size of the trace, this is not reflected in [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF]. Second, the authors discuss the number of messages sent by each algorithm (assuming a round-based scheme). The lowest algorithm is Migr (with m = 1), followed by Chor, which is followed by Orch. We note that in our analysis (Section 7), the number of messages in migration depends on the number of active monitors, in choreography on the number of edges in the network, and in orchestration on the number of components. Considering that the monitors are organized in a DAG, there will be generally less edges than components (using the splitting strategy), this contributes to choreography outperforming orchestration. This can be seen as the authors state that exceptions allow Orch to perform better than Orch. In particular "for [..] randomly generated formulae of size 5, or when the depth of the network is greater than or equal to 3. ". A larger formula and a deeper network require a more complex network organization, which could result in more edges. We recall that the experiment ranged on a number of components between 3 and 5, where not all components were referenced at all times. Third, the authors discuss the size of the messages, ranking the algorithms from short to long messages as follows: Orch, Chor, and Migr. We recall that for Chor the message size is constant, while for Orch the message size depends on the number of observations per component. Either way both are significantly smaller than Migr which sends the full monitoring information. While the analysis shows that in theory, Chor should perform better than Orch with respect to size of the message, we are unsure how the size was captured. Since in the experiments in [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF], the size for Chor grows linearly with the size of the formula, while by definition the message is defined with a fixed size (ids + verdict). We believe the encoding scheme impacts the size of the message.

9.1.6 Trace Variance. In Table 4, we examine the variance by observing metrics with respect to probability distributions used to generate the traces. To exclude the variance due to the number of components, we fix |C| = 6, as it provides the highest variance. For each metric, we present the mean and the standard deviation (between parentheses). All metrics are normalized by the length of the run. The metrics in order of columns are: average information delay (δ t ), average number of messages (#Msgs), total data transferred (Data), average maximum simplifications per monitor (S), and convergence based on expressions evaluated (Conv E ). We observe that by changing the probability distribution, the metrics vary significantly. This is particularly prominent for the information delay (especially in the case of Chor), and data transferred. We explore the differences in the algorithms in Section 9.2 by considering real examples with existing formalized specifications. 9.1.7 Impact of Network Delay. In order to assess the impact of the network delay, we fixed the number of components to three, used traces obtained using the normal distribution, and varied network delay by either delaying all messages by a constant delay, or randomizing the delay (up to a certain bound) on a per-message basis. We experiment with two values of delays: 2 and 5 rounds, and show the impact of the network delay on the information delay in Figure 11 for each monitoring algorithm. First, we verify that all verdicts for all delay values match the initial verdicts. This ensures that all runs returned sound verdicts. We note the exceptions of very few runs (2 runs) where the verdict was delayed past the timeout point and therefore could not be reached. We observe that the higher the network delay the higher the information delay. This would cause the algorithms to manipulate larger EHEs but otherwise would not affect correctness. Furthermore, when the delay is variable, we observe overall smaller resulting EHEs, as partial observations often allow monitors to reach verdicts before all information is received, that is for an expression a ∨ b, if a is sent with a smaller delay than b and is observed to be ⊤, then the expression is resolved without waiting on b.

9.2

The Chiron User Interface 9.2.1 Overview. Moving away from synthetic benchmarks, we consider properties that apply to patterns of programs and specifications. In this section, we compare the algorithms by looking at a real example that uses the publish-subscribe pattern. To that extent, we consider the Chiron user interface example [START_REF] Avrunin | Comparing Finite-State Verification Techniques for Concurrent Software[END_REF]. Chiron consists of artists responsible of rendering parts of a user interface, that register for various events via a dispatcher. A dispatcher receives events from an abstract data type (ADT) and forwards them to the registered artists. We chose Chiron for two practical reasons. Firstly its example source code (in ADA), and its specifications are available online [START_REF]Chiron User Interface[END_REF]. The specification is completely formalized and utilizes various LTL patterns described in [START_REF]Patterns Project[END_REF][START_REF] Matthew | Patterns in Property Specifications for Finite-State Verification[END_REF]. Thus, it covers a multitude of patterns for writing specifications. Secondly, the Chiron system can be easily decomposed into various components, we consider four components, the dispatcher (A), the two artists (B,C) and the main thread (D). The main thread is concerned with observing termination of the program. 9.2.2 Experimental Setup. Table 5 lists the subset of the Chiron specification we considered. For each property, column ID references the original property name in [START_REF]Chiron User Interface[END_REF], column B 3 references the expected verdict at the end of the trace 22 , and column pattern identifies the LTL pattern corresponding to the formula. We modify the Chiron example program [START_REF]Chiron User Interface[END_REF] to output a trace The order in which artists register for events of kind 1 is the order in which they are notified of an event of this kind by the dispatcher. In other words, if artist1 registers for event2 before artist2 does, then once dispatcher receives event2 from the ADT, it will first send it to artist1 and then to artist2. 15a ?

Universal The program never terminates with an artist registered. 15b ⊤

Response An artist always unregisters before the program terminates. Given that you can't register for the same event twice, we need only check that unregisters respond to registers of the program, and consider the specifications listed in Table 5 23 . For example, we consider the specification shown in Listing 1. It states that artists are only notified when the dispatcher receives an event. That is, the dispatcher does not send events to the artists without receiving them properly from the ADT. Since we monitor offline, we generate the trace by inserting a global monitor that contains information about all relevant atomic propositions. The program is then instrumented to notify the monitor of events. Specifications and traces are then provided as input to THEMIS to process with the existing algorithms. The details on the atomic propositions and their assignment to components can be found in Appendix B. We randomized the events dispatched in the Chiron example, and generated 100 traces of length 279. We targeted generating traces under 300 events. This corresponds to the ADT dispatching 91 events, with the addition of events to register, and unregister artists.

On the Monitoring of Decentralized Specifications :41 9.2.3 Comparing algorithms. Figure 12 presents the means for the metrics of average delay, convergence, and both critical and maximum simplifications 24 . We immediately notice for Chor the high average delay for specifications 2 and 15b (133.86, and 116.52, respectively). In these two cases, the heuristic to generate the monitor network for choreography has split the network inefficiently, and introduced a large delay due to dependencies. We recall that the heuristic used for choreography consider LTL formulae. For a given formula it counts the number of references to atomic propositions of a given component. The monitor tasked with monitoring the formula will then be associated with the highest component. To generate a decentralized specification, the heuristic starts with an LTL formula and splits it into two subformulas for each binary operator, then one of the subformulas is chosen to remain on the current component while the other is delegated to the component with the most references to atomic propositions. We see in this case that simply counting references and breaking ties using the lexicographical order of the component name can yield inefficient decompositions. Furthermore, we notice that while Orch maintains the lowest delay, other algorithms can still yield comparable delays. In the case of specification 15a we observe that Orch, Migr, and Chor have similar delay (1.0). While Migr may outperform Chor for specifications 2 and 15b, it is the opposite for specifications 1, 3 and 5. This highlights that the network decomposition of monitors (i.e., the setup phase) is an important consideration when designing decentralized monitoring algorithms.

Figure 12b presents the convergence (computed using the number of expressions evaluated). We see that the poor decomposition also yields imbalanced workloads on the monitors. In the case of specifications 2 and 15b, we observe a convergence of 0.67 to 0.71 for Chor, respectively. The observed convergence is comparable with that of Orch and Migr. Furthermore, it is still possible to improve on the load balance for specifications 3 and 15a, as the convergence is high (0.33 and 0.47).

Figure 12c illustrates critical simplifications, we see that Chor has a higher cost compared to Migr in terms of computation. We also notice that Migr performs better than Migrr for all specifications. The heuristic of migrating the formula based on the atomic proposition with the earliest timestamp (earliest obligation) does indeed improve computation costs. More importantly, we notice that the highest delay for Chor is for specifications 2 and 15b. To inspect that, we look at the maximum delay induced in a given monitor for an entire run, and consider the mean across all traces to obtain the worst-case maximum simplifications in Figure 12d. Indeed, we notice a peak in the maximum number of simplification in a given round for specifications 2 and 15b. Particularly, we notice that while comparable in other specifications (e.g., for specification 15a, we have 10 max simplifications for Chor as opposed to 8.64 and 10.00 for Migr and Migrr, respectively), the maximum number of simplifications for Chor increases to 2,798 (compared to 12 for Migrr), and 3,387 (compared to 16.86 for Migrr) for specifications 2 and 15b, respectively. In this particular case, we see how delay can impact the maximum number of simplifications.

We now consider communication costs by observing the number of messages transferred in Figure 13a. We see that Migr and Migrr perform well compared to the other two algorithms, with Migr performing consistently better than Migrr. We note that the analysis of Migr indicates that the number of messages per round will be in the worst case the number of active monitors (in our case that is 1). One can see in specification 5 that Migr sends only 0.02 messages on average per round, compared to Migrr with 1.01, followed by Orch with 2.95, and finally Chor with 4.89. We see that Orch outperforms Chor in the case of specifications 1, 2, 3 and 5, where generally Orch sends 1-2 messages less. We note that this pattern is in line with the trends shown in Figure 9d. We see for |C| = 4 that Orch and Chor overlap, with Migrr outperforming both, and Migr outperforming all other algorithms. Interestingly, we find that in the case of specification 15a in Figure 13a, we see for Chor a number of messages (0.98) slightly higher than Migr (0.97) and lower than Migrr (1.01), consistent with the lower whiskers in Figure 9d. Similarly, when considering the total data transferred in Figure 13b, we see as a trend across specifications Migr being particularly good, while still being slightly outperformed by Chor in specifications 15a and 15b. Furthermore, we notice that Migrr performs poorly and indeed sends more data than Orch in most cases, indicating On the Monitoring of Decentralized Specifications :43 that a heuristic can indeed be instrumental in the success of designing the family of migration algorithms. We notice also that the trends from Figure 10a seem to apply in most cases, Orch sends a lot more data than Migr and Chor, with Migrr possibly surpassing Orch.

RELATED WORK

Runtime verification/monitoring is a verification technique aiming at checking the correctness of a system using runtime information. We refer to [START_REF] Leucker | A brief account of runtime verification[END_REF] for a comparison between runtime verification and other verification techniques.

In this section, we classify and compare with approaches to decentralized monitoring: monitoring by formula rewriting (Section 10.1), monitoring distributed systems (Section 10.2), fault-tolerant monitoring (Section 10.3), and stream-based monitoring (Section 10.4). We also refer to [START_REF] Francalanza | Runtime Verification for Decentralised and Distributed Systems[END_REF] for a recent overview.

Monitoring by Formula Rewriting

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, to generate a formula that has to hold on the next timestamp. 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. These approaches use a centralized specification to describe the system behavior, they perform decentralized monitoring of a centralized specification (Section 2.2), in a system relying on a global clock.

Monitoring Distributed Systems

Monitoring approaches to monitoring distributed systems typically consider the problem of detecting global predicates. Global predicate detection [START_REF] Natarajan | Efficient abstraction algorithms for predicate detection[END_REF][START_REF] Vinit | Detecting Temporal Logic Predicates on Distributed Computations[END_REF] consists in evaluating predicates on the global state of a distributed system. Approaches performing predicate detection are capable of distributing the evaluation across a distributed system, and evaluate regular predicates which include some temporal logic predicates (such as globally □ and eventually ⋄). The evaluation is done online, and as such can be seen as runtime verification. In [START_REF] Mostafa | Decentralized Runtime Verification of LTL Specifications in Distributed Systems[END_REF] the authors extend the approach beyond safety properties to monitor temporal properties in distributed systems. These techniques perform effectively decentralized monitoring of a centralized specification (Section 2.2), without assumptions of a global clock.

Fault-tolerant Monitoring

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 multiple monitors tasked to 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 the 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 define separate monitors with different specifications, typically consisting in splitting the formula into subformulas. Then, they describe the collaboration between such monitors. However, when performing decentralized monitoring of a centralized specification, approaches 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 (Section 11).

Stream-based Monitoring

Specification languages have been developed that monitor synchronous systems as streams [START_REF] Ben | LOLA: Runtime Monitoring of Synchronous Systems[END_REF][START_REF] Decker | Rapidly Adjustable Non-intrusive Online Monitoring for Multi-core Systems[END_REF]. In this setting, events are grouped as a stream, and streams are then aggregated by various operators. The output domain extends beyond the Boolean domain and encompasses types. The stream approach to monitoring has the advantage of aggregating types, as such operations such as summing, averaging or pulling statistics across multiple streams is also possible. Stream combination is thus provided by general-purpose functions, which are more complex to analyze than automata. This is similar to complex event processing where RV is a special case [START_REF] Hallé | When RV Meets CEP[END_REF]. Specification languages such as LOLA [START_REF] Ben | LOLA: Runtime Monitoring of Synchronous Systems[END_REF] even define dependency graphs between various stream information, and have some properties like well formed, and efficiently monitorable LOLA specifications. The former ensures that dependencies in the trace can be resolved before they are needed, and the latter ensures that On the Monitoring of Decentralized Specifications :45 the memory requirement is no more than constant with respect to the length of the trace. While streams are general enough to express monitoring, they do not address decentralized monitoring explicitly. As such, there is no explicit assignment of monitors to components and parts of the system, nor consideration of architecture. Furthermore, there is no algorithmic consideration addressing monitoring in a decentralized fashion, even-though some works such as [START_REF] Hallé | Event Stream Processing with Multiple Threads[END_REF] do provide multi-threaded implementations.

FUTURE DIRECTIONS

By introducing decentralized specifications, we separate the monitor topology from the monitoring algorithm. As such, we address future directions that result from analyzing the topology of monitors, and thus, define properties on such topologies, studying the monitoring by improving metrics, and applying decentralized specifications to the problem of runtime enforcement [START_REF] Falcone | You Should Better Enforce Than Verify[END_REF][START_REF] Falcone | Runtime Failure Prevention and Reaction[END_REF].

Optimized compatibility. The first direction is to extend the notion of compatibility (Section 6.2) to not only decide whether or not a specification is applicable to the architecture of the system, but also use the architecture to optimize the placement. 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 Section 7).

Verdict equivalence. We can also compare decentralized specifications to ensure that two specifications emit the same verdict for all possible traces, we elaborate on this property as verdict equivalence. We consider two decentralized specifications D and D ′ , constructed with two sets of monitors Mons and Mons ′ (as per Section 5). Let the root monitors be rt, and rt ′ , respectively. We recall the notation from Section 4.1, for a given monitor label ℓ, q ℓ 0 , ∆ ℓ and ver ℓ indicate the initial state, transition relation and the verdict function for a given monitor (automaton). One way to assess equivalence is to verify, that for all traces, both specifications yield similar verdicts. It suffices to evaluate the trace on the transition function starting from the root monitor, and check the verdict of the reached state. That is, two decentralized specifications D and D ′ are verdict equivalent iff ∀t ∈ T : ver rt (∆ ′ * rt (q rt 0 , t, 1)) = ver rt ′ (∆ ′ * rt ′ (q rt ′ 0 , t, 1)). The verdict equivalence property establishes the basis for comparing two specifications that eventually output the same verdicts for the same traces. For all possible traces (∀t ∈ T ), we first evaluate the trace on the root monitor of D (i.e., ∆ ′ * rt (q rt 0 , t)), and similarly we evaluate the same trace on the root monitor of D ′ (i.e., ∆ ′ * rt ′ (q rt ′ 0 , t)). The states reached for both of the automata executions need to be labeled by the same verdict. While both specifications yield the same verdict for a given trace, one could also extend this formulation to add bounds on delay. Specification synthesis. Another interesting problem to explore is that of specification synthesis. Specification synthesis considers the problem of generating a decentralized specification, using various inputs. Typically, we would expect another specification as reference and possibly the system architecture. For example, given a centralized specification, we generate a decentralized specification, by splitting the specification into subspecifications and assigning the subspecifications to monitors. Generating a decentralized specification using a centralized one as reference is used in some algorithms such as choreography [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF] 25 . Starting from an LTL formula, the formula is split into subformulas hosted on the various components of the system (this is detailed further in Section 7.2). Given a decentralized specification D, and a system graph ⟨C, E ′ ⟩, the problem consists in generating a specification D ′ . The variants of the synthesis problem depend on the properties that D ′ must have, we list (non-exhaustively) example properties:

(1) D ′ is monitorable (Section 6.1);

(2) D ′ is compatible with ⟨C, E ′ ⟩ (Section 6.2);

(3) D ′ and D are verdict equivalent.

Synthesis problems could also be expanded to handle optimization techniques, with regards to specifications. The specification determines the computation and communication needed by the monitors. As such, it is possible to optimize, the size of automata, and references so as to fine-tune load and overhead for a given system architecture.

Extending THEMIS metrics. Moreover, one could consider creating new metrics for THEMIS to analyze more aspects of decentralized monitoring algorithms. We see that this is important, as in two specifications out of the five when using Chiron traces (Section 9.2), the choreography algorithm using a simple heuristic generated an inefficient decentralized specification. New metrics would be automatically instrumented on all existing algorithms and experiments could be easily replicated to compare them.

Weakening round constraints. In the current setting, all monitors of the decentralized specifications are required to perform their evaluation based on a global round. This condition can be weakened to a relation between only dependent monitors, instead of the whole system.

CONCLUSION

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. We make a clear distinction between the topology of monitors and the behavior of each monitor. We elaborate on two properties associated with decentralized specifications: compatibility, and monitorability. In addition, we present the EHE data structure which allows us to (i) aggregate monitor states with strong eventual consistency (ii) remain sound with respect to 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 implement four algorithms in THEMIS under our model and data-structures: orchestration (Orch), migration using earliest obligation (Migr), migration using round-robin (Migrr), and choreography (Chor). Using THEMIS and the designed metrics, we explore simulations of the four algorithms on two scenarios and validate the trends observed in the analysis. In the first scenario, we use the synthetic benchmark comprising of random specifications and traces. In the second scenario, we use a real example (Chiron) with existing formalized specifications.

A PROOFS

Proof of Proposition 4.8. The proof is by induction on the number of timestamps in the EHE, i.e., n = |rounds(I)|. Without loss of generality, we can assume the automaton being encoded is normalized (see Remark 1), that is, all shared edges between any two states are replaced by one edge which is labeled by the disjunction of their labels.

One could see that the base case only contains the initial state of an automaton, i.e., I 0 = [0 → q 0 → ⊤], and as such the proposition holds.

Let us consider n = 2, we have I 1 = mov(I 0 , 0, 1). To compute mov, we first consider next(I 0 , 0) which considers all states reachable from q 0 as the only tuple in I 0 is ⟨0, q 0 ⟩, i.e., next(I 0 , 0) = {q ′ ∈ Q | ∃e ∈ Expr : δ (q 0 , e) = q ′ }, we know that only one such e can evaluate to ⊤ for any memory encoded with the identity encoder (idt), since the automaton is deterministic. Let us collect all such states and their expressions as P = {⟨q ′ , e⟩ ∈ Q × Expr | ∃e ∈ Expr : δ (q 0 , e) = q ′ }. We note that I 1 (0, q 0 ) = ⊤ is the only entry for timestamp 0. The property holds trivially for that entry. We now consider the entries in I 1 for timestamp 1. Each of tuple ⟨q ′ , e⟩ ∈ P corresponds to the expression I 1 (1, q ′ ), constructed with to(I 0 , 0, q ′ , ts 1 ) = I 0 (0, q 0 ) ∧ ts 1 (e). We note that ts 1 only adds the timestamp 1 to each atomic proposition. As such, for any given memory encoded with ts 1 only one such expression can be evaluated to ⊤.

Inductive step: We assume that the property holds on I n-1 for some n ∈ N, that is: ∀M ∈ Mem, ∀t ∈ rounds(I n-1 ), ∃q ∈ Q : (eval(I n-1 (t, q), M) = ⊤) =⇒ (∀q ′ ∈ Q \ {q} =⇒ eval(I n-1 (t, q ′ ), M) ⊤). Let us prove that the property holds for I n .

The approach is similar to that of n = 2 using the recursive structure of the EHE to generalize. We decompose I n , using the definition of mov, as follows:

I n = I n-1 † ∨ ∨ q ′ ∈next(I n-1 ,n)
{n → q ′ → to(I n-1 , n -1, q ′ , ts n )}

We know that rounds(I n ) = rounds(I n-1 ) ∪ {n}. The induction hypothesis states that the property holds for all entries in I n-1 (i.e. for t ∈ rounds(I n-1 )), we consider the entries for timestamp n only.

Since ∨ applies † ∨ on the entire set, and it is associative and commutative we consider the expression for a given state after all the merges, without consideration of order of merges. As such the states associated with timestamp n are computed using next(I n-1 , n). We have ∀q ′ ∈ next(I n-1 , n):

I n (n, q ′ ) = to(I n-1 , n -1, q ′ , ts n ) (Def. mov) = { ⟨q,e ′ ⟩ | δ (q,e ′ )=q ′ } (I n-1 (n -1, q) ∧ ts n (e ′ ))

(1) follows from the definition of to. If we examine the disjunction we notice using the induction hypothesis that there can only be a unique q u ∈ Q with I n-1 (n -1, q u ) that evaluates to ⊤ at timestamp n -1. As such, the conjunction can only hold for one such q u . Consequently, we can rewrite (1) by simplifying the disjunction and considering only states reachable from q u , as the rest cannot evaluate to ⊤. Let us collect all such states and expressions in the set P u = {⟨q ′ , e ′ ⟩ | q ′ ∈ next(I n-1 , n) ∧ ∃e ′ ∈ Expr AP : δ (q u , e ′ ) = q ′ }. The only entries that can still evaluate to ⊤ are:

∀⟨q ′ , e ′ ⟩ ∈ P u : I n (n, q ′ ) = I n-1 (n -1, q u ) ∧ ts n (e ′ )

= ts n (e ′ )

Since the automaton is deterministic, we know that we have one unique expression e u that can evaluate to ⊤, given any memory encoded with idt. Since ts n only adds the timestamp n to the atomic propositions without changing the expression, we deduce that only ts n (e u ) evaluates to ⊤.

As such, there is a unique expression that can evaluate to ⊤ for any given memory encoded with ts n . Furthermore, we know that the expression has only been encoded with ts n so when memories encoded with different timestamps or encoders are merged, they do not affect the evaluation of ts n (e u ). As such, we have a unique entry I n (n, q ′ u ) s.t. δ (q u , e u ) that can evaluate to ⊤. Therefore:

∀M ∈ Mem, ∀t ∈ rounds(I n ), ∃q ∈ Q :

(eval(I n (t, q), M) = ⊤) =⇒ (∀q ′ ∈ Q : q ′ q =⇒ eval(I n (t, q ′ ), M) ⊤)

□

Lemma A.1 (Evaluation modulo encoding). Given a trace tr of length i and a reconstructed global trace ρ(tr) = evt 1 • . . . • evt i , we consider two memories M i A and M i generated under different encodings. We consider M i A = memc(evt i , idt), and M i = 2 t ∈[1,i] {memc(evt t , ts t )}. We show that an expression encoded using different encodings evaluates the same for the memories, that is:

∀e ∈ Expr AP : eval(idt(e), M i A ) ⇔ eval(ts i (e), M i ).

Proof of Lemma A.1. We first note that for the first evaluation eval(idt(e), M i A ), we rely only on the event evt i since M i A = memc(evt i , idt). This is not the case for eval(ts i (e), M i ) as M i = 2 t ∈[1,i] {memc(evt t , ts t )}. However, we notice that for the second evaluation we evaluate the expression ts i (e), that is, where the expression where all atomic propositions have been encoded by the timestamp i. Therefore, let us denote the memory with timestamp i by M ′ = memc(evt i , ts i ).

We can rewrite M i as follows:

M i = memc(evt i , ts i ) † 2 2 t ∈[1,k ] {memc(evt k , ts k )}, = M ′ † 2 2 t ∈[1,k ] {memc(evt k , ts k )}.
We know that all entries ⟨k, a⟩ ∈ dom(M i ) with k < i do not affect at all the evaluation of an expression encoded with ts i . As such, we have: ∀e ∈ Expr AP : eval(ts i (e), M i ) ⇔ eval(ts i (e), M ′ )

We now show that the two memories M i A and M ′ contain simply an encoding of the same atomic propositions. By construction, we have the following:

∀a ∈ dom(M i A ) : ⟨i, a⟩ ∈ dom(M i ) ∧ M i A (a) = M ′ (⟨i, a⟩), ∀⟨i, a ′ ⟩ ∈ dom(M ′ ) : a ′ ∈ dom(M i A ) ∧ M ′ (⟨i, a ′ ⟩) = M i A (a ′ ).
As such, we have: ∀e ∈ Expr AP : eval(idt(e), M i A ) ⇔ eval(ts i (e), M ′ ) ⇔ eval(ts i (e), M i ). □

Proof of Proposition 4.10. Given a trace tr of length i and a reconstructed global trace ρ(tr) = evt 1 • . . . • evt i , the proof is done by induction on the length of the trace |ρ(tr)|. We omit the label ℓ for clarity.

Base case: |ρ(tr)| = 0, ρ(tr) = ϵ ∆ * (q 0 , ϵ) = q 0 = sel(I 0 , [ ], 0)

I 0 = mov([0 → q 0 → ⊤], 0, 0) = [0 → q 0 → ⊤]
We only have expression ⊤ which is mapped to q 0 at t = 0. Expression ⊤ requires no memory to be evaluated.

Inductive step: We assume that the property holds for a trace of length i for some i ∈ N, that is ∆ * (q 0 , evt 1 • . . . • evt i ) = sel(I i , M i , i) = q i . Let us prove that the property holds for any trace of length i + 1.

We now consider the transition functions in the automaton: q i+1 = ∆ * (q 0 , evt 1 • . . . • evt i+1 )

= ∆(∆ * (q 0 , evt 1 • . . . • evt i ), evt i+1 ) (Def. 4.2) = ∆(q i , evt i+1 ) (Hyp.) ⇔ ∃e ∈ Expr AP : δ (q i , expr ) = q i+1 ∧ eval(e, M i+1 A ) = ⊤

On the Monitoring of Decentralized Specifications :53

C CHANGES IN THEMIS

Figure 14 shows the data transferred for the migration algorithms, which is associated with the size of the EHE. We reduced the size of the EHE by making calls to the simplifier only for complex simplifications, and implement the basic Boolean simplification while traversing the expression to replace atomic propositions by looking up the memory (in the operation rw). Since we have less calls, we apply a more aggressive simplification that is more costly 26 , but also reduces the size of the expressions. The x-axis indicates the algorithm's variant and the number of components, where Migr (resp. Migrr) stands for earliest the variant obligation (resp. round-robin). The y-axis is presented in logarithmic scale. We notice a significant drop in the size of EHE, dropping from 769 in the ISSTA'17 version for Migrr-5 to 73.12.

D DETAILED COMPARISON

Tables 7 and8 present the detailed comparison for the synthetic scenario and Chiron, respectively. The metrics presented are (in order of columns): average information delay (δ t ), normalized average number of messages (#Msgs), normalized data transferred (Data), maximum simplifications done by any given monitor per run, averaged across all runs (S max ), normalized critical simplifications

E CHOREOGRAPHY SETUP PHASE

Choreography as presented in [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF] splits the initial LTL formula into subformulas and delegates each subformula to a monitor on a component. Thus choreography presents a complicated setup phase. In this section, we present the setup phase. As such, we present the generation of the decentralized specification from a start LTL formula. Choreography begins by taking the main formula, then deciding to split it into subformulas. Each monitor will monitor the subformula, notify other monitors of its verdict, and when needed respawn . Recall from the definition of ∆ ′ (see Definition 5.4), that monitoring is recursively applied to the remainder of a trace starting at the current event. That is, initially we monitor from e 0 to e n and then from e 1 to e n and so forth. To do so, it is necessary to reset the state of a monitor appropriately, this process is called in [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF] a respawn. Once the subformulas are determined, we generate an automaton per subformula to monitor it. Then, we construct the network of monitors in the form of a tree, in which the root is the main monitor. Verdicts for each subformula are then propagated in the hierarchy until a verdict can be reached by the root monitor.

A choreography monitor is a tuple ⟨id, A φ id , ref id , coref id , respawn id ⟩ where:

• id denotes the monitor unique identifier (label);

• A id the automaton that monitors the subformula;

• ref id : 2 Mons the monitors that this monitor should notify of a verdict;

• coref id : 2 Mons the monitors that send their verdicts to this monitor;

Fig. 1 .

 1 Fig. 1. LTL 3 monitor for the light switch and bulb specification. The verdicts associated with the states are ⊥: dotted/red, and ?: solid/yellow.

Fig. 2 .

 2 Fig. 2. Evaluating monitor references.

Definition 3 . 7 (

 37 Rewriting an expression). An expression e is rewritten with a memory M using function rw : Expr Atoms × Mem → Expr Atoms defined as follows: rw(e, M) = match e 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)

: 10 Antoine⊤

 10 El-Hokayem and Yliès Falcone Definition 3.10 (Evaluating an expression). The evaluation of a Boolean expression e ∈ Expr Atoms using a memory M yields a verdict. Function eval : Expr Atoms × Mem → B 3 is defined as: eval(e, M) if simplify(rw(e, M) ⇔ ⊤, ⊥ if simplify(rw(e, M) ⇔ ⊥, ? otherwise.

Proposition 4 . 11 (

 411 Memory obsolescence).

Fig. 3 .

 3 Fig. 3. Monitor(s) for the centralized and decentralized light switch and bulb specification presented in Example 2.1. The verdicts associated with the states are ⊥: dotted red , ⊤: double green, and ?: single yellow.

Definition 5. 2 (

 2 Monitor dependency). The set of monitor dependencies in an expression e is obtained by function dep : Expr AP → Mons, defined as 11 : dep(e) = match e with: | id ∈ AP mons → {A id } | e 1 ∧ e 2 → dep(e 1 ) ∪ dep(e 2 ) | id ∈ AP \ AP mons → ∅ | ¬e → dep(e) | e 1 ∨ e 2 → dep(e 1 ) ∪ dep(e 2 )

  e., O(|Q | + |δ |)). Hence in the worst case, an automaton forms a complete graph, and we have |Q | 2 edges. The worst case complexity is quadratic in the number of states (i.e., O(|Q | + 1 2 |Q |(|Q | -1))

Fig. 6 .

 6 Fig. 6. Example Compatibility

  Verdicts for traces based on the different probability distributions.

Fig. 8 .

 8 Fig. 8. Verdicts emitted by different run lengths.

Fig. 9 .

 9 Fig. 9. Comparison of delay, computation and number of messages. Algorithms are presented in the following order: Orch, Migr, Migrr, Chor.

  Chor(a) Total data transferred.

  Fig. 10. Data Transfer

Fig. 11 .

 11 Fig.11. Effect of network delay on information delay. Variable delay is denoted by min-max and is measured in rounds, stating that each message is randomly delayed for a value between min and max.

Listing 1 .

 1 Example Chiron Specification !( notify_client_event_a1_e1 || notify_client_event_a2_e1 ) U ( notify_artists_e1 || []!( notify_client_event_a1_e1 || notify_client_event_a2_e1 ))

  Monitor (Worst-Case, log scale) (d) Maximum simplifications (worst case).

Fig. 12 .

 12 Fig. 12. Comparison of delay, convergence and number of simplifications. Algorithms are presented in the following order: Orch, Migr, Migrr, Chor. Orch is omitted in the simplifications count as it is zero.

  Chor(a) Number of messages (normalized).

  Total data transferred (normalized).

Fig. 13 .

 13 Fig. 13. Data Transfer

Fig. 14 .

 14 Fig. 14. Size of EHE.

Table 1 .

 1 A tabular representation of I 2 .

Table 2 shows

 2 On the Monitoring of Decentralized Specifications :17

Table 2 .

 2 Reconciling information by combining EHEs.I 2 indicates the non-rewritten EHE. The columns [M 2 0

Table 3 .

 3 Scalability of existing algorithms.

	Algorithm	δ t	# Msg	|Msg|
	Orchestration	Θ(1)	Θ(|C|)	Θ(|AP c |)

Table 4 .

 4 Variation of average delay, number of messages, data transfer, critical simplifications and convergence with traces generated using different probability distributions for each algorithm. Number of components is |C | = 6. Table cells include the mean and the standard deviation (in parentheses).

	Alg.	Trace	δ t	#Msgs	Data	S crit	Conv E
		normal 0.69 (0.46) 7.13 (1.38) 94.87 (18.46)	0.00 (0.00) 0.83 (0.01)
		binomial 0.69 (0.46) 7.15 (1.39) 93.10 (18.13)	0.00 (0.00) 0.83 (0.01)
	Orch
		beta-1	0.70 (0.46) 6.98 (1.47) 96.11 (20.17)	0.00 (0.00) 0.83 (0.02)
		beta-2	0.69 (0.46) 6.91 (1.71) 83.37 (20.66)	0.00 (0.00) 0.82 (0.02)
		normal 1.72 (1.42) 0.50 (0.32) 110.13 (276.43) 7.01 (5.01) 0.82 (0.03)
		binomial 1.67 (1.40) 0.49 (0.32) 95.44 (221.65) 6.86 (4.91) 0.82 (0.04)
	Migr
		beta-1	1.82 (1.44) 0.53 (0.32) 133.15 (313.44) 7.14 (5.16) 0.82 (0.04)
		beta-2	1.53 (1.36) 0.47 (0.38) 56.48 (114.54) 5.95 (4.24) 0.82 (0.03)
		normal 2.64 (1.93) 0.70 (0.35) 177.48 (358.61) 7.50 (5.18) 0.83 (0.03)
		binomial 2.59 (1.95) 0.69 (0.36) 171.64 (318.94) 7.49 (5.21) 0.83 (0.03)
	Migrr
		beta-1	2.82 (1.94) 0.74 (0.34) 210.02 (452.83) 7.49 (5.23) 0.82 (0.03)
		beta-2	2.55 (2.08) 0.66 (0.41) 162.28 (287.28) 6.93 (4.90) 0.82 (0.02)
		normal 2.02 (1.97) 5.92 (1.60) 52.54 (14.23) 12.68 (3.63) 0.13 (0.10)
		binomial 1.93 (1.86) 5.95 (1.61) 52.76 (14.33) 12.55 (3.70) 0.13 (0.10)
	Chor
		beta-1	2.59 (4.58) 5.80 (1.64) 51.54 (14.48) 13.29 (4.33) 0.14 (0.12)
		beta-2	2.95 (7.26) 5.81 (1.79) 51.52 (15.93) 13.50 (9.91) 0.14 (0.14)

Table 5 .

 5 Monitored Chiron specifications. CRC stands for Constrained Response Chain.

	ID B 3	Pattern	Description
	1	?	Absence	An artist never registers for an event if she is already registered for that
				event, and an artist never unregisters for an event unless she is already
				registered for that event.
	2	?	CRC (2-1) If an artist is registered for an event and dispatcher receives this event,
				it will not receive another event before passing this one to the artist.
	3	⊤ Precedence Dispatcher does not notify any artists of an event until it receives this
				event from the ADT.
	5	?	Absence	Dispatcher does not block ADT if no one is registered (this means that
				if no artists are registered for events of kind 1, dispatcher does nothing
				upon receiving an event of this kind from the ADT).
	7*	?	CRC (3-1)

Table 6 .

 6 Chiron Atomic Propositions and Components.

	C	Name	Original (AP)	AP Comments
			registered_event_a1_e1	a0
			registered_event_a1_e2	a1
				True after an artist has completed registration
			registered_event_a2_e1	a2
			registered_event_a2_e2	a3
			notify_a1_e1	a4
			notify_a1_e2	a5
	A	Dispatcher		True when starting to dispatch an event to an artist
			notify_a2_e1	a6
			notify_a2_e2	a7
			lst_sz0_e1	a8
			lst_sz0_e2	a9
				Tracking the size of the list (state)
			lst_gt2_e1	a10
			lst_gt2_e2	a11
			notify_client_a1_e1	b0
				Artist receives a notification
			notify_client_a1_e2	b1
			register_event_a1_e1	b2
	B	Artist1		Artist requests to register for event
			register_event_a1_e2	b3
			unregister_event_a1_e1 b4
				Artist requests to unregister
			unregister_event_a1_e2 b5
			notify_client_a2_e1	c0
			notify_client_a2_e2	c1
			register_event_a2_e1	c2
	C	Artist2		See Artist1
			register_event_a2_e2	c3
			unregister_event_a2_e1 c4
			unregister_event_a2_e2 c5
	D	Main	term	d0 Main program terminates

Table 7 .

 7 Synthetic Benchmark. Cells contains mean and standard deviation in parentheses. S crit ), and convergence based on expressions evaluated (Conv E ). For more details on the metrics, see Section 9.

	Alg.	| C |	δ t	#Msgs	Data	S max	S crit	Conv E
		3	0.48 (0.50) 2.44 (0.61)	31.84 (8.07)	0.00 (0.00)	0.00 (0.00) 0.65 (0.02)
		4	0.53 (0.50) 3.85 (0.94)	50.05 (12.39)	0.00 (0.00)	0.00 (0.00) 0.74 (0.02)
	Orch
		5	0.64 (0.48) 5.30 (1.16)	69.20 (15.55)	0.00 (0.00)	0.00 (0.00) 0.79 (0.02)
		6	0.69 (0.46) 7.04 (1.50)	91.86 (20.02)	0.00 (0.00)	0.00 (0.00) 0.83 (0.02)
		3	0.58 (0.58) 0.27 (0.32)	8.46 (15.32)	4.72 (4.41)	3.08 (2.66) 0.65 (0.02)
		4	0.71 (0.67) 0.32 (0.34)	17.45 (35.87)	6.10 (6.17)	4.03 (3.75) 0.73 (0.03)
	Migr
		5	0.96 (0.71) 0.43 (0.34)	30.41 (56.68)	7.41 (6.18)	4.97 (3.76) 0.79 (0.03)
		6	1.19 (0.86) 0.50 (0.34) 98.80 (244.94)	10.09 (8.32)	6.74 (4.87) 0.82 (0.04)
		3	0.76 (0.69) 0.78 (0.33)	14.51 (18.40)	5.62 (4.99)	3.51 (2.93) 0.65 (0.02)
		4	1.02 (0.90) 0.76 (0.36)	31.76 (51.55)	7.64 (7.16)	4.58 (4.04) 0.74 (0.03)
	Migrr
		5	1.39 (1.04) 0.75 (0.35)	62.83 (91.89)	9.70 (7.88)	5.70 (4.25) 0.79 (0.03)
		6	1.72 (1.19) 0.70 (0.37) 180.35 (360.25)	12.56 (9.76)	7.35 (5.14) 0.82 (0.03)
		3	1.47 (1.99) 2.79 (1.10)	24.98 (9.85)	60.22 (242.88) 12.27 (6.55) 0.16 (0.12)
		4	1.36 (1.52) 3.84 (1.23)	34.36 (10.94)	44.71 (184.05) 12.95 (5.98) 0.13 (0.12)
	Chor
		5	1.41 (1.55) 4.63 (1.37)	41.17 (12.16)	44.06 (223.15) 12.68 (6.06) 0.12 (0.11)
		6	1.29 (1.38) 5.87 (1.66)	52.09 (14.77)	38.35 (215.27) 13.01 (6.01) 0.13 (0.12)

(

Table 8 .

 8 Metrics for Chiron traces. Cells contains mean and standard deviation in parentheses.

	Alg.	Spec	δ t	#Msgs	Data	S max	S crit	Conv E
		1	0.77 (0.42)	2.95 (0.00) 87.46 (0.00)	0.00 (0.00)	0.00 (0.00) 0.74 (0.00)
		2	1.00 (0.00)	2.95 (0.00) 87.46 (0.00)	0.00 (0.00)	0.00 (0.00) 0.74 (0.00)
		3	0.99 (0.10)	3.42 (0.02) 101.62 (1.00)	0.00 (0.00)	0.00 (0.00) 0.75 (0.00)
	Orch
		5	0.94 (0.24)	2.95 (0.00) 87.46 (0.00)	0.00 (0.00)	0.00 (0.00) 0.74 (0.00)
		15a	1.00 (0.00)	2.95 (0.00) 87.46 (0.00)	0.00 (0.00)	0.00 (0.00) 0.74 (0.00)
		15b	1.00 (0.00)	3.00 (0.01) 88.90 (0.16)	0.00 (0.00)	0.00 (0.00) 0.75 (0.00)
		1	1.66 (0.03)	0.02 (0.00)	0.52 (0.00)	8.00 (0.00)	2.03 (0.00) 0.74 (0.00)
		2	1.00 (0.00)	0.57 (0.00) 13.09 (0.10)	4.00 (0.00)	3.10 (0.01) 0.74 (0.00)
		3	1.86 (0.00)	0.88 (0.01) 70.23 (1.00)	13.00 (0.00)	9.76 (0.05) 0.75 (0.00)
	Migr
		5	1.67 (0.00)	0.02 (0.00)	0.52 (0.00)	8.00 (0.00)	2.03 (0.00) 0.74 (0.00)
		15a	1.00 (0.00)	0.97 (0.00) 10.71 (0.04)	4.00 (0.00)	3.90 (0.00) 0.74 (0.00)
		15b	1.00 (0.00)	1.00 (0.00) 19.36 (0.35)	9.02 (2.00)	7.00 (0.03) 0.75 (0.00)
		1	1.98 (0.00)	1.01 (0.01) 50.19 (0.33)	9.80 (1.37)	5.29 (0.07) 0.74 (0.00)
		2	1.81 (0.02)	1.01 (0.01) 212.55 (3.17)	12.00 (0.00)	5.82 (0.05) 0.74 (0.00)
		3	2.37 (0.03)	0.89 (0.02) 147.00 (3.97)	15.97 (0.22)	10.65 (0.09) 0.75 (0.01)
	Migrr
		5	1.98 (0.01)	1.01 (0.00) 50.16 (0.30)	9.80 (1.35)	5.28 (0.06) 0.74 (0.00)
		15a	1.99 (0.01)	1.01 (0.01) 83.80 (0.34)	8.64 (0.94)	4.91 (0.01) 0.74 (0.00)
		15b	2.50 (0.01)	1.00 (0.00) 136.05 (0.27)	16.86 (0.35)	11.41 (0.01) 0.75 (0.00)
		1	1.01 (0.00)	4.89 (0.00) 44.02 (0.00)	20.00 (0.00)	15.88 (0.32) 0.20 (0.01)
		2	133.86 (0.17) 2.95 (0.00) 26.52 (0.00) 2798.38 (211.11) 21.41 (0.74) 0.67 (0.02)
		3	1.22 (0.04)	4.40 (0.13) 39.64 (1.16)	23.65 (0.87)	18.18 (0.93) 0.33 (0.02)
	Chor
		5	1.01 (0.00)	4.89 (0.00) 44.02 (0.00)	20.00 (0.00)	15.85 (0.33) 0.20 (0.01)
		15a	1.00 (0.00)	0.98 (0.00)	8.84 (0.00)	10.00 (0.00)	9.25 (0.07) 0.47 (0.01)
		15b	116.52 (1.19) 2.00 (0.00) 18.00 (0.00) 3387.04 (316.16) 28.01 (1.13) 0.71 (0.00)

ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

We use the example from[START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF]: GF(a) ∧ ¬(GF(a)) (where GF(a) means that a should hold infinitely often) is monitorable, but its subformulas are both non-monitorable.ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October

See Section 10 for details.

We note that centralized monitoring of decentralized specifications makes little sense as there does not exist more than one monitor. ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

On an Intel(R) Core(TM) i7-6700HQ CPU, using 16GB RAM, and running openjdk 1.8.0_172, with ltl2mon 0.0.7. ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

This is also known as The Minimum Equivalent Expression problem[START_REF] Buchfuhrer | The Complexity of Boolean Formula Minimization[END_REF]. ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

This is not necessary, it makes the presentation clearer. For components sharing observations, we can encode their own ID in the atom to make it unique. ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

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

We note that in this case, we are not using any encoding (Atoms = AP).ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

We note that in the case of RV, traces are typically finite. ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

That is, they do not associate with the same atom different truth values. This is ensured by our assumption that the system and monitors do not send wrong information.ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

We note that this definition can be trivially extended to any encoding of such expressions that contains the monitor id.ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

The expressions leading to q ′ must all be also satisfiable. However, satisfiability is guaranteed as our automaton is normalized, see Remark 1. ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

While we use B 2 , this can be extended without loss of generality to an arbitrary set B f . ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

We note that t newkn is not necessarily equal to t kn + 1, as the EHE can determine a known state by simplification, and therefore skip intermediate states. We allow skipping states as it is reasonable for LTL 3 semantics, since final verdicts do not change for all suffixes.

verAt is simply a sel followed by a O(1) lookup. ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

Details of the generation is provided in Appendix E. ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

The THEMIS framework is further described and demonstrated in the 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].

Experiments provided in this paper are provided at[START_REF] El | THEMIS Article Artifact[END_REF], earlier experiments are provided at[START_REF] El | THEMIS Website[END_REF] ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

COLT provides a set of Open Source Libraries for High Performance Scientific and Technical Computing in Java.[13]

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

An observation is assigned ⊤ if the generated number is strictly greater than 0.5, and is otherwise ⊥. For the binomial distribution, we consider p = 0.3 the probability of obtaining ⊤. ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

In the case where the expected verdict is ?, the specification is designed to falsify the property, as such if no falsification is found, we will terminate with verdict ?.ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

We exclude specification 7 as we were unable to generate an automaton using ltl2mon for it. This is due to the formula either being too complex, or non-monitorable.ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

We note that since we broke down the metrics per specification, we have little variation in the data, for details and standard deviations refer to Appendix D. ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

For more details see Appendix E. ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

We use ltlfilt from[START_REF] Duret-Lutz | Manipulating LTL formulas using Spot 1.0[END_REF] with -boolean-to-isop to rewrite Boolean subformulas as irredundant sum of products.ACM Transactions on Software Engineering and Methodology, Vol. 1, No. 1, Article . Publication date: October 2019.

We note that, since the automaton is deterministic, there is a unique q i+1 such that q i+1 = ∆(q i , evt i+1 ).

We now consider the EHE operations to reach q i+1 from q i . q i = sel(I i , M i , i)

⇔ e = I i (i, q i ) with eval(e, M i ) = ⊤ (2) ∧ ∀q ′ i ∈ Q : q ′ i q i =⇒ eval(I i (i, q ′ i )) ⊤ (Prop. 4.8) ⇔ to(I i , i, q i+1 , ts i+1 ) = ⊤

(3) From the induction hypothesis, we know that I i (i, q i ) = ⊤, thus: to(I i ,i, q i+1 , ts i+1 ) = { ⟨q,e ′ ⟩ |δ (q,e ′ )=q ′ i +1 } (I i (i, q) ∧ ts i+1 (e ′ ))

=

{ ⟨q,e ′′ ⟩ |δ (q,e ′′ )=q ′ i +1 ∧q q i } (I i (i, q) ∧ ts i+1 (e ′′ ))

(ts i+1 (e ′′′ )).

We split the disjunction to consider the expressions that only come from state q i , we now show that one such expression evaluates to ⊤. We know from [START_REF]Patterns Project[END_REF], that one such expression can be taken in the automaton:

(4) is obtained using Lemma A.1 and idt(e) = e.

(5) follows from the disjunction. Using the same approach, we can show that ∀q ′ ∈ next(I i , i) : q ′ q i+1 =⇒ to(I i , i, q ′ , ts i+1 ) ⊤, since the first part of the conjunction does not evaluate to ⊤, and we know that the second part cannot evaluate to ⊤ by [START_REF]Patterns Project: List of specifications[END_REF]. Finally, to(I i , i, q i+1 , ts i+1 ) = ⊤ iff sel(I i+1 , M i+1 , i + 1) = q i . □

B CHIRON SYSTEM ATOMIC PROPOSITIONS

We broke down the Chiron system based on analysis of the examples provided in [START_REF] Matthew | Patterns in Property Specifications for Finite-State Verification[END_REF][START_REF]Chiron User Interface[END_REF], using the various specifications rewritten in [START_REF]Patterns Project: List of specifications[END_REF]. Table 6 displays various associations we used to generate our traces and events. Column C assigns an ID to the component. Column Name lists the logical module of the system we considered as a component. Column Original (AP) lists the atomic proposition provided by the authors of Chiron, and then edited by [START_REF] Matthew | Patterns in Property Specifications for Finite-State Verification[END_REF]. Column AP maps the atomic proposition to our traces. Column Comments includes comments on the atomic propositions.

• respawn id : B 2 specifies whether the monitor should respawn;

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. Before splitting a formula, it is necessary to determine the component that hosts its monitor. The component score is computed by counting the number of atomic propositions associated with a component in the subformula.

The chosen component is determined by the component with the highest score, using chc : LT L → C:

In order to setup the network of monitors, firstly the LTL expression is split into subformulas and the necessary monitors are generated to monitor each subformula. The tree of monitors is generated by recursively splitting the formula at the binary operators. We present the setup phase as a tree traversal of the LTL formula to generate the monitor network, merging nodes at each operator, which is a different flavor of the generation procedure in [START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF]. Given the two operands, we choose which operands remains in the host component, and (if necessary) which would be placed on a different component. Therefore, we add the constraint that at least one part of the LTL expression must still remain in the same component. Given two formulas φ and φ ′ and an initial base component c b we determine the two components that should host φ and φ ′ with the restriction that one of them is c b :

Algorithm 3 displays the procedure to split the formula. For each binary operator, we determine which of the operands needs to be hosted in a new component. The result is a tuple: ⟨root, N , E⟩ where:

• root is the root of the tree;

• N is the set of generated monitor data;

• E is the set of edges between the monitors.

Monitor data is a pair ⟨id, spec⟩ that represents the id of the monitor and the formula that it monitors.

• First, chc determines the host component where the root monitor resides.

• Second, the AST of the LT L formula is traversed using netx, which splits on binary operators.

Algorithm 3 Setting up the monitor tree

id ← 0 3:

⟨r oot , mons , edдes ⟩ ← netx(φ , id , c h )

5:

return ⟨{r oot } ∪ mons , edдes ⟩ 6: end procedure 7: procedure net x (φ , id c , c h ) 8:

m ← ⟨φ , id c ⟩ 10:

return ⟨m, ∅, ∅⟩

11:

else if φ matches op e then ▷ Unary Operator 12:

else if φ matches e op e ′ then 16: -Otherwise (1) We recurse on the side kept, to further split the formula;

(2) We recurse on the side split, with a new host and id;

(3) We merge the subnetworks by: (a) Generating the host monitor with the formula resulting from the recursion; (b) Connecting the split branch's root monitor to the current host monitor; (c) Adding the split branch's root monitor to the set of additional monitors; (d) Merging the set of additional monitors and edges from both branches. Once the monitor data tree is created, monitors are created accordingly, generating an automaton for the subformula, where some of its atomic propositions have been replaced with monitor ids. Each monitor is initialized with the refs and corefs set based on the edges setup.

Remark 2 (Compacting the network). The monitor network can further be compacted as follows; monitors with the same subformula are merged into one, and their refs and corefs will be the result of the set union. However, one or more merged monitor will have to replace all occurrences of the id of the other monitors in all subformulas of all monitors.