Victor Roussanaly

Yliès Falcone

Decentralised Runtime Verification of Timed Regular Expressions

Keywords: 2012 ACM Subject Classification Theory of computation → Distributed computing models, Theory of computation → Regular languages, Theory Timed expressions, Timed properties, Monitoring, Runtime verification, Decentralized systems, Asynchronous communication Digital Object Identifier 10.4230/LIPIcs...12

Ensuring the correctness of distributed cyber-physical systems can be done at runtime by monitoring properties over their behaviour. In a decentralised setting, such behaviour consists of multiple local traces, each offering an incomplete view of the system events to the local monitors, as opposed to the standard centralised setting with a unique global trace. We introduce the first monitoring framework for timed properties described by timed regular expressions over a distributed network of monitors. First, we define functions to rewrite expressions according to partial knowledge for both the centralised and decentralised cases. Then, we define decentralised algorithms for monitors to evaluate properties using these functions, as well as proofs of soundness and eventual completeness of said algorithms. Finally, we implement and evaluate our framework on synthetic timed regular expressions, giving insights on the cost of the centralised and decentralised settings and when to best use each of them.

Introduction

Modern systems tend to be more distributed and interconnected. Automated verification methods are required to ensure those systems behave as they should. Moreover, their interactions with their environment are getting increasingly unpredictable, which tends to hinder static verification methods such as model checking, as they require a model of the verified system and do not scale well. On the other hand, runtime verification [START_REF] Falcone | A tutorial on runtime verification[END_REF][START_REF] Bartocci | Introduction to runtime verification[END_REF][START_REF] Falcone | A taxonomy for classifying runtime verification tools[END_REF] requires no model. In this area, several monitoring methods detect if a system violates its given specification based on events observed at runtime. In order to express finer properties over more complex behaviour, several algorithms for monitoring properties based on real continuous time have been proposed in [START_REF] Nickovic | AMT: a property-based monitoring tool for analog systems[END_REF] and [START_REF] Grez | The monitoring problem for timed automata[END_REF]. However, these algorithms assume a central observation point in the system, which might be less robust to an architecture change, more vulnerable to outside attacks, or less compatible with the system's architecture. For this purpose, decentralised monitoring algorithms account for the absence of a central observation point, e.g., [START_REF] Bauer | Decentralised LTL monitoring[END_REF] and [START_REF] Falcone | On decentralized monitoring[END_REF]. Existing decentralised monitoring algorithms consider linear discrete time and synchronous communication between the system components. In contrast, we address the verification of timed properties of continuous time in an asynchronous setting.

We introduce a decentralised monitoring algorithm that uses local knowledge of the global behaviour to express a verdict about a verified global timed property. In a synchronous setting, while a component lacks information on what events happened in other components, it can use a round-based approach to consider only a finite number of possibilities about global behaviour. In contrast, in an asynchronous setting, for a given time interval, there are no bounds on the number of events that can happen on another component, meaning that a local monitor should take into account an infinite number of scenarios for the events that it has not seen. Another challenge is that a monitor can be notified of past events from another component and has to update its local knowledge accordingly. Indeed, a method is proposed in [START_REF] De | Approximate stream reasoning with metric temporal logic under uncertainty[END_REF] to account for a partial view of a global behaviour in a timed context, but it assumes that events that have not been seen cannot be seen afterwards. In our case, we assume that events that are not seen yet can still be seen in the future, and the local knowledge should be updated accordingly.

In this paper, we introduce several algorithms for monitoring timed properties in a decentralised setting, as well as an implementation to simulate and evaluate these algorithms.

In Sec. 1, we present timed regular expressions, which we use to specify timed properties, and we explain how we evaluate them on a timed trace. After formally defining the decentralised monitoring problem (Sec. 2), we define a progression function that updates timed regular expression based on the local knowledge, first for the centralised setting and then for the decentralised one (Sec. 3). Afterwards (Sec. 4), we define two algorithms for decentralised monitoring of timed regular expressions, using the progression function mentioned above. Finally (Sec. 5), we present our implementation and experimental results. We compare with related work in Sec. [START_REF] Bauer | Decentralised LTL monitoring[END_REF] and conclude in Sec. 7.

Timed Words and Timed Regular Expressions

We recall the basic notions related to timed words, timed regular expressions, and regular languages in Sec. 1.1, using the same formalism as in [START_REF] Asarin | Timed regular expressions[END_REF]. In Sec. 1.2, we introduce reduced timed regular expressions and how to transform timed regular expressions into reduced ones, as they will serve in our monitoring framework. In Sec. 1.3, we transpose the semantics of timed regular expressions, from timed words to timed traces. We also propose new operators for timed traces.

We start by defining some basic notation: I denotes the set of intervals in R + and for S a set, P(S) denotes the set of subsets of S. We also use • to denote the concatenation between two words.

Timed Regular Expressions and Timed Regular Languages [3]

We recall the syntax and semantics of timed words and timed regular expressions. Let Σ be an alphabet. A timed word (called time-event sequence in [START_REF] Asarin | Timed regular expressions[END_REF]) over the alphabet Σ is a word of R + ∪ Σ, composed of events in Σ and numerical values that represent delays, that is, the time between two consecutive events. As such, two consecutive delays can be added, which means that for two timed words u and v and for two delays x and y, u

• x • y • v = u • (x + y) • v.
For example, 0.4

• 1.1 • b • a • 0.1 • 0.2 • c • 2.1 and 1.5 • b • a • 0.3 • c • 2.
1 represent the same timed word. We denote by T (Σ) the set of timed words over Σ and by ϵ the empty word. A subset of T (Σ) is called timed language. A function θ : Σ 1 → Σ 2 ∪ {ϵ} is called a renaming. We consider its natural extensions Σ * 1 → Σ * 2 and T (Σ 1 ) → T (Σ 2 ), and we use the same symbol θ to denote them.

We use the classical word concatenation denoted by •, but we also need an absorbing concatenation denoted by the operator •. Let us denote by δ : T (Σ) → R + the function that returns the sum of delays in a timed word. For two timed words u and v, if there exists a word w such that δ(u) • w = v, then we can define u • v = u • w. This means that u • v is defined if and only if v starts with a delay greater than the sum of delays in u, and if that is the case, then we remove this delay from the front of v before concatenating it to u. For example, (a

• 2 • b) • (3 • c) = a • 2 • b • 1 • c while (a • 2 • b) • (1 • c) is not defined. Concatenation
L := ϵ | a | ⟨L⟩ I | L ∧ L | L ∨ L | L • L | L • L | θ(L ′ ) | L ⋆ | L ⃝ ⋆
Intuitively, a timed regular expression can be, respectively, the empty word, the letter a at any time, a language limited to time interval I, the conjunction (∧), disjunction (∨), concatenation (•), and absorbing concatenation (•) of two timed regular expressions, the renaming obtained through function θ, as well as the Kleene star (⋆) and the Kleene star using the absorbing concatenation (⃝ ⋆ ) applied to a timed regular expression. The set of timed regular expressions obtained as above is denoted by E(Σ).

▶ Definition 2 (Semantics of timed regular expressions). The semantics of a timed regular expression is the timed language defined inductively by function • : E(Σ) → P(T (Σ)):

ϵ = {ϵ}, a = {r • a | r ∈ R + }, L 1 ∧ L 2 = L 1 ∩ L 2 , L 1 ∨ L 2 = L 1 ∪ L 2 , L 1 • L 2 = L 1 • L 2 , L 1 • L 2 = L 1 • L 2 , ⟨L⟩ I = {u ∈ L 1 | δ(u) ∈ I}, 118 L ⋆ = ∞ i=0 L i , 119 L ⃝ ⋆ = ∞ i=0 L •i , 120 θ(L) = {θ(u) | u ∈ L }.

121

We call timed regular languages the languages defined by timed regular expressions.

▶ Example 3 (Timed regular expressions). Let us consider some alphabet {a, b}:

(a ∨ b) ⋆ • (a • ⟨b⟩ [0;1] ) • (a ∨ b)
⋆ denotes the language of timed words where at some point b occurs within one time unit after some a;

⟨a⟩ ⋆ [0;1] denotes the language of timed words composed of a's where each event occurs within one time unit from the previous one;

⟨a⟩ ⃝ ⋆ [0;1]
denotes the language of timed words where all events occur within the first time unit. Note that this is semantically equivalent to ⟨a

⃝ ⋆ ⟩ [0;1] and ⟨a ⋆ ⟩ [0;1] .
Two timed regular expressions L and L ′ are equivalent if their language is the same, that is,

L = L ′ .

Reduced Timed Regular Expressions

First, let us introduce reduced timed regular expressions.

▶ Definition 4 (Reduced timed regular expression). A reduced timed regular expression is a timed regular expression where the time constraining operator ⟨•⟩ I is applied only to singular events.

Any timed regular expression can be rewritten into an equivalent reduced timed regular expression that defines the same language.

▶ Proposition 5. Let L, L 1 , L 2 be some timed regular expressions over Σ. We have:

⟨L 1 ∨ L 2 ⟩ I = ⟨L 1 ⟩ I ∨ ⟨L 2 ⟩ I , ⟨L 1 • L 2 ⟩ I = L 1 • ⟨L 2 ⟩ I , θ(L)⟩ I = θ(⟨L⟩ I ) , ⟨L 1 ∧ L 2 ⟩ I = ⟨L 1 ⟩ I ∧ ⟨L 2 ⟩ I , 143 ⟨L 1 • L 2 ⟩ I = L 1 • L 2 ∧ ⟨Σ ⃝ ⋆ ⟩ I , 144 ⟨ϵ⟩ I = {ϵ}, if 0 ∈ I, ∅ otherwise, 145 ⟨L ⃝ ⋆ ⟩ I = ⟨ϵ⟩ I ∨ ⟨L ⃝ ⋆ • L⟩ I = ⟨ϵ⟩ I ∨ L ⃝ ⋆ • ⟨L⟩ I , ⟨L ⋆ ⟩ I = ⟨ϵ⟩ I ∨ (⟨L ⋆ • L⟩ I = ⟨ϵ⟩ I ∨ (L ⋆ • L ∧ ⟨Σ ⃝ ⋆ ⟩ I ) .
In the remainder, we only consider reduced timed regular expressions.

Semantics of Timed Regular Expressions over Timed Traces

In the context of decentralised monitoring, the monitor uses a trace as a sequence of timestamped events. Formally, a timed trace over the alphabet Σ is a finite word over Σ × R + such that for two consecutive letters (α

a↑ t = a, (L 1 ∧ L 2 )↑ t = L 1 ↑ t ∧ L 2 ↑ t , (L 1 ∨ L 2 )↑ t = L 1 ↑ t ∨ L 2 ↑ t , (L 1 • L 2 )↑ t = L 1 ↑ t • L 2 , (L 1 • L 2 )↑ t = L 1 ↑ t • L 2 ↑ t , (⟨L⟩ I )↑ t = ⟨L↑ t ⟩ I-t 170 L ⋆ ↑ t = L↑ t ∨ L ⋆ , 171 L ⃝ ⋆ ↑ t = (L↑ t ) ⃝ ⋆ , 172 θ(L)↑ t = θ(L↑ t ).
ϵ tr = {ϵ} a tr = {(a, t) | t ∈ R + } L 1 ∧ L 2 tr = L 1 tr ∩ L 2 tr L 1 ∨ L 2 tr = L 1 tr ∪ L 2 tr θ(L) tr = {θ(u) | u ∈ (L) tr } ⟨L⟩ I tr = {π ∈ L 1 tr | τ last (u) ∈ I} 181 L ⋆ tr = ∞ i=0 L i tr 182 L ⃝ ⋆ tr = ∞ i=0 L •i tr 183 L 1 • L 2 tr = {u • v | u ∈ L 1 tr , v ∈ L 2 tr } L 1 • L 2 tr = {u • v | u ∈ L 1 tr , v ∈ L 2 ↓ τ last (u) tr }
Let us denote by ω : R(Σ)T (Σ) the function that takes a timed trace (α

1 , t 1 )•(α 2 , t 2 ) • • • (α n , t n )
and returns the time word

t 1 • α 1 • (t 2 -t 1 ) • α 2 • (t 3 -t 2 ) • • • (t n -t n-1 ) • α n .
such that v ∼ u and ω -1 (v) ∈ L tr .
This means that the language obtained by applying ω -1 to the language of timed words of an expression is exactly the language of timed traces of that expression.

Global operators

Using the timed traces semantics, we introduce two new operators ⌊.⌋ I and ⌈•⌉ I . ⌈•⌉ I is similar to the ⟨•⟩ I operators, except that it refers to global time. In this case, global does not refer to the distributed nature of the systems we study, it means that it is based on the absolute time of the events, and not the relative time between two events. Of course, this operator would make no sense in the timed words definition of the semantics, as the concatenation of two words change the value of this global time for the word on the right side of the concatenation.

This is why we express the semantics of these operators by extending • tr .

⌈L⌉ I = {u ∈ L tr | τ last (u) ∈ I} ⌊L⌋ I = {u ∈ L tr | τ first (u) ∈ I} 209
We call global timed regular expressions an expression that contains these operators and denote the set of expressions over Σ by GE(Σ).

▶ Proposition 9. For all L ∈ GE(Σ), there exists

L ′ ∈ E(Σ) such that L tr = L ′ tr .
This can be proven through direct construction or by using the fact that timed regular expressions are semantically equivalent to timed automata, and as such adding global constraints does not add to the expressiveness of timed automata.

▶ Example 10. The expression ⟨a⟩

[0;3] • (⟨b⟩ [0;2] ) ⃝ ⋆ • ⌊(a • b) + ⌋ [4;5] is semantically equivalent to ⟨⟨a⟩ [0;3] • (⟨b⟩ [0;2] ) ⃝ ⋆ • a⟩ [4;5] • b • (a • b) ⋆ .

The Decentralised Timed Monitoring Problem

We formally state the decentralised timed monitoring problem as well as its objectives.

Context and notations.

Let us suppose that the system at hand consists of n independent components denoted by C i , for 0 < i ≤ n. Each component C i emits local events over a local alphabet Σ i . Let Σ = i∈ [1,n] Σ i be the global alphabet of events. We assume that the local alphabets form a partition of Σ, which means that if i ̸ = j then Σ i ∩ Σ j = ∅. Let p i be the projection of a timed trace of R(Σ) onto R(Σ i ) and denote by p the function defined by p(σ) = (p 1 (σ), p 2 (σ), ..., p n (σ)). As such, after observing our local traces σ 1 , σ 2 , ..., σ n , we can apply p -1 to obtain the possible global traces. We also note σ| t as the prefix of σ, which contains all events that occur before t. To each component C i is attached a monitor M i , which can observe a trace over Σ i . We denote the verdict of a monitor by Verdict i : R → {bad, inconclusive}. Monitors are purposed to detect violations.

Assumptions. Our assumptions on the system are as follows.

Messages can be exchanged between any pair of monitors.

The monitors only observe their local trace and the messages they receive.

If a message is sent, it is eventually received, which means that there is no loss of messages.

The communication is done through FIFO channels, meaning that the messages sent from one monitor to another are received in the order they were sent.

All monitors share the same global clock, meaning that there are no clock drifts.

Objectives. Given some timed regular expression L, and a global trace σ, our goal is to find an algorithm for the monitors such that the following properties hold.

▶ Definition 11 (Definitive Verdict). If there is a time t for which there is a verdict

Verdict i (t) = bad, then for all t ′ ≥ t, Verdict i (t ′ ) = bad.
▶ Definition 12 (Soundness). If there is a time t for which there is a verdict Verdict i (t) = bad

then σ| t is a bad prefix of L, i.e. for all σ ′ ∈ R(Σ), if σ| t is a prefix of σ ′ then σ ′ / ∈ L tr .
▶ Definition 13 (Eventual completeness). If there is a time t for which σ| t is a bad prefix of L, then there is a delay

t ′ ≥ 0 such that Verdict i (t + t ′ ) = bad.
The goal is for one monitor, using its partial knowledge, to deduce whether or not its partial vision of the trace can be completed to be L tr . 1 Moreover, we also aim to minimise the time it takes to detect such a violation of the expression. Finally, to limit the communication overhead, we also aim to limit the number of messages sent, as well as the total size of the messages exchanged.

Progression for Timed Regular Expressions

We consider decentralised monitors that observe only their local events, indexed with the time at which they happen. For a monitor of index i, we define a decentralised progression

function Pr i : GE(Σ) → (Σ × R + ) → GE(Σ)
, meaning a function that takes an event locally observed (α, t) and a specification as a timed regular expression L, and returns an expression that represents the new specification now that the monitor knows that (α, t) happened. In a centralised case, where there is only one monitor observing the events in the same order they occur, we denote such function Pr 0 and it should satisfy the following property:

▶ Definition 14 (Centralised progression function). Pr 0 : GE(Σ) → (Σ × R + ) → GE(Σ) is a
centralised progression function iff for any expression L ∈ GE(Σ) and any trace event (α, t),

Pr 0 (L)(α, t) = {u | (t • α) • u ∈ L}.
In other words, it is a left derivative. If a centralised monitor applies this function successively as it observes the events, and the resulting expression represents the empty language, then the monitor can produce a verdict. Whereas in the decentralised case where a monitor observes a local event (α, t), there might have been other events happening in another component at a time before t. In other words, for the decentralised case, Pr i must satisfy the following property:

▶ Definition 15 (Decentralised progression function).

Pr i : GE(Σ) → (Σ × R + ) → GE(Σ) is
a decentralised progression function iff for any expression L ∈ GE(Σ) and any trace event (α, t), we have:

Pr i (L)(α, t) tr = {u • v ∈ R(Σ) | u • (α, t) • v ∈ L tr ∧ u ∈ R(Σ \ Σ i )}.
The above function is not a left derivative, as it allows events that are not from Σ i to occur before the observed event. We now propose a decentralised progression function and detail its inductive definition. To define such a function, we define a filter function Φ : GE(Σ) → P(Σ) → GE(Σ). The proper definition is given in the appendix. This function is defined such that it removes events of a given alphabet from an expression.

▶ Proposition 16. For L ∈ GE(Σ) and Σ ′ ⊆ Σ, Φ(L)(Σ ′ ) = L ∧ (Σ \ Σ ′ ) ⋆ .
In other words, function Φ takes an expression L ∈ GE(Σ) and an alphabet Σ ′ ⊆ Σ and returns an expression that represents the restriction of L to Σ \ Σ ′ . Let us define a progression function Pr i for component C i by looking at each case. First, let us look at the base cases:

Pr i (a)(α, t) = ϵ t , if α = a Pr i (⟨a⟩ I )(α, t) = ∅, if t ̸ ∈ I Pr i (a)(α, t) = ∅, if α ̸ = a 281 Pr i (⟨a⟩ I )(α, t) = Pr i (a)(α, t), if t ∈ I 282 Pr i (L 1 ∨ L 2 )(α, t) = Pr i (L 1 )(α, t) ∨ Pr i (L 2 )(α, t) Pr i (L 1 ∧ L 2 )(α, t) = Pr i (L 1 )(α, t) ∧ Pr i (L 2 )(α, t)
For those cases, the decentralised progression is straightforward, and if the event has been observed, it is removed from the formula. Then, let us look at the absorbing concatenation:

Pr i (L 1 • L 2 )(α, t) = (Pr i (L 1 )(α, t) • ⌊L 2 ⌋ [t;∞[ ) ∨ ⌈Φ(L 1 )(Σ i )⌉ [0;t] • Pr i (L 2 )(α, t) Pr i (L ⃝ ⋆ )(α, t) = ⌈Φ(L)(Σ i ) ⃝ ⋆ ⌉ [0;t] • Pr i (L)(α, t) • ⌊L ⃝ ⋆ ⌋ [t;∞[
For the absorbing concatenation •, we examine whether (α, t) corresponds to an event on each side of the concatenation. If (α, t) is an event on the left side, then events on the right side must have occurred later. Otherwise, if (α, t) is an event on the right side, then the events on the left side must have happened earlier. Since they happened before the current time, it means that the current monitor can not have seen them, so they cannot be events from the monitor of index i.

Let us consider the progression for the global operators. For these cases, we use additional notation. First, for I an interval and t ∈ R, we write t < I (resp. t > I) if and only if for all t ′ ∈ I, t < t ′ (resp. t > t ′ ). We also denote by I↓ the interval obtained by changing the lower bound of I to 0 inclusive, and by I↑ the interval obtained by changing the upper bound of I to ∞. Hence, we have:

Pri(⌈L⌉ I )(α, t) = ⌈Pri(L)(α, t)⌉ I↓ , if t ∈ I Pri(⌈L⌉ I )(α, t) = ⌈Pri(L)(α, t)⌉ I , if t < I Pri(⌈L⌉ I )(α, t) = ∅, otherwise Pri(⌊L⌋I )(α, t) = ⌊Pri(L)(α, t)⌋ I↑ , if t ∈ I 303 Pri(⌊L⌋I )(α, t) = ⌊Pri(L)(α, t)⌋I , if t > I 304 Pri(⌊L⌋I )(α, t) = ∅, otherwise 305
For ⌈L⌉ I , we note that if (α, t) happened and t ∈ I, then it means that we can apply the progression to L provided that all other events occur before t or between t and the upper bound of I, which means that they occur in I↓. On the other hand, if t < I, then it cannot be the last event seen, and we are still waiting for an event in I. We have a similar approach to ⌊L⌋ I .

Finally, let us consider the non-absorbing concatenation. We want something similar to • for • where we consider whether the event occurred on the right or left side. The problem here is that if the event happened on the right-hand side, then the result of our progression function depends on the time of the last event on the left-hand side since the concatenation "resets" the time at which we interpret the expression. Here we use the fact that the function

t ′ → Pr i (L↓ t ′ )(α, t
) is a piece-wise constant function. This means that we can look at a finite number of possible intervals at which the last element of the left-hand side occurs. By building those intervals and computing the expression associated with each one, we can build a function ∆ i : (GE(Σ) × I) → (Σ × R + ) → P(I × GE(Σ)). A more detailed definition of such a function is provided in the appendix.

Pr i (L 1 • L 2 )(α, t) = (I,L ′ )∈∆i(L2,R + )(α,t) ⌈Φ(L 1 )(Σ i )⌉ I • L ′ ∨ Pr i (L 1 )(α, t) • ⌊L 2 ⌋ [t;∞[ Pr i (L ⋆ )(α, t) = (I,L ′ )∈∆i(L,R + )(α,t) ⌈Φ(L)(Σ i ) ⋆ ⌉ I • L ′ • ⌊L ⋆ ⌋ [t;∞[ Pr i (θ(L))(α, t) = α ′ ∈u -1 (α) θ(Pr i (L)(α ′ , t)) ▶ Example 17. Let us consider the language L = (a ∨ b) ⃝ ⋆ • ⟨a⟩ [0;1] with Σ 1 = {a}, Σ 2 = {b}. Then Pr 1 (L)(a, 2) = (⌈b ⃝ ⋆ ⌉ [0;2] • ⌊(a ∨ b) ⃝ ⋆ • ⟨a⟩ [0;1] ⌋ [2;∞[ ) ∨ ⌈b ⃝ ⋆ ⌉ [1;2] .
This means that, either the a observed was on the left of the concatenation, and in that case we have the language defined by L where before the global time t = 2, there can only be b events. Or the a observed was the one on the right side, so we can only observe events b that preceded it, with the last b between the global time t = 1 and t = 2.

We prove in appendix that this is a decentralised progression function Pr i following Definition 15.

As a consequence, we can prove the following theorem.

▶ Theorem 18. For all i, j, i ̸ = j, for all a ∈ Σ i and b ∈ Σ j , for all t a , t b ∈ R + for all

L ∈ GE(Σ), Pr j ((Pr i (L)(a, t a ))(b, t b ) tr = Pr i ((Pr j (L)(b, t b ))(a, t a ) tr .
This means that the order at which we observe two events from two different monitors does not matter, and we always obtain an equivalent expression. Note that in the case Σ i = Σ, then Pr i also satisfies Definition 14 and we denote it Pr 0 , which means that we also have a centralised progression function, defined as a specific case of our decentralised progression function.

Let us inductively define function Pr * such that for (α, t) a trace event of Σ i and π a sequence of timed trace events, Pr * (L)((α, t) • π) = Pr * (Pr i (L)(α, t))(π) and Pr * (L)(ϵ) = L.

Note that we do not require π to be a timed trace, meaning that the events are not necessarily ordered by ascending time.

▶ Corollary 19. For all L ∈ GE(Σ), for all π, π ′ such that for all i, p i (π) = p i (π ′ ),

Pr * (L)(π) tr = Pr * (L)(π ′ ) tr
Corollary 19 implies that the order at which the events are observed does not change the language we obtain, provided that the local order on each component is preserved.

Decentralised Monitoring

We define two algorithms to achieve decentralised monitoring for timed regular expressions.

Both algorithms allow detecting a violation of the specification at runtime. The first algorithm simulates centralised monitoring, while the second algorithm leverages the decentralised progression function.

Simulating Centralised Monitoring

We place ourselves under the assumptions we described in Sec. 2. That is to say that when a message is sent, it is eventually received with no loss, and we assume sequential consistency, meaning that when one component sends multiple messages to another component, then they are received in the same order as they were sent. We also discard the possibility of two events happening at the exact same time in two different components. Since we consider real time, this is not something that would likely occur, but if it happened, we would not know in (b) C3 sends its message when it observes b at t = 0.8. When it receives it later (green message), then it knows for sure that it has seen all events up to t = 0.8.

© V.

Figure 1

Algorithm for decentralised monitoring using centralised progression which order to consider them. But it can also be said that if the order of two simultaneous events on two different components mattered, then the specification would not be adapted to the system either. Finally, we also consider that the components are connected in a ring, as depicted in Figure 1b.

With these assumptions, let us consider that all components apply the algorithm shown in Figure 1a. It means that a component sends events that it sees to its successor. When it receives a message that it did not originate, it saves it into its memory and forwards it to its successor. Using sequential consistency, the following property holds:

▶ Proposition 20. If C i observes (α, t) and C i ′ observes (α ′ , t ′ ) with t < t ′ , then C i ′ receives the message (C i , α, t) before (C i ′ , α ′ , t ′ ).
From this, we can deduce that when a monitor receives a message it originated, then it saw all the events that happened in the system up to the time when this message was first created. So it can simulate centralised monitoring on its memory up to that point. Using Proposition 20 and Definition 14 we can show the following.

▶ Theorem 21. Let σ ∈ R(Σ) be the global timed trace, L the initial expression, and let (α, t) be the last event of this trace, with α ∈ Σ i . After C i receives its last message (C i , α, t),

we have L i tr = {σ ′ ∈ R(Σ) | σ • σ ′ ∈ L}.

Emptiness checking

We know that, if at some point L i tr = ∅ for some i, then the specification is violated.

This entails testing the emptiness of an expression. One way to do so is to build a timed automaton that recognise the same language, using the construction shown in [START_REF] Asarin | Timed regular expressions[END_REF], as we know that the problem of knowing whether or not the language of a timed automaton is empty is PSPACE [START_REF] Alur | Model-checking for real-time systems[END_REF] and there are several tools that solve that problem. While this construction ensures an emptiness check, it is costly, and it is desirable to avoid it at runtime. Instead, we simplify the expression between each progression to detect when the denoted language is empty. The simplification used in this work is very simple. First we simplify every ϵ, ϵ t or ∅ that appear in the expression. Then we find nested time constraints in order to merge them and simplify them as much as possible. This could be improved by simplifying conjunctions and disjunctions, but simplification of timed regular expressions is not well documented, and that is why we limit ourselves to these naive simplifications.

One could also notice that if L i tr = Σ ⋆ tr then it means that from this point onward the specification will always be satisfied. This means that we could possibly detect whether or not the specification is sure to be satisfied if we can test whether or not the language associated with the expression is universal. Unfortunately, this problem is not decidable in the general case [START_REF] Alur | A theory of timed automata[END_REF], and that is why we only propose verdict bad.

Using Decentralised Progression

We now consider another approach where monitors do not exchange observed events, but instead there is one running expression passed along the monitors and that is updated with their progression function. In that case, at any given time, there is at most one monitor holding the expression and being marked as active. Monitors that are not active are only observing local events and recording them in their local memory. The active monitor updates a running expression using decentralised progression, based on its local observations. At some point, it passes this expression to another monitor and becomes not active. The monitor that receives that expression updates it with its own memory of observed events and becomes active. This is shown in Algorithm 1. Hence, in that case, we do not need sequential consistency, nor do we need the assumption of the components communicating in a ring.

This algorithm uses two functions, urgent(L i ) and target(L i ). These functions decide when we want to pass the expression and to whom we want to pass it. There are several possible ways to implement them, as long as the expression is eventually passed to every component.

In that case, the verdict reached by this algorithm is eventually the same as the centralised monitoring as a direct consequence of Corollary 19. We propose the following implementation of these functions. Function urgent(L) replaces every occurrence of ⌈L ′ ⌉ I by ∅ and checks whether the resulting expression represents the empty language. If it is not empty, then it means that the specification can still be satisfied, even if nothing has been seen by the other monitors, and the active monitor returns false. Otherwise it means that we want to know what the other monitors observed and it returns true. The function target(L i ) can be implemented in multiple ways. First, we consider choosing target(L i ) = i + 1 mod n, which gives us something similar to the centralised approach, where the messages are sent to the successor along the ring. We also propose another implementation where we try to detect which monitor is the most relevant for the past constraints ⌈L⌉ I present in the formula and choose it as the target.

Note that this approach has several advantages. The main one being that a monitor can decide that the specification has been violated even if it has only a partial view and has not communicated with all the other monitors. This also means that less messages can be exchanged, so the impact of communication delays is reduced. The next section describes experiments with these approaches.

Simulation and Benchmarks

In this section, we validate the effectiveness of our decentralised monitoring approaches by

showing the benefits over an approach that simulates centralised monitoring. For this, we first briefly describe the implementation of our monitoring algorithms (Sec. 5.1). Then, we detail our experimental setup (Sec. 5.2) and obtained results, as well as some of the conclusions drawn (Sec. 5.3).

Implementation as an OCaml Benchmark

We implemented a simulation environment for the methods described in the previous sections.

For this, we extended DecentMon [START_REF] Bauer | Decentralised LTL monitoring[END_REF][START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF], an OCaml benchmark for decentralised monitoring in the discrete-time setting. We extended it to our timed setting and added support for regular timed expressions and timed traces. We implemented progression-based monitoring for the two methods. The extension for the timed setting consists of 1,400 LLOC. For the approach based on decentralised progression, we consider the following two alternatives for the target component chosen by a monitor when sending a message: (i) a dynamic approach where the target component is chosen based on the current expression, and (ii) a static approach where the target is chosen as the successor in a directed ring, as explained in the previous section.

Experimental Setup

We test and compare the three approaches for decentralised monitoring of timed regular expressions: (i) simulating centralised, (ii) decentralised with a dynamic target, and (iii) decentralised with a static ring target. We consider a network of 10 monitors, each of them capable of observing a different event. We consider the communication delay when a message is sent as a random value between 0 and 40 units of time. Timed regular expressions are not commonly used, since people prefer timed automata that are as expressive as timed regular expressions. This means that one approach could have been to take a benchmark of timed automata, compute a set of equivalent expressions and use them as a benchmark.

But this poses a problem as the performance would be affected by our choice of equivalent expression. Another difficulty is the absence of reference benchmark for timed decentralised monitoring. That is why in this context, we choose to generate random timed regular expressions. We generate 100 expressions of a fixed size, for each size between 2 and 8. For the time constraints that may appear, we randomly chose the lower bound between 0 and 30, and the upper bound is ∞ or a sum between the lower bound and an integer chosen randomly between 0 and 30. For each of these expressions, we generate 100 timed traces of length 200, with a delay between two consecutive events chosen randomly between 0 and 10.

Note that a randomly generated trace will most likely not respect a random specification, and the progression will find an empty language after a couple of steps. In order to avoid those cases, we ensure that for an expression of size k, the progressed expression is not empty after observing the first 5 × k events. To do so, we discard expressions where we cannot find such a trace in a reasonable time. For each trace, we perform monitoring according to the three aforementioned approaches.

During each experiment, we record the number of messages sent, the total size of the messages sent, the number of progressions performed, and the time taken to reach a verdict.

This results in 2,900,000 tests for each of the three algorithms.

We evaluate the algorithms along three dimensions that are relevant for decentralised monitoring.

Communication (messages). We measure the total number and size of the messages exchanged by the monitor. Since there are between 8 and 16 operators, they are encoded over 4 bits. The time values in timed constraints are encoded over 32 bits. There are 10 possible events encoded over 4 bits Computation (progressions). We measure the total number of calls to the progression functions defined in the previous sections, including the recursive calls.

Delay (decision time). We measure the time it takes for one of the monitors to detect that the current global trace violates the monitored timed regular expression.

Note that here we do not consider the computation time associated with each progression computation. We consider that this time should be negligible compared to the communication delays.

Results and Discussion

Tab. 1 reports the results of our experiments, reporting the average values for each of the metrics. In the following, we discuss the results and conclude.

First, let us compare the two decentralised approaches. Choosing a dynamic target gives us slightly better results on all metrics, except for the size of the messages. The difference remains marginal, and it seems that in our experiments, dynamically choosing the target does not give a significantly shorter decision time. Of course, this stems from the choice function, which can be improved, as it showed poor results in some specific cases. Although these are seldom, their impact on the average values is noticeable. We believe that a more in-depth analysis of these cases can give us a better choice of target.

However, the performance of the decentralised approach is significantly better than that of the centralised approach, where the number of messages and progressions is higher. Indeed, in the centralised approach, every monitor records each event and sends a message for each one, meaning that each monitor applies many progressions. This is not the case in the decentralised approach, where only a few messages are seen by each monitor. It is also shown that the time required to pass observations along all monitors in the centralised approach is much longer. Indeed, in order to apply the progression function on a local event it has observed, a monitor has to wait for it to circulate along all the other monitors; with 10 monitors and an average communication delay of 20 time units, it means that the monitor has to wait on average for 200 time units.

Of course, the trade-off can be seen in the size of the sent messages. This is because the centralised approach sends timed events, while the decentralised approach sends timed expressions. Those expressions are written with timed constraints, that tend to pile up after several progressions, and that increase the size of the expression. However, we can imagine two ways to alleviate this issue. The first would be to improve the simplification of expressions to reduce the size of expressions, possibly by simplifying some global time constraints or some conjunctions.

Another idea would be to send either a history of the timed events or an expression depending on which one is smaller. Indeed, each monitor could compute the expression if it received some history of the timed events. This approach is hard to implement, as it would mean that monitors should remember what other monitors have seen so far.

Another data that we did not show in the table is the impact of the communication delay relative to the delay between consecutive events. In fact, with higher communication delays, the simulated centralised approach has a decision time that increases much more than the decentralised approach. This is because the centralised method requires the message to travel along the entirety of the ring before taking any decision, which slows down the decision time proportionality to both the number of monitors and the delay of communication. This is less of a problem for the decentralised approach, which can decide by exchanging fewer messages between a few monitors. In our tests, we have even seen that in many cases, the decentralised approach decided with fewer messages as we increased the communication delay. This happens because when a message is received after being in transit for a long time, the receiving monitor has had enough time to build a long history that would violate the property. So we can deduce that when the communication delay is high, the decentralised approach should be the main option.

Related Work

As this paper introduces decentralised runtime verification for timed properties described by timed regular expressions [START_REF] Asarin | Timed regular expressions[END_REF], the related approaches consist of those for monitoring timed properties and those decentralising the monitoring process. is a tool monitoring using timed pattern matching. The mentioned approaches consider that the monitored system is centralised, and the decision procedure is fed with a unique trace containing complete observations.

Decentralised runtime verification has been introduced in [START_REF] Bauer | Decentralised LTL monitoring[END_REF], see [START_REF] Falcone | On decentralized monitoring[END_REF] for a recent overview.

Approaches in decentralised runtime verification take as input Linear-time Temporal Logic formulas such as [START_REF] Bauer | Decentralised LTL monitoring[END_REF][START_REF] Colombo | Organising LTL monitors over distributed systems with a global clock[END_REF][START_REF] Gallay | Decentralized LTL enforcement[END_REF] or finite-state automata such as in [START_REF] Falcone | Efficient and generalized decentralized monitoring of regular languages[END_REF][START_REF] El | On the monitoring of decentralized specifications: Semantics, properties, analysis, and simulation[END_REF]. All these approaches monitor specifications of discrete time, which is much simpler and does not account for the physical time that impacts the evaluation of the specification as well as the moment at which monitors perform their evaluation.

Finally, we note that decentralised runtime verification resembles diagnosis [22,23], which tries to detect the occurrence of a fault after a finite number of discrete steps and the component responsible for the fault. Our approach differs from diagnosis, as we assume that monitors' (combined) local information suffices to detect violations. However, in diagnosis, the model of the system is taken as input, and a central decision-making point is assumed.

Similar to diagnosis, there is decentralised observability [START_REF] Tripakis | Decentralized observation problems[END_REF]20] that combines the state of local observers with locally or globally bounded or unbounded memory to get a truthful verdict. While [START_REF] Tripakis | Decentralized observation problems[END_REF] requires a central decision-making point, the recent approach in [20] introduces the "at least one can tell" condition, which characterises when local agents can evaluate the global behaviour. While this approach, like ours, does not require a central observation point, it does not allow monitoring of the membership to an arbitrary timed regular expression.

Conclusion and Perspectives

We have introduced centralised and decentralised progression for timed regular expressions and have shown how it can be used to implement several algorithms to achieve decentralised monitoring of timed properties described by timed regular expressions. While several approaches exist for decentralised monitoring of untimed properties and centralised monitoring of timed properties, this is the first realisation of decentralised monitoring of timed properties.

We have implemented the decentralised monitoring algorithms and evaluated their runtime behaviour costs in metrics relevant to decentralised monitoring.

These results give insights and research directions to improve these methods, such as using better simplification rules or having a better choice of targets when the expression is passed between monitors. Alternatively, decentralised monitoring approaches can be designed for properties described by timed automata, as they are well adopted in the community. Since there is an equivalence between timed regular expressions and timed automata, one could simply implement the transformation from automata to expressions. However, we believe that finding an analogue of progression for timed automata seems promising, as it could outperform the methods shown in this paper using knowledge of the states and transitions, as in [START_REF] Falcone | Efficient and generalized decentralized monitoring of regular languages[END_REF] with finite-state automata. Finally, another perspective is to define progression for Metric Temporal Logic (MTL). Indeed, if we find a progression that satisfies the same properties as those shown in this paper, the same algorithms can be applied.

This function satisfies the following properties.

u 2 = v 1 • v 2 with v 1 • (α, t) • v 2 ∈
L 2 tr and v 1 ∈ R(Σ \ Σ i ). We can then deduce

u 1 • v 1 • (α, t) • v 2 ∈ L tr and (u 1 • v 1 ) ∈ R(Σ \ Σ i )
This means that in both cases u ∈ {u 1. Let us assume u ∈ Pr i (L)(α, t) tr . This means that u = u 1 • u 2 • u 3 with u 1 ∈ ⌈Φ(L 1 )(Σ i ) ⃝ ⋆ ⌉ [0;t] tr , u 3 ∈ ⌊L ⃝ ⋆ 1 ⌋ [t;∞[ tr and u 2 ∈ Pr 1 (L 1 )(α, t) tr . Therefore, we know that u 1 ∈ L ⃝ ⋆ 1 tr , u 1 ∈ R(Σ \ Σ i ), and

′ • v ′ | u ′ • (α, t) • v ′ ∈ L tr and u ′ ∈ R(Σ \ Σ i )} 2
u 2 = v 1 • v 2 with v 1 • (α, t) • v 2 ∈ L 1 tr .
Hence

u 1 • v 1 • (α, t) • v 2 • v 3 ∈ L ⃝ ⋆ 1 tr with u 1 • v 1 ∈ R(Σ \ Σ i ) 2

▶ Definition 1 (

 1 operators are extended to timed languages in the classical way. Moreover, for n ∈ N and n ≥ 2, L n and L •n respectively denote the language obtained by concatenating L with itself using operators • and •, respectively; while L 0 = L •0 = {ϵ}. Syntax of timed regular expressions). Timed regular expressions over Σ are defined inductively by the following grammar where I ⊆ I, a ∈ Σ, L ′ a timed regular expression over Σ ′ and θ : Σ ′ → Σ ∪ {ϵ} a renaming:

173▶ Definition 6 (

 6 Semantics of timed regular expressions over timed traces). The semantics of a timed regular expression is the set of timed traces defined inductively by function • tr :

©Algorithm 1 if i = 1 then 2 Li := specification 3 else 4 Li := waiting 5 6 if 8 else 9 Li 10 if 16 if 19 send

 1245689101619 V. Roussalany and Y. Falcone; licensed under Creative Commons License CC-BY 4.0 Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany Algorithm for Ci 1 when an internal event (α, t) is observed do Li = waiting then 7 add (α, t) to the memory := Pri(L)(e, t) Li tr = ∅ then 11 return bad verdict 12 when an expression L is received do 13 Li = L foreach (α, t) in the memory do 14 Li := Pri(L)(α, t) 15 Remove (α, t) from the memory Li tr = ∅ then 17 return bad verdict 18 when urgent(Li) do Li to target(Li) 20 Li := waiting

  ∀t, I, L, ∀(I′ , L ′ ) ∈ ∆ i (L, I)(α, t), ∀t ′ ∈ I ′ , L ′ = Pr i (L ↓ t ′ )(α, t) ∀t, I, L, ∀(I 1 , L 1 ), (I 2 , L 2 ) ∈ ∆ i (L, I)(α, t), (I 1 , L 1 ) ̸ = (I 2 , L 2 ) ⇔ I 1 ∩ I 2 = ∅ ∀t, I, L, (I ′ ,L ′ )∈∆i(L,I)(α,t) I ′ = I CProof that Pr i is a decentralised progression functionProof. Let us prove this by induction. We will consider the cases that are not immediately apparent :Let L = L 1 • L 2 .Let us prove the double inclusion.

.

  Let us prove the other side of the inclusion. Let us assume u and v such thatu • (α, ) • v ∈ L tr ∧ u ∈ R(Σ \ Σ i )}. This means that u • (α, t) • v = u ′ • v ′ with u ′ ∈ L 1 tr and v ′ ∈ L 2 tr .We can then deduce that we either haveu ′ = u • (α, t) • v 1 or have v ′ = u 1 • (α, t) • v. In other words, we have either u • v 1 ∈ Pr i (L 1 )(α, t) tr with v ′ ∈ ⌊L 2 ⌋ [t,∞[ tr or u 1 • v ∈ Pr i (L 2 )(α, t) tr with u ′ ∈ L 1 and in the last case, every element before (α, t) cannot contain elements of Σ i , therefore it must be true for u ′ which means u ′ ∈ ⌈Φ i (L 1 )(Σ i )⌉[0;t] tr . This means that in both casesu • v ∈ Pr i (L)(α, t) tr If L = L ⃝ ⋆ 1 .

  1 , t 1 ) and (α 2 , t 2 ), we havet 1 ≤ t 2 . A timed trace is , t 1 ) • • • (α n , t n ) a timed trace, let us denote by τ first (π) = t 1 (resp. τ last (π) =t n ) the time at which the first (resp. last) event of π occurs. We denote by L↓ t the language represented by θ ϵ (⟨x⟩ [t,t] ) where θ ϵ is the renaming that maps everything to ϵ. Intuitively, L↓ t is the language of timed words {t • u | u ∈ L }. Similarly, we define L↑ t by shifting all

	a sequence of events from Σ where each event is paired with the time at which it occurs. For
	example, (a, 1.5) • (b, 3.1) • (a, 3.1) • (c, 3.4) is a timed trace. Additionally, we also consider
	(ϵ, t) where ϵ is the empty word. Although this does not represent an observed event, it can
	be used to represent the absence of such an event. It can be simplified if there is an element
	following it with (ϵ, t) • (α, t ′ ) = (α, t ′ ) for α ∈ Σ. We denote by R(Σ) the set of timed traces
	over Σ.
	For π = (α 1 the time constraints that appear before the first concatenation (•) in L by subtracting t. It
	can be defined inductively as such:

  Note that the timed words produced by function ω do not have a delay at the end. That is why we denote by ∼ the relation defined by u ∼ v if and only if there exists x ∈ R such that v = u • x or u = v • x. We can show that every equivalence class in T (Σ)/∼ has only one representative that is an image of a timed trace by ω and this equivalence class has one unique reverse image by ω -1 .

	▶ Corollary 8. For u ∈ T (Σ) and L ∈ E(Σ), u ∈ L if and only if there exists v ∈ T (Σ)
	This function
	converts a timed trace into a timed word that represents the same sequence of events over
	physical time.

▶ Proposition 7. For u ∈ R(Σ) and L ∈ E(Σ), u ∈ L tr if and only if ω(u) ∈ L .

Table 1

 1 Summary of the experimental results.

	Algorithm	Target	messages	# progressions decision time
			# sent	total size
	Centralised	-	278.50	10305	278.50	257.99
	Decentralised	dynamic static	5.91 6.70	539426 376944	10.46 11.78	142.71 143.78

1 .

 1 Assume u ∈ Pr i (L)(α, t) tr . There are then two possible cases.First case: u ∈ Pr i (L 1 )(α, t) • ⌊L 2 ⌋ [t;∞[ tr which means that u = u 1 • u 2 with u 1 ∈ Pr i (L 1 )(α, t) tr and u 2 ∈ L 2 tr and τ first (u 2 ) ≥ t. Using our induction hypothesis u 1 = v 1 • v 2 with v 1 • (α, t) • v 2 ∈ L 1 and v 1 ∈ R(Σ \ Σ i ). Therefore, we proved v 1 • (α, t) • v 2 • u 2 ∈ L tr . Second case u ∈ ⌈Φ(L 1 )(Σ i )⌉ [0;t] • Pr i (L 2 )(α, t) tr , then it means that u = u 1 • u 2 with u 1 ∈ Φ(L 1 )(Σ i ) tr and u 2 ∈ Pr i (L 2 )(α, t) tr . This means that u 1 ∈ L 1 tr ∩ R(Σ \ Σ i ).Using our induction hypothesis, we have

  . Now to prove the other inclusion. Let us assume u• v such that w = u • (α, t) • v ∈ L tr . Since w is not empty, it is equal to w 1 • w 2 • .... • w n , with w i ∈ L 1 tr . Becausewe know that w contains (α, t), we can denote by k the index of the w i containing this event. In other words, we havew k = u ′ • (α, t) • v ′ ∈ L 1 tr , which means that u ′ • v ′ ∈ P rog i (L 1 )(α, t) tr . This proves that u • v = w 0 • ... • w k-1 • u ′ • v ′ • w k+1 • ...w n ∈ ⌈Φ(L 1 )(Σ i ) ⃝ ⋆ ⌉ [0;t] • Pr i (L 1 )(α, t) • ⌊L ⃝ ⋆ 1 ⌋ [t;∞[ tr Let L = L 1 • L 2 .Let us prove the double inclusion. 1. Assume u ∈ Pr i (L)(α, t) tr . There are then two possible cases. First case: u ∈ Pr i (L 1 )(α, t) • ⌊L 2 ⌋ [t;∞[ tr then means that u = u 1 • u 2 with u 1 ∈ Pr i (L 1 )(α, t) tr and u 2 ∈ L 2 ↓ τ last (u1) tr and τ first (u

2 ) ≥ t. Using our induction hypothesis

u 1 = v 1 • v 2 with v 1 • (α, t) • v 2 ∈ L 1 and v 1 ∈ R(Σ \ Σ i ). This allows us to conclude that v 1 • (α, t) • v 2 • u 2 ∈ L tr .

Note that we do not consider the alternative problem of determining that the trace will always be in L tr for any possible future completion. This problem is, however, harder, as it requires testing whether or not an expression denotes the universal language, which is undecidable.

© V.Roussalany and Y. Falcone; licensed under Creative Commons License CC-BY 4.0 Leibniz International Proceedings in Informatics Schloss Dagstuhl -Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

Funding Victor Roussanaly: [H2020-ECSEL-2018-IA call -Grant Agreement number 826276 (CPS4EU)] Yliès Falcone: [H2020-ECSEL-2018-IA call -Grant Agreement number 826276 (CPS4EU), Région Auvergne-Rhône-Alpes -"Pack Ambition Recherche" programme, French ANR project ANR-20-CE39-0009 (SEVERITAS), LabEx PERSYVAL-Lab (ANR-11-LABX-0025-01)] © V. Roussalany and Y. Falcone; licensed under Creative Commons

A

Definition of Φ

B Definition of ∆ i

For I, I ′ two intervals, we denote

And

x > t} such that I ◁ I ′ , I ▷ I ′ and I ∩ I ′ are always a partition of I. We define ∆ i as follows:

This means that u 1 ∈ L 1 tr ∩R(Σ\Σ i ). Taking into account the first property of ∆ i , we can also see that u 2 ∈ Pr i (L 2 ↓ τ last (u1) )(α, t) tr . Using our induction hypothesis, we have

Therefore, we have

Let us prove the other side of the inclusion. Assume u and v such that u

We can deduce that we have

In other words, we have u

Let us look at the other case. Every element before (α, t) cannot contain elements of Σ i , therefore it must be true of u ′ , which means u ′ ∈ Φ i (L 1 )(Σ i ) tr . Using the second and third properties of ∆ i , we can see that there is one and only one (I, L ′ ) ∈

1. Assume u ∈ Pr i (L)(α, t) tr . This means that there is (I,

In other words, we know that

Since w is not empty, w = w 1 • w 2 • .... • w n , with w i ∈ L 1 ↓ τ last (wi-1) tr . Because we know that w contains (α, t), we can denote by k the index of w i that contains this event. In other words, we have w k = u ′ • (α, t) • v ′ ∈ L 1 ↓ τ last (w k-1 ) tr , which means that u ′ • v ′ ∈ P rog i (L 1 ↓ τ last (wi-1) )(α, t) tr . Using the second and third properties of ∆ i we deduce that there is one and only one (I, L ′ ) ∈ ∆ i (L 1 , R + )(α, t) such that τ last (w k-1 ) ∈ I and in that case we have w k ∈ L ′ tr . This shows that