Andreas Bauer

Yliès Falcone

Decentralised LTL Monitoring

Andreas Bauer • Yliès Falcone the date of receipt and acceptance should be inserted later Abstract Users wanting to monitor distributed or component-based systems often perceive them as monolithic systems which, seen from the outside, exhibit a uniform behaviour as opposed to many components displaying many local behaviours that together constitute the system's global behaviour. This level of abstraction is often reasonable, hiding implementation details from users who may want to specify the system's global behaviour in terms of a linear-time temporal logic (LTL) formula. However, the problem that arises then is how such a specification can actually be monitored in a distributed system that has no central data collection point, where all the components' local behaviours are observable. In this case, the LTL specification needs to be decomposed into sub-formulae which, in turn, need to be distributed amongst the components' locally attached monitors, each of which sees only a distinct part of the global behaviour.

The main contribution of this paper is an algorithm for distributing and monitoring LTL formulae, such that satisfaction or violation of specifications can be detected by local monitors alone. We present an implementation and show that our algorithm introduces only a negligible delay in detecting satisfaction/violation of a specification. Moreover, our practical results show that the communication overhead introduced by the local monitors is generally lower than the number of messages that would need to be sent to a central data collection point. Furthermore, our experiments strengthen the argument that the algorithm performs well in a wide range of different application contexts, given by different system/communication topologies and/or system event distributions over time.

Introduction

Much work has been done on monitoring systems w.r.t. formal specifications such as lineartime temporal logic (LTL) [START_REF] Pnueli | The temporal logic of programs[END_REF] formulae. For this purpose, a system is thought of more or less as a "black box", and some (automatically generated) monitor observes its outside visible behaviour in order to determine whether or not the runtime behaviour satisfies an LTL formula. Applications include monitoring programs written in Java or C (cf. [START_REF] Seyster | Aspect-oriented instrumentation with GCC[END_REF][START_REF] Patrick | Runtime verification with the RV System[END_REF]) or abstract Web services (cf. [START_REF] Hallé | Runtime verification for the web-a tutorial introduction to interface contracts in web applications[END_REF]) to name just a few.

From a system designer's point of view, who defines the overall behaviour that a system has to adhere to, this "black box" view is perfectly reasonable. For example, most modern cars have the ability to issue a warning if a passenger (including the driver) is not wearing a seat belt after the vehicle has reached a certain speed. One could imagine using a monitor to help issue this warning based on the following LTL formalisation, which captures this abstract requirement: ϕ = G speed low ∨ ((pressure sensor 1 high ⇒ seat belt 1 on) ∧ . . . ∧ (pressure sensor n high ⇒ seat belt n on))

The formula ϕ asserts that, at all times, when the car has reached a certain speed, and the pressure sensor in a seat i ∈ [1, n] detects that a person is sitting in it (pressure sensor i high), it has to be the case that the corresponding seat belt is fastened (seat belt i on).

Moreover, one can build a monitor for ϕ, which receives the respective sensor values and is able to assert whether or not these values constitute a violation-but, only if some central component exists in the car's network of components, which collects these sensor values and consecutively sends them to the monitor as input! When such a central observation point exists in the system, we refer to the setting as centralised monitoring.

In many real-world scenarios, such as the automotive one, this is an unrealistic assumption mainly for economic reasons, but also because the communication on a car's bus network has to be kept as minimal as possible. Therefore, one cannot continuously send unnecessary sensor information on a bus that is shared by critical applications where low latency is paramount (cf. [START_REF] Gunzert | Component-based development and verification of safety critical software for a brake-by-wire system with synchronous software components[END_REF][START_REF] Lukasiewycz | FlexRay schedule optimization of the static segment[END_REF]). In other words, in these scenarios, one has to monitor such a requirement not based on a single behavioural trace, assumed to be collected by some global sensor, but based on the many partial behavioural traces of the components which make up the actual system. When the requirement is given in terms of an LTL formula, we refer to this setting as decentralised LTL monitoring. The requirement could also be given in terms of an automaton, for example. Such other specifications, however, are not subject of this paper.

The main constraint that decentralised LTL monitoring addresses is the lack of a global sensor and a central decision making point asserting whether the system's behaviour has violated or satisfied a specification. We already pointed out that, from a practical point of view, a central decision making point (i.e., global sensor) would require all the individual components to continuously send events over the network, and thereby negatively affecting response time for other potentially critical applications on the network. Moreover, from a theoretical point of view, a central observer (resp. global sensor) basically resembles classical LTL monitoring, where the decentralised nature of the system under scrutiny does not play a role. Arguably, there exist many real-world component-based applications, where the monitoring of an LTL formula can be realised via global sensors or central decision making points, e.g., when network latency and criticality do not play an important role. However, here we want to focus on those cases where there exists no global trace, no central decision making point, and where the goal is to keep the communication, required for monitoring the LTL formula, as low as possible.

In the decentralised setting, we assume that the system under scrutiny consists of a set of components C = {C 1 , C 2 , . . . , Cn}, communicating on a synchronous bus acting as global clock. Each component has a local set of atomic propositions AP i , emits events synchronously, and has a local monitor attached to it. Moreover, we demand for all i, j ≤ n with i = j that AP i ∩ AP j = ∅ holds, i.e., atomic propositions are local w.r.t. the components. 1 The set of all events is Σ 1 ∪ Σ 2 ∪ . . . ∪ Σn, where Σ i = 2 AP i is the set of events visible to the monitor at component C i . The global LTL formula, on the other hand, is specified over a set of propositions, AP = ∪ i∈ [1,n] AP i , and has events in Σ = 2 AP . Note that, in general, Σ = Σ 1 ∪ Σ 2 ∪ . . . ∪ Σn.

Remark 1 At first, the synchronous bus may seem an overly stringent constraint imposed by our setting. However, it is by no means unrealistic, since in many real-world systems, especially critical ones, communication occurs synchronously. For example, the FlexRay bus protocol, used for safety-critical systems in the automotive domain, allows synchronous communication (cf. [START_REF] Pop | Timing analysis of the FlexRay communication protocol[END_REF][START_REF] Gunzert | Component-based development and verification of safety critical software for a brake-by-wire system with synchronous software components[END_REF][START_REF] Miller | Software model checking takes off[END_REF]). Moreover, experts predict "that the data volume on FlexRay buses will increase significantly in the future" [START_REF] Lukasiewycz | FlexRay schedule optimization of the static segment[END_REF]Sec. 2], promoting techniques to minimise the number of used communication slots. Hence, one could argue that synchronous distributed systems such as FlexRay, in fact, motivate the proposed decentralised monitoring approach. What is more, conceptually similar bus systems are also playing an increasing role in industrial automation facilities, where individual production systems (e.g., robots, conveyors, cranes, etc.) are either interconnected on synchronous fieldbusses for the transmission of control signals, or share a common Programmable Logic Controller (PLC), for the exchange of a safety "heart-beat" signal, for example (cf. [START_REF] Pigan | Automating with PROFINET: Industrial Communication Based on Industrial Ethernet[END_REF]). Typical such fieldbus systems include EtherCAT, ProfiBus, ProfiNet (also known as "Industrial Ethernet", cf. [START_REF] Felser | Real-time ethernet-industry prospective[END_REF]), and will include the upcoming standard for Time Sensitive Networking (TSN) by the IEEE's 802 working group (sometimes also referred to as "Deterministic Ethernet" (cf. IEEE802.1 or [START_REF] Serna | Analysis of deterministic ethernet scheduling for the industrial internet of things[END_REF] for an overview). One should stress again, however, that the results in this paper do not directly target FlexRay or any other specific (field-) bus system as the monitoring approach, which is being developed here, is generic. Now, let as before ϕ be an LTL formula formalising a requirement over the system's global behaviour. Then every local monitor, M i , will at any time, t, monitor its own LTL formula, ϕ t i , w.r.t. a partial behavioural trace, u i . Let us use u i (m) to denote the (m + 1)-th event in a trace u i , and u = (u 1 , u 2 , . . . , un) for the global trace, obtained by pair-wise parallel composition of the partial traces, each of which at time t is of length t + 1 (i.e., u = u 1 (0) ∪ . . . ∪ un(0) • u 1 (1) ∪ . . . ∪ un(1) • . . . • u 1 (t) ∪ . . . ∪ un(t), a sequence of union sets). Note that from this point forward we will use u only when, in a given context, it is important to consider a global trace. However, when the particular type of trace (i.e., partial or global) is irrelevant, we will simply use u, u i , etc. We also shall refer to partial traces as local traces due to their locality to a particular monitor in the system.

The decentralised monitoring algorithm is based on formula rewriting (also known as progression or derivation) which has been used for centralised monitoring, as seen for instance in [START_REF] Havelund | Monitoring programs using rewriting[END_REF][START_REF] Grigore | Rewriting-based techniques for runtime verification[END_REF][START_REF] Barringer | Rule systems for run-time monitoring: from Eagle to RuleR[END_REF]. The algorithm evaluates the global trace u by considering the locally observed traces u i , i ∈ [1, n], in separation. In particular, it exhibits the following properties.

• If a local monitor yields

ϕ t i = ⊥ (resp. ϕ t i = ) on some component C i by observing u i , it implies that uΣ ω ⊆ Σ ω \ L(ϕ) (resp. uΣ ω ⊆ L(ϕ))
holds where L(ϕ) is the set of infinite sequences in Σ ω described by ϕ. That is, a locally observed violation (resp. satisfaction) is, in fact, a global violation (resp. satisfaction). Or, in other words, u is a bad (resp. good) prefix for ϕ.

• If centralised monitoring by progression would detect that uΣ ω ⊆ Σ ω \ L(ϕ) (resp.

uΣ ω ⊆ L(ϕ)), one of the local monitors on some component C i yields ϕ t i = ⊥ (resp.

ϕ t i = ), t ≥ t,
for an observation u i , an extension of u i , the local observation of u on C i , because of some latency induced by decentralised monitoring, as we shall see. However, in order to allow for the local detection of global violations (and satisfactions), monitors must be able to communicate, since their traces are only partial w.r.t. the global behaviour of the system. Therefore, our second objective is to monitor with significantly reduced communication overhead (in comparison with a centralised solution where at any time, t, all n monitors send the observed events to a central decision making point).

At this point, one should also add that this article constitutes an extended version of a conference paper. In comparison to [START_REF] Bauer | Decentralised LTL monitoring[END_REF], its most noteworthy additions are as follows: this paper now contains a complete formalisation of our monitoring algorithm (Sec. 6.1) as well as a proof of its correctness based on said formalisation (Sec. 6.2). Based on this formalisation, we have added a number of formal statements that help clarify the relationship between the central and the decentralised case, all of which contain full proofs. Yet we have decided to add some proofs to a separate appendix for improved readability of the paper (Appendix A). Also, we have undertaken further practical experiments with our implementation of the monitoring algorithm (Sec. 7), in order to evaluate different system topologies as well as distributions of system events. Both are interesting parameters to consider, since the experiments strengthen our argument that the monitoring algorithm performs well in a wide range of application contexts and not just those we have previously shown.

Outline. The rest of this paper is structured as follows. In the next section, we introduce basic notions and notation. LTL monitoring via formula rewriting (progression), a central concept to our paper, is discussed in Sec. 3. In Sec. 4, we lift it to the decentralised setting. The semantics induced by decentralised LTL monitoring is outlined in Sec. 5, whereas Sec. 6 details on how the local monitors operate in this setting and gives a concrete algorithm for this purpose. Experimental results, showing the feasibility of our approach, are presented in Sec. 7. Section 8 concludes and gives pointers to related work. Appendix A contains detailed, formal proofs of theorems.

Preliminaries

Each component of the system emits events at discrete time instances. An event σ is a set of actions denoted by some atomic propositions from the set AP , i.e., σ ∈ 2 AP . We denote 2 AP by Σ and call it the alphabet (of system events).

As our system operates under the perfect synchrony hypothesis (cf. [START_REF] Jantsch | Modeling Embedded Systems and SoC's: Concurrency and Time in Models of Computation[END_REF]), we assume that its components communicate with each other in terms of sending and receiving messages (which, for the purpose of easier presentation, can also be encoded by actions) at discrete instances of time, which are represented using identifier t ∈ N ≥0 . Under this hypothesis, it is assumed that neither computation nor communication take time. In other words, at each time t, a component may receive up to n -1 messages and dispatch up to 1 message, which in the latter case will always be available at the respective recipient of the messages at time t + 1. Note that these assumptions extend to the components' monitors, which operate and communicate on the same synchronous bus. The hypothesis of perfect synchrony essentially abstracts away implementation details of how long it takes for components or monitors to generate, send, or receive messages. As indicated in the introduction, this is a common hypothesis for certain types of systems, which can be designed and configured (e.g., by choosing an appropriate duration between time t and t + 1) to not violate this hypothesis (cf. [START_REF] Jantsch | Modeling Embedded Systems and SoC's: Concurrency and Time in Models of Computation[END_REF]).

We use a projection function Π i to restrict atomic propositions or events to the local view of monitor M i , which can only observe those of component C i . For atomic propositions, Π i : 2 AP → 2 AP and we denote AP i = Π i (AP ) for i ∈ [1, n]. For events, Π i : 2 Σ → 2 Σ and we denote Σ i = Π i (Σ) for i ∈ [1, n]. We also assume ∀i, j ≤ n. i = j ⇒ AP i ∩AP j = ∅ and consequently ∀i, j ≤ n. i = j ⇒ Σ i ∩ Σ j = ∅. Seen over time, each component C i produces a trace of events, also called its behaviour, which for t time steps is encoded as

u i = u i (0) • u i (1) • . . . • u i (t -1) with ∀t < t. u i (t ) ∈ Σ i .
Finite traces over an alphabet Σ are elements of the set Σ * and are typically encoded by u, u , . . ., whereas infinite traces over Σ are elements of the set Σ ω and are typically encoded by w, w , . . . The set of all traces is given by the set Σ ∞ = Σ * ∪Σ ω . The set Σ * \{ } is noted Σ + . The finite or infinite sequence w t is the suffix of the trace w ∈ Σ ∞ , starting at time t, i.e., w t = w(t) • w(t + 1) • . . . •. The system's global behaviour, u = (u 1 , u 2 , . . . , un) can now be described as a sequence of pair-wise unions of the local events in component traces, each of which at time t is of

length t + 1 i.e., u = u(0) • . . . • u(t).
We monitor a system w.r.t. a global specification, expressed as an LTL [START_REF] Pnueli | The temporal logic of programs[END_REF] formula, that does not state anything about its distribution or the system's architecture. Formulae of LTL can be described using the following grammar:

ϕ ::= p | (ϕ) | ¬ϕ | ϕ ∨ ϕ | Xϕ | ϕUϕ,
where p ∈ AP . Additionally, we allow the following operators, each of which is defined in terms of the above ones:

= p ∨ ¬p, ⊥ = ¬ , ϕ 1 ∧ ϕ 2 = ¬(¬ϕ 1 ∨ ¬ϕ 2 ), Fϕ = Uϕ,
and Gϕ = ¬F(¬ϕ). The operators typeset in bold are the temporal operators. Formulae without temporal operators are called state formulae. We describe the set of all LTL formulae over AP by the set LTL(AP), or just LTL when the set of atomic propositions is clear from the context or does not matter. For reasons of selfcontainedness, we also recall the formal semantics of LTL in detail as follows.

Definition 1 ([17])

The semantics of LTL is defined w.r.t. infinite traces. Let for this purpose w ∈ Σ ω be an infinite trace and i ∈ N ≥0 . Satisfaction of an LTL formula by w at time i is inductively defined as follows.

w i |= p ⇔ p ∈ w(i), for any p ∈ AP w i |= ¬ϕ ⇔ w i |= ϕ w i |= ϕ 1 ∨ ϕ 2 ⇔ w i |= ϕ 1 ∨ w i |= ϕ 2 w i |= Xϕ ⇔ w i+1 |= ϕ w i |= ϕ 1 Uϕ 2 ⇔ ∃k ∈ [i, ∞[. w k |= ϕ 2 ∧ ∀l ∈ [i, k[. w l |= ϕ 1
When w 0 |= ϕ holds, we also write w |= ϕ to denote the fact that w is a logical model for ϕ. Finally, for some ϕ ∈ LTL(AP ), L(ϕ) ⊆ Σ ω denotes the individual models of ϕ (i.e., set of traces). A set L ⊆ Σ ω is also called a language (over Σ).

Monitoring LTL formulae by progression

Central to our monitoring algorithm is the notion of good and bad prefixes for an LTL formula or, to be more precise, for the language it describes:

Definition 2 Let L ⊆ Σ ω be a language. The set of all good prefixes (resp. bad prefixes) of L is given by good(L) (resp. bad(L)) and defined as follows:

good(L) = {u ∈ Σ * | u • Σ ω ⊆ L}, bad(L) = {u ∈ Σ * | u • Σ ω ⊆ Σ ω \ L}.
We will shorten good(L(ϕ)) (resp. bad(L(ϕ))) to good(ϕ) (resp. bad(ϕ)).

Although there exist a myriad of different approaches to monitoring LTL formulae, based on various finite-trace semantics (cf. [START_REF] Bauer | Comparing LTL semantics for runtime verification[END_REF]), one valid way of looking at the monitoring problem for some formula ϕ ∈ LTL is the following: The monitoring problem of ϕ ∈ LTL is to devise an efficient monitoring algorithm which, in a stepwise manner, receives events from a system under scrutiny and states whether or not the trace observed so far constitutes a good or a bad prefix of L(ϕ). One monitoring approach along those lines is described in [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF]. We review an alternative monitoring procedure based on formula rewriting, which is also known as formula progression, or just progression in the domain of planning with temporally extended goals (cf. [START_REF] Bacchus | Planning for temporally extended goals[END_REF]).

Progression splits a formula into a formula expressing what needs to be satisfied by the current observation and a new formula (referred to as a future goal or obligation), which has to be satisfied by the trace in the future. As progression plays a crucial role in decentralised LTL monitoring, we recall its definition for the full set of LTL operators, instead of only the expressively complete set as given in Definition 1.

Definition 3 Let ϕ, ϕ 1 , ϕ 2 ∈ LTL, and σ ∈ Σ be an event. Then, the progression function P : LT L × Σ → LT L is inductively defined as follows.

P (p ∈ AP, σ) = if p ∈ σ, ⊥ otherwise P ( , σ) = P (⊥, σ) = ⊥ P (¬ϕ, σ) = ¬P (ϕ, σ) P (Xϕ, σ) = ϕ P (ϕ 1 ∨ ϕ 2 , σ) = P (ϕ 1 , σ) ∨ P (ϕ 2 , σ) P (ϕ 1 Uϕ 2 , σ) = P (ϕ 2 , σ) ∨ P (ϕ 1 , σ) ∧ ϕ 1 Uϕ 2 P (Gϕ, σ) = P (ϕ, σ) ∧ G(ϕ) P (Fϕ, σ) = P (ϕ, σ) ∨ F(ϕ)
Note that monitoring using rewriting with similar rules as above has been described, for example, in [START_REF] Havelund | Monitoring programs using rewriting[END_REF][START_REF] Grigore | Rewriting-based techniques for runtime verification[END_REF][START_REF] Barringer | Rule systems for run-time monitoring: from Eagle to RuleR[END_REF], although not necessarily with the same finite-trace semantics in mind that we are discussing in this paper. Informally, the progression function "mimics" the LTL semantics on an event σ, as it is stated by the following lemmas.

Lemma 1 Let ϕ be an LTL formula, σ an event and w an infinite trace, we then have σ • w |= ϕ ⇐⇒ w |= P (ϕ, σ).

Proof By structural induction on LTL formulae (see Appendix A.1).

Lemma 2 Let ϕ be an LTL formula, σ an event, we then have if P (ϕ, σ) = , then σ ∈ good(ϕ), if P (ϕ, σ) = ⊥, then σ ∈ bad(ϕ).

Proof By structural induction on LTL formulae and using Lemma 1 (see Appendix A.1).

Let us now get back to [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF], which introduces a finite-trace semantics for LTL monitoring called LTL 3 . It is captured by the following definition.

Definition 4 Let u ∈ Σ * , the satisfaction relation of LTL 3 , |= 3 : Σ * × LTL → B 3 , with B 3 = { , ⊥, ?}, is defined as follows. u |= 3 ϕ =    if u ∈ good(ϕ), ⊥ if u ∈ bad(ϕ), ? otherwise.
Based on this definition, it now becomes clear how progression could be used as a somewhat naïve monitoring algorithm for a 3-valued finite-trace semantics akin to LTL 3 : Definition 5 Given a formula ϕ ∈ LTL and a trace u = u(0) • . . . • u(t) ∈ Σ + , the application of extended progression function P to ϕ and u is obtained by t + 1 consecutive applications of the progression function of ϕ on u: P(ϕ, u(0) • . . . • u(t)) = P(ϕ, u) = P (. . . (P (ϕ, u(0)), . . . , u(t)))).

Moreover, P(ϕ, ) = ϕ. The semantic relation of (centralised) monitoring by progression,

|= C : Σ * × LTL → B 3 , is defined as follows. u |= C ϕ =    if P(ϕ, u) = , ⊥ if P(ϕ, u) = ⊥, ? otherwise.
For the sake of readability, in the remainder, we overload the notation of the progression function on events to traces, i.e., P(ϕ, u) is denoted P (ϕ, u).

Theorem 1 Let ϕ ∈ LTL and u ∈ Σ * , then u |= C ϕ = /⊥ =⇒ u |= 3 ϕ = /⊥, and u |= 3 ϕ = ? =⇒ u |= C ϕ = ?.
Proof The theorem can be shown by an induction based on Definitions 2-4 and Lemma 2. The formal proof can be found in Appendix A.1.

However, in comparison with the monitoring procedure for LTL 3 , described in [START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF], the algorithm that is implied by this theorem has the disadvantage that the formula, which is being progressed, may grow in size relative to the number of events. It should be added though that in practice, the use of some simplification rules in the progression function normally prevents this problem from occurring.

Remark 2 As progression is purely syntax-driven, one can construct pathological cases that "defeat" it, if one does not take precautions [START_REF] Kupferman | Model checking of safety properties[END_REF][START_REF] Sen | Generating Optimal Linear Temporal Logic Monitors by Coinduction[END_REF]. For example, consider ϕ = XX . As ϕ is a tautology, every prefix of length one is already a good prefix for ϕ, however, P (ϕ, σ) = X for any σ ∈ Σ, meaning that progression would detect the good prefix with a delay of one extra step. Should the tautology be syntactically more involved than that, e.g., ϕ = G( U(Fb ∨ G¬b)), then progression may fail to detect it completely; in this example, progression would fail to detect it unless b became true along the trace. Arguably, however, these pathological cases are more of theoretical than practical merit and seldom occur in real specifications as they usually contain redundancy. In our experiments, in which we generated literally thousands of LTL specifications, we did not encounter this problem once, for example. Moreover, one could check the syntactic closure of a given specification for tautologies, prior to monitoring without any detriment to runtime performance. Checking each such formula ϕ of the syntactic closure would correspond to solving a PSpace-complete problem (cf. [START_REF] Sistla | The complexity of propositional linear temporal logics[END_REF]).

Remark 2 also indicates that the other direction of Theorem 1 does not hold.

Decentralised progression

Conceptually, a monitor, M i , attached to component C i , which observes events over Σ i ⊆ Σ, is a rewriting engine that accepts as input an event σ ∈ Σ i , and an LTL formula ϕ, and then applies LTL progression rules. Additionally at each time t, in our n-component architecture, a monitor can send a message and receive up to n -1 messages in order to communicate with the other monitors in the system, using the same synchronous bus that the system's components communicate on. The purpose of these messages is to send future or even past obligations to other monitors, encoded as LTL formulae. In a nutshell, a formula is sent by some monitor M i , whenever the most urgent outstanding obligation imposed by M i 's current formula at time t, ϕ t i , cannot be checked using events from Σ i alone. Intuitively, the urgency of an obligation is defined by the occurrences (or lack of) certain temporal operators in it. For example, in order to satisfy p ∧ Xq, a trace needs to start with p, followed by a q. Hence, the obligation imposed by the subformula p can be thought of as "more urgent" than the one imposed by Xq. A more formal definition is given later in this section.

When progressing an LTL formula, e.g., in the domain of planning to rewrite a temporally extended LTL goal during plan search, the rewriting engine, which implements the progression rules, will progress a state formula p ∈ AP , with an event σ such that p / ∈ σ, to ⊥, i.e., P (p, ∅) = ⊥ (see Definition 3). However, doing this in the decentralised setting, could lead to wrong results. Hence, we need to make a distinction as to why p / ∈ σ holds locally, and then to progress accordingly. Consequently, the progression rule for atomic propositions is simply adapted by parameterising it with a local set of atomic propositions AP i :

P (p, σ, AP i ) =    if p ∈ σ, ⊥ if p / ∈ σ ∧ p ∈ AP i , Xp otherwise, (1)
where for every w ∈ Σ ω and j > 0, we have w j |= Xϕ if and only if w j-1 |= ϕ. In other words, X is the dual to the X-operator, sometimes referred to as the "previouslyoperator" in past-time LTL (cf. [START_REF] Lichtenstein | The glory of the past[END_REF]). To ease presentation, the formula X m ϕ is a short for m XX . . . X ϕ.

Our operator is somewhat different to the standard use of X: it can only precede an atomic proposition or an atomic proposition which is preceded by further Xoperators. Hence, the restricted use of the X-operator does not give us the full flexibility (or succinctness gains [START_REF] Markey | Temporal logic with past is exponentially more succinct, concurrency column[END_REF]) of past-time LTL. Using the X-operator, let us now formally define the urgency of a formula ϕ using a pattern matching as follows:

Definition 6 Let ϕ be an LTL formula, and Υ : LTL → N ≥0 be an inductively defined function assigning a level of urgency to an LTL formula as follows.

Υ (ϕ) = match ϕ with ϕ 1 ∨ ϕ 2 | ϕ 1 ∧ ϕ 2 → max(Υ (ϕ 1 ), Υ (ϕ 2 )) | Xϕ → 1 + Υ (ϕ ) | → 0.
A formula ϕ is said to be more urgent than formula ψ, if and only if Υ (ϕ) > Υ (ψ) holds. A formula ϕ where Υ (ϕ) = 0 holds is said to be not urgent.

Obviously, the above modification to the progression rules has the desired effect: If p ∈ σ, then nothing changes, otherwise if p / ∈ σ, we return Xp in case that the monitor M i cannot observe p at all, i.e., in case that p / ∈ AP i holds. This effectively means, that M i cannot decide whether or not p occurred, and will therefore turn the state formula p into an obligation for some other monitor to evaluate rather than produce a truth-value. Of course, the downside of rewriting future goals into past goals that have to be processed further, is that violations or satisfactions of a global goal will usually be detected after they have occurred. However, since there is no central observer which records all events at the same time, the monitors need to communicate their respective results to other monitors, which, on a synchronous bus, occupies one or more time steps, depending on how often a result needs to be passed on until it reaches a monitor which is able to actually state a verdict. We shall later give an upper bound on these communication times, and show that our decentralised monitoring framework does not introduce any additional delay due to communication under the given assumptions (see Theorem 2).

Example 1 Let us assume we have a decentralised system consisting of components A, B, C, s.t. AP A = {a}, AP B = {b}, and AP C = {c}, and that a formula ϕ = F(a ∧ b ∧ c) needs to be monitored in a decentralised manner. Let us further assume that, initially,

ϕ 0 A = ϕ 0 B = ϕ 0 C = ϕ.
Let σ = {a, b} be the system event at time 0; that is,

M A observes Π A (σ) = {a} (resp. Π B (σ) = {b}, Π C (σ) = ∅ for M B and M C
) when σ occurs. The rewriting that takes place in all three monitors to generate the next local goal formula, using the modified set of rules, and triggered by σ, is as follows:

ϕ 1 A = P (ϕ, {a}, {a}) = P (a, {a}, {a}) ∧ P (b, {a}, {a}) ∧ P (c, {a}, {a}) ∨ ϕ = Xb ∧ Xc ∨ ϕ, ϕ 1
B = P (ϕ, {b}, {b}) = P (a, {b}, {b}) ∧ P (b, {b}, {b}) ∧ P (c, {b}, {b}) ∨ ϕ = Xa ∧ Xc ∨ ϕ, ϕ 1
C = P (ϕ, ∅, {c}) = P (a, ∅, {c}) ∧ P (b, ∅, {c}) ∧ P (c, ∅, {c}) ∨ ϕ = Xa ∧ Xb ∧ ⊥ ∨ ϕ = ϕ.
But we have yet to define progression for past goals: For this purpose, each monitor has local storage to keep a bounded number of past events. The event that occurred at time t -k is referred as σ(-k). On a monitor observing Σ i , the progression of a past goal X m ϕ, at time t ≥ m, is defined as follows:

P (X m ϕ, σ, AP i ) =    if ϕ = p for some p ∈ AP i ∩ Π i (σ(-m)), ⊥ if ϕ = p for some p ∈ AP i \ Π i (σ(-m)), X m+1 ϕ otherwise, (2)
where, for i ∈ [1, n], Π i is the projection function associated to each monitor M i , respectively. Note that since we do not allow X for the specification of a global system monitoring property, our definitions will ensure that the local monitoring goals, ϕ t i , will never be of the form XXXp, which is equivalent to a future obligation, despite the initial X. In fact, our rules ensure that a formula preceded by the X-operator is either an atomic proposition, or an atomic proposition which is preceded by one or many X-operators. Hence, in rule (2), we do not need to consider any other cases for ϕ.

Semantics

In the previous example, we can clearly see that monitors M A and M B cannot determine whether or not σ, if interpreted as a trace of length 1, is a good prefix for the global goal formula ϕ. 2 Monitor M C on the other hand did not observe an action c and, therefore, is the only monitor after time 0, which knows that σ is not a good prefix and that, as before, after time 1, ϕ is the goal that needs to be satisfied by the system under scrutiny. Intuitively, the other two monitors know that if their respective past goals were satisfied, then σ would be a good prefix, but in order to determine this, they need to send and receive messages to and from each other, containing LTL obligations.

Before we outline how this is done in our setting, let us discuss the semantics, obtained from this decentralised application of progression. We already said that monitors detect good and bad prefixes for a global formula; that is, if a monitor's progression yields (resp. ⊥), then the trace seen so far is a good (resp. bad) prefix, and if neither monitor yields a Boolean truth-value as verdict, we keep monitoring. The latter case indicates that, so far, the trace is neither a good nor a bad prefix for the global formula.

Definition 7 Let C = {C 1 , . . . , Cn} be the set of system components, ϕ ∈ LTL be a global goal, and M = {M 1 , . . . , Mn} be the set of component monitors. Further,

let u = u 1 (0) ∪ . . . ∪ un(0) • u 1 (1) ∪ . . . ∪ un(1) • . . . • u 1 (t) ∪ . . . ∪ un(t) be the global behavioural trace, at time t ∈ N ≥0 . If for some component C i , with i ≤ n, containing a local obligation ϕ t i , M i reports P (ϕ t i , u i (t), AP i ) = (resp. ⊥), then u |= D ϕ = (resp. ⊥). Otherwise, u |= D ϕ = ?.
By |= D we denote the satisfaction relation on finite traces in the decentralised setting to differentiate it from LTL 3 , standard LTL which is defined on infinite traces, and the satisfaction relation in the centralised setting. Obviously, |= 3 , |= C , and |= D yield values from the same truth-domain. However, the semantics are not equivalent, since the modified progression function used in the above definition sometimes rewrites a state formula into an obligation concerning the past rather than returning a conclusive verdict. On the other hand, in the case of a one-component system (i.e., all propositions of a formula can be observed by a single monitor), the definition of |= D matches the definition of |= C and Theorem 1.

Communication and decision making

Let us now describe the communication mechanism that enables local monitors to determine whether a trace is a good or a bad prefix. Recall that each monitor only sees a projection of an event to its locally observable set of actions, encoded as a set of atomic propositions, respectively.

Generally, at time t, when receiving an event σ, a monitor, M i , will progress its current obligation, ϕ t i , into P (ϕ t i , σ, AP i ), and send the result to another monitor, M j =i , whenever the most urgent obligation, ψ ∈ sus(P (ϕ t i , σ, AP i )), is such that Prop(ψ) ⊆ (AP j ) holds, where sus(ϕ) is the set of urgent subformulae of ϕ and Prop : LTL → 2 AP yields the set of occurring propositions of an LTL formula. Definition 8 Function sus : LTL → 2 LTL is inductively defined as follows:

sus(ϕ) = match ϕ with ϕ 1 ∨ ϕ 2 | ϕ 1 ∧ ϕ 2 → sus(ϕ 1 ) ∪ sus(ϕ 2 ) | ¬ϕ → sus(ϕ ) | Xϕ → {Xϕ } | → ∅
The set sus(ϕ) contains the past sub-formulae of ϕ, i.e., sub-formulae starting with a future temporal operator are discarded. It uses the fact that, in decentralised progression, Xoperators are only introduced in front of atomic propositions or other X-operators. Thus, only the cases mentioned explicitly in the pattern matching need to be considered. Moreover, for formulae of the form Xϕ , i.e., starting with an X-operator, it is not necessary to apply sus to ϕ because ϕ is bound to be of the form X d p with d ≥ 0 and p ∈ AP , and does not contain more urgent formulae than Xϕ . Note that if there are several equally urgent obligations for distinct monitors, then M i sends the formula to only one of the corresponding monitors according to a priority order between monitors. This order ensures that the delay induced by evaluating the global system specification in a decentralised fashion is bounded, as we shall see in Theorem 2. For simplicity in the following, for a set of component monitors M = {M 1 , . . . , Mn}, the sending order is the natural order on the interval [1, n]. This choice of the local monitor to send the obligation is encoded through the function Mon : M × 2 AP → M. For a monitor M i ∈ M and a set of atomic propositions AP ∈ 2 AP , Mon(M i , AP ) is the monitor M jmin s.t. j min is the smallest integer in [1, n] s.t. there is a monitor for an atomic proposition in AP . Formally:

Mon(M i , AP ) = j min = min{j ∈ [1, n] \ {i} | AP ∩ AP j = ∅}. Once M i has sent P (ϕ t i , σ, AP i ), it sets ϕ t+1 i = #
, where # / ∈ AP is a special symbol for which we define progression by

P (#, σ, AP i ) = #, (3)
and ∀ϕ ∈ LTL. ϕ ∧ # = ϕ. Moreover, whenever M i receives a formula, ϕ j =i , sent from a monitor M j , it will add the new formula to its existing obligation, i.e., its current obligation ϕ t i will be replaced by the conjunction ϕ t i ∧ ϕ j =i . Should M i receive further obligations from other monitors but j, it will add each new obligation as an additional conjunct in the same manner.

Let us now summarise the above steps in the form of an explicit algorithm that describes how the local monitors operate and make decisions.

Algorithm L (Local Monitor). Let ϕ be a global system specification, and M = {M 1 , . . . , Mn} be the set of component monitors.

= return , if ϕ t+1 i = ⊥ return ⊥. L6. [Communicate.] Let Ψ ⊆ sus(ϕ t+1 i ) be the set of most urgent obligations of ϕ t+1 i determined with function Υ (cf. Definition 6). Send ϕ t+1 i to monitor Mon(M i , ∪ ψ∈Ψ Prop(ψ)).
L7. [Replace goal.] If in step L6 a message was sent at all, set ϕ t+1 i := #. Then go back to step L1.

The input to the algorithm, σ, will usually resemble the latest observation in a consecutively growing trace,

u i = u i (0) • . . . • u i (t), i.e., σ = u i (t). We then have that σ |= D ϕ t i (i.e., the algorithm returns ) implies that u |= D ϕ holds (resp. for σ |= D ϕ t i ). Table 1: Decentralised progression of ϕ = F(a ∧ b ∧ c) in a 3-component system. t: 0 1 2 3 σ: {a, b} {a, b, c} ∅ ∅ M A : ϕ 1 A = P (ϕ, σ, AP A ) = Xb ∧ Xc ∨ ϕ ϕ 2 A = P (ϕ 1 B ∧ #, σ, AP A ) = X 2 c ∨ (Xb ∧ Xc ∨ ϕ) ϕ 3 A = P (ϕ 2 C ∧ #, σ, AP A ) = X 2 b ∨ (Xb ∧ Xc ∨ ϕ) ϕ 4 A = P (ϕ 3 C ∧ #, σ, AP A ) = X 3 b ∨ (Xb ∧ Xc ∨ ϕ) M B : ϕ 1 B = P (ϕ, σ, AP B ) = Xa ∧ Xc ∨ ϕ ϕ 2 B = P (ϕ 1 A ∧ #, σ, AP B ) = X 2 c ∨ (Xa ∧ Xc ∨ ϕ) ϕ 3 B = P (#, σ, AP B ) = # ϕ 4 B = P (ϕ 3 A ∧ #, σ, AP B ) = M C : ϕ 1 C = P (ϕ, σ, AP C ) = ϕ ϕ 2 C = P (ϕ, σ, AP C ) = Xa ∧ Xb ∨ ϕ ϕ 3 C = P (ϕ 2 A ∧ ϕ 2 B ∧ #, σ, AP C ) = X 2 a ∧ X 2 b ∨ ϕ ϕ 4 C = P (#, σ, AP C ) = #
Example 2 To see how this algorithm works, let us continue the decentralised monitoring process initiated in Example 1. Table 1 shows how the situation evolves for all three monitors, when the global LTL specification in question is

F(a ∧ b ∧ c), the global trace is {a, b} • {a, b, c} • ∅ • ∅,

and the ordering between components is

A < B < C. An evolution of M A 's local obligation, encoded as P (ϕ 1 B ∧ #, σ, AP A ) (see cell M A at t = 1)
indicates that communication between the monitors has occurred: M B (resp. M A ) sent its obligation to M A (resp. to M B ), at the end of step 0. Likewise for the other obligations and monitors. The interesting situations are marked in grey: In particular at t = 0, M C is the only monitor who knows for sure that, so far, no good nor bad prefix occurred (see grey cell at t = 0). At t = 1, we have the desired situation σ = {a, b, c}, but because none of the monitors can see the other monitors' events, it takes another two rounds of communication until both M A and M B detect that, indeed, the global obligation had been satisfied at t = 1 (see grey cell at t = 3).

This example highlights a worst case communication delay between the occurrence and the detection of a good (resp. bad) trace by a good (resp. bad) prefix, caused by the time it takes for the monitors to communicate obligations to each other. This delay depends on the number of monitors in the system, and is also the upper bound for the number of past events each monitor needs to store locally to be able to progress all occurring past obligations: Theorem 2 Let, for any p ∈ AP , X m p be a local obligation obtained by Algorithm L executed on some monitor M i ∈ M. At any time t ∈ N ≥0 , m ≤ min(|M|, t + 1).

Proof The formal proof is based upon the formalisation of the algorithm, given in the next section and available in full later in the paper.

Here, we only want to provide a sketch, explaining the intuition behind the theorem. Recall that X-operators are only introduced directly in front of atomic propositions according to rule (1) when M i rewrites a propositional formula p with p / ∈ AP i . Further X-operators can only be added according to rule (2) when M i is unable to evaluate an obligation of the form X h p. The interesting situation occurs when a monitor M i maintains a set of urgent obligations of the form {X h p 1 , . . . , X j p l } with h, j ∈ N ≥0 , then, according to step L6 of Algorithm L, M i will transmit the obligations to one monitor only thereby adding one additional X-operator to the remaining obligations:

{X h+1 p 2 , . . . , X j+1 p l }.
Obviously, a single monitor cannot have more than |M|-1 outstanding obligations that need to be sent to the other monitors at any time t. So, the worst case communication delay is initiated during monitoring, if at some time all outstanding obligations of each monitor

M i , i ∈ [1, |M|],
are of the form {Xp 1 , . . . , Xp l } with p 1 , . . . , p l / ∈ AP i (i.e., the obligations are all equally urgent), in which case it takes |M|-1 time steps until the last one has been chosen to be sent to its respective monitor M j . Using an ordering between components ensures here that each set of obligations will decrease in size after being transmitted once. Finally, a last monitor, M j will receive an obligation of the form X |M| p k with 1 ≤ k ≤ l and p k ∈ AP j .

Consequently, the monitors only need to memorise a bounded history of the trace read so far, i.e., the last |M| events.

Algorithm formalisation

In order to prove the above result, let us first formalise Algorithm L a bit more and introduce some additional notation:

send(i, t, j) ∈ {true, false} is a predicate indicating whether or not the monitor i sends a formula to monitor j at time t with i = j. send(i, t) ∈ {true, false} is a predicate indicating whether or not the monitor i sends a formula to some monitor at time Based on the previous notation and Algorithm L, we have the following relations:

send(i, t, j) is true if monitor M j is the first monitor containing the most urgent obligation contained in the local obligation of M i , according to the order in [1, m]. Formally:

send(i, t, j) = true if M j = Mon M i , Prop(ulo(i, t, ϕ)) ∧ ulo(i, t, ϕ) = ∅, false otherwise.
send(i, t) is true if monitor M i sends his local obligation to some monitor. Formally:

send(i, t) = ∃j ∈ [1, n] \ {i}. send(i, t, j). -kept(i, t) ∈ LTL is either # if M i
sends its local obligation to some monitor at time t -1 or its local obligation at time t -1 otherwise. Formally:

kept(i, t) = # if ∃j ∈ [1, n] \ {i}. send(i, t -1, j), lo(i, t -1, ϕ) otherwise.
received(i, t, j) is the local obligation of M j received by M i at time t if t ≥ 1 and M j sends actually something to M i . Formally:

received(i, t, j) = lo(j, t -1, ϕ) if ∃j ∈ [1, n] \ {i}. send(j, t -1, i) ∧ t ≥ 1, # otherwise.
received(i, t) is the conjunction of all obligations received by monitor i from all other monitors at time t. Formally:

received(i, t) = |M| j=1,j =i received(i, t, j).
inlo(i, t, ϕ) is at time t ≥ 1 what was kept by M i at time t -1 and the received obligation at time t;

at time t = 0 the initial obligation, i.e., the global specification ϕ. Formally:

inlo(i, t, ϕ) = ϕ if t = 0, kept(i, t -1) ∧ received(i, t) otherwise.
lo(i, t, ϕ) is at time t ≥ 1 the result of progressing what was kept by M i at time t -1 and the received obligation at time t with the current local event u i (t); at time t = 0 the result of progressing the initial obligation, i.e., the global specification with the current local event u i (0). Formally:

lo(i, t, ϕ) = P (ϕ, u i (0), AP i ) if t = 0, P (kept(i, t -1) ∧ received(i, t), u i (t), AP i ) otherwise.
Now, we can clearly state the theorem as follows:

∀t ∈ N ≥0 .∀ϕ ∈ LTL.∀i ∈ [1, n].∀X d p ∈ ulo(i, t, ϕ). d ≤ min(n, t + 1).
Preliminaries to the proof. Let us first start with some remarks. At step L3 in Algorithm L, the local obligation of a monitor M i is defined to be ϕ t i ∧ j∈[1,m],j =i ϕ j where ϕ j is an obligation received from monitor M j and ϕ t i is the local obligation kept from time t -1 (if t = 0, ϕ t i = ϕ). Let us note that the local obligation kept by the monitor from time t -1 to time t, with t ≥ 1, are not urgent. The result should thus be established on the urgent local obligations transmitted and rewritten by local monitors. More formally, this is stated by the following lemma.

Lemma 3 According to Algorithm L, we have:

ulo(i, t, ϕ) = |M| j=1,j =i sus (P (received (i, t) , u i (t) , AP i )) .
Proof First let us notice that the formulae kept by any monitor M i at any time t are not urgent. Indeed, we have

: ∀i ∈ [1, n].∀t ∈ N ≥0 . sus(kept(i, t)) = sus(#) if ∃j ∈ [1, n] \ {i}. send(i, t, j), sus(lo(i, t -1, ϕ)) if sus(lo(i, t -1, ϕ)) = ∅. That is ∀i ∈ [1, n].∀t ≥ 0. sus(kept(i, t)) = ∅. Thus, ∀i ∈ [1, n].∀t ∈ N ≥0 .∀ϕ ∈ LTL. ulo(i, t, ϕ) = sus P (received(i, t), u i (t), AP i ) = sus P ( |M| j=1,j =i received(i, t, j), u i (t), AP i ) (definition of received(i, t, j)) = sus ( |M| j=1,j =i P (received(i, t), u i (t), AP i )) (progression on events) = |M| j=1,j =i sus P (received(i, t), u i (t), AP i ) (definition of sus)
Another last lemma will be needed before entering specifically into the proof. This lemma states that if a past obligation X d p is part of a progressed formula, then the past obligation X d-1 p is part of its un-progressed form. More formally, this is stated by the following lemma.

Lemma 4 Let us consider M = {M 1 , . . . , Mn} where each monitor M i has a set of local atomic propositions AP i = Π i (AP ) and observes the set of events Σ i , we have:

∀i ∈ [1, n].∀σ ∈ Σ i .∀ϕ ∈ LTL.∀X d p ∈ sus P (ϕ, σ, AP i ) . d > 1 =⇒ X d-1 p ∈ sus(ϕ).
Proof The proof is done by structural induction on ϕ ∈ LTL.

Algorithm correctness

Example 2 also illustrates the relationship to the LTL 3 and centralised semantics discussed earlier in Sec. 3. This relationship is formalised by the two following theorems stating essentially the soundness and completeness of the algorithm.

Theorem 3 Let ϕ ∈ LTL and u ∈ Σ * , then u |= D ϕ = /⊥ =⇒ u |= C ϕ = /⊥, and u |= C ϕ = ? =⇒ u |= D ϕ = ?.
Proof The proof is performed by showing that the initial obligation (the global specification) is "propagated" along monitors' local obligations. The formal proof can be found in Appendix A.2.

Corollary 1 Let ϕ ∈ LTL and u ∈ Σ * , then u |= D ϕ = /⊥ =⇒ u |= 3 ϕ = /⊥, and u |= 3 ϕ = ? =⇒ u |= D ϕ = ?.
In particular, Example 2 shows how the other direction of Theorem 2 does not necessarily hold. Consider the trace u = {a, b} • {a, b, c}: clearly,

u |= 3 F(a ∧ b ∧ c) = , but we have u |= D F(a ∧ b ∧ c) = ? in our example.
Again, this is a direct consequence of the communication delay introduced in our setting. However, Algorithm L eventually detects all verdicts for a specification as it could be done with centralised progression if the system was not distributed.

Theorem 4 Let ϕ ∈ LTL, u ∈ Σ * , and n be the number of components in the system.

Whenever u |= C ϕ = /⊥, we have ∀u ∈ Σ * . |u | ≥ n =⇒ u • u |= D ϕ = /⊥.
Proof For a full proof of this theorem including several additional intermediate lemmas, see Appendix A.2.

7 Implementation and experimental results

DECENTMON: an OCaml benchmark for decentralised monitoring of LTL formulae

DECENTMON is an implementation, simulating the above distributed LTL monitoring algorithm in 1,800 LLOC, written in the functional programming language OCaml. It can be freely downloaded and run from [START_REF]DECENTMON Website[END_REF]. The system takes as input multiple traces (that can be automatically generated), corresponding to the behaviour of a distributed system, and an LTL formula. Then the formula is monitored against the traces in two different modes: a) by merging the traces to a single, global trace and then using a "central monitor" for the formula (i.e., all local monitors send their respective events to the central monitor who makes the decisions regarding the trace), and b) by using the decentralised approach introduced in this paper (i.e., each trace is read by a separate monitor).

Experimental setup

We have evaluated the two different monitoring approaches (i.e., centralised vs. decentralised) using randomly generated LTL formulae and LTL formulae generated from specification patterns. Each of the following experiments were conducted on three architectures:

an architecture where the alphabet is {a, b, c} and distributed alphabet is {a|b} ¸(each atomic proposition is observed on a local component); an architecture where the alphabet is We also extended this setting by considering specific probability distributions for the occurrence of local propositions: a so-called flipcoin distribution where each atomic proposition has probability 0.5 of occurring on each event, and Bernouilli distribution with parameters 0.1 and 0.01.

{a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } and distributed alphabet is {a 1 |a 2 |b 1 |b 2 |c 1 |c 2 } (each atomic proposition is observed on a local component); -an architecture where the alphabet is {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } and distributed alphabet is {a 1 , a 2 |b 1 , b 2 |c 1 , c 2 } (atomic propositions a 1 , a 2 (resp.
Monitoring metrics. Several monitoring metrics were used.

-The length of the trace, |trace|, needed for the monitor to reach a verdict.

-The number of messages, #msg., exchanged between monitors. In the centralised setting, it corresponds to the number of events sent by the local monitors to the central monitor (i.e., the length of the trace times the number of components). In the decentralised setting, it corresponds to the number of obligations transmitted between local monitors. -The maximal and average delay of decentralised monitoring compared to centralised monitoring.

Remark 3

We have used continuous simplification of the goal formulae in order to avoid a formula explosion problem caused by rewriting. In DECENTMON, advanced syntactic simplification rules 3 were introduced and sufficient for the purpose of our experiments. 7.3 Evaluation using randomly generated formulae DECENTMON randomly generated 1,000 LTL formulae of various sizes in the architectures described above. Note, our system measures formula size in terms of the operator entailment 4 inside it (state formulae excluded), e.g., G(a ∧ b) ∨ Fc is of size 2. How both monitoring approaches compared on these formulae can be seen in Tables 2, 3, 4, and 5. For each experiment, the first column shows the size of the monitored LTL formulae. The entry |trace| denotes the average length of the traces needed to reach a verdict. For example, the last line in Table 2 (a) says that we monitored 1,000 randomly generated LTL formulae of size 6. On average, traces were of length 72.437 when the central monitor came to a verdict, and of length 73.013 when one of the local monitors came to a verdict. The difference ratio, given in the second last column, then shows the average communication delay; that is, on average the traces were 1.0079 times longer in the decentralised setting than the traces in the centralised setting. What is striking here, however, is that the amount of communication needed in the decentralised setting is ca. only 25% of the communication overhead induced by central monitoring, where local monitors need to send each event to a central monitor.

Evaluation using specification patterns

In order to evaluate our approach also at the hand of realistic LTL specifications, we conducted benchmarks using LTL formulae following the well-known LTL specification patterns ( [START_REF] Matthew | Patterns in property specifications for finite-state verification[END_REF], whereas the actual formulae underlying the patterns are available at this site [START_REF]Specification Patterns Website[END_REF] and recalled in [START_REF]DECENTMON Website[END_REF]). In this context, to randomly generate formulae, we proceeded as follows. For a given specification pattern, we randomly select one of the formulae associated to it. Such a formula is "parameterised" by some atomic propositions. To obtain the randomly generated formula, using the distributed alphabet, we randomly instantiate the atomic propositions. The results of this evaluation are reported in Tables 6, 7, 8, 9: for each setting, for each kind of pattern (absence, existence, bounded existence, universal, precedence, response, precedence chain, response chain, constrained chain), we generated again 1,000 formulae, monitored over the three architectures.

Discussion

Generally speaking, both benchmarks substantiate the claim that decentralised monitoring of an LTL formula can induce a much lower communication overhead compared to a centralised solution. In fact, when considering the more realistic benchmark using the specification patterns, the communication overhead was significantly lower compared to monitoring randomly generated formulae. The same holds true for the communication delay: in case of monitoring LTL formulae corresponding to specification patterns, the communication delay is almost negligible; that is, the local monitors detect violation/satisfaction of a monitored formula at almost the same time as a global monitor with access to all observations. Let us consider the settings with traces where local propositions have the same probability of occurring as of not occurring (flipcoin distribution).

-When the policy is such that, in the centralised case, components report the truth value of atomic propositions at each time step (see Tables 2 and6), the experimental results are clearly in favour of decentralised monitoring. Decentralised monitoring is more effective as the size of formulae grows (until formulae of size 3-4). The performance of decentralised monitoring seems to deteriorate with formulae with a nesting level above 4. We explain this phenomenon by the fact that decentralised monitoring generate more complicated obligations and our syntactic simplification techniques handles semantically equivalent formulae until 3 nesting levels. -When the policy is such that, in the centralised case, components report the truth value of atomic propositions only in case of a change w.r.t. the previous event (see Tables 3 and7), the experimental results generally vary with the size of the formulae, but the decentralised case induced only around half the number messages under this policy. Moreover, the advantage remains in favour of decentralised monitoring as the size of the local alphabets was increased. Let us consider the settings with traces where the occurrence of a local proposition has a very high or a very low probability (see Tables 4,5, 8, and 9). 5 In this setting, we still favour centralised monitoring by considering that, in case of centralised monitoring, components send the value of atomic propositions only if there is change w.r.t. previous events. As one would expect, the performance of decentralised monitoring deteriorates since it induces a

Conclusions and related work

Centralised monitoring of LTL requirements has been addressed by using automata-based techniques (cf. [START_REF] Sen | Generating Optimal Linear Temporal Logic Monitors by Coinduction[END_REF][START_REF] Bauer | Runtime verification for LTL and TLTL[END_REF]) or rewriting-based techniques (cf. [START_REF] Havelund | Monitoring programs using rewriting[END_REF][START_REF] Grigore | Rewriting-based techniques for runtime verification[END_REF][START_REF] Barringer | Rule systems for run-time monitoring: from Eagle to RuleR[END_REF] for instance). While, automata-based approaches do not suffer from the "incompleteness problem" of rewritingbased techniques as illustrated in Remark 2, we intentionally chose to have a rewriting-based monitoring algorithm as it confers several advantages in the decentralised setting (see also the end of the discussion section). This work is by no means the first to introduce an approach to monitoring the behaviour of distributed systems. For example, the diagnosis (of discrete-event systems) has a similar objective (i.e., detect the occurrence of a fault after a finite number of discrete steps) (cf. [START_REF] Wang | New results on decentralized diagnosis of discrete event systems[END_REF][START_REF] Wang | Diagnosis of discrete event systems using decentralized architectures[END_REF][START_REF] Cassez | The complexity of codiagnosability for discrete event and timed systems[END_REF]). In diagnosis, however, one tries to isolate root causes for failure (i.e., identify the component in a system which is responsible for a fault). A key concept is that of diagnosability: a system model is diagnosable if it is always the case that the occurrence of a fault can be detected after a finite number of discrete steps. In other words, in diagnosis the model of a system, which usually contains both faulty and nominal behaviour, is assumed to be part of the problem input, whereas we consider systems more or less as a "black box". Diagnosability does not transfer to our setting, because we need to assume that the local monitors always have sufficient information to detect violation (resp. satisfaction) of a specification. Also, it is common in diagnosis of distributed systems to assert a central decision making point, even if that reflects merely a Boolean function connecting the local diagnosers' verdicts, while in our setting the local monitors directly communicate without a central decision making point.

A natural counterpart of diagnosability is that of observability as defined in decentralised observation [START_REF] Tripakis | Decentralized observation problems[END_REF]: a distributed system is said to be x-observable, where x ranges over different parameters such as whether local observers have finite or infinite memory available to store a trace (i.e., jointly unbounded-memory, jointly bounded-memory, locally unboundedmemory, locally finite-memory), if there exists a total function, always able to combine the local observers' states after reading some trace to a truthful verdict w.r.t. the monitored property. Again, the main difference here is that we take observability for granted, in that we assume that the system can always be monitored w.r.t. a given property, because detailed system topology or architectural information is not part of our problem input. Moreover, unlike in our setting, even in the locally-observable cases, there is still a central decision making point involved, combining the local verdicts. Note also that, to the best of our knowledge, both observation and diagnosis do not concern themselves with attempting to minimise the communication overhead needed for observing/diagnosing a distributed system.

A specific temporal logic, MTTL, for expressing properties of asynchronous multithreaded systems has been presented in [START_REF] Sen | Decentralized runtime analysis of multithreaded applications[END_REF]. Its monitoring procedure takes as input a safety formula and a partially ordered execution of a parallel asynchronous system. It then establishes whether or not there exist runs in the execution that violate the MTTL formula. While the synchronous case can be interpreted a special case of the asynchronous one, there are some noteworthy differences between [START_REF] Sen | Decentralized runtime analysis of multithreaded applications[END_REF] and our work. Firstly, we take LTL "off-the-shelf"; that is, we do not add modalities to express properties concerning the distributed/multi-threaded nature of the system under scrutiny. On the contrary, our motivation is to enable users to conceive a possibly distributed system as a single, monolithic system by enabling them to specify properties over the outside visible behaviour only-independent of implementation specific-details, such as the number of threads or components-and to automatically "distribute the monitoring" process for such properties for them. Secondly, we address the fact that in some distributed systems it may not be possible to collect a global trace or insert a global decision making point, thereby forcing the automatically distributed monitors to communicate. But at the same time we try and the reduce overall communication overhead. This aspect, on the other hand, does not play a role in [START_REF] Sen | Decentralized runtime analysis of multithreaded applications[END_REF] where the implementation was tried on parallel (Java) programs which are not executed on physically separated CPUs, and where one can collect a set of global behaviours to then reason about. Finally, our setting is not restricted to safety formulae, i.e., we can monitor any LTL formula as long as its set of good (resp. bad) prefixes is not empty. However, we have not investigated whether or not the restriction of safety formulae is inherent to [START_REF] Sen | Decentralized runtime analysis of multithreaded applications[END_REF] or made by choice. Other recent works like [START_REF] Genon | Monitoring distributed controllers[END_REF] target physically distributed systems, but do not focus on the communication overhead that may be induced by their monitoring. Similarly, this work also mainly addresses the problem of monitoring systems which produce partially ordered traces (à la Diekert and Gastin), and introduces abstractions to deal with the combinational explosion of these traces.

To the best of our knowledge, our work is the first to address the problem of automatically distributing LTL monitors, and to introduce a decentralised monitoring approach that not only avoids a global point of observation or any form of central trace collection, but also tries to keep the number of communicated messages between monitors at a minimum. Moreover, our experimental results show that this approach does not only "work on paper", but that it is feasible to be implemented. Indeed, even the expected savings in communication overhead could be observed for the set of chosen LTL formulae and the automatically generated traces, when compared to a centralised solution in which the local monitors transmit all observed events to a global monitor.

Subsequent to our work, [START_REF] Falcone | Efficient and generalized decentralized monitoring of regular languages[END_REF] alternatively studies decentralised monitoring of finitestate automata. While the monitoring algorithm and communication protocol in [START_REF] Falcone | Efficient and generalized decentralized monitoring of regular languages[END_REF] make use of smaller messages and have a lower memory consumption, decentralised monitoring of LTL formulae keeps several advantages over [START_REF] Falcone | Efficient and generalized decentralized monitoring of regular languages[END_REF]. First, in terms of monitoring metrics, our approach imposes lower delays to reach the verdict and requires a lower number of messages between the monitors. Second, the approach in [START_REF] Falcone | Efficient and generalized decentralized monitoring of regular languages[END_REF] requires monitors to exchange chunks of (incomplete) global traces, which, from a security perspective, is a confidentiality downside. On the contrary, our approach better "hides" what happens on local components within the exchanged (LTL) obligations. Third, our approach is formally-proven sound and complete.

Proof We shall prove the following statement:

∀σ ∈ Σ.∀w ∈ Σ ω .∀ϕ ∈ LTL. σ • w |= ϕ ⇐⇒ w |= P (ϕ, σ).
Let us consider an event σ ∈ Σ and an infinite trace w ∈ Σ ω , the proof is done by a structural induction on ϕ ∈ LTL.

Base Case: ϕ ∈ { , ⊥, p ∈ AP }.

-Case ϕ = . This case is trivial since, according to the definition of the progression function, ∀σ ∈ Σ. P ( , σ) = . Moreover, according to the LTL semantics of , ∀w ∈ Σ ω . w |= . -Case ϕ = ⊥. This case is symmetrical to the previous one.

-Case ϕ = p ∈ AP . Recall that, according to the progression function for atomic propositions, we have P (p, σ) = if p ∈ σ and ⊥ otherwise.

-Let us suppose that σ•w |= p. According to the LTL semantics of atomic propositions, it means that p ∈ σ, and thus P (p, σ) = . And, due to the LTL semantics of , we have ∀w ∈ Σ ω . w |= . -Let us suppose that w |= P (p, σ). Since P (p, σ) ∈ { , ⊥}, we have necessarily P (p, σ) = .

According to the progression function, P (p, σ) = amounts to p ∈ σ. Using the LTL semantics of atomic propositions, we deduce that σ • w |= p.

Induction Case: ϕ ∈ {¬ϕ , ϕ 1 ∨ ϕ 2 , ϕ 1 ∧ ϕ 2 , Gϕ , Fϕ , Xϕ , ϕ 1 Uϕ 2 }.
Our induction hypothesis states that the lemma holds for some formulae ϕ , ϕ 1 , ϕ 2 ∈ LTL.

-Case ϕ = ¬ϕ . On the one hand, using the progression function for ¬, we have P (¬ϕ , σ) = ¬P (ϕ , σ). On the other hand, using the LTL semantics of operator ¬, we have w |= ϕ ⇐⇒ w |= ¬ϕ. Thus, we have σ

• w |= ¬ϕ iff σ • w |= ϕ iff (induction hypothesis on ϕ ) w |= P (ϕ , σ) iff w |= ¬P (ϕ , σ) iff w |= P (¬ϕ , σ). -Case ϕ = ϕ 1 ∨ ϕ 2 .
Recall that, according to the progression function for operator ∨, we have

P (ϕ 1 ∨ ϕ 2 , σ) = P (ϕ 1 , σ) ∨ P (ϕ 2 , σ). -Let us suppose that σ • w |= ϕ 1 ∨ ϕ 2 .
We distinguish again two sub-cases:

ϕ 1 ∨ ϕ 2 = or ϕ 1 ∨ ϕ 2 = . If ϕ 1 ∨ ϕ 2 =
, then this case reduces to the case where ϕ = , already treated.

If ϕ 1 ∨ ϕ 2 = , it means that either σ • w |= ϕ 1 or σ • w |= ϕ 2 .
Let us treat the case where σ • w |= ϕ 1 (the other case is similar). From σ • w |= ϕ 1 , we can apply the induction hypothesis on ϕ 1 to obtain w |= P (ϕ 1 , σ), then,

w |= P (ϕ 1 , σ) ∨ P (ϕ 1 , σ) = P (ϕ 1 ∨ ϕ 2 , σ). -Let us suppose that w |= P (ϕ 1 ∨ ϕ 2 , σ) = P (ϕ 1 , σ) ∨ P (ϕ 2 , σ). We distinguish again two sub-cases: P (ϕ 1 ∨ ϕ 2 , σ) = or P (ϕ 1 ∨ ϕ 2 , σ) = .
• If P (ϕ 1 ∨ ϕ 2 , σ) = , then we again distinguish two sub-cases:

• If P (ϕ 1 , σ) = or P (ϕ 2 , σ) = .
Let us treat the case where P (ϕ 1 , σ) = (the other case is similar). Applying the induction hypothesis on ϕ 1 , we have σ • w |= ϕ 1 ⇐⇒ w |= P (ϕ 1 , σ). Then, consider w ∈ Σ ω , we have σ • w |= ϕ 1 , and consequently σ • w |= ϕ 1 ∨ ϕ 2 .

• If P (ϕ 1 , σ) = and P (ϕ 2 , σ) = , then we have P (ϕ 1 , σ) = ¬P (ϕ 2 , σ). Applying the induction hypothesis on ϕ 1 and ϕ 2 , we obtain σ -Case ϕ = ϕ 1 Uϕ 2 . Recall that, according to the progression function for operator U, P (ϕ

• w |= ϕ 1 ⇐⇒ σ • w |= ϕ 2 . Let us consider w ∈ Σ ω . If σ • w |= ϕ 1 , then we have σ • w |= ϕ 1 ∨ ϕ 2 . Else (σ • w |= ϕ 1 ), we have σ |= ϕ 2 , and then σ • w |= ϕ 1 ∨ ϕ 2 . • If P (ϕ 1 ∨ ϕ 2 , σ) = ,
1 Uϕ 2 , σ) = P (ϕ 2 , σ) ∨ (P (ϕ 1 , σ) ∧ ϕ 1 Uϕ 2 ). -Let us suppose that σ • w |= ϕ 1 Uϕ 2 . According to the LTL semantics of operator U, we have ∃i ∈ N ≥0 . (σ • w) i |= ϕ 2 ∧ ∀0 ≤ l < i. (σ • w) l |= ϕ 1 .
Let us distinguish two cases: i = 0 and i > 0.

• If i = 0, then we have σ • w |= ϕ 2 . Applying the induction hypothesis on ϕ 2 , we have w |= P (ϕ 2 , σ), and consequently

w |= P (ϕ 1 Uϕ 2 , σ). • Else (i > 0), we have ∀0 ≤ l < i. (σ • w) l |= ϕ 1 . Consequently, we have (σ • w) 0 |= ϕ 1 ,
and thus σ

• w |= ϕ 1 . Moreover, from ∀0 ≤ l < i. (σ • w) l |= ϕ 1 , we deduce ∀0 ≤ l < i -1. w l |= ϕ 1 . From (σ • w) i |= ϕ 2 , we deduce w i-1 |= ϕ 2 . From w i-1 |= ϕ 2 and ∀0 ≤ l < i. (σ • w) l |= ϕ 1 , we deduce w |= ϕ 1 Uϕ 2 .
Applying, the induction hypothesis on ϕ 1 , from σ • w |= ϕ 1 , we obtain w |= P (ϕ 1 , σ). Finally, from w |= ϕ 1 Uϕ 2 and w |= P (ϕ 1 , σ), we obtain w |= P (ϕ 1 Uϕ 2 , σ). -Let us suppose that w |= P (ϕ 1 Uϕ 2 , σ).

We distinguish two cases: P (ϕ 1 Uϕ 2 , σ) = and P (ϕ 1 Uϕ 2 , σ) = .

• If P (ϕ 1 Uϕ 2 , σ) = P (ϕ 2 , σ) ∨ (P (ϕ 1 , σ) ∧ ϕ 1 Uϕ 2 ) = . We distinguish again two sub-cases. We shall prove the following statement.

• If P (ϕ 2 , σ) = or P (ϕ 1 , σ) ∧ ϕ 1 Uϕ 2 = . If P (ϕ 2 , σ) = ,
∀ϕ ∈ LT L.∀σ ∈ Σ. P (ϕ, σ) = =⇒ σ ∈ good(ϕ) ∧ P (ϕ, σ) = ⊥ =⇒ σ ∈ bad(ϕ).
The proof uses the definition of the LTL semantics (Definition 1), the definition of good and bad prefixes (Definition 2), the progression function (Definition 3), and Lemma 1.

Proof According to Lemma 1, we have ∀σ ∈ Σ.∀w ∈ Σ ω . σ•w |= ϕ ⇐⇒ w |= P (ϕ, σ). Consequently, we have ∀σ ∈ Σ.∀w ∈ Σ ω . σ • w |= ϕ ⇐⇒ ∀σ ∈ Σ.∀w ∈ Σ ω . w |= P (ϕ, σ) and ∀σ ∈ Σ.∀w ∈ Σ ω . σ • w |= ϕ ⇐⇒ ∀σ ∈ Σ.∀w ∈ Σ ω . w |= P (ϕ, σ). Consequently, when P (ϕ, σ) = , we have ∀σ ∈ Σ.∀w ∈ Σ ω . σ • w |= ϕ, i.e., σ ∈ good(ϕ). Similarly, when P (ϕ, σ) = ⊥, we have ∀σ ∈ Σ.∀w ∈ Σ ω . σ • w |= ϕ, i.e., σ ∈ bad(ϕ).

The proof can also be obtained in a more detailed manner as shown below. Let us consider σ ∈ Σ and ϕ ∈ LTL. The proof is performed by a structural induction on ϕ.

Base Case: ϕ ∈ { , ⊥, p ∈ AP }.

-Case ϕ = . In this case, the proof is trivial since P ( , σ) = and, according to the LTL semantics of and the definition of good prefixes, good( ) = Σ * .

-Case ϕ = p ∈ AP . Let us distinguish two cases: p ∈ u(0) or p / ∈ u(0). -If p ∈ u(0), we have: P (p, u • σ) = P (P (p, u), σ) (extended progression) = P ( , σ) (induction hypothesis on u) = (progression on events)

-If p / ∈ u(0), we have:

P (p, u • σ) = P (P (p, u), σ) (extended progression) = P (⊥, σ) (induction hypothesis on u) = ⊥
(progression on events)

Induction Case: ϕ ∈ {¬ϕ , ϕ 1 ∨ ϕ 2 , ϕ 1 ∧ ϕ 2 , Gϕ , Fϕ , Xϕ , ϕ 1 Uϕ 2 }.
Our induction hypothesis states that the lemma holds for some formulae ϕ , ϕ 1 , ϕ 2 ∈ LTL.

-Case ϕ = ¬ϕ . We have:

P (¬ϕ , u • σ) = P (P (¬ϕ , u), σ) (extended progression) = P (¬P (ϕ , u), σ) (induction hypothesis on u and ϕ ) = ¬P (P (ϕ , u), σ) (progression on events) = ¬P (ϕ , u • σ) (extended progression)

-Case ϕ = Xϕ . We have:

P (Xϕ , u • σ) = P (P (Xϕ , u), σ) (extended progression) = P (P (ϕ , u 1 ), σ) (induction hypothesis on u and ϕ ) = P (ϕ , u 1 σ)

(extended progression) = P (ϕ , (u • σ) 1 )
-Case ϕ = ϕ 1 ∨ ϕ 2 . We have:

P (ϕ 1 ∨ ϕ 2 , u • σ) = P (P (ϕ 1 ∨ ϕ 2 , u), σ) (extended progression) = P (P (ϕ 1 , u) ∨ P (ϕ 2 , u), σ)
(induction hypothesis on u and ϕ 1 , ϕ 2 ) = P (P (ϕ 1 , u), σ) ∨ P (P (ϕ 2 , u), σ) (progression on events)

= P (ϕ 1 , u • σ) ∨ P (ϕ 2 , u • σ) (extended progression) -Case ϕ = ϕ 1 ∧ ϕ 2 .
This case is similar to the previous one.

-Case ϕ = Gϕ . We have:

P (Gϕ , u • σ) = P (P (Gϕ , u), σ) (extended progression) = P ( |u|-1 i=0 P (ϕ , u i ) ∧ Gϕ , σ)
(induction hypothesis on u and ϕ ) = P ( |u|-1 i=0 P (ϕ , u i ), σ) ∧ P (Gϕ , σ) (progression on events for ∧) = |u|-1 i=0 P (P (ϕ , u i ), σ) ∧ P (Gϕ , σ)

(extended progression for ∧) = |u|-1 i=0 P (ϕ , u i • σ) ∧ P (Gϕ , σ) (extended progression) = |u|-1 i=0 P (ϕ , u i • σ) ∧ P (ϕ , σ) ∧ Gϕ (progression on events for G) = |u•σ|-2 i=0 P (ϕ , (u • σ) i ) ∧ P (ϕ , (u • σ) |u•σ|-1 ) ∧ Gϕ (u i • σ = (u • σ) i and σ = (u • σ) |u•σ|-1 ) = |u•σ|-1 i=0 P (ϕ , (u • σ) i ) ∧ Gϕ
-Case ϕ = Fϕ . We have:

P (Fϕ , u • σ) = P (P (Fϕ , u), σ) (extended progression) = P ( |u|-1 i=0 P (ϕ , u i ) ∨ Fϕ , σ)
(induction hypothesis on u and ϕ ) = P (

|u|-1 i=0 P (ϕ , u i ), σ) ∨ P (Fϕ , σ) (progression on events) = |u|-1 i=0 P (ϕ , u i • σ) ∨ P (Fϕ , σ) (extended progression for ∨) = |u|-1 i=0 P (ϕ , u i • σ) ∨ P (ϕ , σ) ∨ Fϕ (progression on events for F) = |u•σ|-2 i=0 P (ϕ , (u • σ) i ) ∨ P (ϕ , (u • σ) |u•σ|-1 ) ∨ Fϕ (u i • σ = (u • σ) i and σ = (u • σ) |u•σ|-1 ) = |u•σ|-1 i=0 P (ϕ , (u • σ) i ) ∨ Fϕ -Case ϕ = ϕ 1 Uϕ 2 .
We have:

P (ϕ 1 Uϕ 2 , u • σ) (extended progression)
= P (P (ϕ 1 Uϕ 2 , u), σ) (induction hypothesis on u, and structural induction hypothesis on ϕ 1 and ϕ 2 )

= P |u|-1 i=0 P (ϕ 2 , u i ) ∧ i-1 j=0 P (ϕ 1 , u j ) ∨ |u|-1 i=0 P (ϕ 1 , u i ) ∧ ϕ 1 Uϕ 2 , σ (progression on events for ∨) = P |u|-1 i=0 P (ϕ 2 , u i ) ∧ i-1 j=0 P (ϕ 1 , u j ) , σ) ∨ P ( |u|-1 i=0 P (ϕ 1 , u i ) ∧ ϕ 1 Uϕ 2 , σ (
progression on events for ∧ and ∨) =

|u|-1 i=0

P (P (ϕ 2 , u i ), σ) ∧ i-1 j=0 P (P (ϕ 1 , u j ), σ) ∨ |u|-1 i=0 P (P (ϕ 1 , u i ), σ) ∧ P (ϕ 1 Uϕ 2 , σ) (extended progression) = |u|-1 i=0 P (ϕ 2 , u i • σ) ∧ i-1 j=0 P (ϕ 1 , u j • σ) ∨ |u|-1 i=0 P (ϕ 1 , u i • σ) ∧ P (ϕ 1 Uϕ 2 , σ) Moreover: |u|-1 i=0 P (ϕ 1 , u i • σ) ∧ P (ϕ 1 Uϕ 2 , σ) (progression on events for U) = |u|-1 i=0 P (ϕ 1 , u i • σ) ∧ (P (ϕ 2 , σ) ∨ P (ϕ 1 , σ) ∧ ϕ 1 Uϕ 2 ) (distribution of ∧ over ∨) = |u|-1 i=0 P (ϕ 1 , u i • σ) ∧ P (ϕ 2 , σ) ∨ |u|-1 i=0 P (ϕ 1 , u i • σ) ∧ P (ϕ 1 , σ) ∧ ϕ 1 Uϕ 2 (σ = (u • σ) |u•σ|-1 and elimination of P (ϕ 1 , σ)) = |u|-1 i=0 P (ϕ 1 , u i • σ) ∧ P (ϕ 2 , σ) ∨ |u•σ|-1 i=0 P (ϕ 1 , u i • σ) ∧ ϕ 1 Uϕ 2 Furthermore: |u|-1 i=0 P (ϕ 2 , u i • σ) ∧ i-1 j=0 P (ϕ 1 , u j • σ) ∨ |u|-1 i=0 P (ϕ 1 , u i • σ) ∧ P (ϕ 2 , σ) (variable renaming) = |u|-1 i=0 P (ϕ 2 , u i • σ) ∧ i-1 j=0 P (ϕ 1 , u j • σ) ∨ P (ϕ 2 , σ) ∧ |u|-1 j=0 P (ϕ 1 , u j • σ) (σ = (u • σ) |u•σ|-1 ) = |u•σ|-2 i=0 P (ϕ 2 , (u • σ) i ) ∧ i-1 j=0 P (ϕ 1 , u j • σ) ∨ P (ϕ 2 , (u • σ) |u•σ|-1 ) ∧ |u•σ|-2 j=0 P (ϕ 1 , u j • σ) = |u•σ|-1 i=0 P (ϕ 2 , (u • σ) i ) ∧ i-1 j=0 P (ϕ 1 , (u • σ) j )
Finally:

P (ϕ 1 Uϕ 2 , u • σ) = |u|-1 i=0 P (ϕ 2 , u i • σ) ∧ i-1 j=0 P (ϕ 1 , u j • σ) ∨ |u|-1 i=0 P (ϕ 1 , u i • σ) ∧ P (ϕ 2 , σ) ∨ |u•σ|-1 i=0 P (ϕ 1 , u i • σ) ∧ ϕ 1 Uϕ 2 = |u•σ|-1 i=0 P (ϕ 2 , u i • σ) ∧ i-1 j=0 P (ϕ 1 , u j • σ) ∨ |u•σ|-1 i=0 P (ϕ 1 , u i • σ) ∧ ϕ 1 Uϕ 2 = |u•σ|-1 i=0 P (ϕ 2 , (u • σ) i ) ∧ i-1 j=0 P (ϕ 1 , (u • σ) j ) ∨ |u•σ|-1 i=0 P (ϕ 1 , (u • σ) i ) ∧ ϕ 1 Uϕ 2
We introduce another intermediate lemma, which is a consequence of the definition of LTL semantics (Definition 1) and the definition of the progression function (Definition 5). This lemma will be useful in the remaining proofs. This lemma states that the progression function "mimics" the semantics of LTL on a trace u ∈ Σ * . Lemma 6 Let ϕ be an LTL formula, u ∈ Σ * a finite trace and w ∈ Σ ω an infinite trace, we have u • w |= ϕ ⇐⇒ w |= P (ϕ, u).

Proof We shall prove the following statement:

∀u ∈ Σ * .∀w ∈ Σ ω .∀ϕ ∈ LTL. u • w |= ϕ ⇐⇒ w |= P (ϕ, u).
Let us consider u ∈ Σ + , the proof is done by a structural induction on ϕ ∈ LTL (when u = , the lemma holds vacuously). Base case: ϕ ∈ { , ⊥, p ∈ AP }.

-Case ϕ = . This case is trivial since, using Lemma 5 on and u, we have P ( , u) = . Moreover, according to the LTL semantics of , ∀w ∈ Σ ω . u • w |= . -Case ϕ = ⊥. This case is symmetrical to the previous one.

-Case ϕ = p ∈ AP .

-Let us suppose that u•w |= p. By applying Lemma 5 on and u, we have P (u, p) = . Moreover, due to the LTL semantics of , we have ∀w ∈ Σ ω . w |= = P (u, p). -Let us suppose that w |= P (p, u). Since P (p, u) ∈ { , ⊥}, we have necessarily P (p, u) = .

According to the progression function, P (p, u) = necessitates that p ∈ u(0). Using the LTL semantics of atomic propositions, we deduce that (u • w) 0 |= p, i.e., u • w |= p.

Induction Case: ϕ ∈ {¬ϕ , ϕ 1 ∨ ϕ 2 , ϕ 1 ∧ ϕ 2 , Gϕ , Fϕ , Xϕ , ϕ 1 Uϕ 2 }. Our induction hypothesis states that the lemma holds for some formulae ϕ , ϕ 1 , ϕ 2 ∈ LTL.

-Case ϕ = ϕ 1 ∨ ϕ 2 . Recall that, by applying Lemma 5 on ϕ 1 ∨ ϕ 2 and u, we have P (ϕ 1 ∨ ϕ 2 , u) = P (ϕ -Case ϕ = ϕ 1 ∧ ϕ 2 . This case is similar to the previous one.

-Case ϕ = Gϕ . Recall that, by applying Lemma 5 on Gϕ and u, we have -Case ϕ = ϕ 1 Uϕ 2 . Recall that, by applying Lemma 5 on u and ϕ 1 Uϕ 2 , we have:

P (Gϕ , u) = |u|-1 i=0 P (ϕ , u i ) ∧ Gϕ . -Let us suppose that u • w |= Gϕ . From the LTL semantics of operator G, we have ∀i ∈ N ≥0 . (u • w) i |= ϕ . In particular, it implies that ∀0 ≤ i ≤ |u| -1. u i • w |= ϕ and ∀i ≥ 0. ((u • w) |u|-1 ) i |= ϕ . Using, ∀0 ≤ i ≤ |u| -1. u i • w |= ϕ
P (ϕ 1 Uϕ 2 , u) = |u|-1 i=0 P (ϕ 2 , u i ) ∧ i-1 j=0 P (ϕ 1 , u j ) ∨ |u|-1 i=0 P (ϕ 1 , u i ) ∧ ϕ 1 Uϕ 2 . -Let us suppose that u • w |= ϕ 1 Uϕ 2 . According to the LTL semantics of operator U, ∃k ∈ N ≥0 . (u • w) k |= ϕ 2 ∧ ∀0 ≤ l < k. (u • w) l |= ϕ 1 . Let us distinguish two cases: k > |u| and k ≤ |u|. • If k > |u|, then we have in particular ∀0 ≤ l ≤ |u| -1. u l • w |= ϕ 1 .
Applying the structural induction hypothesis on ϕ 1 and the u l 's, we find ∀0 ≤ l ≤ |u|.

w |= P (ϕ 1 , u l ), i.e., w |= |u|-1 l=0 P (ϕ 1 , u l ). From (σ • w) k |= ϕ 2 and k > |u| -1, we deduce that ∃k ≥ 0. w k |= ϕ 2 and k = k -|u| + 1. Furthermore, we have ∀0 ≤ i ≤ k . ((u • w) |u|-1 ) k = w |= P (ϕ 1 , u), i.e., w |= k i=0 P (ϕ 1 , u i ). Finally, w |= P (ϕ 1 Uϕ 2 , u). • If k ≤ |u| -1, then from (u • w) k |= ϕ 2 , we have u k • w |= ϕ 2 .
Using the induction hypothesis on ϕ 2 and u k , we have w |= P (ϕ 2 , u k ). Moreover, using ∀l ≤ |k|. (u • w) l = u l • w |= ϕ 1 and the induction hypothesis on ϕ 1 and the u l 's, we obtain ∀l ≤ |k|. (u • w) l = w |= P (ϕ 1 , u l ). Finally, we have w |= k l=0 |= P (ϕ 1 , u l ) ∧ P (ϕ 2 , u k ), and thus w |= P (ϕ 1 Uϕ 2 , u).

-Let us suppose that w |= P (ϕ 1 Uϕ 2 , u). We distinguish two sub-cases: P (ϕ 1 Uϕ 2 , u) = and P (ϕ 1 Uϕ 2 , u) = .

• Sub-case P (ϕ 1 Uϕ 2 , u) = . We distinguish again three sub-cases:

• Sub-case |u|-1 i=0 P (ϕ 2 , u i ) ∧ i-1 j=0 P (ϕ 1 , u j ) = . Necessarily, we have ∃0 ≤ i ≤ |u| -1. P (ϕ 2 , u i ) ∧ i-1 j=0 P (ϕ 1 , u j ) = . Otherwise, that would mean that ∃i 1 , i 2 ∈ [0, |u|-1]. P (ϕ 2 , u i 1 )∧ i 1 -1 j=0 P (ϕ 1 , u j ) = ¬P (ϕ 2 , u i 2 )∧ i 2 -1 j=0 P (ϕ 1 , u j
) and we would obtain a contradiction. From P (ϕ 2 , u i )∧ i-1 j=0 P (ϕ 1 , u j ) = , we have P (ϕ 2 , u i ) = and i-1 j=0 P (ϕ 1 , u j ) = . Using the induction hypothesis on ϕ 1 and ϕ 2 , we obtain

u i • w |= ϕ 2 and ∀0 ≤ j < i. u j • w |= ϕ 1 . According to the LTL semantics of operator U, it means u • w |= ϕ 1 Uϕ 2 . • Sub-case |u|-1 i=0 P (ϕ 1 , u i )∧ϕ 1 Uϕ 2 = .
In this case, we have necessarily ϕ 1 Uϕ 2 = , and this case reduces to the case where ϕ = .

• Sub-case

|u|-1 i=0 P (ϕ 2 , u i ) ∧ i-1 j=0 P (ϕ 1 , u j ) = and |u|-1 i=0 P (ϕ 1 , u i ) ∧ ϕ 1 Uϕ 2 = . We have then |u|-1 i=0 P (ϕ 2 , u i ) ∧ i-1 j=0 P (ϕ 1 , u j ) = ¬ |u|-1 i=0 P (ϕ 1 , u i ) ∧ ϕ 1 Uϕ 2 . Let us suppose that ∀i ∈ N ≥0 . (u • σ) |= ϕ 2 . Following the induction hypothesis on ϕ 2 , it means in particular that ∀0 ≤ i ≤ |u| -1. w |= P (ϕ 2 , u i ). Then, since w |= P (ϕ 2 Uϕ 2 ), it would imply that w |= |u|-1 i=0 P (ϕ 1 , u i ) ∧ ϕ 1 Uϕ 2 . But, from w |= ϕ 1 Uϕ 2 ,
we would obtain a contradiction according to the LTL semantics. Hence, let us consider i the minimal k A.1.4 Proof for Theorem 1 (p. 7)

∈ N ≥0 s.t. (u • w) k |= ϕ 2 . If i > |u| -1, then similarly we have w |= |u|-1 i=0 P (ϕ 1 , u i ) ∧ ϕ 1 Uϕ 2 . It follows that ∀0 ≤ l ≤ |u| -1. u l • w |= ϕ 1 and ∀|u| -1 ≤ l < i. (u • w) l |= ϕ 1 ,
We shall prove the following statement:

∀u ∈ Σ * .∀ϕ ∈ LTL. (u |= C ϕ = /⊥ =⇒ u |= 3 ϕ = /⊥) ∧ (u |= 3 ϕ = ? =⇒ u |= C ϕ = ?)
The proof uses the definition of LTL semantics (Definition 1), the definition of good and bad prefixes (Definition 5), the progression function (Definition 3), and Lemma 6.

Proof According to Lemma 6, we have ∀u ∈

Σ + .∀w ∈ Σ ω . u • w |= ϕ ⇐⇒ w |= P (ϕ, u). Consequently, we have ∀u ∈ Σ + .∀w ∈ Σ ω . u • w |= ϕ ⇐⇒ ∀u ∈ Σ + .∀w ∈ Σ ω . w |= P (ϕ, u) and ∀u ∈ Σ + .∀w ∈ Σ ω . u • w |= ϕ ⇐⇒ ∀u ∈ Σ + .∀w ∈ Σ ω .
) . d > 1 =⇒ X d-1 p ∈ sus(ϕ)
Let us consider σ ∈ Σ, Σ i ⊆ Σ. The proof is done by structural induction on ϕ ∈ LTL.

Base Case: ϕ ∈ { , ⊥, p } for some p ∈ AP .

-Case ϕ = . In this case, the proof is trivial since P ( , σ, AP i ) = and sus( ) = ∅.

-Case ϕ = ⊥. This case is similar to the previous one.

- -Case ϕ = ¬ϕ . On the one hand, we have sus P (¬ϕ , σ, AP i ) = sus ¬P (ϕ , σ, AP i ) = sus P (ϕ , σ, AP i ) .

On the other hand, we have sus(¬ϕ ) = sus(ϕ ). Thus, by applying directly the induction hypothesis on ϕ , we obtain the expected result. -Case ϕ = ϕ 1 ∨ ϕ 2 . On the one hand, we have

sus P (ϕ 1 ∨ ϕ 2 , σ, AP i ) = sus P (ϕ 1 , σ, AP i ) ∨ P (ϕ 2 , σ, AP i ) = sus P (ϕ 1 , σ, AP i ) ∪ sus P (ϕ 2 , σ, Σ i ) . Thus, X d ∈ sus P (ϕ 1 ∧ ϕ 2 , σ, AP i ) implies that X d p ∈ sus P (ϕ 1 , σ, AP i ) or X d p ∈ sus P (ϕ 2 , σ, AP i ) .
On the other hand, sus(ϕ 1 ∧ ϕ 2 ) = sus(ϕ 1 ) ∪ sus(ϕ 2 ). Hence, the result can be obtained by applying the induction hypothesis on either ϕ 1 or ϕ 2 depending on whether X d p ∈ sus P (ϕ 1 , σ, AP i ) or X d p ∈ sus P (ϕ 2 , σ, AP i ) .

- -Case ϕ = Gϕ . By definition of the progression rule for G and the definition of sus, we have sus P (Gϕ , σ, AP i ) = sus P (ϕ , σ, AP i ) ∧ Gϕ = sus P (ϕ , σ, AP i ) .

Since ϕ is behind a future temporal operator, the only case where sus P (ϕ , σ, AP i ) = ∅ is when ϕ is a state-formula. In that case, we have X d p ∈ sus P (ϕ , σ, AP i ) implies that d = 1.

-Cases ϕ ∈ {Fϕ , Xϕ , ϕ 1 Uϕ 2 }. These cases are similar to the previous one.

A.2.2 Proof of Theorem 2 (p. 12)

We have to prove that for any X m p ∈ LTL, a local obligation of some monitor M i ∈ M, m ≤ min(|M|, t + 1) at any time t ∈ N ≥0 . We will suppose that there are at least two components in the system (otherwise, the proof is trivial), i.e., |M| ≥ 2. The proof is done by distinguishing three cases according to the value of t ∈ N ≥0 .

First case: t = 0. In this case, we shall prove that m ≤ 1. The proof is done by a structural induction on ϕ ∈ LTL. Recall that for this case, where t = 0, we have ∀i ∈ [1, |M|]. lo(i, 0, ϕ) = P (ϕ, u i (0), AP i ).

Base case: ϕ ∈ { , ⊥, p ∈ AP }.

-Case ϕ = . In this case we have ∀i ∈ [1, |M|]. lo(i, 0, ) = P ( , u i (0), AP i ) = . Moreover, sus( ) = ∅. -Case ϕ = ⊥. This case is symmetrical to the previous one.

-Case ϕ = p ∈ AP . We distinguish two cases: p ∈ AP i and p / ∈ AP i . If p ∈ AP i , then lo(i, 0, p) ∈ { , ⊥} and sus lo(i, 0, p) = ∅. Else (p / ∈ AP i ), we have lo(i, 0, p) = Xp, and sus lo(i, 0, p) = {Xp} = {X 1 p}.

Structural Induction Case: ϕ ∈ {¬ϕ , ϕ 1 ∨ ϕ 2 , ϕ 1 ∧ ϕ 2 , Gϕ , Fϕ , Xϕ , ϕ 1 Uϕ 2 }. Our induction hypothesis states that the result holds for some formulae ϕ , ϕ 1 , ϕ 2 ∈ LTL.

-Case ϕ = ϕ 1 ∨ ϕ 2 . We have:

lo(i, 0, ϕ 1 ∨ ϕ 2 ) = P (ϕ 1 ∨ ϕ 2 , u i (0), AP i ) (lo definition for t = 0) = P (ϕ 1 , u i (0), AP i ) ∨ P (ϕ 2 , u i (0), AP i ) (progression on events) = lo(i, 0, ϕ 1 ) ∨ lo(i, 0, ϕ 2 )

(lo definition for t = 0) sus lo(i, 0, ϕ 1 ∨ ϕ 2 )

= sus lo(i, 0, ϕ 1 ) ∨ lo(i, 0, ϕ 2 ) = sus lo(i, 0, ϕ 1 ) ∪ sus lo(i, 0, ϕ 2 ) (sus definition)

We can apply the induction hypothesis on ϕ 1 and ϕ 2 to obtain successively: -Case ϕ = ¬ϕ . We have:

∀t ≥ N ≥0 .
lo(i, 0, ¬ϕ ) = P (¬ϕ , u i (0), AP i ) (lo definition) = ¬P (ϕ , u i (0), AP i ) (progression on events) sus lo(i, 0, ¬ϕ ) = sus ¬P (ϕ , u i (0), AP i ) = sus P (ϕ , u i (0), AP i ) (sus definition) = sus lo(i, 0, ϕ ) -Case ϕ = Xϕ . We have: lo(i, 0, Xϕ ) = P (Xϕ , u i (0), AP i ) (lo definition) = ϕ (progression on events) sus lo(i, 0, Xϕ ) = sus(ϕ )

Since ϕ is behind a future temporal operator, we have sus(ϕ ) = ∅.

-Case ϕ = Gϕ . We have: lo(i, 0, Gϕ ) = P (Gϕ , u i (0), AP i ) (lo definition) = P (ϕ , u i (0), AP i ) ∧ Gϕ (progression on events) = lo(i, 0, ϕ ) ∧ Gϕ (lo definition for ϕ ) sus lo(i, 0, Gϕ ) = sus lo(i, 0, ϕ ) ∧ Gϕ = sus lo(i, 0, ϕ ) ∪ sus(Gϕ ) (sus definition) = sus lo(i, 0, ϕ ) (sus(Gϕ ) = ∅)

-Case ϕ = Fϕ . This case is similar to the previous one.

-Case ϕ = ϕ 1 Uϕ 2 . We have: lo(i, 0, ϕ 1 Uϕ 2 ) (lo definition) = P (ϕ 1 Uϕ 2 , u i (0), AP i ) (progression on events) = P (ϕ 2 , u i (0), AP i ) ∨ P (ϕ 1 , u i (0), AP i ) ∧ ϕ 1 Uϕ 2 (lo definition for ϕ 1 and ϕ 2 )

= lo(i, 0, ϕ 2 ) ∨ lo(i, 0, ϕ 1 ) ∧ ϕ 1 Uϕ 2 sus lo(i, 0, ϕ 1 Uϕ 2 ) = sus lo(i, 0, ϕ 1 ) ∨ lo(i, 0, ϕ 2 ) ∧ ϕ 1 Uϕ 2 (sus definition)

= sus lo(i, 0, ϕ 2 ) ∪ sus lo(i, 0, ϕ 1 ) ∪ sus(ϕ 1 Uϕ 2 ) (sus(ϕ 1 Uϕ 2 = ∅) = sus lo(i, 0, ϕ 2 ) ∪ sus lo(i, 0, ϕ 1 ) We can apply the same reasoning on X d-1 p to find that i < j 1 < i and p / ∈ Π j 1 (AP ). Following the same reasoning and using Lemma 4, we can find a set of indexes {j 1 , . . . , j d } s.

For t ≥

A.2.3 Intermediate Lemmas and Notation

Let us first define some notations. Consider ϕ ∈ LTL, u ∈ Σ + , i ∈ [1, |M|]:

rp(ϕ, u) is the formula ϕ where past sub-formulae are removed and replaced by their evaluations using trace u. Formally: rp(ϕ, u) = match ϕ with

| X d p =⇒ if p ∈ u(|u| -d) ⊥ otherwise | ϕ 1 ∧ ϕ 2 =⇒ rp(ϕ 1 , u) ∧ rp(ϕ 2 , u) | ϕ 1 ∨ ϕ 2 =⇒ rp(ϕ 1 , u) ∨ rp(ϕ 2 , u) | ¬ϕ =⇒ ¬ rp(ϕ , u) | =⇒ ϕ
rp(ϕ, u, i) is the formula ϕ where past sub-formulae are removed (if possible) and replaced by their evaluations using only the sub-trace u i of u.

rp(ϕ, u, i) = match ϕ with The proof is done by induction on the formula ϕ ∈ LTL. Notice that when ϕ is not an atomic proposition, the lemma reduces to Lemma 1. Thus, we just need to treat the case ϕ = p ∈ AP . If ϕ = p ∈ AP . We have σ • w |= p ⇐⇒ p ∈ σ. Let us consider i ∈ [1, n], according to the definition of the progression function (1):

| X d p =⇒    if p ∈ u(|u| -d) ⊥ if p / ∈ u(
P (p, σ i , AP i ) =    if p ∈ σ i , ⊥ if p / ∈ σ i ∧ p ∈ AP i , Xp otherwise.
Let us distinguish three cases.

-Suppose p ∈ σ i . On the one hand, we have p ∈ σ and then Proof The proof is done by induction on t ∈ N ≥0 .

-For t = 0, the proof is trivial since ∀i ∈ [1, n].∀ϕ ∈ LTL. inlo(i, 0, ϕ) = ϕ and w 0 = w.

-Let us consider some t ∈ N ≥0 and suppose that the lemma holds. Let us consider i ∈ [1, n], we have: inlo(i, t + 1, ϕ) = kept(i, t) ∧ received(1, t + 1).

Let us now distinguish four cases according to the communication performed by local monitors at the end of time t, i.e., according to send(i, t) and send(j, t, i), for j ∈ [1, n] \ {i}.

-If send(i, t) = false and ∃j ∈ [1, n] \ {i}. send(j, t, i) = true. Then, we have: inlo(i, t + 1, ϕ) = P inlo(i, t, ϕ) ∧ j∈J inlo(j, t, ϕ), u i (t + 1), Σ i .

where ∀j ∈ J. send(j, t, i) = true. Applying the definition of the progression function, we have: inlo(i, t + 1, ϕ) = P inlo(i, t, ϕ), u i (t + 1), Σ i ∧ j∈J P inlo(j, t, ϕ), u i (t + 1), Σ i . Now, we have: w t+1 |= inlo(i, t + 1, ϕ) ⇐⇒ w t+1 |= P inlo(i, t, ϕ), u i (t + 1), Σ i ∧ ∀j ∈ J. w t+1 |= P inlo(j, t, ϕ), u i (t + 1), Σ i With:

w t+1 |= P inlo(i, t, ϕ), u i (t + 1), Σ i ⇐⇒ (w t ) 1 |= P inlo(i, t, ϕ), u i (t + 1), Σ i (w t+1 = (w t ) 1 ) ⇐⇒ (w(t) • w t+1 ) 1 |= P inlo(i, t, ϕ), u i (t + 1), Σ i ((w t ) 1 = (w(t) • w t+1 Proof By an easy induction on the number of components merged using Lemma 13.

Proof of

b 1 , b 2 ,

 12 and c 1 , c 2 ) are observed on a local component);

  then we have either w |= P (ϕ 1 , σ) or w |= P (ϕ 2 , σ). Let us treat the case where w |= P (ϕ 1 , σ) (the other case is similar). From w |= P (ϕ 1 , σ), we can apply the induction hypothesis on ϕ 1 to obtain σ • w |= ϕ 1 , and thus σ• w |= ϕ 1 ∨ ϕ 2 . -Case ϕ = ϕ 1 ∧ ϕ 2 .This case is similar to the previous one. -Case ϕ = Gϕ . Recall that, according to the progression function for operator G, P (Gϕ , σ) = P (ϕ , σ) ∧ Gϕ . -Let us suppose that σ • w |= Gϕ . According to the LTL semantics of operator G, we have ∀i ∈ N ≥0 . (σ • w) i |= ϕ . In particular, it implies that (σ • w) 0 |= ϕ , i.e., σ • w |= ϕ and ∀i ∈ N ≥0 . (σ • w 1 ) i |= ϕ , i.e., (σ • w) 1 = w |= Gϕ . Using the induction hypothesis on ϕ , from σ • w |= ϕ , we obtain w |= P (ϕ , σ). As expected, according to the LTL semantics of operator ∧, we have w |= P (Gϕ , σ) ∧ Gϕ = P (Gϕ , σ). -Let us suppose that w |= P (Gϕ , σ) = P (ϕ , σ) ∧ Gϕ . It follows that w |= P (ϕ , σ), and thus, using the induction hypothesis on ϕ , σ • w |= ϕ . Using the LTL semantics of operator G, from σ • w |= ϕ and w |= Gϕ , we deduce ∀i ∈ N ≥0 . w i |= ϕ , and then ∀i ∈ N. (σ • w) i |= ϕ , i.e., σ • w |= Gϕ . -Case ϕ = Fϕ . This case is similar to the previous one. -Case ϕ = Xϕ . On one hand, using the progression function for X, we have P (Xϕ , σ) = ϕ . On the other hand, using the LTL semantics of operator X, we have σ • w |= Xϕ iff w |= ϕ . Thus, we have σ • w |= Xϕ iff w |= ϕ iff (induction hypothesis on ϕ ) w |= P (Xϕ , σ).

  and applying the structural induction hypothesis on ϕ and the u i 's, we obtain ∀0 ≤ i ≤ |u| -1. w |= P (ϕ , u i ), and thus w |=|u|-1 i=0 P (ϕ , u i ). Using ∀i ≥ 0. w i = ((u•w) |u|-1 ) i |= ϕ , we obtain w |= Gϕ . As expected, according to the LTL semantics of ∧, we have w |= |u|-1 i=0 P (ϕ , u i ) ∧ Gϕ = P (Gϕ , u). -Let us suppose that w |= P (Gϕ , u). We have ∀0 ≤ i ≤ |u| -1. w |= P (ϕ , u i ) and w |= Gϕ .Using the structural induction hypothesis on ϕ and the u i 's, it follows that∀0 ≤ i ≤ |u| -1. u i • w = (u • w) i |= ϕ .Using the semantics of operator G, from w |= Gϕ and ∀0 ≤ i ≤ |u| -1. u i • w = (u • w) i |= ϕ , we deduce u • w |= Gϕ . -Case ϕ = Fϕ . This case is similar to the previous one. -Case ϕ = Xϕ . Recall that, by applying Lemma 5 on u and Xϕ , we have P (Xϕ , u) = P (ϕ , u 1 •σ). Using the LTL semantics of X, we have u • w |= Xϕ iff u 1 • w |= ϕ . Thus we have u • w |= Xϕ iff u 1 • σ • w |= ϕ iff (induction hypothesis on ϕ ) w |= P (ϕ , u 1 • σ) = P (Xϕ , u). -Case ϕ = ¬ϕ . Recall that, by applying Lemma 5 on u and ¬ϕ , we have P (¬ϕ , u) = ¬P (ϕ , u). Using the LTL semantics of operator ¬, we have ∀ϕ ∈ LTL.∀w ∈ Σ ω . w |= ϕ ⇐⇒ w |= ¬ϕ. Thus, we have u • w |= ¬ϕ iff u • w |= ϕ iff (induction hypothesis on ϕ ) w |= P (ϕ , u) iff w |= ¬P (ϕ , u) iff w |= P (¬ϕ , u).

  and thus u • w |= ϕ 1 Uϕ 2 . Else (i ≤ |u| -1), we can follow a similar reasoning to obtain the expected result. • Sub-case P (ϕ 1 Uϕ 2 , u) = . Similarly, in this case, we can show that ∃k ∈ N ≥0 . (u • w) k |= ϕ 2 . Then we consider k min the minimal k s.t. (u • w) k |= ϕ 2 . Then, we can show that ∀k < k min . (u • w) k |= ϕ 1 . And then u • w |= ϕ 1 Uϕ 2 .

) 1 )

 1 ⇐⇒ w t |= inlo(i, t, ϕ) (Induction Hypothesis) where ϕ is a local obligation at time |u | and {i 1 , . . . , in} ⊇ [1, |M |] (because of the ordering between components). According to Lemma 7 -item 5, we have:rp(• . . . • rp(rp(ϕ, u , i), u , i 1 ) • . . . •, in) = rp(ϕ, u ) = .Following the definition of the progression function for , necessarily, the resulting local obligation at time |u | + n is .Lemma 14 Let us consider the architecture M = {merge(Mn, merge(. . . , merge(M 2 , M 1 )}, then we have:∀u ∈ Σ + .∀ϕ ∈ LTL. u |= M D ϕ = /⊥ =⇒ ∀u ∈ Σ + . |u | ≥ n =⇒ u • u |= M D = /⊥.

  Theorem 4 (p. 15). Based on Lemma14, we can easily show Theorem 4. Proof Let us consider an n-component architecture M = {M 1 , . . . , Mn}, a trace u ∈ Σ + and a formula ϕ ∈ LTL. Let us suppose that u |= C ϕ = /⊥. As the alphabets of monitors are respectively Σ 1 , . . . , Σn and each monitor M i is observing a sub-trace u i of u where the hypothesis about alphabets partitioning mentioned in Section 2 holds, we can consider the centralised setting equivalent to monitoring with architecture M = {merge(Mn, merge(. . . , merge(M 2 , M 1 )} where there is a unique monitor M observing the same trace u. Using Lemma14, from u |= M D ϕ = /⊥, we get ∀u ∈ Σ + . |u | ≥ n =⇒ u • u |= M D = /⊥, as required.

  The algorithm Local Monitor, executed on each M i , returns (resp. ⊥), if σ |= D ϕ t i (resp. σ |= D ϕ t i ) holds, where σ ∈ Σ i is the projection of an event to the observable set of actions of the respective monitor, and ϕ t i the monitor's current local obligation. L1. [Next goal.] Let t ∈ N ≥0 denote the current time step and ϕ t i be the monitor's current local obligation. If t = 0, then set ϕ t i := ϕ. L2. [Receive event.] Read next σ. L3. [Receive messages.] Let {ϕ j } j∈[1,n],j =i be the set of received obligations at time t from other monitors. Set ϕ t

i := ϕ t i ∧ j∈[

1,n],j =i ϕ j . L4. [Progress.] Determine P (ϕ t i , σ, AP i ) and store the result in ϕ t+1 i . L5. [Evaluate and return.] If ϕ t+1 i

  t.kept(i, t) ∈ LTL is the local obligation kept by monitor i at time t for the next round (time t + 1). received(i, t, j) ∈ LTL is the obligation received by monitor i at time t by monitor j with i = j. received(i, t) ∈ LTL is the obligation received by monitor i at time t from all monitors.inlo(i, t, ϕ) ∈ LTL is the local obligation of monitor i at time t when monitoring the global specification formula ϕ, before applying the progression function, i.e, after applying step L3 of Algorithm L. lo(i, t, ϕ) ∈ LTL is the local obligation of monitor i at time t when monitoring the global specification formula ϕ after applying the progression function, i.e., after applying step L4 of Algorithm L. mou(ϕ) ∈ sus(ϕ) is the most urgent formula belonging to the set of urgent subformulae of ϕ. ulo(i, t, ϕ) = sus lo(i, t, ϕ) is the set of urgent local obligations of monitor i at time

t when monitoring the global specification formula ϕ.

Table 2 :

 2 Benchmarks for random LTL formulae -flipcoin distrib. Alphabet {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 , a 2 |b 1 , b 2 |c 1 , c 2 } Alphabet {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 |a 2 |b 1 |b 2 |c 1 |c 2 }

		centralised	decentralised	diff. ratio	delay
	|ϕ|	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	1	1.344	4.032	1.642	1.049	1.2217	0.2601	1	3
	2	6.673	20.019	7.038	2.652	1.0546	0.1324	1	3
	3	12.196	36.588	12.694	5.672	1.0408	0.155	1	3
	4	29.415	88.245	29.949	13.125	1.0181	0.1487	1	3
	5	64.935	194.805	65.501	36.782	1.0087	0.1888	1	3
	6	72.437	217.311	73.013	52.499	1.0079	0.2415	1	3
	(b) centralised	decentralised	diff. ratio	delay
	|ϕ|	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	1	1.698	5.094	2.082	1.37	1.2261	0.2689	1	3
	2	2.69	8.07	3.212	2.038	1.194	0.2525	1	3
	3	8.19	24.57	8.748	4.39	1.0681	0.1786	1	3
	4	10.546	31.638	11.368	8.293	1.0779	0.2621	1	3
	5	11.284	33.852	11.99	9.504	1.0625	0.207	1	3
	6	20.984	62.952	21.676	17.484	1.0329	0.2777	1	3
	(c) centralised	decentralised	diff. ratio	delay
	|ϕ|	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	1	1.948	11.688	2.64	3.482	1.552	0.2979	1	3
	2	4.194	25.164	5.128	5.44	1.2226	0.2161	1	3
	3	6.748	40.488	7.844	8.73	1.1624	0.2156	1	3
	4	8.4	50.4	9.746	10.656	1.1602	0.2114	1	3
	5	10.154	60.924	11.512	11.354	1.1337	0.1863	1	3
	6	22.536	135.216	24.014	24.512	1.0655	0.1812	1	3

(a) Alphabet {a, b, c} -Distributed alphabet {a|b|c}

Table 3 :

 3 Benchmarks for random LTL formulae -flipcoin distrib. -only change. Alphabet {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 , a 2 |b 1 , b 2 |c 1 , c 2 } Alphabet {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 |a 2 |b 1 |b 2 |c 1 |c 2 }

		centralised	decentralised	diff. ratio	delay
	|ϕ|	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	1	1.3894	3.558	1.73	1.171	1.2455	0.3291	1	2
	2	1.801	4.214	2.315	2.083	1.2853	0.4943	1	3
	3	7.429	12.767	8.041	3.562	1.0823	0.279	1	3
	4	19.854	31.424	20.529	9.742	1.0309	0.31	1	3
	5	24.32	38.0	25.073	19.594	1.0309	0.5156	1	3
	6	51.34	78.34	52.12	46.84	1.0151	0.5979	1	3
	(b) centralised	decentralised	diff. ratio	delay
	|ϕ|	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	1	1.464	4.056	1.93	1.478	1.3183	0.3643	1	2
	2	2.156	5.636	2.728	2.246	1.2653	0.3985	1	2
	3	4.208	10.198	4.942	4.11	1.1744	0.403	1	3
	4	5.692	13.524	6.506	5.6	1.143	0.414	1	2
	5	9.568	22.27	10.37	9.476	1.0838	0.4255	1	2
	6	9.808	22.84	10.72	11.68	1.0931	0.5114	1	3
	(c) centralised	decentralised	diff. ratio	delay
	|ϕ|	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	1	1.224	3.351	1.55	1.075	1.2663	0.3207	1	2
	2	1.855	3.942	2.381	2.056	1.2835	0.5215	1	2
	3	4.2	5.383	4.844	3.587	1.1511	0.6663	1	2
	4	9.346	8.404	10.044	7.834	1.0746	0.9321	1	2
	5	13.884	11.344	14.681	11.174	1.0574	0.985	1	3
	6	19.1	14.314	19.892	19.475	1.0414	1.3605	1	3

(a) Alphabet {a, b, c} -Distributed alphabet {a|b|c}

Table 4 :

 4 Benchmarks for random LTL formulae -Bernouilli distrib. 0.1 -only change. Alphabet {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 , a 2 |b 1 , b 2 |c 1 , c 2 }. Alphabet {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 |a 2 |b 1 |b 2 |c 1 |c 2 }.

		centralised	decentralised	diff. ratio	delay
	|ϕ|	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	1	1.246	3.576	1.745	1.546	1.4004	0.4323	1	2
	2	1.817	4.279	2.491	2.35	1.3709	0.5491	1	3
	3	3.741	6.437	4.041	3.562	1.0823	0.279	1	3
	4	19.854	31.424	20.529	9.742	1.0309	0.31	1	3
	5	24.32	38.0	25.073	19.594	1.0309	0.5156	1	3
	6	51.34	78.34	52.12	46.84	1.0151	0.5979	1	3
	(b) centralised	decentralised	diff. ratio	delay
	|ϕ|	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	1	1.246	3.576	1.745	1.546	1.400	0.4323	1	2
	2	1.817	4.279	2.491	2.35	1.3709	0.5491	1	2
	3	3.741	6.437	4.561	3.931	1.2191	0.6106	1	3
	4	4.971	7.673	5.853	5.546	1.7774	0.7227	1	2
	5	6.773	9.523	7.685	7.918	1.1346	0.8314	1	3
	6	11.505	14.219	12.399	13.7014	1.077	0.9637	1	3
	(c) centralised	decentralised	diff. ratio	delay
	|ϕ|	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	1	1.253	6.738	2.131	3.942	1.7007	0.585	1	5
	2	1.989	7.876	3.254	5.749	1.6359	0.7299	1	5
	3	3.586	9.795	5.096	8.087	1.421	0.8256	1	5
	4	4.914	11.299	6.744	9.949	1.3724	0.8805	1	6
	5	8.773	15.803	10.636	14.663	1.2123	0.9278	1	6
	6	9.943	16.893	11.978	16.047	1.2046	0.9499	1	6

(a) Alphabet {a, b, c} -Distributed alphabet {a|b|c}.

Table 5 :

 5 Benchmarks for random LTL formulae -Bernouilli distrib. 0.01 -only change. (a) Alphabet {a, b, c} -Distributed alphabet {a|b|c}. Alphabet {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 , a 2 |b 1 , b 2 |c 1 , c 2 }. Alphabet {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 |a 2 |b 1 |b 2 |c 1 |c 2 }.

		centralised	decentralised	diff. ratio	delay
	|ϕ|	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	1	1.226	3.363	1.628	1.289	1.3278	0.3832	1	2
	2	2.78	3.644	3.267	2.423	1.1751	0.6649	1	2
	3	6.091	3.992	6.67	5.382	1.095	1.3481	1	3
	4	10.548	4.416	11.118	10.397	1.0631	2.3543	1	3
	5	14.056	4.765	14.771	14.493	1.0508	3.0415	1	3
	6	19.463	5.004	20.114	23.72	1.0334	4.7402	1	3
	(b) centralised	decentralised	diff. ratio	delay
	|ϕ|	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	1	1.236	3.552	1.744	1.544	1.411	0.4346	1	2
	2	2.204	4.3	2.916	2.815	1.323	0.7032	1	2
	3	4.992	4.652	5.835	6.69	1.1668	1.438	1	3
	4	10.604	5.353	11.46	12.076	1.0807	2.2559	1	3
	5	12.473	5.733	13.34	17.651	1.0695	3.0788	1	3
	6	19.443	6.38	20.256	26.771	1.0418	4.196	1	3
	(c) centralised	decentralised	diff. ratio	delay
	|ϕ|	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	1	1.205	6.669	2.053	3.889	1.7037	0.5831	1	4
	2	2.752	7.411	3.994	6.861	1.4513	0.9257	1	5
	3	6.75	8.233	8.357	13.632	1.238	1.6557	1	6
	4	10.329	8.798	12.042	18.158	1.1658	2.0638	1	5
	5	13.723	9.247	15.537	23.124	1.1321	2.5007	1	6
	6	17.732	9.862	19.613	29.316	1.106	2.9726	1	6

Table 6 :

 6 Benchmarks for LTL specification patterns -flipcoin distrib. Alphabet {a 1 , a 2 , b , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 , a 2 |b 1 , b 2 |c 1 , c 2 }.

		centralised	decentralised	diff. ratio	delay
	pattern	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	absence	136.56	409.68	137.16	27.451	1.0043	0.067	0.597	2
	existence	189.27	567.81	189.77	38.737	1.0026	0.0682	0.501	3
	bounded existence	157.20	471.60	157.88	62.96	1.0043	0.1335	0.682	3
	universal	93.64	290.92	94.29	5.952	1.0069	0.0211	0.65	2
	precedence	294.93	749.80	250.48	55.85	1.0022	0.0744	0.552	3
	response	636.44	1,909.32	636.71	386.11	1.0004	0.2022	0.27	3
	precedence chain	198.96	596.89	199.47	54.23	1.0025	0.0908	0.506	3
	response chain	573.92	1,721.78	574.26	374.22	1.0005	0.2173	0.334	3
	constrained chain	385.96	1,156.22	385.96	198.84	1.0014	0.1719	0.556	2
	(b) centralised	decentralised	diff. ratio	delay
	pattern	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	absence	146.49	439.47	147.23	38.58	1.005	0.0877	0.744	2
	existence	203.20	609.81	203.91	57.41	1.0034	0.0941	0.702	3
	bounded existence	214.34	643.03	214.96	91.20	1.0028	0.1418	0.62	3
	universal	82.93	248.79	83.84	17.27	1.011	0.0694	0.914	2
	precedence	176.61	529.85	177.27	40.33	1.0037	0.0761	0.658	2
	response	632.56	1,897.68	632.93	394.87	1.0005	0.208	0.368	2
	precedence chain	181.84	545.53	182.43	52.69	1.0032	0.0965	0.592	3
	response chain	584.28	1,752.84	584.70	434.80	1.0007	0.248	0.426	2
	constrained chain	376.63	1,129.89	377.33	249.71	1.0018	0.221	0.706	3
		centralised	decentralised	diff. ratio	delay
	pattern	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	absence	159.37	956.22	160.73	73.76	1.0085	0.0771	1.36	6
	existence	222.57	1329.45.81	222.9	92.29	1.0059	0.0694	1.324	5
	bounded existence	276.94	1607.67	269.11	171.242	1.0043	0.1065	1.166	5
	universal	73.62	441.75	75.44	25.86	1.0246	0.0585	1.814	5
	precedence	187.22	1123.34	188.66	67.78	1.0076	0.0603	1.438	6
	response	690.02	4,140.14	690.73	521.52	1.001	0.1259	0.71	5
	precedence chain	171.25	1027.54	172.62	83.36	1.0079	0.0811	1.364	5
	response chain	588.74	3,532.48	589.66	489.67	1.0015	0.1386	0.912	5
	constrained chain	364.86	2,189.17	366.37	300.82	1.0041	0.1374	1.512	6

(a) Alphabet {a, b, c} -Distributed alphabet {a|b|c}.

(c) Alphabet {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 |a 2 |b 1 |b 2 |c 1 |c 2 }.

Table 7 :

 7 Benchmarks for LTL specification patterns -flipcoin distrib. -only change. Alphabet {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 , a 2 |b 1 , b 2 |c 1 , c 2 }. Alphabet {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 |a 2 |b 1 |b 2 |c 1 |c 2 }.

		centralised	decentralised	diff. ratio	delay
	pattern	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	absence	140.74	212.67	141.33	33.74	1.0041	0.1586	0.589	2
	existence	181.23	273.56	181.76	33.172	1.0029	0.1212	0.537	3
	bounded existence	177.91	268.37	178.45	56.912	1.003	0.212	0.54	2
	universal	89.86	135.99	90.55	8.779	1.0077	0.0645	0.692	3
	precedence	239.84	361.54	240.33	48.78	1.002	0.1349	0.49	3
	response	617.4	927.87	617.74	358.40	1.0004	0.3862	0.287	3
	precedence chain	226.88	341.83	227.35	65.09	1.002	0.1904	0.469	2
	response chain	588.65	883.89	589.01	384.78	1.0006	0.4353	0.359	3
	constrained chain	382.07	574.46	382.60	210.66	1.0013	0.3667	0.534	2
	(b) centralised	decentralised	diff. ratio	delay
	pattern	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	absence	130.23	293.75	130.92	42.06	1.005	0.1431	0.692	2
	existence	189.83	426.33	189.83	55.17	1.0037	0.1294	0.718	3
	bounded existence	265.51	597.78	266.1	114.16	1.022	0.1909	0.588	2
	universal	83.36	188.24	84.33	18.06	1.0116	0.0959	0.972	2
	precedence	228.54	515.43	229.19	61.18	1.0028	0.1187	0.657	3
	response	671.2	1,511.66	671.54	432.48	1.0005	0.286	0.34	2
	precedence chain	174.40	393.25	175.02	56.26	1.0035	0.143	0.615	3
	response chain	600.9	1,352.32	601.34	444.26	1.0007	0.3285	0.436	3
	constrained chain	349.41	786.06	350.18	232.42	1.0021	0.2956	0.762	3
	(c) centralised	decentralised	diff. ratio	delay
	pattern	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	absence	122.70	370.93	124.12	67.52	1.011	0.182	1.419	5
	existence	195.22	590.0	196.4	90.65	1.0065	0.0694	1.324	5
	bounded existence	231.20	695.66	232.49	152.81	1.0051	0.2196	1.88	5
	universal	86.65	262.6	88.44	43.79	1.0206	0.1667	1.79	6
	precedence	220.53	665.01	221.89	99.07	1.0061	0.1489	1.359	6
	response	669.78	2,012.61	670.45	530.57	1.001	0.2636	0.675	5
	precedence chain	181.91	548.66	183.28	88.97	1.0075	0.1621	1.376	5
	response chain	608.81	1,830.5	609.69	515.21	1.0014	0.2814	0.884	5
	constrained chain	327.75	985.73	329.35	276.10	1.0048	0.2801	1.599	6
	low probability for change of the truth value of a local proposition to occur. Similar to the
	first setting, as the size of local alphabets grows, the performance of decentralised monitor-
	ing improves again.

(a) Alphabet {a, b, c} -Distributed alphabet {a|b|c}.

Table 8 :

 8 Benchmarks for LTL specification patterns -Bernouilli distrib. 0.1 -only change. Alphabet {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 , a 2 |b 1 , b 2 |c 1 , c 2 }. Alphabet {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 |a 2 |b 1 |b 2 |c 1 |c 2 }.

		centralised	decentralised	diff. ratio	delay
	pattern	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	absence	205.864	114.083	206.373	46.29	1.0024	0.4057	0.509	2
	existence	209.101	116.307	209.616	44.902	1.0024	0.386	0.515	2
	bounded existence	240.913	132.553	241.395	101.907	1.002	0.7688	0.482	2
	universal	115.629	64.682	116.269	19.286	1.0055	0.2981	0.64	2
	precedence	275.837	151.444	276.357	58.52	1.0018	0.3864	0.52	3
	response	674.052	367.017	674.297	382.044	1.0003	1.0409	0.245	2
	precedence chain	262.873	144.468	263.324	87.233	1.0017	0.6038	0.451	2
	response chain	600.545	327.678	600.884	364.14	1.0005	1.1112	0.339	2
	constrained chain	414.809	226.17	415.331	251.869	1.0012	1.1136	0.522	2
	(b) centralised	decentralised	diff. ratio	delay
	pattern	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	absence	230.052	247.7861	230.61	100.18	1.0024	0.4041	0.558	2
	existence	268.23	288.802	268.845	106.454	1.0022	0.3686	0.607	2
	bounded existence	279.834	301.00	280.35	170.31	1.0018	0.5658	0.524	2
	universal	160.29	174.023	161.11	36.879	1.0051	0.2119	0.82	2
	precedence	304.71	327.66	305.25	119.57	1.0017	0.3649	0.536	3
	response	703.48	757.00	706.79	475.053	1.0004	0.6275	0.307	2
	precedence chain	234.17	253.82	234.67	111.248	1.0021	0.4382	0.506	2
	response chain	643.90	689.22	644.26	486.95	1.0006	0.7065	0.36	3
	constrained chain	449.05	482.39	449.66	348.43	1.0013	0.7223	0.609	3
	(c) centralised	decentralised	diff. ratio	delay
	pattern	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	absence	70.216	90.342	71.02	44.054	1.0114	0.4876	0.804	5
	existence	70.424	89.15	71.402	49.974	1.0138	0.5381	0.978	5
	bounded existence	349.78	383.04	350.64	260.72	1.0024	0.6807	0.864	5
	universal	40.37	53.984	41.932	28.07	1.0386	0.5199	1.562	6
	precedence	78.412	98.72	79.352	53.302	1.0119	0.5399	0.94	5
	response	148.25	181.846	148.774	133.324	1.0035	0.7331	0.524	5
	precedence chain	58.66	75.23	59.6	44.486	1.016	0.5913	0.94	5
	response chain	140.366	172.744	140.916	119.324	1.0039	0.6907	0.55	2

(a) Alphabet {a, b, c} -Distributed alphabet {a|b|c}.

Table 9 :

 9 Benchmarks for LTL specification patterns -Bernouilli distrib. 0.01 -only change. Alphabet {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 , a 2 |b 1 , b 2 |c 1 , c 2 }. Alphabet {a 1 , a 2 , b 1 , b 2 , c 1 , c 2 } -Distributed alphabet {a 1 |a 2 |b 1 |b 2 |c 1 |c 2 }.

		centralised	decentralised	diff. ratio	delay
	pattern	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	absence	93.93	9.314	97.162	28.2894	1.0023	3.1022	0232	2
	existence	102.9	9.406	103.136	41.52	1.0022	4.4142	0.236	2
	bounded existence	512.44	34.33	512.67	309.31	1.004	9.01	0.23	2
	universal	63.664	7.794	60.092	22.942	1.0067	2.9435	0.428	2
	precedence	91.958	8.952	92.222	32.656	1.0028	3.6478	0.264	2
	response	155.262	13.022	155.372	105.336	1.0007	8.089	0.11	2
	precedence chain	100.782	9.566	100.962	51.138	1.0017	5.3458	0.18	2
	response chain	157.972	13.384	158.102	102.224	1.0008	7.6377	0.13	2
	constrained chain	142.842	12.244	143.038	104.018	1.0013	8.4954	0.196	2
	(b) centralised	decentralised	diff. ratio	delay
	pattern	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	absence	110.68	17.008	110.93	75.17	1.0023	4.4196	0.258	2
	existence	114.256	17.716	114.498	59.954	1.0021	3.3841	0.242	2
	bounded existence	549.37	69.11	549.68	404.98	1.0005	5.86	0.314	2
	universal	83.972	13.874	84.22	42.69	1.0065	3.0769	0.548	2
	precedence	102.132	16.386	102.376	68.208	1.0023	4.1625	0.244	2
	response	169.29	24.878	169.352	153.262	1.0003	6.1605	0.062	2
	precedence chain	103.198	15.93	103.426	85.126	1.0022	5.3437	0.228	2
	response chain	161.816	23.466	161.976	150.63	1.0009	6.419	0.16	2
	constrained chain	147.836	22.136	148.06	143.086	1.0015	6.4639	0.224	2
	(c) centralised	decentralised	diff. ratio	delay
	pattern	|trace|	#msg.	|trace|	#msg.	|trace|	#msg.	avg	max
	absence	107.12	20.18	107.62	86.134	1.0047	4.2682	0.506	5
	existence	110.974	20.636	111.452	92.148	1.0043	4.4675	0.478	4
	bounded existence	532.72	71.74	533.23	455.47	1.0009	6.3481	0.511	5
	universal	76.602	17.55	77.692	54.562	1.0142	3.1089	1.09	5
	precedence	97.616	19.458	98.196	71.196	1.0059	3.6569	0.58	5
	response	166.492	28.322	166.662	176.488	1.001	6.2314	0.17	5
	precedence chain	98.04	19.01	98.608	90.046	1.0057	4.7367	0.568	5
	response chain	162.5	28.084	162.804	160.982	1.0018	5.7321	0.304	5
	constrained chain	149.92	25.952	150.38	173.814	1.003	6.6975	0.46	5

(a) Alphabet {a, b, c} -Distributed alphabet {a|b|c}.

  then applying the induction hypothesis on ϕ 2 , we have σ • w |= ϕ 2 ⇐⇒ w |= . Then, from σ•w |= ϕ 2 , we obtain, according to the LTL semantics of operator U, σ•w |= ϕ 1 Uϕ 2 . If P (ϕ 1 , σ) ∧ ϕ 1 Uϕ 2 = , we directly deduce that ϕ 1 Uϕ 2 = , and then this case reduces to the case where ϕ = , already treated.• If P (ϕ 2 , σ) = and P (ϕ 1 , σ)∧ϕ 1 Uϕ 2 = , then we have P (ϕ 2 , σ) = ¬(P (ϕ 1 , σ)∧ ϕ 1 Uϕ 2 ) = ¬P (ϕ 1 , σ) ∨ ¬(ϕ 1 Uϕ 2 ).Applying the induction hypothesis on ϕ 1 and ϕ 2 , we have σ•w |= ϕ 1 ⇐⇒ w |= P (ϕ 1 , σ), and σ•w |= ϕ 2 ⇐⇒ w |= P (ϕ 2 , σ), and thus σ • w |= ϕ 2 ⇐⇒ (σ • w |= ϕ 1 ∨ w |= ϕ 1 Uϕ 2 ). Let us now follow the LTL semantics of operator U and consider the two cases: σ • w |= ϕ 2 or σ • w |= ϕ 2 . If σ • w |= ϕ 2 , thus σ • w |= ϕ 1 Uϕ 2 (according to the LTL semantics of U). Else (σ • w |= ϕ 2 ), then σ • w |= ϕ 1 and w |= ϕ 1 Uϕ 2 , and thus σ • w |= ϕ 1 Uϕ 2 . • If P (ϕ 1 Uϕ 2 , σ) = , it means that either w |= P (ϕ 2 , σ) or w |= P (ϕ 1 , σ) ∧ϕ 1 Uϕ 2 . • If w |= P (ϕ 2 , σ), then applying the induction hypothesis on ϕ 2 , we have σ • w |= ϕ 2 . Then, following the LTL semantics of operator U, we obtain σ • w |= ϕ 1 Uϕ 2 . • If w |= P (ϕ 1 , σ)∧ϕ 1 Uϕ 2 , then we have w |= P (ϕ 1 , σ) and w |= ϕ 1 Uϕ 2 . Applying the induction hypothesis on ϕ 1 , we have σ • w |= ϕ 1 . From w |= ϕ 1 Uϕ 2 , we have ∃i ∈ N ≥0 . w i |= ϕ 2 ∧ ∀0 ≤ l < i. w l |= ϕ 1 . It implies that (σ • w) i+1 |= ϕ 2 and ∀0 < l < i + 1. (σ • w) l |= ϕ 1 . Using, σ • w |= ϕ 1 , i.e., (σ • w) 0 |= ϕ 1 and the LTL semantics of operator U, we finally obtain σ • w |= ϕ 1 Uϕ 2 .

	A.1.2 Proof of Lemma 2 (p. 6)

  1 , u) ∨ P (ϕ 2 , u).-Let us suppose that u•w |= ϕ 1 ∨ϕ 2 . Let us distinguish two cases: ϕ 1 ∨ϕ 2 = and ϕ 1 ∨ϕ 2 = .Ifϕ 1 ∨ ϕ 2 = ,then this case reduces to the case where ϕ = already treated. If ϕ 1 ∨ ϕ 2 = , it means that either u • w |= ϕ 1 or u • w |= ϕ 2 . Let us treat the case where u • w |= ϕ 1 (the other case is similar). From u • w |= ϕ 1 , we can apply the structural induction hypothesis on ϕ 1 to obtain w |= P (ϕ 1 , u), and then, w |= P (ϕ 1 , u) ∨ P (ϕ 2 , u) = P (ϕ 1 ∨ ϕ 2 , u). -Let us suppose that w |= P (ϕ 1 ∨ ϕ 2 , u). Let us again distinguish two cases. If P (ϕ 1 , u) ∨ P (ϕ 2 , u) = , then it reduces to the case where ϕ = already treated. If P (ϕ 1 , u)∨P (ϕ 2 , u) = , then we have either w |= P (ϕ 1 , u) or w |= P (ϕ 2 , u). Let us treat the case where w |= P (ϕ 1 , u) (the other case is similar). From w |= P (ϕ 1 , u), we can apply the structural induction hypothesis on ϕ 1 to obtain u • w |= ϕ 1 , and thus, using the LTL semantics of ∨, u • w |= ϕ 1 ∨ ϕ 2 .

  w |= P (ϕ, u). Consequently, when P (ϕ, u) = , we have ∀u ∈ Σ + .∀w ∈ Σ ω . u • w |= ϕ, i.e., u ∈ good(ϕ). Also, when P (ϕ, u) = ⊥, we have ∀u ∈ Σ + .∀w ∈ Σ ω . u • w |= ϕ, i.e., u ∈ bad(ϕ).Consider M = {M 1 , . . . , Mn} where each monitor M i has a set of local atomic propositions AP i = Π i (AP ) and observes the set of events Σ i , we shall prove that: ∀i ∈[1, n].∀σ ∈ Σ i .∀ϕ ∈ LTL.∀X

	A.2 Proofs for Section 6
	A.2.1 Proof of Lemma 4 (p. 15)

d p ∈ sus P (ϕ, σ, AP i

  Case ϕ = p ∈ AP . If p ∈ AP i , then P (p , σ, AP i ) ∈ { , ⊥} and sus(P (p , σ, AP i )) = ∅. Else (p / ∈ AP i ), P (p , σ, AP i ) = Xp and sus P (p , σ, AP i ) = ∅. Induction Case: ϕ ∈ {¬ϕ , ϕ 1 ∨ϕ 2 , ϕ 1 ∧ϕ 2 , X d p , Gϕ , Fϕ , Xϕ , ϕ 1 Uϕ 2 }. Our induction hypothesis states that the result holds for some formulae ϕ , ϕ 1 , ϕ 2 ∈ LTL.

  ∀ϕ ∈ LTL.∀X m p ∈ sus lo(i, t, ϕ 1 ) . m ≤ 1 ∀t ≥ N ≥0 .∀ϕ ∈ LTL.∀X m p ∈ sus lo(i, t, ϕ 2 ) . m ≤ 1 ∀t ≥ N ≥0 .∀ϕ ∈ LTL.∀X m p ∈ sus lo(i, t, ϕ 1 ) ∪ sus lo(i, t, ϕ 2 ) . m ≤ 1

  1, the proof is done by reductio ad absurdum. Let us consider some t ∈ N and suppose that the theorem does not hold at time t. It means that: ∃ϕ ∈ LTL.∃i ∈ [1, |M|].∃X d p ∈ ulo(i, t, ϕ). d > min(|M|, t + 1). According to Lemma 3, since ulo(i, t, ϕ) = |M| j=1,j =i sus P (received(i, t), u i (t)) , it means that ∃j 1 ∈ [1, |M|] \ {i}.X d p ∈ sus P (received(i, t, j 1 ), u i (t), AP i ) . Using Lemma 4, we have X d-1 p ∈ sus(received(i, t, j 1 )). It implies that send(j 1 , t -1, i) = true andM i = Mon M j 1 , Prop(ulo(j 1 , t -1, ϕ)) . We deduce that i = min j ∈ [1, |M|] \ {j 1 } | ∃p ∈ Prop(ulo(j, t -1, ϕ)). p ∈ AP i .Moreover, from X d p ∈ ulo(i, t, ϕ), we find p / ∈ AP i , with i < i .

  t. {j 1 , . . . , j d } ⊇ [1, |M|] ∧ ∀j ∈ {j 1 , . . . , j d }. p / ∈ AP j ∧ j ∈ [1, |M|]Moreover, due to the ordering between components, we know that∀k 1 , k 2 ∈ [1, d]. k 1 < k 2 =⇒ j k 1 < j k 2 .Case 0 < t < |M|. In this case we have d > t + 1, and thus, we haveX Case t ≥ |M|. In this case, ∀k 1 , k 2 ∈ [1, d]. k 1 < k 2 =⇒ j k 1 < j k 2 implies that ∀j k 1 , j k 2 ∈ {j 1 , . . . , j d }. k 1 = k 2 =⇒ j k 1 = j k 2 .Hence, we have p / ∈

d p ∈ sus lo(jt, 0, ϕ) with d > 1 which is a contradiction with the result shown for t = 0. j d j=j 1 AP j ⊇ AP . This is impossible.

  |u| -d) and p ∈ AP i X d p otherwise | ϕ 1 ∧ ϕ 2 =⇒ rp(ϕ 1 , u, i) ∧ rp(ϕ 2 , u, i) | ϕ 1 ∨ ϕ 2 =⇒ rp(ϕ 1 , u, i) ∨ rp(ϕ 2 , u, i)Proof We shall prove that:∀i ∈ [1, n]. ∀ϕ ∈ LTL.∀σ ∈ Σ.∀σ i ∈ Σ i .∀w ∈ Σ ω . σ • w |= ϕ ⇐⇒ (σ • w) 1 |= P (ϕ, σ i , AP i ).

	| ¬ϕ	=⇒ ¬ rp(ϕ , u, i)
	|	=⇒ ϕ

  σ • w |= p. On the other hand, we have P (p, σ i , AP i ) = and thus w |= P (p, σ i , AP i ). -Suppose p / ∈ σ i and p ∈ AP i . One the one hand, we have p ∈ σ, and, because p ∈ AP i we have p / ∈ σ; and thus σ • w |= p. On the other hand, we have P (p, σ i , AP i ) = ⊥. -Suppose p / ∈ σ i and p / ∈ AP i , we have(σ • w) 1 |= Xp ⇐⇒ (σ • w) -1 1 |= Xp ⇐⇒ σ • w |= p.The following lemma states that "the satisfaction of an LTL formula" is propagated by the decentralised monitoring algorithm. ≥0 .∀i ∈ [1, n].∀ϕ ∈ LTL.∀w ∈ Σ ω . inlo(i, t, ϕ) = # =⇒ w |= ϕ ⇐⇒ w t |= inlo(i, t, ϕ) .

	Lemma 10
	∀t ∈ N

The assumption of atomic proposition locality is not a restriction of our approach but it simplifies the presentation.

Note that L(ϕ), being a liveness language, does not have any bad prefixes.

Compared to RuleR[START_REF] Barringer | Rule systems for run-time monitoring: from Eagle to RuleR[END_REF], the state-of-art rule-based runtime verification tool, for LTL specifications, our simplification function produced better results (see[START_REF]DECENTMON Website[END_REF]).

Our experiments show that this way of measuring the size of a formula is more representative of how difficult it is to progress it in a decentralised manner. Formulae of size above 6 are not realistic in practice.

We conducted benchmarks (not reported here) with traces generated with the Bernouilli probability distributions with parameters 0.9 and 0.99 and the results followed the same trends.

Without loss of generality, we assume that the priority of a monitor is given by its index. If this hypothesis does not hold initially, the indexes of components can be re-arranged prior to monitoring so that this hypothesis holds.

A Proofs

A.1 Proofs for Sec. 3

A.1.1 Proof of Lemma 1 (p. 6)

The following inductive proof follows the argument conveyed by Proposition 3 of [START_REF] Bacchus | Planning for temporally extended goals[END_REF]. For completeness sake, here we want to give the complete, formal, detailed proof.

The lemma is a direct consequence of the semantics of LTL and the definition of progression (Definition 2). Recall that this lemma states that the progression function "mimics" LTL semantics on some event σ.

-Case ϕ = ⊥. Similarly, in this case, the proof is trivial since P (⊥, σ) = ⊥ and bad(⊥) = Σ * .

-Case ϕ = p ∈ AP .

Let us suppose that P (ϕ, σ) = . According to the progression function, it means that p ∈ σ. Moreover, since ϕ = p, according to the LTL semantics of atomic propositions, for any w ∈ Σ ω , we have σ • w |= ϕ. According to the definition of good prefixes, it means that σ ∈ good(ϕ).

The proof for P (ϕ, σ) = ⊥ =⇒ σ ∈ bad(ϕ) is similar.

Induction Case: ϕ ∈ {¬ϕ , ϕ 1 ∨ ϕ 2 , ϕ 1 ∧ ϕ 2 , Gϕ , Fϕ , Xϕ , ϕ 1 Uϕ 2 }. The induction hypothesis states that the lemma holds for some formulae ϕ , ϕ 1 , ϕ 2 ∈ LTL.

-Case ϕ = ¬ϕ . In this case, the result is obtained by using the induction hypothesis on ϕ and the equality's ⊥ = ¬ and ¬(¬ϕ) = ϕ. -Case ϕ = ϕ 1 ∨ ϕ 2 . Recall that, according to the progression function for operator ∨, P (ϕ 1 ∨ ϕ 2 , σ) = P (ϕ 1 , σ) ∨ P (ϕ 2 , σ).

Let us suppose that P (ϕ, σ) = . We distinguish two cases:

-If P (ϕ 1 , σ) = or P (ϕ 2 , σ) = . Let us treat the case where P (ϕ 1 , σ) = . Using the induction hypothesis on ϕ 1 , we have σ ∈ good(ϕ 1 ). According to the definition of good prefixes, we have ∀w ∈ Σ ω . σ • w |= ϕ 1 . We easily deduce, using the LTL semantics of operator ∨, that ∀w ∈ Σ ω . σ

Let us suppose that P (ϕ, σ) = ⊥. In this case, we have P (ϕ 1 , σ) = ⊥ and P (ϕ 2 , σ) = ⊥. Similarly, we can apply the induction hypothesis on ϕ 1 and ϕ 2 to find that σ is bad prefix of both ϕ 1 and ϕ 2 , and is thus a bad prefix of ϕ 1 ∨ ϕ 2 (using the LTL semantics of operator ∨).

-Case ϕ = ϕ 1 ∧ ϕ 2 . This case is symmetrical to the previous one.

-Case ϕ = Gϕ . Recall that, according to the progression function for operator G, P (Gϕ , σ) = P (ϕ , σ) ∧ Gϕ .

Let us suppose that P (ϕ, σ) = . It means that P (ϕ , σ) = and Gϕ = . This case reduces to the case where ϕ = . Let us suppose that P (ϕ, σ) = ⊥. We distinguish two cases.

-If P (ϕ , σ) = ⊥ or Gϕ = ⊥. We distinguish again two sub-cases.

• Sub-case P (ϕ , σ) = ⊥. Using the induction hypothesis on ϕ , we deduce that σ ∈ bad(ϕ ), i.e., ∀w ∈ Σ ω . σ • w |= ϕ . Following the LTL semantics of operator G, we deduce that ∀w ∈ Σ ω . σ • w |= Gϕ , i.e., σ ∈ bad(Gϕ ). • Sub-case Gϕ = ⊥. This case reduces to the case where ϕ = ⊥.

-If P (ϕ , σ) = ⊥ and Gϕ = ⊥. From P (ϕ , σ) ∧ Gϕ = ⊥, we deduce that P (ϕ , σ) = ¬Gϕ . Using Lemma Let us suppose that P (ϕ, σ) = . We distinguish two cases.

-If P (ϕ , σ) = or Fϕ = .

• Sub-case P (ϕ , σ) = . Following the previous reasoning, using the induction hypothesis on ϕ , the LTL semantics of operator F, and the definition of good prefixes, we obtain the expected result. • Sub-case Fϕ = . This case reduces to the case where ϕ = .

-If P (ϕ , σ) = and Fϕ = . From P (ϕ , σ) ∨ Gϕ = ⊥, we deduce that P (ϕ , σ) = ¬Fϕ .

Using Let us suppose that P (ϕ, σ) = ⊥. It means that P (ϕ , σ) = ⊥ and Fϕ = ⊥. A similar reasoning as the one used for the case ϕ = Gϕ and P (ϕ, σ) = can be applied to obtain the expected result.

-Case ϕ = Xϕ . Recall that, according to the progression function for operator X, P (Xϕ , σ) = ϕ .

Let us suppose that P (ϕ, σ) = . It means that ϕ = . According to the LTL semantics of , we have ∀w ∈ Σ ω . w |= ϕ . Then, ∀w ∈ Σ ω . σ • w |= Xϕ = ϕ. That is, σ ∈ good(Xϕ ).

Let us suppose that P (ϕ, σ) = ⊥. It means that ϕ = ⊥. According to the LTL semantics of ⊥, we have ∀w ∈

Recall that, according to the progression function for operator U, P (ϕ

Let us suppose that P (ϕ, σ) = . We distinguish two cases.

-

• Sub-case P (ϕ 2 , σ) = . Using the induction hypothesis on ϕ 2 , we have σ ∈ good(ϕ 2 ).

Let us consider w ∈ Σ ω , we have σ

Necessarily, ϕ 1 Uϕ 2 = and this case reduces to the first one already treated.

A.1.3 Some Intermediate Lemmas

The following lemma states some equality's that directly follow from an inductive application of the definition of the progression function on events. (Proofs of Lemmas 3 and 4 are given p. 14 and 36, respectively).

Lemma 5 Given some formulae ϕ, ϕ 1 , ϕ 2 ∈ LTL, and a trace u ∈ Σ + , the progression function can be extended to the trace u by successively applying the previously defined progression function to each event of u in order. Moreover, we have:

Proof The proof is done by two inductions: an induction on the length of the trace u (which is also the number of times the progression function is applied) and a structural induction on ϕ ∈ LTL.

In this case, the result holds thanks to the definition of the progression function.

Induction case:

Let us suppose that the lemma holds for any trace u ∈ Σ + of some length t ∈ N and let us consider the trace u • σ ∈ Σ + , we perform a structural induction on ϕ ∈ LTL.

Structural Base case: ϕ ∈ { , ⊥, p ∈ AP }.

-Case ϕ = . In this case the result is trivial since we have:

(progression on events)

-Case ϕ = ⊥. This case is symmetrical to the previous one.

The following lemma exhibits some straightforward properties of function rp.

Lemma 7 Let ϕ be an LTL formula, u ∈ Σ + be a trace of length t + 1, i ∈ [1, |M|] a monitor of one of the components, u i (t) ∈ Σ i the last event of u on component i, we have:

ϕ ∈sus(ϕ) Prop(ϕ ) ⊆ AP i =⇒ rp(ϕ, u, i) = rp(ϕ, u); 5. For {i 1 , . . . , in} = [1, |M|]: rp(rp(. . . rp(ϕ, u, i 1 ), . . .), u, in) = rp(ϕ, u).

Proof The proofs of these properties can be done by induction on ϕ ∈ LTL and follow directly from the definitions of rp and the progression function.

Lemma 8 Given a trace and a local obligation on a monitor obtained by running the decentralised algorithm from an initial obligation on the trace, the local obligation where past sub-formulae have been evaluated using the trace is equal to the initial obligation progressed with this same trace. Formally:

Proof We shall prove this lemma by induction on t ∈ N * . Let us consider some component

-For t = 0. In this case, |u| = 1 and we have rp(lo(i, 0, ϕ), u) = rp P (ϕ, σ i , AP i ) where σ i = Π(u(0)). We can obtain the expected result by doing an induction on ϕ ∈ LTL where the only interesting case is ϕ = p ∈ AP . According to the definition of the progression function, we have:

∈ u(0). On the one hand, according to the definition of rp, we have:

Thus, we have:

∈ u(0). On the other hand, according to the definition of the progression function, we have:

∈ u(0). -Let us consider some t ∈ N * and suppose that the property holds. We have: lo(i, t + 1, ϕ) = P kept(i, t) ∧ received(i, t), u i (t + 1), AP i .

Similarly to the proof of Lemma 10, let us distinguish four cases according to the communication that occurred at the end of time t.

-If send(i, t) = false and ∀j ∈ [1, |M|] \ {i}. send(j, t, i) = false. Then, we have: = j∈J rp(P (rp(lo(j, tϕ), u(0)

-If send(i, t) = false and ∃j ∈ [1, |M|] \ {i}. send(j, t, i) = true. Then, we have:

where ∀j ∈ J. send(j, t, i) = true. The proof this case is just a combination of the proofs of the two previous cases. -If send(i, t) = true and ∀j ∈ [1, |M|] \ {i}. send(j, t, i) = false. Then, we have: lo(i, t + 1, ϕ) = #. The result holds vacuously.

A.2.4 Proof of Theorem 3 (p. 15)

The soundness of Algorithm L wrt. centralised progression is now a straightforward consequence of Lemma 8. Indeed, let us consider u ∈ Σ * s.t. u |= D ϕ = . It implies that ∃i ∈ [1, n]. lo(i, t, ϕ) = = rp(lo(i, t, ϕ), u). Applying Lemma 8, we have P (ϕ, u) = , i.e., u |= C ϕ = .

The proof for u

A.2.5 Alternative Proof of the Correctness of Decentralised Monitoring wrt. LTL 3

Soundness of the decentralised monitoring algorithm wrt. LTL 3 semantics is a consequence of the soundness of the monitoring algorithm wrt. centralised progression (Theorem 3), as stated by Corollary 1, i.e., whenever the decentralised monitoring algorithm yields a verdict for a given trace, then the evaluation of this trace wrt. LTL 3 semantics is the same. For the sake of completeness, we provide an alternative and direct proof..

Some intermediate lemmas.

We introduce some intermediate lemmas.

The following lemma extends Lemma 1 to the decentralised case, i.e., it states that the progression function mimics LTL semantics in the decentralised case.

Lemma 9 Let ϕ be an LTL formula, σ ∈ Σ an event, σ i a local event observed by monitor M i , and w an infinite trace, we have σ

And similarly: ∀j ∈ J. w t+1 |= P inlo(j, t, ϕ), u i (t + 1), Σ i ⇐⇒ w t |= inlo(j, t, ϕ) It follows that:

And finally:

-If send(i, t) = true and ∃j ∈ [1, n] \ {i}. send(j, t, i) = true. Then, we have:

where ∀j ∈ J. send(j, t, i) = true. The previous reasoning can be followed in the same manner to obtain the expected result. -If send(i, t) = false and ∀j ∈ [1, n] \ {i}. send(j, t, i) = false. Then, we have:

The previous reasoning can be followed in the exact same manner to obtain the expected result.

-If send(i, t) = true and ∀j ∈ [1, n] \ {i}. send(j, t, i) = true. Then, we have:

In this case, the result holds vacuously.

Back to the proof of soundness. The soundness of Algorithm L is now a straightforward consequence of Lemmas 9 and 10. Indeed, let us consider

The proof for u

A.2.6 Proof of Theorem 4 (p. 15)

The proof of Theorem 4 intuitively consists in showing that in a given architecture, we can take successively two components and merge them to obtain an equivalent architecture in the sense that they produce the same verdicts. The difference is that if in the merged architecture a verdict is emitted, then, in the non-merged architecture the same verdict will be produced with an additional delay.

Lemma 11 In a two-component architecture, if in the centralised case a verdict is produced for some trace u, then, in the decentralised case, one of the monitors will produce the same verdict, after any event. Formally:

Proof Let us consider a formula ϕ ∈ LTL and a trace u ∈ Σ + s.t. |u| = t + 1. We shall only consider the case where P (ϕ, u) = . The other case is symmetrical. Let us suppose that lo(1, t, ϕ) = and lo(2, t, ϕ) = (otherwise the results holds immediately). Because of the correctness of the algorithm (Theorem 3), we know that lo(1, t, ϕ) = ⊥ and lo(2, t, 1) = ⊥. Moreover, according to Lemma 8, necessarily lo(1, t, ϕ) and lo(2, t, ϕ) are urgent formulae: Υ (lo(1, t, ϕ)) > 0 and Υ (lo(2, t, ϕ)) > 0. Since, there are only two components in the considered architecture, we have ϕ ∈sus(lo(1,t,ϕ)) Prop(ϕ ) ⊆ AP 2 and ϕ ∈sus(lo(2,t,ϕ)) Prop(ϕ ) ⊆ AP 1 . According to Algorithm L, we have then send(1, t, 2) = true and send(2, t, 1) = true. Then inlo(1, t + 1, ϕ) = lo(2, t, ϕ) ∧ lo(2, t, ϕ) = #. Hence: lo(1, t + 1, ϕ) = P (lo(2, t, ϕ), u 1 (t + 1), AP 1 ). According to Lemma 7 item 4, we have lo(1, t + 1, ϕ) = P (rp(lo(2, t, ϕ), u(0)

Symmetrically, we can find that lo(2, t, ϕ) = . In the remainder, we consider an n-component architecture M, with n ≥ 2 such that the priority between components is M 1 < M 2 < . . . < Mn. 6 The following lemma relates verdict production in an n-component architecture and verdict production in the same architecture where the two components with the lowest priority have been merged. From the theorem about the maximal delay (Theorem 2), we have |u| -|u | ≤ (n -1). Thus, each of the local obligations in architecture M will transit through at most n monitors following the ordering between components. That is, in the worst case (i.e., if a verdict is not produced before time |u|), any obligation will be progressed according to all components. More precisely, each time a local obligation is progressed on some component C i , past obligations w.r.t. component C i are removed (Lemma 7 -item 3). Using the compositionality of rp and the progression function on conjunction, in the worst case the local obligation at time |u | + n will be a conjunction of formulae of the form P (

• . . .