Matthieu Renard

Antoine Rollet

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

Under consideration for publication in Formal Aspects of Computing Runtime Enforcement of Timed Properties using Games

Introduction

Runtime Verication (RV) ([LS09, FHR13, BFFR18, BF18]) is a powerful technique aiming at checking that the current execution of a running system conform to a given specication. In RV, one uses a monitor that acts as a decision procedure giving verdicts from a sequence of events gathered from the execution of the system under scrutiny. The monitor is usually synthesised from a property formalising the specication (e.g. an automaton or a temporal logic formula). This sequence is obtained via instrumentation. RV ressembles passive testing ([CGP03, ACC

+ 04]) and permits to obtain alerts in case of wrong behaviour while the system is running.

This paper deals with Runtime Enforcement (RE, [Sch00, LBW09, FMFR11, BJKZ13]) of properties, an extension of Runtime Verication. While RV deals with sequence observation, RE deals with sequence transformation. In RE, one uses a so-called enforcement mechanism/monitor (EM) which modies the sequence of events produced by the system, if needed. According to a set of rules, the EM transforms a possibly incorrect input sequence into another one verifying the required property. Most works on RE abstract away implementation details. Then, it generally consists in dening an input-output relation describing how to transform a (possibly incorrect) input sequence of events into an output sequence of events using an EM (see Fig. 1). This transformation is done according to the required property which is used in order to synthesise the EM. One of the advantages of RE is that the whole specication of the system under scrutiny is not necessary to generate an EM, only a property that should be satised by its output is needed. Depending on the specication formalism of properties, various classes of properties can be enforced on systems, safety properties and transactions for instance; see [START_REF] Falcone | You should better enforce than verify[END_REF][START_REF] Falcone | What can you verify and enforce at runtime?[END_REF][START_REF] Khoury | Which security policies are enforceable by runtime monitors? A survey[END_REF][START_REF] Falcone | Runtime failure prevention and reaction[END_REF] for overviews and surveys.

Usually, the input-output relation realised by the EM should be sound and transparent. Soundness and transparency mean that the output sequence should satisfy the required property and that the output should be as close as possible to the input sequence (implying that a correct input sequence should not be modied), respectively. This notion of transparency is rather general since it depends on the denition of closeness, and contains an implicit notion of optimality (which may also be considered separately as in [START_REF] Pinisetty | Runtime enforcement of regular timed properties[END_REF]).

In case of timed properties, the EM acts as a delaying lter on the input ([PFJ + 13, PFJM14b, PFJM15]) ; see [START_REF] Falcone | On the runtime enforcement of timed properties[END_REF] for a recent overview. It uses a buer in order to store input events and releases them only at an instant where the satisfaction of the property is ensured (possibly never).

Motivations. This paper deals with RE of timed properties with uncontrollable events. In some situations events should be observed by the EM, permitting initiating a reaction if necessary, but without the possibility to modify it. This may happen e.g. in case of a broadcast of an alert, or in case of an interruption message in a system. Such an event is said to be uncontrollable. They naturally arise in many concrete scenarios. Uncontrollable events can indeed model some physical event (coming from the environment) that is impossible to prevent, but that the system under scrutiny should observe to react correctly. For instance, in an autonomous car control system, the crossing line event could be seen as an uncontrollable event, i.e.

only observable by the EM, permitting initiating the necessary trajectory correction. More formally, it is necessary to consider two sets of events: the controllable ones that can be modied by the EM (e.g. stored in a buer as in [PFJ + 14]), and the uncontrollable ones which cannot.

Challenges. Considering uncontrollable events in the framework implies new challenges. Indeed, the occurrence of uncontrollable events, which should be released instantaneously, may have an impact on the release date of stored events. Thus it is necessary to recompute all of them in such a situation. Moreover, it is necessary to anticipate uncontrollable events, i.e. to compute all the possible reachable (bad) states for any sequence of uncontrollable events. This computing may be costly. Since an EM should react in a reasonable time laps, optimisation strategies should be investigated. Finally, with the classical denitions (e.g. used in [Sch00, LBW09, PFJ + 13, PFJM14b, PFJM15]) some properties may never be enforceable. This may arise for instance in case of a sequence of uncontrollable events leading directly in a forbidden state from the initial one. Thus new enforcement approaches are necessary.

Contributions. The rst proposition of RE framework for timed properties with uncontrollable events has been proposed in [START_REF] Renard | Optimal enforcement of (timed) properties with uncontrollable events[END_REF]. Now, we introduce a new RE framework for timed properties using Büchi games (see [START_REF] Gradel | Automata, logics, and innite games: a guide to current research[END_REF] for a detailed description of innite games, including Büchi games) for generating the EM. This kind of game is adapted since it corresponds to games in which one tries to always be able to reach some nodes called Büchi nodes. An EM tries to always be able to reach an accepting state of the automaton representing the property, even if some uncontrollable events are received, thus it is similar to solving a Büchi game. Using games permits to pre-compute some of the decisions of the EM. It permits to avoid the exploration of the whole execution tree at runtime, thus improving the time overhead of an implementation.

A rst RE framework using games has been proposed in [START_REF] Renard | Runtime enforcement using Büchi games[END_REF]. We generalise this approach in case of timed properties. The generated EM is sound, compliant and optimal. Compliance is a weakened variant of L ⊆ Σ * is extension-closed if for any words w ∈ L and w ∈ Σ * , w • w ∈ L. Given a word w = a 1 • a 2 . . . a |w| and an integer i such that 1 ≤ i ≤ |w|, we note w(i) the i-th element of w, i.e. w(i) = a i . We also note w [..i] the prex of w of size i: w [..i] = a 1 • a 2 . . . a i . Given a tuple e = (e 1 , e 2 , . . . , e n ) of size n, for an integer i such that 1 ≤ i ≤ n, we note Π i the projection on the i-th coordinate, i.e. Π i (e) = e i . The tuple (e 1 , e 2 , . . . , e n ) is sometimes noted e 1 , e 2 , . . . , e n in order to help reading. It can be used, for example, if a tuple contains a tuple. Given a word w ∈ Σ * and Σ ⊆ Σ, we dene the restriction of w to Σ , noted w |Σ , as the word w ∈ Σ * whose letters are the letters of w belonging to Σ in the same order. Formally, |Σ = and for any σ ∈ Σ * , and any a ∈ Σ, (w • a) |Σ = w |Σ • a if a ∈ Σ , or (w • a) |Σ = w |Σ otherwise. We also note = Σ the equality of the restrictions of two words to Σ : for σ and σ in Σ * , σ = Σ σ if σ |Σ = σ |Σ . We dene in the same way the operator Σ by : σ Σ σ whenever σ |Σ σ |Σ .

Timed Languages

Let R ≥0 be the set of non-negative real numbers, and Σ a nite alphabet of actions. An event is a pair (δ, a) ∈ R ≥0 × Σ. We dene delay((δ, a)) = δ and act((δ, a)) = a the projections of events on delays and actions respectively. A timed word over Σ, is a nite sequence of events of (R ≥0 × Σ). The set of timed words over Σ is denoted tw(Σ). For σ = (δ 1 , a 1 )

• (δ 2 , a 2 ) • • • (δ n , a n ), δ i (2 ≤ i ≤ n)
is the delay between action a i-1 and action a i , and δ 1 is the time elapsed before the rst event (i.e. the delay between the beginning of the enforcement process and the occurrence of the rst action a 1 ). We naturally extend the notions of prex and residual to timed words.

We denote the total time needed to read a timed word σ by time(σ). Formally, time(σ) = |σ| i=1 δ i . The observation of σ at time t is the timed word noted obs(σ, t) and dened as: obs(σ, t) = max ({σ | σ σ ∧ time(σ ) ≤ t}). It corresponds to the word that would be observed at date t when reading σ. We also dene the remainder of the observation of σ at date t as nobs(σ, t) = (obs(σ, t)) -1 • σ, which corresponds to the events that are to be received after obs(σ, t) when reading σ. Note that the rst delay of nobs(σ, t) is relative to the nal action of obs(σ, t) and not to t itself.

The untimed projection of a timed word σ is noted Π Σ (σ), and is dened as: Π Σ ((δ 1 , a 1 )•(δ 2 , a 2 )

• • • (δ n , a n )) = a 1 • a 2 • • • a n .
It is the sequence of actions of the timed word with dates ignored. For a timed word σ = (δ 1 , a 1 ) • (δ 2 , a 2 ) • • • (δ n , a n ), and a delay t ∈ R ≥0 , σ delayed by t is the word noted σ + t t and such that t is added to the rst delay of σ: σ + t δ = (δ 1 + t, a 1 ) • (δ 2 , a 2 ) • • • (δ n , a n ). Similarly, we dene σt t, when δ 1 ≥ t, as σt δ = (δ 1 -t, a 1 ) • (δ 2 , a 2 ) • • • (δ n , a n ). We also extend the denition of the restriction of σ to Σ ⊆ Σ to timed words, such that only actions belonging to Σ remain. This operation keeps the dates of the events unchanged, not the delays, thus, it is formally dened by induction as follows:

|Σ = ,
and for σ ∈ tw(Σ) and (δ, a) ∈ R ≥0 × Σ,

(σ • (δ, a)) |Σ = σ |Σ • (time(σ • (δ, a)) -time(σ |Σ ), a) if a ∈ Σ σ |Σ otherwise.
Note that to concatenate two restrictions, it is also needed to adjust the delay at the beginning of the second word: for σ ∈ tw(Σ) and σ ∈ tw(Σ), (σ

• σ ) |Σ = σ |Σ • (σ |Σ + t (time(σ) -time(σ |Σ ))
). The notations = Σ and Σ are then naturally extended to timed words.

A timed language is any subset of tw(Σ). The notion of extension-closed languages is naturally extended to timed languages, i.e. if L ⊆ tw(Σ) is a timed language, L is extension-closed if L = L • tw(Σ). We also extend the notion of extension-closed languages to sets of elements composed of a timed word and a date: a set S ⊆ tw(Σ) × R ≥0 is time-extension-closed if for any (σ, t) ∈ S, for any w ∈ tw(Σ), and for any t ≥ t, (σ • w, t ) ∈ S. In other words, S is time-extension-closed if for every σ ∈ tw(Σ), there exists a date t from which σ and all its extensions are in S, that is, associated with a date greater or equal to t.

Moreover, we dene an order on timed words: we say that σ is a delayed prex of σ, noted σ d σ, whenever Π Σ (σ ) Π Σ (σ) and for any i ∈ [1; |σ | -1], time(σ [..i] ) ≤ time(σ [..i] ). Intuitively, σ d σ if σ is a prex of σ whose actions have been delayed, considering dates. Note that the order is not the same in the dierent constraints: Π Σ (σ ) is a prex of Π Σ (σ), but dates in σ exceed dates in σ. As for the equality = and the prex order , we note σ dΣ σ whenever σ |Σ d σ |Σ , and σ ≺ d σ whenever σ d σ and σ = σ. We also dene a lexical order ≤ lex on timed words with identical untimed projections, such that ≤ lex , and for two words σ and σ such that Π Σ (σ) = Π Σ (σ ), and two events (δ, a) and (δ , a), (δ , a) • σ ≤ lex (δ, a) • σ if δ < δ ∨ (δ = δ ∧ σ ≤ lex σ).

Timed Automata as Timed Properties

In the following part we recall some notions on timed automata ( [START_REF] Alur | The theory of timed automata[END_REF]). These notions are classical. A reader not familiar with timed automata may nd more details and explanations in [START_REF] Alur | The theory of timed automata[END_REF].

Let X = {X 1 , X 2 , . . . , X n } be a nite set of clocks, i.e. variables that increase regularly with time. A clock valuation is a function ν from X to R ≥0 . The set of clock valuations for the set of clocks X is noted V(X), i.e. V(X) = {ν | ν : X → R ≥0 }. We consider the following operations on valuations:

• for any valuation ν ∈ V(X), ν + δ is the valuation representing the elapse of δ time units from ν, such that for any G(X) denotes the set of guards consisting of boolean combinations (i.e. conjunctions or disjunctions) of constraints of the form X i c with X i ∈ X, c ∈ N, and ∈ {<, ≤, =, ≥, >}. Given g ∈ G(X) and a valuation ν, we write ν |= g when g holds according to ν.

X i ∈ X, (ν + δ)(X i ) = ν(X i ) + δ; • for any subset X ⊆ X, ν[X ← 0] is the valuation representing ν with clocks in X reset, such that: (ν[X ← 0]) : X i → 0 if X i ∈ X ν(X i ) otherwise.

Timed automaton [AD92]

A timed automaton (TA) is a tuple A = L, l 0 , X, Σ, ∆, G , such that L is a set of locations, l 0 ∈ L is the initial location, X is a set of clocks, Σ is a nite set of events, ∆ ⊆ L × G(X) × Σ × 2 X ×
L is the transition relation, and G ⊆ L is a set of accepting locations. A transition (l, g, a, X , l ) ∈ ∆ is a transition from l to l , labelled with event a, with guard g, and with the clocks in X to be reset.

The semantics of a timed automaton

A is a timed transition system A = Q, q 0 , Γ, →, F G where Q = L × V(X) is the (innite) set of states, q 0 = (l 0 , ν 0 ) is the initial state, with ν 0 = ν[X ← 0], F G = G × V(X)
is the set of accepting states, Γ = R ≥0 ∪ Σ is the set of transition labels, that can be either a number representing a delay, or an action. The transition relation → ⊆ Q × Γ × Q is made of transitions of two possible kinds:

• Delay transitions: for δ ∈ R ≥0 and (l, ν) ∈ Q, (l, ν), δ, (l, ν + δ) ∈→.

• Action transitions: for a ∈ Σ, (l, ν) ∈ Q, (l, ν), a, (l , ν ) ∈→ if there exists (l, g, a, Y, l ) ∈ ∆, such that ν |= g and ν = ν[Y ← 0].

A timed automaton A = L, l 0 , X, Σ, ∆, G is deterministic if for any (l, g 1 , a, Y 1 , l 1 ) and (l, g 2 , a, Y 2 , l 2 ) in ∆, g 1 ∧ g 2 is unsatisable, meaning that only one transition can be red at any time. A is complete if for any l ∈ L and any a ∈ Σ, the disjunction of the guards of all the transitions leaving l and labelled by a holds for any clock valuation.

Example 1. Examples of timed automata are given in Fig. 2. In Fig. 2a, L = {l 0 , l 1 , l 2 }, X = {x}, Σ = {click}, ∆ = {(l 0 , , click, {x}, l 1 ), (l 1 , x > 2, click, {x}, l 1 ), (l 1 , x ≤ 2, click, ∅, l 2 ), (l 2 , , click, {x}, l 1 )}, and G = {l 2 }, where evaluates to true for any clock valuation. This automaton models a double click: considering that the click event is a mouse click, the automaton only accepts sequences of clicks that ends with a double-click. The condition for two clicks to be considered as a double-click is that the second one is made less than two time units after the rst one. Note that with this modelling, double-clicks can not overlap, i.e. clicking three times in less than two time units will not be considered as ending with a double-click, since only the rst two clicks will be considered as a double-click. Allowing overlaps would only require splitting the transition from l 2 to l 1 in two, as described in Fig. 2b.

A run ρ from q ∈ Q is a valid sequence of transitions in A starting from q, of the form ρ = q δ1 -→ q 1 a1 -→ q 2 δ2 -→ q 3 . . . an --→ q 2n δn+1 ---→ q 2n+1 ,
where δ i ∈ R ≥0 and a i ∈ Σ, for any i. We can consider runs that alternate between delay and action transitions, since two consecutive delay transitions can be merged into one whose value is the sum of the delays of the original transitions, and two consecutive actions can be separated by a null delay transition (i.e. a delay transition whose delay is 0). The set of runs from q 0 is noted Run(A) and Run F G (A) denotes the subset of runs accepted by A, i.e. ending in a state in F G .

The trace of the run ρ previously dened is the timed word σ = (δ 1 , a 1 ) • (δ 2 , a 2 ) . . . (δ n , a n ). Note that δ n+1 does not appear in the trace, meaning that all runs with dierent values for δ n+1 share the same trace as ρ. We allow ourselves to denote by q (δ,a)

---→ q if q δ -→ q a -→ q , and thus ρ can be denoted q

σ -→ q 2n δn+1 ---→ q 2n+1 .
A regular timed property is a timed language ϕ ⊆ tw(Σ) that is accepted by a timed automaton. For a timed word σ, we say that σ satises ϕ, noted σ |= ϕ whenever σ ∈ ϕ. We only consider regular timed properties whose associated automaton is complete and deterministic.

Traces Manipulation

Given a deterministic timed automaton A = L, l 0 , X, Σ, ∆,

F whose semantics is A = Q, q 0 , Γ, - →, F G ,
and a timed word σ ∈ tw(Σ), for q ∈ Q, we note q after σ = q , where q is such that q σ -→ q , i.e. q is the state reached from q after reading word σ. Since A is deterministic, there exists only one such q . We also note Reach(σ) = q 0 after σ. We extend these denitions to languages: if L is a language, q after L = σ∈L {q after σ} and Reach(L) = q 0 after L. We also allow ourselves to use after with actions or delays, with the same denition: for δ ∈ R ≥0 , q after δ = q , if q δ -→ q , and for a ∈ Σ, q after a = q if q a -→ q .

We allow the use of the operators after and Reach with an extra parameter, representing an observation time, such that if t ∈ R ≥0 , then q after (σ, t) = q after obs(σ, t) after (ttime(obs(σ, t))), and Reach(σ, t) = q 0 after (σ, t). Moreover, for q = l, ν ∈ Q, we note up(q) = { l, ν + t ∈ Q | t ∈ R ≥0 }, it is the set of states that will be reached from q as time elapses if no action occurs. This denition is extended to sets of states: for S ⊆ Q, up(S) = q∈S up(q). Example 2. Consider the property accepting sequences of clicks ending by a double-click, described in Fig. 2a. Let us consider that the set Q of states of the semantics of this TA is Q = L × R ≥0 , with L = {l 0 , l 1 , l 2 }, and where the valuations are replaced by the value of the unique clock x. Then, for instance, Reach((1, click)) = (l 0 , 0) after (1, click) = (l 1 , 0), and (l 1 , 1) after ((1, click), 3) = (l 2 , 4), since x = 2 when the action click occurs, enabling the transition to l 2 , and then 2 time units remain to wait, giving a nal value of 4 for x.

Büchi Games

We recall some general notions on Büchi games in an informal way. More details and formal notations may be found in [START_REF] Gradel | Automata, logics, and innite games: a guide to current research[END_REF]. Considering a directed graph V, E such that V is a set of vertices, and E ⊆ V × V a set of edges. V is partitioned into two subsets: V 0 the player P 0 vertices, and V 1 the player P 1 ones. As usual in game graphs, we assume that there always exists an outgoing edge from a vertex. The two players play a game on the graph by forming a (innite) path from the initial vertex in the graph by moving a token along edges. If the token is in V 0 (resp. V 1 ), the player P 0 (resp. P 1 ) moves the token following an edge going out of the vertex. The resulting (innite) path in the graph is called a play. A strategy for a player is a way to extend plays. Formally, a strategy for player P 0 is a mapping σ : V * V 0 → V that, given a nite sequence of vertices (the history of the play) ending in a player P 0 vertex, chooses the next vertex. In order to ensure that strategies always exist, we will consider that the graph is strongly connected.

A play π = v 0 , v 1 , . . . is consistent with the strategy σ if for any v i ∈ V 0 , v i+1 = σ(v 0 • v 1 • • • • • v i )
, meaning that the strategy was followed for any vertex in V 0 . The goal of a game can be, for example, to reach a state in a given subset of V (reachability game), or to ensure that a given subset of V is visited an innite number of times (Büchi games). Thus, given a subset F G ⊆ V of vertices, the Büchi game for P 0 consists in nding a winning strategy σ such that all plays π consistent with σ visit an innite number of times the set F G . We refer to the nodes in F G as Büchi nodes.

It is known that it is possible ([CHP08]) to compute the set W 0 of winning vertices for P 0 (i.e. the set of vertices from where there exists a winning strategy for P 0 ), and the associated winning strategy from all these vertices. From all the other vertices (in V \W 0 ), there exists a winning strategy for P 1 , i.e. W 1 = V \W 0 , thus P 0 can not win the game if P 1 plays perfectly from one of these vertices. Moreover, it is possible to nd a strategy that is memoryless, meaning that the only the last vertex is needed to compute the next. Formally, a memoryless strategy for P 0 is a strategy σ : V 0 → V . Such strategies are easier to compute, since they do not require to read the entire history before choosing the transition to follow.

Functions

In all this paper, we use functions to describe the input/output behaviour of EMs. We then use input and output to refer to argument and image of such functions, respectively.

Enforcing Timed Properties using a Büchi Game

In this section, we present the theoretical framework for enforcing timed properties using games. This approach has been implemented in the GREP tool. A rst approach has been published in [START_REF] Renard | Runtime enforcement using Büchi games[END_REF], but for untimed properties only.

Given a timed regular property described by a TA, the objective is to synthesise an EM which is sound according to this property, compliant and optimal. To synthesise the EM, we propose to build a two-player game graph representing the possible actions of the EM and the system under scrutiny. Each edge of this graph corresponds to a possible action of a player. The last step consists in computing the set of nodes of the graph from which there exists a winning strategy, i.e. solving a Büchi game. More precisely, the approach is divided into three steps: rst, it computes a symbolic graph, which is a nite abstraction of the (innite) semantics of the TA; then it computes the game graph and the winning strategy for the EM; nally the EM follows the strategy to enforce the property. Using this approach permits to pre-compute some of the decisions of the EM, thus avoiding to explore all paths of the execution tree at runtime. GREP is a tool designed to produce EMs, such as the ones described in [RFR + 17]. However, the formal denitions from [RFR + 17] did not t well with an eective implementation, thus we propose EMs that are formally equivalent, but that are built in a more implementation-friendly way.

We rst introduce enforcement functions and their requirements, namely soundness, compliance and optimality. Enforcement functions are functional descriptions of EMs that represent their input/output behaviour, as depicted in Fig. 1. Enforcement functions serve as abstract non-operational descriptions of EMs which can possibly be reused to obtain alternative operational descriptions of EMs. In addition, enforcement functions facilitate the expression of requirements on EMs. Then, we give details about the EM synthesis framework using games, and show that the obtained EM is sound, compliant and optimal. Then, we provide another operational description of the EM, based on transition systems, and show their equivalence.

Enforcement Functions and their Properties

In the rest of this section, we consider an alphabet of actions Σ. We give formal denitions of enforcement functions and the requirements of such functions, i.e. soundness, compliance, and optimality. The denitions in this section are equivalent to the ones in [RFR + 17]. In the following, ϕ is a timed property dened by a timed automaton A ϕ = L, l 0 , X, Σ, ∆, F with semantics A ϕ = Q, q 0 , Γ, -→, F G , and the set of actions Σ is partitioned into a set of uncontrollable actions Σ u , (which can not be modied by the EM) and a set of controllable actions Σ c (the other actions). As in [PFJ + 14], the EM is equipped with a buer permitting to store (only controllable) actions and release them later. The EM is modelled by a function from tw(Σ) × R ≥0 to tw(Σ). Before detailing the denitions, we provide some intuitions about the synthesis of the EM. For this purpose, we illustrate its desired behaviour on an example. Example 3. Consider property ϕ t (Fig. 3) which models the use of a shared writable device with a centralised controller. To be able to Write to the device, one must rst authenticate (uncontrollable event Auth), then wait 2 time units for synchronisation. Uncontrollable events LockOn and LockO are used by the controller to notify that someone is writing, meaning that the lock has been taken by someone else, and that the lock has been released, respectively. While the lock is held by someone else, writings are not allowed. And after the lock has been released, one must wait 2 time units before writing. Indeed, in ϕ t all transitions arriving in location l 1 reset the clock x. From l 1 , emitting event Write after 2 time units loops on the same location, whereas emitting it before 2 time units leads to location l 3 , which is a non-accepting state. Consider an EM aiming to enforce this property with the input σ = Finally, given the input σ = ((1, Auth) Write). Consider now the situation where the uncontrollable event LockOn is received at the beginning of the process (i.e. in location l 0 ). It leads inevitably ϕ t to location l 3 which is a non-accepting state without any possibility to go back to an accepting one. This illustrates the fact that ϕ t is not always enforceable as we shall discuss later.

((1, Auth) • (1, LockOn) • (2, Write) • (1, LockO ) • (1, LockOn) • (1, Write) • (1, LockO )). At time t =
• (1, LockOn) • (2, Write) • (1, LockO ) • (1, LockOn) • (1, Write) • (1, LockO )), the output of the EM should be (1, Auth)•(1, LockOn)•(3, LockO )•(1, LockOn)•(2, LockO )• (2, Write) • (0,
An enforcement function is a functional representation of the input/output behaviour of an EM, thus an enforcement function takes a timed word and the current time as input, and outputs a timed word: Denition 1 (Enforcement Function). An enforcement function (over Σ) is a function E : tw(Σ) × R ≥0 → tw(Σ) that satises the two following constraints:

1. ∀σ ∈ tw(Σ), ∀t ∈ R ≥0 , ∀t ≥ t, E(σ, t) E(σ, t ), 2. ∀σ ∈ tw(Σ), ∀δ ∈ R ≥0 , ∀a ∈ Σ, E(σ, time(σ • (δ, a))) E(σ • (δ, a), time(σ • (δ, a))).
We note F enf (Σ) (or F enf when clear from the context) the set of all enforcement functions over Σ.

The requirements in Denition 1 model physical constraints (i.e. the irreversibility of time): an enforcement function can only append events to its output as the input grows. The rst constraint (E(σ, t) E(σ, t )) corresponds to the elapse of time, whereas the second one (E(σ, time(σ

•(δ, a))) E(σ •(δ, a), time(σ •(δ, a))))
corresponds to the read of a new event. They require the new output to be an extension of the previous one.

An enforcement function should full the three following requirements: soundness, compliance and optimality. These notions are usual in the RE literature (see e.g. in [START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF][START_REF] Falcone | Runtime enforcement monitors: composition, synthesis, and enforcement abilities[END_REF]), but have to be adapted to a timed context and uncontrollable events. More precisely, the denitions proposed in this section are adapted from [PFJ + 14] (RE framework in a timed context, only with controllable events) and [START_REF] Renard | Runtime enforcement using Büchi games[END_REF] (RE framework in an untimed context, with uncontrollable events). Soundness states that the output of an enforcement function should satisfy the desired property. This means that the corresponding EMs should modify executions in order to keep the property satised. Compliance indicates which operations are allowed on the executions, i.e. how the EM can modify the output. Compliance is a weaker version of the usual notion of transparency (e.g. used in [FMFR11, PFJ + 13, PFJM14b, PFJM15]). Indeed, the framework con- siders controllable and uncontrollable events. Since uncontrollable events have to be released immediately, it may happen that the order of input events is dierent from the output ones. Moreover, contrary to the usual notion of transparency which contains an implicit notion of optimality, we distinguish explicitly the two notions. Then, optimality requires the EM to emit as many events as possible, while preserving the property from being violated.

We give formal denitions of these requirements as constraints on enforcement functions. In a timed context, soundness states that the output of an enforcement function should eventually always satisfy the desired property (here, ϕ):

Denition 2 (Soundness). An enforcement function E ∈ F enf is sound with respect to ϕ in a time-

extension-closed set S ⊆ tw(Σ) × R ≥0 if: ∀(σ, t) ∈ S, ∃t ≥ t, ∀t ≥ t , E(σ, t ) |= ϕ.
We note F snd (ϕ, S) the set of all enforcement functions that are sound with respect to ϕ in S.

An enforcement function is sound with respect to ϕ in S if for any (σ, t) ∈ S, the output of the enforcement function with input σ from date t eventually always satises ϕ. Notice that in some situations, the occurrence of some words may inevitably lead the system to a non-accepting state. Considering e.g. ϕ t in Fig. 3, the occurrence of the uncontrollable action LockOn in q 0 would inevitably lead the system to the non-accepting state q 3 . For this reason, similarly to [START_REF] Renard | Runtime enforcement using Büchi games[END_REF] in the untimed case, soundness is restricted to an extensionclosed set S.

Compliance states that an EM can only delay controllable events, without modifying uncontrollable events (i.e. keeping their dates unchanged). This is a direct adaptation of the choice made in [START_REF] Pinisetty | Runtime enforcement of timed properties revisited[END_REF] where the EM acts as a delaying lter on the input. We recall that Σ c and Σ u are the sets of controllable and uncontrollable actions respectively, and that Σ u ∩ Σ c = ∅:

Denition 3 (Compliance). An enforcement function E ∈ F enf is compliant with respect to Σ u and Σ c , noted compliant(E, Σ u , Σ c ) (or compliant(E) when clear from the context), if it satises the following constraints:

1. ∀σ ∈ tw(Σ), ∀t ∈ R ≥0 , E(σ, t) dΣ c obs(σ, t), 2. ∀σ ∈ tw(Σ), ∀t ∈ R ≥0 , E(σ, t) = Σu obs(σ, t), 3. ∀σ ∈ tw(Σ), ∀(δ, u) ∈ R ≥0 × Σ u , E(σ, time(σ • (δ, u))) • (time(σ • (δ, u)) -time(E(σ, time(σ • (δ, u)))), u) E(σ • (δ, u), time(σ • (δ, u))).
We note F cpl (Σ u , Σ c ) (or F cpl when clear from the context) the set of all enforcement functions that are compliant with respect to Σ u and Σ c .

In Denition 3, the rst constraint allows the EM to delay controllable events without changing their order;

the second constraint requires that uncontrollable events are not modied; and the third constraint requires that the EM does not react to the reception of an uncontrollable event before outputting it.

For a compliant enforcement function E ∈ F enf and a timed word σ ∈ tw(Σ), we say that E(σ, ∞) is the output of E with input σ at innite time (i.e. when it has stabilised). More formally, E(σ, ∞) = E(σ, t), with t ∈ R ≥0 such that for all t ≥ t, E(σ, t ) = E(σ, t). Since the input σ is nite, and E is a compliant function (guaranteeing that the size of the output is lower or equal than that of the input), the output of E with input word σ is nite, thus such a t exists, and E(σ, ∞) is well-dened.

Another objective of an EM is to provide an output as close as possible to the input. Then, a notion of optimality has to be dened. It requires that an EM outputs as many events as possible, without breaking compliance and avoiding the possibility of breaking soundness: Denition 4 (Optimality). A sound and compliant enforcement function

E ∈ F snd (ϕ, S) ∩ F cpl (Σ u , Σ c ) is optimal in S if: ∀E ∈ F cpl (Σ u , Σ c ), ∀σ ∈ tw(Σ), ∀(δ, a) ∈ R ≥0 × Σ, (σ, time(σ • (δ, a))) ∈ S ∧ E(σ, time(σ • (δ, a))) = E (σ, time(σ • (δ, a))) ∧ E(σ • (δ, a), ∞) ≺ d E (σ • (δ, a), ∞) =⇒ ∃σ u ∈ tw(Σ u ), E (σ • (δ, a) • σ u , ∞) |= ϕ.
Intuitively, a sound and compliant enforcement function is optimal if at any moment, it outputs the longest possible word, with the lowest possible delays, ensuring soundness and compliance. In Denition 4, we suppose that a compliant enforcement function outputs a greater word (with respect to d ) than an optimal one, and then conclude that it is not sound (since the other function is optimal).

Synthesising Timed Enforcement Functions

In this part, we dene a sound, compliant and optimal inductive enforcement function E ϕ . This function is equivalent to the one described in [RFR + 17], the dierence residing in the use of a Büchi game to compute the safe states. The interest of this approach is twofold: it permits to simplify the denition of the EM, and to obtain globally better performance than in [RFR + 17] by precomputing some decisions of the EM.

First, we need to compute the set of words that can be emitted by an enforcement function while ensuring compliance and soundness. This set depends on the current state in A ϕ , and on the controllable actions of the input that have not been output yet. These actions are the actions that can be output, in the same order as they were received, with arbitrary delays, by the EM. This sequence of actions is called the buer of the EM. At any moment, the EM has to select the best sequence that should be emitted when an event occurs.

For this purpose, it is necessary to design a set Safe containing the set of words that it is possible to emit at a given instant, while staying sound, then identify the best one. Since Safe depends on the sequence that has already been emitted, it needs two parameters: the state q reached by the sequence already released, and the current state of the buer, i.e. a word in Σ * c . Then Safe contains all the prexes of the buer verifying soundness, i.e. leading to safe states. However, this notion of safe state is not simple. It nearly corresponds to accepting states of the property, from which any sequence of uncontrollable events, or letting the time elapse, leads to accepting states. Thus we dene the safe emitting function Safe :

Q × Σ * c → tw(Σ c
) such that Safe(q, w) is the set of timed words whose actions are the actions of w, associated with some delays, such that outputting such a word from q ensures compliance and soundness.

To compute this set of words, we use a Büchi game played on a graph representing the possible actions of the EM, as in [START_REF] Renard | Runtime enforcement using Büchi games[END_REF]. We represent the EM as player P 0 , and the environment as the other player, P 1 . The nodes of this graph should be taken in the set Q × Σ * c × {0, 1}, where node (q, w, p) belongs to player P p , and represents the state of the EM where q is the corresponding state of ϕ, and w the buer. Considering all such nodes, the graph would have an innite number of nodes, rst because the size of the buer is not bounded, but also because the semantics of a timed automaton has itself an innite number of states (i.e.

Q is also innite). We then reduce the number of possible buers to a nite set Σ n c . Intuitively, since the validity of a sequence only depends on the location that is reached after reading it, Σ n c is composed of all the controllable actions that can allow the EM to reach a new location. Then, we dene Σ n c as follows:

Σ n c = {w ∈ Σ * c | ∃q ∈ Q, ∃c ∈ Σ c , ∀σ ∈ tw(Σ), ∀σ ∈ tw(Σ), Π Σ (σ) = w • c ∧ Π Σ (σ ) w ∧ (l , ν ) = q after σ ∧ (l , ν ) = q after σ =⇒ l = l } Σ n
c is dened as the set of sequences of controllable actions that can be used to form a word that allows to reach a new location, the length of a word in Σ n c can not be greater than the number of locations in the timed automaton. Thus, Σ n c is nite since L is nite. The other component Q is also innite since in our denition of the semantics of a TA time is continuous. We reduce it to a nite set using a nite symbolic abstraction of the semantics of A ϕ .

A Symbolic Graph

Several abstractions for timed automata exist to reduce their semantics to a nite representation. The simplest, that satises all the requirements we need, is the region graph (see [START_REF] Alur | The theory of timed automata[END_REF]) of the timed automaton.

Unfortunately, this region graph is often very large, thus some more ecient abstractions have been studied.

A very common abstraction is the zone graph used to compute reachability in a timed automaton ([BY04]).

A zone is a convex set of clock valuations, usually represented by clock constraints of the form x n, where x is a clock, ∈ {<, ≤, =, ≥, >}, and n is a (rational) number, or more generally by xy n, where y is another clock. This graph is usually small compared to the region graph. Nevertheless, this graph only preserves information about the existence of a state in the zones (i.e. a transition in the graph represents the existence of a location and a valuation in the source node to a location and a valuation in the destination node). This is not sucient for our needs, i.e. to play a Büchi game. Indeed, when computing reachability, the used zones ensure that it is possible to reach a state in another zone from a source zone. However, when considering enforcement, the reception of an uncontrollable event can force a transition, disabling the possibility to wait a desired amount of time. Thus, it is needed to rene zones in such a way that all states in a zone behave the same, with respect to the emission of actions, and with respect to the elapse of time. In other words, the zones need to prevent players from cheating, for example doing time leaps. A time leap could be, for instance, starting in a zone x ≤ 2 and going from that zone to the zone x > 4. To play a Büchi game, it is needed that zone x ≤ 2 leads rst to zone 2 < x ≤ 4 that then leads to zone x > 4. The zone graph we use is thus dierent from the one used to compute reachability, since zones are divided in such a way that they prevent time leaps and t well the purpose of playing a Büchi game.

The graph described in [ACH

+ 92] ts our needs and seems to be a good choice. However, we give a list of constraints that are sucient for a graph to t our needs. Any symbolic graph satisfying these constraints could be used to generate the game graph, on which we can play a Büchi game. We say that such symbolic graphs are compatible with Büchi games according to the following denition (we use the standard notation ∃! for unique-existence):

Denition 5 (Compatible symbolic graph). A symbolic graph G s = V s , E s , with E s ⊆ V s ×(Σ∪{t})×
V s is compatible (with Büchi games) if it satises the following constraints:

1. V s ⊆ Q is a nite set such that ∀v ∈ V s , ∃l ∈ L, v ⊆ l × 2 V(X) , 2. ∀q ∈ Q, ∃!v ∈ V s , q ∈ v, 3. E s = E a s ∪ E δ s , 4. ∀v ∈ V s , ∀a ∈ Σ, ∃!v ∈ V s , (∀q ∈ v, ∀q ∈ Q, q a -→ q =⇒ q ∈ v ), and E a s = {(v, a, v ) ∈ V s × Σ × V s | ∃(q, q ) ∈ v × v , q a -→ q }, 5. ∀(v, v ) ∈ V 2 s , ∀(q, q ) ∈ v × v , ∀δ ∈ R ≥0 , q δ -→ q =⇒ (∀q ∈ v, ∃δ ∈ R ≥0 , ∃q ∈ v , q δ -→ q ), 6. ∀v ∈ V s , up(v) = v =⇒ ∃!v ∈ V s , v = v ∧ ∀(q, q ) ∈ v × v , ∃δ ∈ R ≥0 , q = q after δ ∧ ∀δ ≤ δ, q after δ ∈ v ∪ v , and E δ s = {(v, t, v ) ∈ V s × {t} × V s | v = v ∧ ∀(q, q ) ∈ v × v , ∃δ ∈ R ≥0 , q = q after δ ∧ ∀δ ≤ δ, q after δ ∈ v ∪ v }.
Constraint [START_REF]∀σ ∈ tw(Σ), ∀t ∈ R ≥0 , E ϕ (σ, t) dΣ c obs(σ, t)[END_REF] imposes that all the states of the semantics that are in a node of the symbolic graph share the same location. This allows us to easily dene accepting nodes (as nodes whose locations are accepting). Constraint (2) allows us to match each state of the semantics with a unique node in the symbolic graph. Constraint (3) splits the set of edges between edges corresponding to actions and edges corresponding to delays. Each of these sets has its own constraints, described in (4) and (6).

Constraint (4) propagates the reachability and determinism of the timed automaton to the symbolic graph for actions, and denes the set E a s of edges corresponding to actions. The edges in E a s are labelled with the corresponding action from Σ.

Constraint (5) states that if a state of the semantics leads to another with a delay, and they are not in the same node, then all states in the rst node can reach a state in the second node with a delay.

Constraint (6) requires that each node of the graph has at most one direct time successor, with which it is linked by an edge in the set E δ s of edges corresponding to delays. The edges in E δ s are labelled with the special action t, which is supposed not to belong to Σ.

The graph dened in [ACH

+ 92] is a graph that is compatible with Büchi games, as per Denition 5. This graph is the one that has been used as symbolic graph in the implementation of GREP (see Section 4).

Example 4. Consider again property ϕ t (Fig. 3). The corresponding symbolic compatible graph of ϕ t as edges with empty diamond heads ( ) represent transitions with controllable events. Purple edges with vee heads ( ) represent the elapse of time.

Thus, in Fig. 4, orange edges correspond to transitions labelled by Write, since it is the only controllable event. Red edges can represent transitions of any other event, LockOn, LockO , or Auth. Edges are not duplicated, meaning that two events with the same controllability that label the same transition will appear as a unique edge in the graph. For example, from node (l0, ), events LockO and LockOn lead to (l3, ), but only one red edge is drawn.

From this symbolic graph, we dene another graph, as in [START_REF] Renard | Runtime enforcement using Büchi games[END_REF], on which we play a Büchi game.

This graph is called game graph.

The Game Graph

This part describes how to construct the graph on which a Büchi game is played. Let us consider G s = (V s , E s ), a symbolic graph compatible with Büchi games. We use Σ n c and a compatible symbolic graph G s to dene a game graph G, the nite graph on which to play the Büchi game:

Denition 6 (Game graph). A graph G = V, E is a game graph if: • V = V s × Σ n c × {0, 1}, • E = 6 i=1 E i , with E 1 = {( v, w, 0 , v, w, 1 ) ∈ V 2 }, E 2 = {( v, c.w, 0 , v after c, w, 0 ) ∈ V 2 | c ∈ Σ c }, E 3 = {( v, w, 1 , v after u, w, 0 ) ∈ V 2 | u ∈ Σ u }, E 4 = {( v, w, 1 , v, w.c, 0 ) ∈ V 2 | c ∈ Σ c ∧ w.c ∈ Σ n c }, E 5 = {( v, w, 1 , v , w, 0 ) ∈ V 2 | (v, t, v ) ∈ E δ s }, E 6 = {( v, w, 1 , v, w, 0 ) ∈ V 2 | up(v) = v},
As per Denition 6, a node in a game graph G is composed of a node of a symbolic graph G s , a buer, and a player it belongs to. The two players are the enforcement mechanism P 0 , whose associated number is 0, and the environment P 1 , whose associated number is 1. The set of edges is partitioned into six sets, each representing a dierent type of action. E 1 contains the edges corresponding to P 0 letting P 1 play; edges in E 2 represent P 0 emitting the rst event of its buer; E 3 and E 4 contain edges corresponding to receiving an uncontrollable or controllable event, respectively, both of which being actions of P 1 . Edges in E 5 represent time elapse: it changes the node of the symbolic graph to its time successor if it has one. E 6 contains edges that allow us to consider nite inputs. Since plays are innite, such edges are needed to allow the environment to receive nothing (it can be seen as adding an empty event to the input). Since time elapses when no event is received, these edges exist only from nodes that have no time successor, i.e. nodes that are stable by elapse of time.

On this graph, we play a Büchi game with the set of Büchi nodes being dened as:

B = { (l, Z), w, 0 ∈ V | l ∈ F }
We can now consider W 0 the set of winning nodes of this game for player P 0 .

Example 5. Consider again property ϕ t (Fig. 3) whose symbolic graph was represented in Fig. 4. The game graph associated with ϕ t is given in Fig. 5. In this graph, the initial node is the square node, the Büchi nodes are the double-circled nodes, and the winning nodes (the nodes in W 0 ) are the rounded rectangular ones. The two rst members represent a node of the corresponding compatible symbolic graph G s (see Fig. 4), and the third member is a prex of the buer of the EM, where w stands for the Write event, which is the only controllable event. As in the untimed setting, edges are represented dierently according to the set they belong to:

• blue edges, with empty triangular heads ( ) belong to E 1 (the EM skips its turn), • green edges, with lled triangular heads ( ) belong to E 2 (the EM emits the rst event of its buer),

• orange edges, with empty diamond heads ( ) belong to E 4 (a controllable event is received), • red edges, with lled diamond heads ( ) belong to E 3 (an uncontrollable event is received) or E 6

(no more event is to be received),

• purple edges, with vee heads ( ) belong to E 5 (elapse of time).

For example in Fig. 5, let us consider that the node (l 1 , {x < 2}, -, 1) has been reached. This node belongs to P 1 , meaning that the environment is now playing. To leave this node, there are four cases:

• receiving the uncontrollable event LockOn (red edge), which leads to the node (l 2 , T, -, 0) corresponding to the location l 2 of the TA.

• receiving the uncontrollable events LockO or Auth (red edge), which leads to node (l 1 , { x < 2}, -, 0).

• receiving the controllable event Write (orange edge), which leads to node (l 1 , {x < 2}, w, 0), meaning that the event Write has been added to the buer. • letting time elapse (purple edge), which leads to node (l 1 , {x ≥ 2}, -, 0), thus updating the symbolic state.

In these four situations, the Environment (P 1 ) gives back the turn to the EM (P 0 ). From this game graph, knowing the winning set W 0 for P 0 allows to compute the safe states of an EM.

The Enforcement Function

Now, we can nally dene safe emitting function Safe, and use it to dene function E ϕ , through function store ϕ . Then, we show that E ϕ is an enforcement function that is sound, compliant and optimal.

We use W 0 , the set of winning nodes of this game for player P 0 , to dene, for q ∈ Q and w ∈ Σ * c , safe emitting function Safe(q, w), computing the set of words that can be output by an EM from state q with buer w, ensuring compliance and soundness. We also dene the notion of maximal safe word κ ϕ (q, w) that will be used for dening store ϕ .

Safe emitting function (Safe) For q ∈ Q, and w ∈ Σ * c , the safe emitting function Safe is dened by:

Safe(q, w) = {σ ∈ tw(Σ) | Π Σ (σ) w ∧ q after σ ∈ F G ∧ ∀t ∈ R ≥0 , ∀v ∈ V s , (q after (σ, t) ∈ v) =⇒ v, maxbuffer(Π Σ (obs(σ, t)) -1 • w), 1 ∈ W 0 },
maxbuffer(w) = max ({w w | w ∈ Σ n c }).
Maximal safe word (κ ϕ ) For q ∈ Q, and w ∈ Σ * c , the maximal safe word κ ϕ is dened by:

κ ϕ (q, w) = min lex (max ({ } ∪ t ∈T(q,w) {w + t t | w ∈ Safe(q after ( , t ), w)}))
where:

T(q, w) = {t ∈ R ≥0 | ∀t < t , Safe(q after ( , t ), w) = ∅},
Now that the safe emitting function and the maximal safe word have been dened, they can be used to dene function E ϕ . For this purpose, an intermediate function (store ϕ ) is necessary:

Denition 7 (E ϕ ). Let store ϕ : tw(Σ) → tw(Σ) × Σ * c be the function dened inductively by: store ϕ ( ) = , ,

and for σ ∈ tw(Σ), (δ, a) ∈ R ≥0 × Σ, if t = time(σ • (δ, a)), (σ ∞ , σ c ) = store ϕ (σ), and σ s = obs(σ ∞ , t), then store ϕ (σ • (δ, a)) = σ s • (t -time(σ s ), a) • σ s , σ c if a ∈ Σ u σ s • σ s , σ c if a ∈ Σ c where, buf c = Π Σ (nobs(σ ∞ , t)) • σ c ,
and

σ s = κ ϕ (Reach(σ s • (t -time(σ s ), a)), buf c ) σ c = Π Σ (σ s ) -1 • buf c , σ s = κ ϕ (Reach(σ s , t), buf c • a) + t (t -time(σ s )) σ c = Π Σ (σ s ) -1 • (buf c • a).
We then dene function E ϕ as follows: For σ ∈ tw(Σ) and t ∈ R ≥0 , E ϕ (σ, t) = obs(Π 1 (store ϕ (obs(σ, t))), t).

Function store ϕ takes a timed word σ as input, and outputs two words: σ ∞ and σ c . σ ∞ is a timed word corresponding to the output of the EM at innite time, i.e. the events already emitted followed by the controllable events expected to be released according to the fact that no other event occurs meanwhile. σ c is an untimed word representing the controllable events stored in order not to break the property. Note that contrary to [PFJ + 14] when an event is in σ ∞ , there is no guarantee that it will be emitted. Indeed, if an uncontrollable event occurs meanwhile, the latter has to be emitted immediately, and the state of the TA is updated. At this moment, it is necessary to check again if the events in σ ∞ may be emitted without violating the property. store ϕ is dened in an inductive way, distinguishing the occurrence of an uncontrollable event and a controllable one. In both cases, it is necessary to compute the best correct sequence using the safe emitting function Safe. In the denition of Safe(q, w), the last condition requires that all nodes of the game graph G that are reached by a word in Safe(q, w) from q belong to W 0 . This is a strong condition, that is required to ensure that it is always possible to compute a word leading to an accepting state. Nevertheless, if the source node is not in W 0 , it is possible that letting time elapse leads to a node in W 0 , because it disabled some transition in the timed automaton. This explains why we dened the set T(q, w), that allows us to consider words as potential outputs of the EM if it becomes sound (i.e. can ensure that the property will be satised) before the emission of the rst event of this word, even if it is not at the time when the last event was received. Intuitively, T(q, w) contains all the delays t such that an EM must wait at least t time units to be able to be sound. In other words, the EM can not ensure that the property will eventually always be satised from state q with buer w, and it can not ensure it either by waiting less than t time units, for every t in T(q, w). Then, κ ϕ (q, w) is the word that is to be output by the EM from state q with buer w provided that the input does not change. It is the maximal word (with respect to d ) that belongs to Safe(q, w). If Safe(q, w) is empty, then κ ϕ (q, w) is the maximal word that belongs to Safe(q after ( , t), w), where t is the minimal time for which Safe(q after ( , t), w) is not empty. If Safe(q after ( , t), w) is empty for every Table 1. Table showing the evolution of σ ∞ and σ c in store ϕ and the output of the EM for the input

σ = ((1, Auth) • (1, LockOn) • (2, Write) • (1, LockO ) • (1, LockOn) • (1, Write) • (1, LockO )). t Output of the EM at time t σ∞ σc 1 (1, Auth) (1, Auth) 2 (1, Auth) • (1, LockOn) (1, Auth) • (1, LockOn) 4 (1, Auth) • (1, LockOn) (1, Auth) • (1, LockOn) Write 5 (1, Auth) • (1, LockOn) • (3, LockO ) (1, Auth) • (1, LockOn) • (3, LockO ) • (2, Write) 6 (1, Auth) • (1, LockOn) • (3, LockO ) • (1, LockOn) (1, Auth) • (1, LockOn) • (3, LockO ) • (1, LockOn) Write 7 (1, Auth) • (1, LockOn) • (3, LockO ) • (1, LockOn) (1, Auth) • (1, LockOn) • (3, LockO ) • (1, LockOn) Write • Write 8 (1, Auth) • (1, LockOn) • (3, LockO ) • (1, LockOn) • (2, LockO ) (1, Auth) • (1, LockOn) • (3, LockO ) • (1, LockOn) • (2, LockO ) • (2, Write) • (0, Write) 10 (1, Auth) • (1, LockOn) • (3, LockO ) • (1, LockOn) • (2, LockO ) • (2, Write) • (0, Write) (1, Auth) • (1, LockOn) • (3, LockO ) • (1, LockOn) • (2, LockO ) • (2, Write) • (0, Write)
t ∈ R ≥0 , then κ ϕ (q, w) = , meaning that the EM does not output anything. Thus, when the enforcement function is not sound, it outputs nothing but uncontrollable events.

Example 6. We can follow in Table 1 the output of function E ϕ and the values of σ ∞ and σ c over time

with input word σ = (1, Auth) • (1, LockOn) • (2, Write) • (1, LockO ) • (1, LockOn) • (1, Write) • (1, LockO ).
As depicted before, at time t = 4 the controllable event Write occurs but can not be emitted. It is stored in σ c . At t = 5, the occurrence of the uncontrollable event LockO leads the TA into location l 1 and permits to consider Write to be released. Then (3, LockO) • (2, Write) is added at the end of σ ∞ , which means that LockO should be emitted immediately, followed by the emission of Write expected 2 time units after. The occurrence at t = 6 of LockOn leads the TA to l 2 . Emitting Write is not possible anymore, thus the latter is stored again in σ c , and so on. To understand the behaviour of store ϕ , note that in the associated game graph, shown in Fig. 5, l 1 , Z, w, p ∈ W 0 and l 2 , Z, w, p ∈ W 0 , for any l 1 , Z, w, p ∈ V and l 2 , Z, w, p ∈ V .

As mentioned previously, an EM may not be sound from the beginning of an execution, but some uncontrollable events may lead to a state from which it becomes possible to be sound. In Denition 7, function E ϕ is sound whenever T(q, w) is empty, with q the state reached by the output of E ϕ at date t and w its buer at this date. If T(q, w) is empty, then the last value of σ s (or σ s depending on the controllability of the last input action) is in Safe(q, w), meaning that the node in the game graph G reached by the EM is in W 0 , therefore it is always possible to compute a word that leads to a state in F G . This leads us to the denition of the stabilised set of inputs Pre(ϕ), which is the time-extension-closed set of inputs in which function E ϕ is sound (i.e. the S set from the denition of soundness, see Denition 2):

Denition 8 (Stabilised set of inputs (Pre(ϕ))). Considering a property ϕ to enforce, the stabilised set of inputs Pre(ϕ) is dened by:

Pre(ϕ) = {(σ, t) | σ ∈ Pre(ϕ, t)},
where, for σ ∈ tw(Σ) and t ∈ R ≥0 :

Pre(ϕ, t) = {σ ∈ tw(Σ) | ∃t ≤ t, Safe(Reach(σ |Σu , t ), Π Σ (obs(σ, t ) |Σc )) = ∅} • tw(Σ)
Note that Pre(ϕ) is time-extension-closed, meaning that once E ϕ is sound, its output will always eventually satisfy ϕ in the future. Considering that the output of function E ϕ was only containing uncontrollable events so far, if Safe(Reach(σ |Σu , t), Π Σ (obs(σ, t) |Σc )) is not empty, this means that function E ϕ becomes sound with input σ from time t, since there is a word that is safe to emit. Thus, Pre(ϕ, t) is the set of inputs for which E ϕ is sound after date t, and then E ϕ is sound for any input in Pre(ϕ) after its associated date.

Properties of function E ϕ

We list the dierent propositions stating that E ϕ fulls all the requirements of enforcement functions: it is an enforcement function, which is sound with respect to ϕ in Pre(ϕ), compliant with respect to Σ u and Σ c , and optimal in Pre(ϕ). Proofs can be found in appendix A.

Proposition 1. E ϕ as per Denition 7 is an enforcement function, as per Denition 1. Proposition 2. E ϕ is sound with respect to ϕ in Pre(ϕ) as per Denition 2. Proposition 3. E ϕ is compliant, as per Denition 3.

Proposition 4. E ϕ is optimal in Pre(ϕ) as per Denition 4.

Enforcement Monitors

In this part, we give an operational description of an EM whose output is exactly the output of E ϕ , using a transition system obeying to a set of rules. Denition 9. An enforcement monitor

E for ϕ is a transition system C E , c E 0 , Γ E , → E such that: • C E = tw(Σ) × Σ * c × Q × R ≥0 is the set of congurations. • c E 0 = , , q 0 , 0 ∈ C E is the initial conguration. • Γ E = ((R ≥0 × Σ) ∪ { }) × Op × ((R ≥0 × Σ) ∪ { })
is the alphabet, composed of an optional input, an operation and an optional output.

The set of operations is {dump(.), pass-uncont(.), store-cont(.), delay(.)}. Whenever (σ, , σ ) ∈ Γ E , it will be noted σ/ /σ .

• → E is the transition relation dened as the smallest relation obtained by applying the following rules given by their priority order: Dump: (δ, a) • σ b , σ c , q, δ / dump((δ,a))/(δ,a)

-------------→ E σ b , σ c , q , 0 , with q = q after a, Pass-uncont: σ b , σ c , q, δ u/ pass-uncont(u)/(δ,u) ---------------→ E σ b , σ c , q , 0 , with q = q after u,

σ b = κ ϕ (q , Π Σ (σ b )• σ c ), and σ c = Π Σ (σ b ) -1 • (Π Σ (σ b ) • σ c ), Store-cont: σ b , σ c , q, δ c/ store-cont(c)/ -----------→ E σ b , σ c , q, δ , with σ b = κ ϕ (q, Π Σ (σ b ) • σ c • c) + t δ and σ c = Π Σ (σ b ) -1 • (Π Σ (σ b ) • σ c • c), Delay: σ b , σ c , (l, v), δ / delay(δ )/ --------→ E σ b , σ c , (l, v + δ ), δ + δ .
In a conguration (σ b , σ c , q, δ), σ b is the word of controllable events waiting to be emitted (at innite time), which corresponds to σ ∞ of store ϕ , but without the events already emitted. σ c is the word of controllable events stored to avoid to break the property (similar to σ c in store ϕ ), q is the current state in the TA of the property, and δ is the time elapsed since the emission of the last event. For each rule, the elements composing a conguration are updated. In the notation σ/ /σ , σ and σ can be seen as an input/output snapshot of the EM. σ corresponds to the occurrence of an event as input of the EM, and refers to the rst event of the green input sequence in Fig. 6. Similarly, σ corresponds to the EM releasing an event, and refers to the last event of the red output sequence in Fig. 6 Example 7. An example of execution of an enforcement monitor as per Denition 9 enforcing property ϕ t (see Fig. 3) is given in Fig. 6. We use the following notation: in each line, the input is on the right, the output on the left, and the middle is the current conguration of the enforcement monitor. Variable t denes the global time of the execution. The input used for the monitor in Fig. 6 is the same as in Table 1:

(1, Auth)•(1, LockOn)•(2, Write)•(1, LockO )•(1, LockOn)•(1, Write)•(1, LockO ). In
) • (1, LockOn) • (2, Write) • (1, LockO ) • (1, LockOn) • (1, Write) • (1, LockO )
monitor and green text depicts the remaining input word at this date. The nal output is the same as the one of the enforcement function E ϕ as per Denition 7: (1, Auth)

• (1, on) • (2, o ) • (1, on) • (2, o ) • (2, w) • (0, w).
Proposition 5. The output o of E as per Denition 9 for input σ at date t is such that o = E ϕ (σ, t).

The output of the enforcement monitor is the concatenation of the outputs of the word labelling the path followed by the enforcement monitor when reading σ. A formal denition is given in the proof of this proposition, in appendix A.

Remark 1. For a conguration of the enforcement monitor c = σ b , σ c , q, δ , we can associate a node of the game graph (Π 1 (q), Z, w, 0), such that Π 2 (q) ∈ Z, and w is the longest prex of the buer of the enforcement monitor, i.e. Π Σ (σ b ) • σ c , such that (Π 1 (q), Z, w, 0) is a node of the game graph. Then, if (σ, t) ∈ Pre(ϕ), and c is the conguration reached by the enforcement monitor with input σ at date t, then (Π 1 (q), Z, w, 0) is a winning node for player P 0 .

GREP: Games for Runtime Enforcement of Properties

In this section, we present GREP (Games for Runtime Enforcement of Properties), a tool for RE of timed properties with uncontrollable events. GREP implements the RE framework described in Section 3. It is a tool of about 6,000 lines of code 2 developed using the C language. GREP is open-source, and is available at https://github.com/matthieurenard/GREP. Installation instructions are available in the INSTALL le in the repository. However, installing GREP can be tedious, due to some dependencies, thus we also provide a virtual machine (VM) with a pre-compiled version of GREP. This VM also contains all the tools required to run benchmarks and generate plots like the ones given in this section (see Section 4.4). For more information about how to get the VM and run the tool, see https://github.com/matthieurenard/testGREP.

In this section, we rst recall general aspects of the approach used in GREP, then we present implementation details of the dierent modules composing it. Then we detail the possible options available, and nally we evaluate the performance and compare the results with another tool called TiPEX.

Description of the approach

The strategy of GREP is the one described in Section 3. Given a timed regular property ϕ, and a partition of its alphabet into a set of controllable events Σ c and a set of uncontrollable events Σ u , GREP rst builds a symbolic graph that is compatible with Büchi games, as per Denition 5. The graph used is the one described in [ACH + 92]. Then, GREP builds a game graph as per Denition 6, using Σ c as the set of controllable events and Σ u as the set of uncontrollable events. Once the game graph is constructed, GREP computes the set W 0 of winning nodes for player P 0 (the EM).

GREP can follow a real execution on the game graph, by watching the node that has been reached so far by its output, and the nodes that can be reached by emitting stored controllable actions (i.e. following the corresponding edges in the game graph). Whenever a winning node is reached by P 0 , the strategy is to emit as many events as possible, remaining in a winning node all the time. Since the game played is a Büchi game, it is always possible for P 0 to stay in a winning node whenever one is reached. Whenever a winning node is reached, the output of the EM is then guaranteed to satisfy the property.

General Functioning of GREP

GREP is essentially composed of two modules (cf Fig. 7): the Symbolic Computing Module (SCM) and the Enforcement Monitor Module (EMM). It loads a TA le describing the desired property, and reads the inputs directly from stdin. The output of the EM is sent to stdout. This approach allows one to use GREP with o-the-shelf applications.

Symbolic Computing Module (SCM)

The Symbolic Computing Module is composed of three main components: a TA loader, the Zone Graph Generator, and the Game Graph Generator.

TA Loader

The TA loader is the component that parses a le containing the description of a timed automaton and loads it into a C structure. The le of the automaton is a textual description following a grammar designed for this purpose.

The le is parsed using a custom grammar, implemented using lex and yacc. The automaton must also be deterministic and complete (see [START_REF] Alur | The theory of timed automata[END_REF]). If the automaton is not deterministic, the behaviour is undened.

Once the timed automaton is loaded, a symbolic graph is computed by the Zone Graph Generator to abstract its innite semantics into a nite graph that is compatible with Büchi games, as per Denition 5. The graph that is built is actually the one described in [ In GREP, zones are represented by Dierence Bound Matrices (DBMs), using the UPPAAL DBM library (UDBM, see [START_REF] Udbm | Uppaal DBM Library[END_REF]), and its C API. The algorithm requires some functionality not provided by this API (some of them exist in some higher-level wrappers), such as complementing zones into a list of zones. This functionality was added to our own wrapper of UDBM. No other third-party library was needed to compute the symbolic graph. This symbolic graph is used to build the nal game graph, that will be used by the enforcement monitor.

Game Graph Generator

Using the symbolic graph, the Game Graph Generator builds a graph over which to play a Büchi game whose strategy is the one to be followed by the enforcement monitor. The graph is constructed as described in Denition 6. Once the graph is constructed, the Büchi game is solved for player P 0 (the enforcement monitor), with the set of Büchi nodes being the set of nodes whose location is accepting. The winning nodes are then the nodes from which the enforcement monitor ensures that its output will satisfy the property.

Following a path of winning nodes in the graph gives a strategy to follow such that the nal output satises the property. This is how the EM uses the graph to actually enforce the property.

Enforcement Monitor Module (EMM)

The EMM uses the SCM to compute the output for a given input. It has ve main public functions: init(G), getStrat(), delay(δ), eventRcvd(e), and emit(). Function init(G) initialises the EMM following the strategy from graph G. Function getStrat() gives the strategy to follow, i.e. whether the rst action of the buer should be output or not. Since time is abstracted by the zone graph for the SCM, it needs to be notied that some time has passed, which is done by the use of function delay(δ), where δ is the number of time units that have elapsed since the last call to delay(), or the creation of the EM for the rst call. Time units only need to be consistent with the ones used in the property. Function eventRcvd(e) is used to inform the EMM that an event e has been read from the input. In this case, the EMM acts dierently depending on the controllability of the event. Function emit() is used to output the rst action of the buer. Uncontrollable events are output by function eventRcvd(), as required by compliance.

Note that these functions allow to use the EMM in both online (on the y) and oine (with a trace as input) settings. All these functions, except function getStrat(), return the number of time units required to reach the time successor of the current node (∞ if there is no time successor). It is the number of time units given to function delay() if no event is received before and the strategy is not to emit. Algorithms for these functions are given in algorithms 1 to 5.

The EM is represented by a tuple containing the game graph, the current conguration, i.e. location, valuation and buer, thus it is initialised by init(G), given in algorithm 1.

input : A game graph G, that has all information about its related TA output: An enforcement mechanism, represented by a tuple containing the graph, and the initial state, i.e. initial location, with all clocks evaluating to 0 and an empty buer 1 Function Init(G) 2 return (G, l 0 , ν 0 , ); Algorithm 1: Function Init(G)

The three functions delay(), eventRcvd(), and emit() are used to modify the EM. They implement the rules of the enforcement monitor described in Denition 9: function delay() corresponds to the rule Delay, function eventRcvd() corresponds to rules Pass and Store, depending on the controllability of the event received, and function emit() corresponds to rule Dump. These functions are described in algorithms 2 to 4.

In the algorithms, only the actions are emitted, with no delays, because we considered that the enforcement mechanism was used in online mode, thus delays are not output, since they are computed from the real instant at which the event is written by function writeOutput(). These algorithms can easily be adapted to be used in oine mode, by adding a delay to the enforcement mechanism, that is increased by function delay(), and used as the delay of the actions that are written by function writeOutput() before being reset.

input : The EM = (G, q, w) as returned by function Init or another function described here, and a delay δ output: The state of the EM after delay δ, and the delay needed to reach the next zone (∞ if there is not any)

1 Function delay((G = (V, E), q, w), δ)

2 delayToNextZone ← min({δ ∈ R ≥0 | q after (δ + δ ) ∈ v, with v ∈ V such that
q after δ ∈ v} ∪ {∞}) ; 3 return (G, q, w), delayToNextZone ;

Algorithm 2: Function delay(EM, δ)

input : The EM = (G, q, w), and the event e that is received output: The EM after having received the event e, and the delay to the time successor of the new zone, as in algorithm 2. If the event is uncontrollable, it is output (written) by function writeOutput 1 Function eventRcvd((G = (V, E), q, w), e) The other primitive of our enforcement mechanism is function getStrat() that indicates whether the rst event of the buer should be emitted or not. This is the function in which the game graph, and the set input : The EM = (G, q, w) output: The EM after having emitted the rst event e of w, and the delay to the time successor of the new zone. Again, e is written with function writeOutput 1 Function emit((G = (V, E), q, w = e • w ))

2 if e is controllable then 3 EM ← (G, q, w • e) ; 4 delayToNextZone ← min({δ ∈ R ≥0 | q after δ ∈ v, with v ∈ V such that q ∈ v} ∪ {∞}) ; 5 else /* e is uncontrollable */ 6 EM ← (G, q after e, w) ; 7 delayToNextZone ← min({δ ∈ R ≥0 | q after e after δ ∈ v with v ∈ V such that q ∈ v} ∪ {∞}) ;
2 delayToNextZone ← min({δ ∈ R ≥0 | q after w(1) after δ ∈ v, with v ∈ V such that q after w(1) ∈ v} ∪ {∞}) ; 3 writeOutput((w(1)) ; 4 return (G, q after w(1), w [2..] ), delayToNextZone ;

Algorithm 4: Function emit(EM)

of winning nodes W 0 are used to determine the strategy to follow. Algorithm 5 describes this function. In algorithm 5, a path in W 0 is a path in G whose nodes belong to W 0 . Moreover, we use (q, w, 0) as a node to simplify, but its existence is not guaranteed in V . Normally, we should consider instead (q, maxbuffer(w), 0) and search paths by simulating the reception of the remaining events of w that are not in maxbuffer(w) as soon as possible. Note that computing this condition requires to explore all the possible executions in order to compute the maximal number of green edges.

input : The EM = (G, q, w) output: EMIT if the strategy is to emit the rst event of the buer, DONTEMIT otherwise 1 Function getStrat((G, q, w))

2
if there is a path in W 0 from (q, w, 0) with maximal number of green edges (those in E 2 ) that starts with nodes (q, w, 0) • (q after w(1), w Then, the general algorithm to use the EMM in the oine setting is given in algorithm 6. Basically, the EMM builds an EM with function Init(G), and then uses the primitive previously dened to produce a compliant output that is sound whenever possible. In algorithm 6, the EM is updated whenever a change of the zone happens (condition del ≤ δ, line 5), or an event is received (lines 12 and 13). The rst event of the buer of the EM is output if the strategy indicates so (i.e. getStrat() returns EMIT). Once all the events of the input have been read (line 14), the remaining events of the buer can be emitted with good delays (line 15 to line 22).

Note that computing an output such that all actions are emitted whenever it is possible to emit them does not require to explore the strategy tree. Depending on the property, the two outputs could be the same. It is the case if the property is such that letting time elapse never enables a transition that eventually allows the EMM to output more events. Then the EMM can work faster by using an optimisation that does not compute any tree, but outputs actions whenever possible, i.e. when the successor node by emitting is winning, if it is specied to do so.

To visualise the dierence between the two computations, consider the property described in Fig. 3. For this property, considering for instance that the input word is (0, Write) • (1, Write), the output of GREP when exploring the execution tree would be (using delays): (4, Write) • (4, Write), whereas using the other algorithm, that emits events as soon as possible, the output would be (2, Write). The rst one outputs more events, but the second one outputs the Write event before.

To produce the second output, function getStrat() can be reimplemented as per algorithm 7.

Running GREP

GREP is shipped with two executables: one to use EM in oine mode, and the other in the online mode. Both of them take their input on the standard input. In the oine mode, the input is composed of events in the input : The game graph G, the input sequence of events, through function read () output: The output of the EM, written through functions emit and eventRcvd 1 EM ← Init(G); 2 del ← ∞; form (t, a), where t is a date and a is an action, controllable or uncontrollable. In the online mode, only the action is given, the date is computed from the real time through a call to gettimeofday(). Note that these executables may be built only on UNIX-like systems because of some system calls such as gettimeofday() and clock_gettime(). Excepting this, the tool is not system-dependent. The output (events with their dates) is printed on the standard output.

GREP provides a fast mode (-f), where actions are output whenever they can be instead of outputting the longest word possible with minimal dates. This option corresponds to using function getStratFast() presented in algorithm 7 instead of function getStrat() described in algorithm 5, which is used by default. Using option -f is usually faster, but the outputs might dier depending on the property.

Let us show an example of command for GREP:

game_enf_offline -a phit.tmtn -l log -d gameGraph.pdf < input will enforce the property described in the le phit.tmtn, logging in the le log, reading its events from the le input. It will also draw the game graph in the le gameGraph.pdf.

The EM logs the mode in which it runs (default or fast) at the beginning, and when it stops, it logs the input, its output, the controllable actions that have not been output (what remains in its buer), and a verdict For example, considering property ϕ t , the previous command with the input le containing the sequence

(0, Write) • (1, Auth) • (2, Write) • (3, LockOn) • (4, Write) • (5, LockO) (6, LockOn) • (7, LockO), produces the output (1, Auth) • (2, Write) • (2, Write) • (3, LockOn) • (5, LockO) • (6, LockOn) (7, LockO) • (9, Write).

Performance Evaluation

Comparison with TiPEX

The performance of GREP has been evaluated on three properties that come along with TiPEX, the tool to which we compare. TiPEX (see [START_REF] Pinisetty | TiPEX: A Tool Chain for Timed Property Enforcement During eXecution[END_REF]) is, to our knowledge, the only other tool that acts as an EM for timed regular properties. The three properties are described in Fig. 8. The safety property states that after the rst r action, there should be at least 5 time units between any two subsequent r actions. Moreover, a actions are not constrained. The co-safety property states that the rst r action should be followed by a g action, with a delay of at least 6 time units, and no intervening r action. After this prescribed sequence, g and r actions can happen freely. The response property states that every g action should be followed by a r action within 15 to 20 time units, without any g action occurring between them, and no r action should occur before its corresponding g action.

For each of these properties, GREP has been run 100 times on every input among 100 inputs of 1000 events randomly generated. The time between the reception of two events has been saved for all of these Figures 9 and 10 are obtained as follows: each input is iterated several times (100 for GREP, less for TiPEX 4 ), and the computation times (in nanoseconds) of the tool between the reads of two consecutive events of the input are stored. Then, the median time is computed for each of these times between all the iterations. We then plot the logarithm (in base 10) of these times against the reads of the events. We use a logarithmic scale because many values are low, and they would be merged in a line when using a linear scale. The results for GREP with option -f are given only for the safety property because they are similar to the results without the option for the two other properties. We can see that GREP is faster than TiPEX by several orders of magnitude. GREP outputs many events in less than 10 µs (4 on the scale of the graphs), whereas TiPEX takes at least 1 ms (6 on the scale of the graph) to output them. For the safety property, we can see that for some inputs, GREP takes an increasing amount of time to compute the strategy. This is due to the exploration of the strategy tree, which grows with the number of stored controllable actions. Using the optimised setting (-f) allows GREP to compute its output faster, as shown in Fig. 9b. The last vertical line has also many high values, because it represents the time to emit all the remaining actions after the last event from the input was read. For the co-safety and response properties, the time GREP takes between . Timings of GREP and TiPEX on the response and co-safety properties. The x axis corresponds to the events of the input (from 1 to 1000), and the y axis corresponds to the logarithm of the timings (in nanoseconds) between the reads of the events. two events is less variable than for the safety property, mainly because the strategy of GREP is simpler: it consists in either emitting everything for the co-safety property (once state s 3 is reached) or emitting nothing for the response property, if the rst stored controllable is an r while in state s 1 . TiPEX, on the other hand, takes a linearly-increasing amount of time to emit some events. Thus GREP performs globally better than TiPEX on these properties. Besides, another advantage of GREP over TiPEX is its ability to handle uncontrollable events. To our knowledge, no other RE tool has this functionality. However, using uncontrollable events can lower the performance of GREP, as discussed in Section 4.4.2.

Performance Evaluation with Uncontrollable Events

In this section, we show the limits of GREP when using uncontrollable events, with a property that is voluntarily designed to be hard to be enforced by GREP, at least in its default mode. Consider property ϕ u described in Fig. 11, with u an uncontrollable event and c a controllable one. This property has two locations, s 1 and s 2 that are symmetrical: both of them require that a certain delay (15 time units for s 1 and 10 time units for s 2 ) has elapsed since the last event to emit a c event. As in Section 4.4.1, GREP has been tested for this property, using 100 random inputs of 1000 events. The results are presented in Fig. 12. As in Section 4.4.1, the x-axis of the plots represents the events of the inputs, from 1 to 1000, and the y-axis is the logarithm of the timings, in nanoseconds, between the reads of two consecutive events. The timings have been plotted with (Fig. 12b) and without (Fig. 12a) option -f. Considering Fig. 12a, one can notice four apparent dierent behaviours: for some inputs, the timings between events is constant, and can be low, i.e. of about one microsecond, or a little bit higher, i.e. of about 10 microseconds; for some other inputs the timings are increasing, up to about 10 microseconds, or up to about 10 milliseconds for the last events. This dierence between runs can be explained by the randomness of the events of the inputs. This benchmark has been made to show the limitation of GREP, thus the delays between events have been taken randomly between 0 and 3, meaning that events are received faster than it is possible to output controllable events (remember that c events must have a delay greater than 10 time units). Thus, depending on the proportion of uncontrollable events, that are emitted immediately, the buer of stored controllable events grows as events are read. Property ϕ u has been specically designed to increase the number of stored controllable events.

Thus, in the worst case, the computation time of GREP increases with the size of its buer. For some properties such as ϕ u , receiving events with small delays (compared to guards) increases the size of the buer, meaning that the computational overhead introduced by GREP could become too high for a use in online mode.

However, considering Fig. 12b, we can see that GREP performs better with option -f. Note that for ϕ u , the outputs are the same with or without option -f. In the worst case, where GREP used 10 milliseconds without option -f, it only requires about 100 microseconds with option -f. In both cases, the timings increase with the size of the buer, but option -f reduces the growth of the timings, and may allow using GREP in online mode where it is not possible without option -f. This dierence between the use of option -f and not using it can be explained by the fact that with option -f, GREP does not explore all the possible executions to output the longest word possible, but only decides if it is possible to emit a limited number of events.

Discussion

Limitations of GREP are theoretical and practical. Because of uncontrollable events, some properties may not be enforceable. The framework considers innite buers, but in practice, such a situation would inevitably lead to the saturation of the buer. Adding bounds to the buer in the theoretical framework is currently under investigation. Even in case of enforceable property, we have identied situations where the size of the buer would inevitably grow. It is the case when the EM receives events with small delays compared to the required staying time in a state of the property (as shown in Fig. 12). In this case, the overhead may be too important to use the EM online. It depends on the inputs which are usually unpredictable. Another obstacle is hardware : such things are more likely to be used in embedded environments, which can have small computational power/memory. GREP is a proof of concept tool. Despite these limitations, it ts pretty well in practice on usual properties.

Related Work

A rst RE approach has been proposed by Schneider et al. in [START_REF] Schneider | Enforceable security policies[END_REF]. They propose an EM synthesising security automata permitting to enforce safety properties described with Büchi automata. The EM watches the executions step by step and terminates whenever the property is going to be violated. Later, Bloem et al. present in [START_REF] Bloem | Shield synthesis: Runtime enforcement for reactive systems[END_REF] a framework to synthesise an enforcement mechanism (named shield) from safety automata by solving a 2-player game. A shield acts instantaneously and cannot buer actions. It is k-stabilising: whenever a property violation is unavoidable, the shield allows to deviate from the property for k consecutive steps (as in [START_REF] Charafeddine | Runtime enforcement for componentbased systems[END_REF]). Whenever a second violation occurs within k steps, then the shield enters into a fail-safe mode, where it ensures only correctness. A similar approach has been proposed by Wu et al. in [START_REF] Wu | Synthesizing runtime enforcer of safety properties under burst error[END_REF], adding the ability to handle burst errors.

In [START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF], Ligatti et al. synthesise edit automata from nite-state automata. They add in their framework the ability to insert or suppress events from the execution of the system, and use a memory to store the sux of an invalid execution until it becomes valid again. Thus it permits to enforce a bigger set of properties than safety ones, and more precisely the set of renewal properties. Falcone et al. present in [FMFR11] a framework to enforce response properties from the Safety-Progress classication ([MP90, CMP92]). These properties are similar to the innite renewal properties of [START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF]. In [START_REF] Dolzhenko | Modeling runtime enforcement with mandatory results automata[END_REF], the authors model enforcement mechanisms as Mandatory Results Automata (MRA). MRAs extend edit automata by rening the input/output relationship of an EM and thus allowing a more precise description of the enforcement abilities.

All these previously mentioned approaches deal only with untimed properties. The rst RE framework considering timed properties has been proposed by Pinisetty et al. in [PFJ + 13]. In this approach, the EM acts as a delaying lter on the input sequence of timed events in order to provide a correct output sequence according to the property modelled as a timed automaton ( [START_REF] Alur | The theory of timed automata[END_REF]). The framework of [PFJ + 13] is able to enforce safety and co-safety properties, and has been generalised in [PFJ + 14] for any regular timed property described by a timed automaton. Variants of this work have been proposed ( [START_REF] Falcone | Runtime enforcement of regular timed properties by suppressing and delaying events[END_REF] for suppressing events, [START_REF] Pinisetty | Runtime enforcement of parametric timed properties with practical applications[END_REF] for parametric properties), and a tool has been developed [START_REF] Pinisetty | TiPEX: A Tool Chain for Timed Property Enforcement During eXecution[END_REF].

To our knowledge, very little work has been done on RE with uncontrollable events. Basin et al. extend in [START_REF] Basin | Algorithms for monitoring real-time properties[END_REF] the approach of Schneider et al. [START_REF] Schneider | Enforceable security policies[END_REF]), permitting to enforce safety properties where some of the events in the specication are uncontrollable. This work has been generalised in [START_REF] Basin | Enforceable security policies revisited[END_REF], presenting enforcement of security policies with controllable and uncontrollable events. As in [Sch00], the system stops the execution in case of violation of the property. Basin et al. propose to adapt their framework for timed properties. In this case, time constraints are represented with special uncontrollable tick events. In our approach, we consider dense time using the expressiveness power of timed automata, any regular property, and our EM are more exible since they block the system only when delaying events cannot prevent from violating the property, thus oering the possibility to correct more violations.

In previous work, we introduced runtime enforcement for timed properties described by timed automata, with uncontrollable events ([RFR + 17]). We have adapted the usual notions of soundness, transparency (changed to compliance) and optimality in this new context, and provided an approach to synthesise a sound, compliant and optimal EM. A rst attempt of using games in the generation process has been proposed in [START_REF] Renard | Runtime enforcement using Büchi games[END_REF]. This framework considers only untimed properties. A tool permitting to enforce timed properties with uncontrollable events and using game theory has been implemented and presented in [START_REF] Renard | Grep: Games for the runtime enforcement of properties[END_REF].

Conclusion and Future Work

Conclusion This paper presents a complete RE framework for timed properties with uncontrollable events.

It describes the theoretical framework based on a Büchi game approach, and presents GREP, the corresponding implemented tool. GREP builds a two-player game graph representing the possible actions of the EM and the system under scrutiny (that acts as the environment). Each vertex of the graph belongs to one of these two players, and each edge represents a possible action of the player owning the source vertex.

GREP then solves a Büchi game by computing a set of nodes of the graph from which there exists a winning strategy. Using this approach allows to avoid the exploration of the whole execution tree at runtime. This paper provides benchmarks and compares the results with a state of the art tool TiPEX. They show that GREP provides better computing times in case of properties without uncontrollable events, since TiPEX does not handle uncontrollable events. To our knowledge, there exists no tool for enforcing timed properties with uncontrollable events.

Future work

We propose several ways for future works. The proposed approach considers RE in an abstracted way. Even if GREP is build in a way permitting to plug it directly on a system using stdin and stdout ows, we did not consider practical aspects. In some real situations, instrumentation considerations may be investigated in order to plug GREP. Moreover, our EM is allowed only to delay events. Adding richer primitives, such as suppressing events for instance, could increase the enforcing power of the mechanism, and may be adapted to dierent situations. Besides, this framework considers only timed regular properties described by timed automata. One could build EM for properties with dierent formalism, such as TLTL properties for instance. Finally, in this work we focus on EM for single systems. Extending this for distributed systems is a challenging task. For instance, it may be necessary to use several EMs, implying communication (problems) between them. The enforcing ability of the EM according to distributed properties also appears to be a challenging open question.

A. Proofs Proposition 1. E ϕ as per Denition 7 is an enforcement function, as per Denition 1.

Proof. We have to prove the two following properties:

1. ∀σ ∈ tw(Σ), ∀t ∈ R ≥0 , ∀t ≥ t, E ϕ (σ, t) E ϕ (σ, t ) 2. ∀σ ∈ tw(Σ), ∀δ ∈ R ≥0 , ∀a ∈ Σ, E ϕ (σ, time(σ • (δ, a))) E ϕ (σ • (δ, a), time(σ • (δ, a))) For σ ∈ tw(Σ), let P(σ) be the predicate ∀t ∈ R ≥0 , ∀t ≥ t, ∀(δ, a) ∈ R ≥0 × Σ, E ϕ (σ, t) E ϕ (σ, t ) ∧ E ϕ (σ, time(σ • (δ, a))) E ϕ (σ • (δ, a), time(σ • (δ, a))) ( (σ, t), o 1 ∈ E ϕ ∧ (σ, t ), o 2 ∈ E ϕ ∧ (σ, time(σ • (δ, a))), o 3 ∈ E ϕ ∧ (σ • (δ, a), time(σ • (δ, a))), o 4 ∈ E ϕ ) =⇒ (o 1 o 2 ∧ o 3 o 4 ).
Let us show by induction that P(σ) holds for any σ ∈ tw(Σ):

Induction basis: for σ = , let us consider t ∈ R ≥0 and t ≥ t. Then, E ϕ ( , t) = = E ϕ ( , t ) E ϕ ( , t ).

Moreover, for (δ, a) ∈ R ≥0 × Σ, E ϕ (σ, δ) = E ϕ ((δ, a), δ) Thus, P( ) holds.

Induction step: suppose that P(σ) holds for some σ ∈ tw(Σ). Then, let us consider (δ, a) ∈ R ≥0 × Σ, t ∈ R ≥0 , and t ≥ t. We rst prove that the rst condition holds. Let us consider (σ, t), o

1 ∈ E ϕ , (σ, t ), o 2 ∈ E ϕ , (σ•(δ, a), t), o 1 ∈ E ϕ , and (σ•(δ, a), t ), o 2 ∈ E ϕ . We have to prove that E ϕ (σ•(δ, a), t) E ϕ (σ•(δ, a), t ).
Three cases are possible:

1. t ≤ t < time(σ • (δ, a)).
Then obs(σ • (δ, a), t ) = obs(σ, t ), and obs(σ • (δ, a), t) = obs(σ, t). Let us consider σ s1 , σ c = store ϕ (obs(σ, t)) and σ s2 , σ c = store ϕ (obs(σ, t )). Then, considering the denition of E ϕ Since time(σ

(Denition 7), E ϕ (σ, t) = obs(σ s1 , t) = E ϕ (σ • (δ, a), t), and E ϕ (σ, t ) = obs(σ s2 , t ) = E ϕ (σ • (δ, a), t ) (since obs(σ, t) = obs(σ • (δ, a), t) and obs(σ, t ) = obs(σ • (δ, a), t )). Following the induction hypothesis, P(σ) holds, meaning that E ϕ (σ, t) E ϕ (σ, t ). This means that E ϕ (σ • (δ, a), t) E ϕ (σ • (δ, a), t ).
• (δ, a)) ≤ t , this means that E ϕ (σ • (δ, a), time(σ • (δ, a))) E ϕ (σ • (δ, a), t ). Thus E ϕ (σ • (δ, a), t) E ϕ (σ • (δ, a), t ). 3. time(σ • (δ, a)) ≤ t ≤ t . Then, obs(σ • (δ, a), t) = obs(σ • (δ, a), t ) = σ • (δ, a). Thus, if σ s0 , σ c = store ϕ (σ • (δ, a)), then E ϕ (σ • (δ, a), t) = obs(σ s0 , t) and E ϕ (σ • (δ, a), t ) = obs(σ s0 , t ). Since t ≤ t , this means that E ϕ (σ • (δ, a), t) E ϕ (σ • (δ, a), t ).
Thus, in all cases, the rst required condition holds (i.e. E ϕ (σ

• (δ, a), t) E ϕ (σ • (δ, a), t )). Let us now consider (δ , a ) ∈ R ≥0 × Σ. We have to show that E ϕ (σ • (δ, a), time(σ • (δ, a) • (δ , a ))) E ϕ (σ • (δ, a) • (δ , a ), time(σ • (δ, a) • (δ , a ))). Since obs(σ • (δ, a), time(σ • (δ, a) • (δ , a ))) = σ • (δ, a) and obs(σ • (δ, a) • (δ , a ), time(σ • (δ, a) • (δ , a ))) = σ • (δ, a) • (δ , a ), if σ s3 , σ c = store ϕ (σ • (δ, a)) and σ s4 , σ c = store ϕ (σ • (δ, a) • (δ , a )), then E ϕ (σ • (δ, a), time(σ • (δ, a) • (δ , a ))) = obs(σ s3 , time(σ • (δ, a) • (δ , a ))) and E ϕ (σ • (δ, a) • (δ , a ), time(σ • (δ, a) • (δ , a ))) = obs(σ s4 , time(σ • (δ, a) • (δ , a ))). Following the denition of store ϕ (Denition 7), it is clear that E ϕ (σ • (δ, a), time(σ • (δ, a) • (δ , a ))) σ s4 . Thus, since time(E ϕ (σ • (δ, a), time(σ • (δ, a) • (δ , a )))) ≤ time(σ • (δ, a) • (δ , a )), E ϕ (σ • (δ, a), time(σ • (δ, a) • (δ , a ))) E ϕ (σ • (δ, a) • (δ , a ), time(σ • (δ, a) • (δ , a ))).
This means that P(σ • (δ, a)) holds. Thus, for any σ ∈ tw(Σ) and (δ, a) ∈ R ≥0 × Σ, P(σ) =⇒ P(σ • (δ, a)).

Thus, by induction on σ, P(σ) holds for any σ ∈ tw(Σ). Thus E ϕ is an enforcement function.

Lemma 1. ∀σ ∈ tw(Σ), ∀t ≥ time(σ), (σ ∈ Pre(ϕ, t) ∧ σ s0 , σ c = store ϕ (σ)) =⇒ (obs(σ s0 , t) = σ |Σu ∧ Π Σ (nobs(σ s0 , t)) • σ c = Π Σ (σ |Σc )).
Proof. For σ ∈ tw(Σ) and t ≥ time(σ), let P(σ, t) be the predicate

(σ ∈ Pre(ϕ, t)∧ σ s0 , σ c = store ϕ (σ)) =⇒ (obs(σ s0 , t) = σ |Σu ∧ Π Σ (nobs(σ s0 , t)) • σ c = Π Σ (σ |Σc ))
, and P(σ) be the predicate ∀t ≥ time(σ), P(σ, t).

Let us then prove by induction on σ that P(σ) holds for any σ ∈ tw(Σ).

Induction basis: for σ = , let us consider t ∈ R ≥0 . Then, store ϕ ( ) = , . Since obs( , t) = |Σu , and

Π Σ (nobs( |Σc , t)) • = Π Σ ( |Σc )
, it follows that P( , t) holds, and thus P( ) holds.

Induction step: let us suppose that for σ ∈ tw(Σ), P(σ) holds. Let us consider (δ, a) ∈ R ≥0 ×Σ, σ s0 , σ c = store ϕ (σ), σ t0 , σ d = store ϕ (σ • (δ, a)), and σ s = obs(σ s0 , time(σ

• (δ, a))). Let us also consider t ≥ time(σ • (δ, a)). If σ • (δ, a) ∈ Pre(ϕ, t), then P(σ • (δ, a), t) trivially holds.
Let us consider that σ • (δ, a) ∈ Pre(ϕ, t).

• If a ∈ Σ u , then σ t0 = σ s • (time(σ • (δ, a)) -time(σ s ), a) • σ s for some σ s ∈ tw(Σ). Since σ • (δ, a) ∈ Pre(ϕ, t),
this means that for any t ≤ t, Safe(Reach((σ

• (δ, a)) |Σu , t ), Π Σ (obs(σ • (δ, a), t )) |Σc ) = ∅. This means that for any t ≤ t-time(σ•(δ, a)), t ∈ T(Reach((σ•(δ, a)) |Σu ), Π Σ (σ•(δ, a)) |Σc ). Now, by induction hypothesis, since σ ∈ Pre(ϕ, time(σ • (δ, a))) (otherwise σ • (δ, a) would be in Pre(ϕ, t)), σ |Σu = σ s , and Π Σ (nobs(σ s0 , time(σ •(δ, a)))) |Σc •σ c = Π Σ (σ) |Σc . Thus, for any t ≤ t-time(σ •(δ, a)), t ∈ T(Reach(σ s •(time(σ •(δ, a))- time(σ s ), a)), Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c ). Thus, obs(σ s , t -time(σ • (δ, a))) = . It follows that obs(σ t0 , t) = σ s • (time(σ • (δ, a)) -time(σ s ), a) • obs(σ s , t -time(σ • (δ, a))) = σ s • (time(σ • (δ, a)) -time(σ s ), a) = (σ • (δ, a)) |Σu and Π Σ (nobs(σ t0 , t)) • σ d = σ s • σ d = Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c = Π Σ (σ) |Σc = Π Σ ((σ • (δ, a)) |Σc ). Thus P(σ • (δ, a), t) holds.
• Otherwise, a ∈ Σ c , and there exists σ s such that

σ t0 = σ s • σ s . Since σ • (δ, a) ∈ Pre(ϕ, t), for any t ≤ t, Safe(Reach((σ • (δ, a)) |Σu , t ), Π Σ (obs(σ • (δ, a), t )) |Σc ) = ∅. Thus, for any t ≤ t -time((σ • (δ, a)) |Σu ), t ∈ T(Reach((σ •(δ, a)) |Σu ), Π Σ ((σ •(δ, a)) |Σc )). Now, by induction hypothesis, considering that (σ •(δ, a)) |Σu = σ |Σu and (σ • (δ, a)) |Σc = σ |Σc • (time(σ • (δ, a)) -time(σ |Σc ), a), and since σ ∈ Pre(ϕ, time(σ • (δ, a))), for any t ≤ t -time(σ • (δ, a)), t ∈ T(Reach(σ s , time(σ • (δ, a))), Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c • a). Thus, obs(σ s -t (time(σ • (δ, a)) -time(σ s )), t -time(σ • (δ, a))) = . Thus, obs(σ s , t -time(σ • (δ, a)) + time(σ • (δ, a)) -time(σ s )) -t (t -time(σ • (δ, a)
)) = , meaning that obs(σ s , ttime(σ s )) = . Thus, obs(σ t0 , t) = σ s • obs(σ s , ttime(σ s )) = σ s = σ |Σu , and Π Σ (nobs(σ t0 , t))

• σ d = Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c • a = Π Σ (σ |Σc ) • a = Π Σ ((σ • (δ, a)) |Σc ).
Thus P(σ • (δ, a), t) holds.

In both cases, P(σ • (δ, a), t) holds. Thus, it holds for any t ≥ time(σ • (δ, a)), meaning that P(σ • (δ, a)) holds. This means that for any σ ∈ tw(Σ) and (δ, a) ∈ R ≥0 × Σ, P(σ) =⇒ P(σ • (δ, a)).

Thus, we have shown by induction on σ that P(σ) holds for any σ ∈ tw(Σ).

Lemma 2. ∀q ∈ Q, ∀w ∈ Σ * c , ∀σ ∈ tw(Σ), ∀t ∈ R ≥0 , σ ∈ Safe(q, w) =⇒ nobs(σ, t) -t (t -time(obs(σ, t))) ∈ Safe(q after (σ, t), Π Σ (obs(σ, t)) -1 • w).
Proof. Let us consider q, w and σ such that σ ∈ Safe(q, w), and t ∈ R ≥0 . Following the denition of Safe, this means that the three following properties hold:

1. Π Σ (σ) w, 2. q after σ ∈ F G , 3. ∀t ∈ R ≥0 , ∀v ∈ V s , q after (σ, t) ∈ v =⇒ v, maxbuffer(Π Σ (obs(σ, t)) -1 • w), 1 ∈ W 0 .
Now, considering σ = nobs(σ, t)t (ttime(obs(σ, t))), σ satises the following properties:

1. Π Σ (σ ) = Π Σ (nobs(σ, t) -t (t -time(obs(σ, t)))) = Π Σ (nobs(σ, t)), thus, Π Σ (obs(σ, t)) • Π Σ (σ ) = Π Σ (obs(σ, t)) • Π Σ (nobs(σ, t)) = Π Σ (σ).
Since Π Σ (σ) w, this means that: Π Σ (σ ) Π Σ (obs(σ, t)) -1 • w.

2. (q after (σ, t)) after σ = (q after (σ, t)) after (nobs(σ, t)t (ttime(obs(σ, t)))) = q after σ. Thus, (q after (σ, t)) after σ ∈ F G . 3. For t ∈ R ≥0 , (q after (σ, t)) after (σ , t ) = (q after (σ, t)) after (nobs(σ, t)t (ttime(obs(σ, t))), t ) = q after (σ, t + t ).

Since t+t ∈ R ≥0 , then if v ∈ V s is such that (q after (σ, t)) after (σ , t ) ∈ v, then v, maxbuffer(Π Σ (obs(σ, t+ t )) -1 • w), 1 ∈ W 0 . Moreover, since t ≥ time(obs(σ, t)), Π Σ (obs(σ, t + t )) -1 • w = Π Σ (obs(σ , t )) -1 • (Π Σ (obs(σ, t)) -1 • w). Thus, v, maxbuffer(Π Σ (obs(σ , t )) -1 • (Π Σ (obs(σ, t)) -1 • w)), 1 ∈ W 0 .
This means that σ = nobs(σ, t)t (ttime(obs(σ, t))) ∈ Safe(q after (σ, t), Π Σ (obs(σ, t)) -1 • w).

Proposition 2. E ϕ is sound with respect to ϕ in Pre(ϕ) as per Denition 2.

Proof. Notation from Denition 7 is to be used in this proof: for σ ∈ tw(Σ), if σ s0 , σ c = store ϕ (σ), (δ, a) ∈ R ≥0 × Σ, t = time(σ • (δ, a)), and σ s = obs(σ s0 , t), then,

buf c = Π Σ (nobs(σ ∞ , t)) • σ c , and σ s = κ ϕ (Reach(σ s • (t -time(σ s ), a)), buf c ) σ c = Π Σ (σ s ) -1 • buf c , σ s = κ ϕ (Reach(σ s , t), buf c • a) + t (t -time(σ s )) σ c = Π Σ (σ s ) -1 • (buf c • a).
We have to prove that for any (σ, t) ∈ Pre(ϕ), there exists t ≥ t such that for any t ≥ t , E ϕ (σ, t ) |= ϕ.

For σ ∈ tw(Σ), and t ≥ time(σ), let P(σ, t) be the predicate ((σ, t) ∈ Pre(ϕ) ∧ σ s , σ c = store ϕ (σ)) =⇒ (σ s |= ϕ ∧ nobs(σ s , t)t (ttime(obs(σ s , t))) ∈ Safe(Reach(σ s , t), Π Σ (nobs(σ s , t)) • σ c )). Let also P(σ) be the predicate: ∀t ≥ time(σ), P(σ, t). Let us show by induction that for any σ ∈ tw(Σ), P(σ) holds.

Induction basis: for σ = , let us consider t ∈ R ≥0 .

• If ∈ Pre(ϕ, t), then, P( ) trivially holds.

• Otherwise, ∈ Pre(ϕ, t). Then, following the denition of Pre( , t) (Denition 8), there exists t ≤ t such that Safe(Reach( |Σu , t ), ) = ∅, meaning that Safe(Reach( , t ), ) = ∅. Thus, following the denition of Safe(Reach( , t ), ), ∈ Safe(Reach( , t ), ), and Reach( ) ∈ F G , thus |= ϕ. Since store ϕ ( ) = , and |= ϕ, P( , t) holds.

Thus, in both cases, P( , t) holds, meaning that P( ) holds.

Induction step: suppose that for σ ∈ tw(Σ), P(σ) holds. Let us consider (δ, a) ∈ R ≥0 ×Σ, t ≥ time(σ•(δ, a)), σ s0 , σ c = store ϕ (σ), σ s = obs(σ s0 , time(σ • (δ, a))), σ t0 , σ d = store ϕ (σ • (δ, a)), and σ t = obs(σ t0 , t).

We have to prove that (σ

• (δ, a), t) ∈ Pre(ϕ) =⇒ σ t |= ϕ ∧ nobs(σ t , t) -t (t -time(obs(σ t , t))) ∈ Safe(Reach(σ t , t), Π Σ (nobs(σ t , t)) • σ d ). • If σ • (δ,
nobs(σ t0 , t) = obs(σ t0 , t) -1 • σ t0 = obs(σ s • (δ , a) • σ s , t) -1 • σ t0 Since t ≥ time(σ • (δ, a)) = time(σ s • (δ , a)), nobs(σ t0 , t) = (σ s • (δ , a) • obs(σ s , t -time(σ s • (δ , a)))) -1 • σ t0 = obs(σ s , t -time(σ • (δ, a))) -1 • ((σ s • (δ , a)) -1 • (σ s • (δ , a) • σ s )) = obs(σ s , t -time(σ • (δ, a))) -1 • σ s = nobs(σ s , t -time(σ • (δ, a)))
We know that σ st t ∈ Safe(Reach(σ s •(δ , a), t ), buf c ), thus following lemma 2, since t ≥ t , t-t ≥ 0, and nobs(σ st t , tt )t (tttime(obs(σ st t , tt ))) ∈ Safe(Reach(σ s • (δ , a), t ) after (σ st t , tt ),

Π Σ (obs(σ s -t t , t -t )) -1 • buf c ) (2)
Now, note that for any σ ∈ tw(Σ), t ∈ R ≥0 and t ∈ R ≥0 , nobs(σt t, t ) = nobs(σ, t + t )t t if delay(σ(1)) > t + t nobs(σ, t + t ) otherwise The reason is that the operatort aects only the rst delay of the word, thus if this delay is in obs(σt t, t ), i.e. delay(σ(1)) ≥ t + t , the remaining events are not changed by thet operator. Thus, if delay(σ s (1)

) > t -t + t = t -t + t -time(σ • (δ, a)) = t -time(σ • (δ, a)), then nobs(σ s -t t , t -t ) = nobs(σ s , t -t + t ) -t t = nobs(σ s , t -time(σ • (δ, a))) -t t Moreover, since delay(σ s (1)) > t -time(σ • (δ, a)), obs(σ s -t t , t -t ) = , and obs(σ t0 , t) = σ s • (δ, a), thus: nobs(σ s -t t , t -t ) -t (t -t -time(obs(σ s -t t , t -t ))) = (nobs(σ s , t -time(σ • (δ, a))) -t t ) -t (t -t ) = nobs(σ t0 , t) -t (t -t + t ) = nobs(σ t0 , t) -t (t -time(σ • (δ, a))) = nobs(σ t0 , t) -t (t -time(obs(σ t0 , t)))
On the other hand, if delay(σ s (1)) ≤ ttime(σ • (δ, a)), then nobs(σ st t , tt ) = nobs(σ s , ttime(σ • (δ, a))) Moreover, since delay(σ s (1)) ≤ t-time(σ•(δ, a)), obs(σ s -t t , t-t ) = obs(σ s , t-time(σ•(δ, a)))-t t , thus nobs(σ st t , tt )t (tttime(obs(σ st t , tt )))

= nobs(σ s , ttime(σ • (δ, a)))

-t (t -t -time(obs(σ s , t -time(σ • (δ, a))) -t t )) = nobs(σ t0 , t) -t (t -t + t -time(obs(σ s , t -time(σ • (δ, a))))) = nobs(σ t0 , t) -t (t -time(σ • (δ, a))- time(obs(σ s , t -time(σ • (δ, a))))) = nobs(σ t0 , t) -t (t -time(σ • (δ, a)- (time(obs(σ t0 , t)) -time(σ • (δ, a))))) = nobs(σ t0 , t) -t (t -time(obs(σ t0 , t)))
Thus, in both cases, (2) becomes:

nobs(σ t0 , t) -t (t -time(obs(σ t0 , t))) ∈ Safe(Reach(σ s • (δ , a), t ) after (σ s -t t , t -t ), Π Σ (obs(σ s -t t , t -t )) -1 • buf c ) Now, since t ≥ time(σ • (δ, a)), Reach(σ s •(δ , a), t ) after (σ s -t t , t -t ) = Reach(σ s • (δ , a)) after ( , t -time(σ s • (δ , a))) after (σ s -t t , t -t ) = Reach(σ s • (δ , a)) after ((σ s -t t ) + t t , t -t + t ) = Reach(σ s • (δ , a)) after (σ s , t -time(σ • (δ, a))) = Reach(σ s • (δ , a) • σ s , t) = Reach(σ t0 , t) and Π Σ (nobs(σ t0 , t)) • σ d = Π Σ (nobs(σ s , t -time(σ • (δ, a)))) • (Π Σ (σ s ) -1 • buf c ) = Π Σ (obs(σ s , t -time(σ • (δ, a))) -1 • σ s )• (Π Σ (σ s ) -1 • buf c ) = Π Σ (obs(σ s , t -time(σ • (δ, a)))) -1 • Π Σ (σ s )• (Π Σ (σ s ) -1 • buf c ) = Π Σ (obs(σ s , t -time(σ • (δ, a)))) -1 • buf c
On the other hand,

Π Σ (obs(σ s -t t , t -t )) -1 • buf c = Π Σ (obs(σ s , t -time(σ • (δ, a))) -t t ) -1 • buf c = Π Σ (obs(σ s , t -time(σ • (δ, a)))) -1 • buf c Thus, Π Σ (nobs(σ t0 , t)) • σ d = Π Σ (obs(σ s -t t , t -t )) -1 • buf c .
Considering all this, (2) becomes:

nobs(σ t0 , t) -t (t -time(obs(σ t0 , t))) ∈ Safe(Reach(σ t0 , t), Π Σ (nobs(σ t0 , t)) • σ d ) Otherwise, a ∈ Σ c . Then, (σ • (δ, a)) |Σu = σ |Σu = σ s , and Π Σ ((σ • (δ, a)) |Σc ) = Π Σ (σ |Σc ) • a = Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c • a.
nobs(σ t0 , t) = obs(σ t0 , t) -1 • σ t0 = obs(σ s • σ s , t) -1 • σ t0 Since time(σ s ) ≤ t, it follows that nobs(σ t0 , t) = (σ s • obs(σ s , t -time(σ s ))) -1 • (σ s • σ s ) = obs(σ s , t -time(σ s )) -1 • (σ -1 s • (σ s • σ s )) = obs(σ s , t -time(σ s )) -1 • σ s = nobs(σ s , t -time(σ s ))
We know that σ st t ∈ Safe(Reach(σ s , t ), buf c • a) and that t ≥ t meaning that tt ≥ 0. Thus, following lemma 2:

nobs(σ s -t t , t -t ) -t (t -t -time(obs(σ s -t t , t -t ))) ∈ Safe(Reach(σ s , t ) after (σ s -t t , t -t ), Π Σ (obs(σ s -t t , t -t )) -1 • (buf c • a))
If delay(σ s (1)) > ttime(σ s ) (i.e. delay((σ st t )(1)) > tt ), then: nobs(σ st t , tt ) = nobs(σ s , tt + t )t t = nobs(σ s , ttime(σ s ))t t and obs(σ st t , tt ) = and obs(σ t0 , t) = σ s . Thus, nobs(σ st t , tt )t (tttime(obs(σ st t , tt ))) = (nobs(σ s , ttime(σ s ))t t )t (tt ) = nobs(σ s , ttime(σ s ))t (tt + t ) = nobs(σ t0 , t)t (ttime(σ s )) = nobs(σ t0 , t)t (ttime(obs(σ t0 , t)))

Otherwise, delay(σ s (1)) ≤ t -time(σ s ), and then nobs(σ s -t t , t -t ) = nobs(σ s , t -time(σ s )), thus: nobs(σ st t , tt )t (tttime(obs(σ st t , tt ))) = nobs(σ s , ttime(σ s ))t (tttime(obs(σ s , ttime(σ s ))

-t t )) = nobs(σ t0 , t)-t (t -t -(time(obs(σ s , t -time(σ s ))) -t )) = nobs(σ t0 , t)-t (t -t + t -(time(obs(σ t0 , t)) -time(σ s ))) = nobs(σ t0 , t)-t (t -time(σ s ) -time(obs(σ t0 , t)) + time(σ s )) = nobs(σ t0 , t) -t (t -time(obs(σ t0 , t)))
Π Σ (obs(σ s -t t , t -t )) -1 • (buf c • a) = Π Σ (obs(σ s , t -time(σ s )) -t t ) -1 • (buf c • a) = Π Σ (obs(σ s , t -time(σ s ))) -1 • (buf c • a)
Moreover, since Since this holds for any t ∈ R ≥0 , in particular, if t = time(σ t0 ), this means that ∈ Safe(Reach(σ t0 ), σ d ),

Π Σ (nobs(σ t0 , t)) • σ d = Π Σ (obs(σ t0 , t) -1 • σ t0 ) • σ d = (Π Σ (obs(σ t0 , t)) -1 • Π Σ (σ t0 )) • σ d = Π Σ (obs(σ s • σ s , t)) -1 • (Π Σ (σ t0 ) • σ d ) = Π Σ (σ s • obs(σ s , t -time(σ s ))) -1 • (Π Σ (σ t0 ) • σ d ) = (Π Σ (σ s ) • Π Σ (obs(σ s , t -time(σ s )))) -1 • (Π Σ (σ s • σ s ) • σ d ) = Π Σ (obs(σ s , t -time(σ s ))) -1 • (Π Σ (σ s ) -1 • (Π Σ (σ s ) • Π Σ (σ s ) • σ d )) = Π Σ (obs(σ s , t -time(σ s ))) -1 • (Π Σ (σ s ) • σ d ) = Π Σ (obs(σ s , t -time(σ s ))) -1 • (Π Σ (σ s ) • (Π Σ (σ s ) -1 • (buf c • a))) = Π Σ (obs(σ s , t -time(σ s ))) -1 • (buf c • a) it follows that Π Σ (obs(σ s -t t , t -t )) -1 • (buf c • a) = Π Σ (nobs(σ t0 , t)) • σ d ,
meaning that Reach(σ t0 ) after = Reach(σ t0 ) ∈ F G . This means that σ t0 |= ϕ.

Thus, if σ • (δ, a) ∈ Pre(ϕ, t) ∧ σ ∈ Pre(ϕ, time(σ • (δ, a))), P(σ) =⇒ P(σ • (δ, a), t). • Otherwise, σ • (δ, a) ∈ Pre(ϕ, t) and σ ∈ Pre(ϕ, time(σ • (δ, a))). Then, by induction hypothesis: nobs(σ s0 , time(σ • (δ, a)))-t (time(σ • (δ, a)) -time(obs(σ s0 , time(σ • (δ, a))))) ∈ Safe(Reach(σ s0 , time(σ • (δ, a))), Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c ) If a ∈ Σ u , since Safe(Reach(σ s0 , time(σ • (δ, a))), Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c ) = ∅,
following the denition of Safe, it means that there exists σ ∈ tw(Σ c ) such that the three following properties hold:

1. Π Σ (σ ) Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c , 2. Reach(σ s0 , time(σ • (δ, a))) after σ ∈ F × R ≥0 , 3. for any t ∈ R ≥0 , if v ∈ V s is such that Reach(σ s0 , time(σ•(δ, a))) ∈ v, then v, maxbuffer(Π Σ (obs(σ , t )) -1 • buf c ), 1 ∈ W 0 .
In particular, for item 3, with t = 0, we get v, maxbuffer(buf c ), 1 ∈ W 0 , with Reach(σ s0 , time(σ • (δ, a))) ∈ v. Thus, following the edge ( v, maxbuffer(buf c ), 1 , v after a, maxbuffer(buf c ), 0 ) ∈ E 3 , since W 0 is the winning region for player 0, it follows that v after a, maxbuffer(buf c ), 0 ∈ W 0 . Thus, there exists a winning strategy for player 0 from node v, maxbuffer(buf c ), 0 , meaning that there exists a play π such that the set of nodes visited innitely often by π, noted inf(π), is such that inf(π) ∩ F G × Σ n c × {0, 1} = ∅, and π(1) = v, maxbuffer(buf c ), 0 . Moreover, we can choose π such that no edge from E 3 or E 4 (corresponding to receiving uncontrollable or controllable events, respectively) is taken when playing π. This is possible since W 0 is the winning region for player 0, thus it is winning for all the strategies of player 1, and the edges of E 3 and E 4 leave a node belonging to player 1. Now, since the only cycles in the graph without the edges of E 3 and E 4 are cycles of the form v, w, 0 v, w, 1 v, w, 0 , with ( v, w, 0 , v, w, 1 ) ∈ E1 and ( v, w, 1 , v, w, 0 ) ∈ E6, it follows that π ends with such a cycle repeated indenitely, i.e. π = π 0 • ( v e , w e , 0 • v e , w e , 1 ) ω for some nite π 0 . Thus, inf(π) = { v e , w e , 0 , v e , w e , 1 }, meaning that v e ⊆ F G . This allows us to associate a word σ to π. To build it, we rst build a sequence in Q × R ≥0 × tw(Σ c ) by induction as follows:

(q 0 , δ 0 , w 0 ) = (Reach(σ s , time(σ • (δ, a))) after (0, a), 0, ) and, for i ∈ N,

(q i+1 , δ i+1 , w i+1 ) =              (q i , δ i , w i ) if (π(i), π(i + 1)) ∈ E 1 ∪ E 6 (q i after (δ i , c), 0, w i • (δ i , c)) if (π(i), π(i + 1)) ∈ E 2 , with π(i) = v, c • w, 0 for some (c, w) ∈ Σ c × Σ * c (q i , δ i + δ, w i ) if (π(i), π(i + 1)) ∈ E 5 , with δ = min({δ ∈ R ≥0 | q i after ( , δ i + δ ) ∈ Π 1 (π(i + 1))})
Now since π = π 0 • ( v e , w e , 0 • v e , w e , 1 ) ω , there exists n ∈ N such that for any n ≥ n, (π(n ), π(n + 1)) ∈ E 1 ∪ E 6 , meaning that (q n , δ n , w n ) = (q n , δ n , w n ). Thus, the sequence stabilises. Let us consider σ = w n , where w n is the third component of the previous sequence when it is stabilised. Then, σ satises:

1. Π Σ (σ ) maxbuffer(buf c ), because there is no edge (π(i), π(i + 1)) belonging to E 3 or E 4 , and Π 2 (π(1)) = maxbuffer(buf c ).

2. Reach(σ s0 , time(σ • (δ, a))) after (0, a) after σ ∈ F G , because it belongs to v e ⊆ F G (v e is such that π = π 0 • ( v e , w e , 0 • v e , w e , 1 ) ω ).

For any

t ∈ R ≥0 , if v ∈ V s is such that Reach(σ s0 , time(σ • (δ, a))) after (0, a) after (σ , t ) ∈ v, then v, Π Σ (nobs(σ , t )) -1 • buf c , 1 ∈ W 0 ,
because π is winning for player 0. By construction of σ , and because of the dierent constraints required on G s , this implies that all states v ∈ V s such that Reach(σ s0 , time(σ • (δ, a))) after (0, a) after (σ , t ) ∈ v are in W 0 , for any t ∈ R ≥0 . We know by construction of σ that this holds for some t , when an edge belonging to E 5 can be followed. The constraint item (6) required on V s (see Denition 5) ensures that this is thus true for all t .

Thus,

σ ∈ Safe(Reach(σ s0 , time(σ • (δ, a))) after (0, a), buf c ), so Safe(Reach(σ s • (time(σ • (δ, a)) -time(σ s ), a)), buf c ) = ∅. Thus, 0 ∈ T(Reach(σ s • (time(σ • (δ, a)) - time(σ s ), a)), buf c ), meaning that σ s ∈ Safe(Reach(σ s • (time(σ • (δ, a)) -time(σ s ), a)), buf c ). Let us consider t = time(σ • (δ, a)). Now, following lemma 2, since t ≥ t , t -t ≥ 0, then: nobs(σ s , t -t ) -t (t -t -time(obs(σ s , t -t ))) ∈ Safe(Reach(σ s • (t -time(σ s ), a)) after (σ s , t -t ), Π Σ (obs(σ s , t -t )) -1 • buf c ) Since t ≥ t = time(σ • (δ, a)), nobs(σ t0 , t) = nobs(σ s • (t -time(σ s ), a) • σ s , t) = nobs(σ s , t -time(σ s • (t -time(σ s ), a))) = nobs(σ s , t -time(σ • (δ, a)))
= nobs(σ s , tt ) and obs(σ t0 , t) = σ s • (ttime(σ s ), a) • (obs(σ s , tt )). Thus, time(obs(σ t0 , t)) = time(σ s • (ttime(σ s ), a)) + time(obs(σ s , tt )) = t + time(obs(σ s , tt )).

This means that:

nobs(σ s , t -t ) -t (t -t -time(obs(σ s , t -t ))) = nobs(σ t0 , t) -t (t -t -(time(obs(σ t0 , t) -t ))) = nobs(σ t0 , t) -t (t -time(obs(σ t0 , t))) Thus, nobs(σ t0 , t) -t (t -time(obs(σ t0 , t))) ∈ Safe(Reach(σ s • (t -time(σ s ), a)) after (σ s , t -t ), Π Σ (obs(σ s , t -t )) -1 • buf c ) Since Reach(σ s • (t -time(σ s ), a)) after (σ s , t -t ) = Reach(σ s • (t -time(σ s , a)) • σ s , t -t + time(σ s • (t -time(σ s ), a))) = Reach(σ t0 , t -t + time(σ • (δ, a))) = Reach(σ t0 , t) and Π Σ ( nobs(σ t0 , t)) • σ d = Π Σ (obs(σ t0 , t) -1 • σ t0 ) • σ d = (Π Σ (obs(σ t0 , t)) -1 • Π Σ (σ t0 )) • σ d = Π Σ (obs(σ s • (t -time(σ s ), a) • σ s , t)) -1 • (Π Σ (σ s • (t -time(σ s ), a) • σ s ) • σ d ) = (Π Σ (σ s • (t -time(σ s ), a)) • Π Σ (obs(σ s , t -t ))) -1 • (Π Σ (σ s • (t -time(σ s ), a)) • Π Σ (σ s ) • σ d ) = Π Σ (obs(σ s , t -t )) -1 • (Π Σ (σ s • (t -time(σ s ), a)) -1 • (Π Σ (σ s • (t -time(σ s ), a)) • Π Σ (σ s ) • σ d )) = Π Σ (obs(σ s , t -t )) -1 • (Π Σ (σ s ) • σ d ) = Π Σ (obs(σ s , t -t )) -1 • (Π Σ (σ s ) • (Π Σ (σ s ) -1 • buf c )) = Π Σ (obs(σ s , t -t )) -1 • buf c it follows that: nobs(σ t0 , t) -t (t -time(obs(σ t0 , t))) ∈ Safe(Reach(σ t0 , t), Π Σ (nobs(σ t0 , t)) • σ d )
Otherwise, a ∈ Σ c , and then, since Safe(Reach(σ s0 , time(σ

•(δ, a))), Π Σ (nobs(σ s0 , time(σ•(δ, a))))•σ c ) =
∅, there exists σ ∈ tw(Σ) that satises the three following constraints:

1. Π Σ (σ ) Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c , 2. Reach(σ s0 , time(σ • (δ, a))) after σ ∈ F × R ≥0 , 3. for any t ∈ R ≥0 , if v ∈ V s is such that Reach(σ s0 , time(σ•(δ, a))) ∈ v, then v, maxbuffer(Π Σ (obs(σ , t )) -1 • buf c ), 1 ∈ W 0 .
Thus, item 1 can be written as Π Σ (σ ) buf c •a, and from item 3 we can deduce that for any t

∈ R ≥0 , if v ∈ V s is such that Reach(σ s0 , time(σ • (δ, a))) ∈ v, then v, maxbuffer(Π Σ (obs(σ , t )) -1 • (buf c • a)), 1 ∈ W 0 .
, t) = σ s , nobs(σ s -t t , t -t ) -t (t -t -time(obs(σ s , t -t ))) = nobs(σ t0 , t) -t (t -t + t ) = nobs(σ t0 , t) -t (t -time(σ s )) = nobs(σ t0 , t) -t (t -time(obs(σ t0 , t)))
On the other hand, if delay(σ s (1)) ≤ t-time(σ s ), then nobs(σ s -t t , t-t ) = nobs(σ s , t-time(σ s )) = nobs(σ t0 , t), and since time(obs(σ t0 , t)) = time(obs(σ s • σ s , t))

= time(σ s • (obs(σ s , t -time(σ s )), t)) = time(σ s ) + time(obs(σ s , t -time(σ s ))) it follows that nobs(σ s -t t , t -t ) -t (t -t -time(obs(σ s -t t , t -t ))) = nobs(σ s , t -time(σ s ))-t (t -t -time(obs(σ s , t -t + t ) -t t )) = nobs(σ t0 , t) -t (t -t -(time(obs(σ s , t -time(σ s ))) -t )) = nobs(σ t0 , t) -t (t -t + t -(time(obs(σ t0 , t)) -time(σ s ))) = nobs(σ t0 , t) -t (t -time(σ s ) + time(σ s ) -time(obs(σ t0 , t))) = nobs(σ t0 , t) -t (t -time(obs(σ t0 , t))) Thus, in both cases, nobs(σ t0 , t) -t (t -time(obs(σ t0 , t))) ∈ Safe(Reach(σ s0 , t ) after (σ s -t t , t -t ), Π Σ (obs(σ s -t t , t -t )) -1 • (buf c • a)) Since Reach(σ s0 , t ) after (σ s -t t , t -t ) = Reach(σ s ) after ( , t -time(σ s )) after (σ s -t t , t -t ) = Reach(σ s ) after ((σ s -t t ) + t t , t -t + t ) = Reach(σ s ) after (σ s , t -time(σ s )) = Reach(σ s • σ s , t) = Reach(σ t0 , t)
We start by proving items 1 and 2.

For σ ∈ tw(Σ), let P(σ) be the predicate σ s0 , σ

c = store ϕ (σ) =⇒ (σ s0 dΣ c σ ∧ σ s0 = Σu σ ∧ Π Σ (σ s0 ) |Σc • σ c = Π Σ (σ) |Σc ).
Let us prove by induction that P(σ) holds for any σ ∈ tw(Σ).

Induction basis: for σ = , store ϕ ( ) = , , and since dΣ c , = Σu , and Π Σ ( ) |Σc • = Π Σ ( ) |Σc , it follows that P( ) holds.

Induction step: Suppose that for σ ∈ tw(Σ), P(σ) holds. Let us consider (δ, a) ∈ R ≥0 × Σ, σ s0 , σ c = store ϕ (σ), σ t0 , σ d = store ϕ (σ • (δ, a)), and σ s = obs(σ s0 , time(σ • (δ, a))).

• If a ∈ Σ u , then there exists σ s such that σ t0 = σ s • (time(σ • (δ, a)) -time(σ s ), a) • σ s , and Π Σ (σ s ) • σ d = Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c . Thus, since a ∈ Σ u Π Σ (σ t0 ) |Σc • σ d = Π Σ (σ s • (time(σ • (δ, a)) -time(σ s ), a) • σ s ) |Σc • σ d = Π Σ (σ s ) |Σc • Π Σ (σ s ) |Σc • σ d Now,
following the induction hypothesis, σ s0 = Σu σ, and since nobs(σ, time(σ • (δ, a))) = , it follows that nobs(σ s0 , time(σ • (δ, a))) ∈ tw(Σ c ), and thus σ s ∈ tw(Σ c ) too. Also following the induction hypothesis, we know that Π In both cases, P(σ) =⇒ P(σ • (δ, a)).

Σ (σ s0 ) |Σc • σ c = Π Σ (σ) |Σc . It follows that Π Σ (σ t0 ) |Σc • σ d = Π Σ (σ s ) |Σc • Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c = Π Σ (obs(σ s0 , time(σ • (δ, a)))• nobs(σ s0 , time(σ • (δ, a)))) |Σc • σ c = Π Σ (σ s0 ) |Σc • σ c = Π Σ (σ) |Σc = Π Σ (σ • (δ, a
Thus, we have shown by induction that for all σ ∈ tw(Σ), P(σ) holds. Consequently, for any σ ∈ tw(Σ), if σ s0 , σ c = store ϕ (σ), then σ s0 dΣ c σ and σ s0 = Σu σ. Thus, for any t ∈ R ≥0 , E ϕ (σ, t) = obs(σ s0 , t) dΣ c obs(σ, t), and E ϕ (σ, t) = obs(σ s0 , t) = Σu obs(σ, t). We have then shown that E ϕ is compliant with respect to Σ u and Σ c . • If a ∈ Σ u , since (σ, time(σ•(δ, a))) ∈ Pre(ϕ), we know that (see proof of Proposition 2) σ s ∈ Safe(Reach(σ s ), Π Σ (σ s ) -1 |Σc • Π Σ (σ) |Σc ). Now, since σ s ≺ d σ E s , and since σ s is the maximal word for d that is in Safe, this means that σ E s ∈ Safe(Reach(σ s ), Π Σ (σ s ) -1 |Σc • Π Σ (σ) |Σc ). This means that one of the following does not hold :

1. Π Σ (σ E s ) Π Σ (σ s ) -1 |Σc • Π Σ (σ)
|Σc , but if this did not hold, then E would not be compliant.

. ∀t ∈ R ≥0 , ∀v ∈ V s , Reach(σ s • σ E s , t) ∈ v =⇒ v, maxbuffer(Π Σ (σ s • obs(σ E s , t)) -1 • Π Σ (σ) |Σc ), 1 ∈ W 0 .
If this does not hold, then there exists t ∈ R ≥0 and v ∈ V s such that Reach(σ s • σ E s , t) ∈ v and v, maxbuffer(Π Σ (σ • obs(σ E s , t)) -1 • Π Σ (σ) |Σc ), 1 ∈ W 0 . Then, there exists a winning strategy for player 1 from this node. This means that we can construct a word by following the winning strategy of player 1, like it is done in the proof of Proposition 2: depending on the edge followed in the game graph, player 1 can add an uncontrollable event to the input word (the delays are given by the edges corresponding to letting time elapse) that allows to stay in a node not belonging to W 0 . This can be done until the strategy of player 0 goes back to the previous node, making a loop if it has no time successor. This must ultimately happen since adding controllable events to the input only gives player 0 more possibilities, thus player 1 can choose only edges corresponding to adding uncontrollable events or letting time elapse. By privileging the elapse of time, it can ensure that the word will be nite. Thus, player 1 can build a word σ u ∈ tw(Σ u ) such that E(σ • (δ, a) • σ u , ∞) |= ϕ.

In any possible case, there exists σ u ∈ tw(Σ u ) such that E(σ • (δ, a) • σ u , ∞) |= ϕ (in the second case, σ u = ).

• Otherwise, a ∈ Σ c , and we can prove as in the previous case that there exists σ u ∈ tw(Σ u ) such that This means that E ϕ is optimal in Pre(ϕ).

Proposition 5. The output o of E as per Denition 9 for input σ at date t is such that o = E ϕ (σ, t).

Proof. In this proof, we use some notation from Section 3.3:

• C E = tw(Σ) × Σ * c × Q × R ≥0 is the set of congurations.

• c E 0 = , , q 0 , 0 ∈ C E is the initial conguration.

• Γ E = ((R ≥0 × Σ) ∪ { }) × Op × ((R ≥0 × Σ) ∪ { }) is the alphabet, composed of an optional input, an operation and an optional output.

The set of operations is {dump(.), pass-uncont(.), store-cont(.), delay(.)}.

For a sequence of rules w ∈ (Γ E ) * , we note the concatenation of all the inputs of w, input(w) = Π 1 (w(1))• Π 1 (w(2)) . . . Π 1 (w(|w|)) , and output(w) = Π 3 (w(1)) • Π 3 (w(2)) . . . Π 3 (w(|w|)) the concatenation of all the outputs of w. Since all congurations are not reachable from c E 0 , for w ∈ (Γ E ) * , we note Reach E (w) = c if c E 0 w -→ E c for some conguration c ∈ C E , or Reach E (w) = ⊥ if such a conguration does not exist. For a word σ ∈ tw(Σ), and a date t ∈ R ≥0 , we note Rules(σ, t) = max ({w ∈ (Γ E ) * | input(w) = obs(σ, t)∧Reach E (w) = ⊥ ∧ Π 4 (Reach E (w)) = ttime(output(w))}). We also note Reach E (σ, t) = Reach E (Rules(σ, t)). Rules(σ, t) represent the sequence that the EM applies with input word σ until date t. Since rule delay() can be applied an innite number of times by slicing time, we only consider words in (Γ E ) * that are minimal in the number of rules delay(), i.e. the word obtained by merging two consecutive rules delay() into one with the sum of delays of the two rules, until stabilisation. This allows to dene Rules(σ, t) correctly, without cheating by slicing time to increase the length of the word. Note that the words obtained by merging or adding delay() rules this way reach exactly the same congurations in the end. We will also allow ourselves to extend the use of output to timed words, such that output(σ, t) = output(Rules(σ, t)).

We have to show that for any σ ∈ tw(Σ), and t ∈ R ≥0 , output(σ, t) = E ϕ (σ, t). Now, for σ ∈ tw(Σ) and t ∈ R ≥0 , let P(σ, t) be the predicate σ s0 , σ c = store ϕ (σ) =⇒ (output(σ, t) = obs(σ s0 , t) ∧ Reach E (σ, t) = nobs(σ s0 , t), σ c , Reach(σ s0 , t), ttime(obs(σ s0 , t)) ), and P(σ) be the predicate ∀t ∈ R ≥0 , P(σ, t). Let us then show by induction that P(σ) holds for any σ ∈ tw(Σ).

Induction basis: if σ = , then let us consider t ∈ R ≥0 . Then, store ϕ ( ) = , . On the other hand, the only rule that can be applied is delay(t), thus Reach E ( , t) = , , q 0 after ( , t), t .

Thus, output( , t) = obs( , t), and Reach E ( , t) = nobs( , t), , Reach( , t), ttime( , t) . Thus, P( , t)

holds. Thus, for any t ∈ R ≥0 , P( , t) holds, meaning that P( ) holds. If t < time(σ • (δ, a)), then Reach E (σ • (δ, a), t) = Reach E (σ, t), and obs(σ t0 , t) = obs(σ s0 , t), meaning that P(σ • (δ, a), t) holds.

Then, let us consider that t ≥ time(σ • (δ, a)).

• If a ∈ Σ u , then rule pass-uncont(a) can be applied, meaning that c after (a/ pass-uncont(a)/a) = σ b , σ c , q, 0 , with q = Reach(σ Then, rules delay() and dump() can be applied, until date t is reached, leading to the conguration nobs(σ t0 , t), σ d , Reach(σ t0 , t), ttime(obs(σ t0 , t)) .

Moreover, considering the transitions taken, This means that for any t ∈ R ≥0 , P(σ • (δ, a), t) holds. Thus P(σ) =⇒ P(σ • (δ, a)).

We have then shown by induction that P(σ) holds for any σ ∈ tw(Σ). In particular, this means that for any σ ∈ tw(Σ), if σ s0 , σ c = store ϕ (σ), then for any t ∈ R ≥0 , obs(σ s0 , t) = output(σ, t). Thus, E ϕ (σ, t) = obs(σ s0 , t) = output(σ, t).

Figure 1 .

 1 Figure 1. Conceptual view of the runtime enforcement problem.

  Consider for example the timed wordσ = (1, a) • (1, b) • (1, c) • (2, a) over the alphabet Σ = {a, b, c}. Then, Π Σ (σ) = a • b • c • a, obs(σ, 4) = (1, a) • (1, b) • (1, c), nobs(σ, 4) = (2,a), and if Σ = {b, c}, σ |Σ = (2, b) • (1, c), and for instance (1, a) • (1, b) • (3, c) d σ, and σ ≤ lex (1, a) • (0, b) • (3, c) • (3, a). Moreover, if w = (1, a) • (1, b), then w -1 • σ = (1, c) • (2, a).

Figure 2 .

 2 Figure 2. Timed automata modelling double-clicks, without and with overlaps

Figure 4 .

 4 Figure 4. A symbolic compatible graph of ϕ t as per [ACH + 92].

(

  Figure 5. Game graph associated with property ϕ t

1 ( 1 , 2 ( 1 , 2 ( 1 , 4 ( 1 , 4 ( 1 , 5 ( 1 , 5 ( 1 , 6 ( 1 , 6 ( 1 , 7 ( 1 , 7 ( 1 , 8 ( 1 , 8 ( 1 , 10 ( 1 , 10 ( 1 , 10 ( 1 ,

 11212141415151616171718181101101101 Figure 6. Execution of an enforcement monitor with input (1, Auth) • (1, LockOn) • (2, Write) • (1, LockO ) • (1, LockOn) • (1, Write) • (1, LockO )

Algorithm 3 :

 3 Function eventRcvd(EM, e)

3 while

 3 The input sequence has not been read entirely do 4 (δ, a) ← read(); 5 while del ≤ δ do 6 δ ← δdel; 7 (EM, del) ← delay(EM, del); 8 while getStrat(EM) = EMIT do 9 (EM, del) ← emit(EM); del) ← delay(EM, δ); 13 (EM, del) ← eventRcvd(EM, a); 14 end 15 while del < ∞ or getStrat(EM) = EMIT do 16 while getStrat(EM) = EMIT do 17 (EM, del) ← emit(EM); 18 end 19 if del < ∞ then 20 (EM, del) ← delay(EM, del); 21 end 22 end Algorithm 6: Main algorithm to enforce a property in oine modeinput : The EM = (G, q, w) output: EMIT if the strategy is to emit the rst event of the buer, DONTEMIT otherwise 1 Function getStratFast((G, q, w))2if (q after w(1), maxbuffer(w [2..] ), 0) ∈ W 0

Figure 8 .

 8 Figure 8. Properties used to benchmark GREP

Figure 9 .

 9 Figure 9. Comparison of timings of GREP and TiPEX on the safety property. GREP fast means that option-f is used. The x axis corresponds to the events of the input (from 1 to 1000), and the y axis corresponds to the logarithm of the timings (in nanoseconds) between the reads of the events.

  Figure10. Timings of GREP and TiPEX on the response and co-safety properties. The x axis corresponds to the events of the input (from 1 to 1000), and the y axis corresponds to the logarithm of the timings (in

  Figure 11. Property ϕ u .

Figure 12 .

 12 Figure 12. Timings of GREP for property ϕ u with and without option -f.

2 .

 2 t < time(σ•(δ, a)) ≤ t . Then, obs(σ•(δ, a), t) = obs(σ, t), meaning that (see previous case) E ϕ (σ•(δ, a), t) = E ϕ (σ, t). Following the induction hypothesis, since P(σ) holds, E ϕ (σ, t) E ϕ (σ, time(σ • (δ, a))) E ϕ (σ • (δ, a), time(σ • (δ, a))).Thus, we have to show that E ϕ (σ • (δ, a), time(σ • (δ, a))) E ϕ (σ • (δ, a), t ). Since time(σ •(δ, a)) ≤ t , obs(σ •(δ, a), time(σ •(δ, a))) = σ •(δ, a) = obs(σ •(δ, a), t ), thus if σ s2 , σ c = store ϕ (σ • (δ, a)), then E ϕ (σ • (δ, a), time(σ • (δ, a))) = obs(σ s2 , time(σ • (δ, a))), and E ϕ (σ • (δ, a), t ) = obs(σ s2 , t ).

  a) ∈ Pre(ϕ, t), then P(σ • (δ, a), t) trivially holds.• If σ•(δ, a) ∈ Pre(ϕ, t)∧σ ∈ Pre(ϕ, time(σ•(δ, a))), then, since σ ∈ Pre(ϕ, time(σ•(δ, a))), following lemma 1, since obs(σ, time(σ • (δ, a))) = σ, obs(σ s0 , time(σ • (δ, a))) = σ s = obs(σ |Σu , time(σ • (δ, a))) = σ |Σu and Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c = Π Σ (σ |Σc ). Since σ • (δ, a) ∈ Pre(ϕ, t),and σ ∈ Pre(ϕ, time(σ • (δ, a))), following the denition of Pre(ϕ, t) and Pre(ϕ, time(σ • (δ, a))) (Denition 8), there exists t ∈ R ≥0 such that time(σ•(δ, a)) ≤ t ≤ t, and Safe(Reach((σ•(δ, a)) |Σu , t ), Π Σ (obs(σ•(δ, a), t ) |Σc )) = ∅. Let us consider the minimum such t . Since t ≥ time(σ • (δ, a)), then obs(σ • (δ, a), t ) = σ • (δ, a). This means that: Safe(Reach((σ • (δ, a)) |Σu , t ), Π Σ ((σ • (δ, a)) |Σc )) = ∅.

( 1 )

 1 If a ∈ Σ u , then considering that (σ• (δ, a)) |Σu = σ |Σu • (time(σ • (δ, a)) -time(σ |Σu ), a) = σ s • (time(σ • (δ, a)) -time(σ s ), a), and Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c = Π Σ (σ |Σc ) = Π Σ ((σ • (δ, a)) |Σc ), (1) becomes: Safe(Reach(σ s • ( time(σ • (δ, a)) -time(σ s ), a), t ), Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c ) = ∅.Let us consider δ = time(σ • (δ, a)) -time(σ s ), such that time(σ • (δ, a)) = time(σ s • (δ , a)), and t = ttime(σ • (δ, a)).

  )) |Σc Moreover, following the induction hypothesis, σ s0 dΣ c σ, thus in particular, σ s dΣ c σ, meaning that if i ∈ [1; |σ s |], then time(σ s|Σc[..i] ) ≤ time(σ |Σc[..i] ), and since i ≤ |σ |Σc |, that means that time(σ s|Σc[..i] ) ≤ time((σ • (δ, a)) |Σc[..i] ). Since time(σ s • (time(σ • (δ, a)) -time(σ s ), a)) = time(σ • (δ, a)), it follows that for any i ∈ [|σ s | + 1; |σ t0|Σc |], time(σ t0|Σc[..i] ) ≥ time(σ • (δ, a)) (remember that the restriction to an alphabet conserves dates, not delays). Thus, for anyi ∈ [1; |σ t0|Σc |], time(σ t0|Σc[..i] ) ≥ time((σ • (δ, a)) |Σc[..i] ). Since we have already shown that Π Σ (σ t0 ) |Σc • σ d = Π Σ (σ) |Σc , we know that Π Σ (σ t0 ) |Σc Π Σ (σ) |Σc . This means that σ t0 dΣ c σ • (δ, a). Finally, by induction hypothesis, σ s0 = Σu σ, thus, since σ t0|Σu = (σ s • (time(σ • (δ, a)) -time(σ s ), a)) |Σu = σ s|Σu • ((time(σ • (δ, a)) -time(σ s ), a)+ t (time(σ s ) -time(σ s|Σu ))) = σ s|Σu • (time(σ • (δ, a)) -time(σ s )+ time(σ s ) -time(σ s|Σu ), a) = σ s|Σu • (time(σ • (δ, a)) -time(σ s|Σu ), a) = σ |Σu • ((δ, a) + t (time(σ) -time(σ |Σu ))) = (σ • (δ, a)) |Σu Thus, P(σ • (δ, a)) holds.• Otherwise, a ∈ Σ c , and then, there exists σ s ∈ tw(Σ)such that σ t0 = σ s • σ s and Π Σ (σ s ) • σ d = Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c • a. Thus, Π Σ (σ t0 ) |Σc • σ d = Π Σ (σ s ) |Σc • Π Σ (σ s ) • σ d = Π Σ (σ s ) |Σc • Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c • a = Π Σ (σ s0 ) |Σc • σ c • a = Π Σ (σ) |Σc • a = Π Σ (σ • (δ, a)) |ΣcAs in the case where a ∈ Σ u , for any i ∈ [1; |σ s|Σc |], time(σ t0|Σc[..i] ) ≤ time(σ |Σc[..i] ). Moreover, by construction, delay(σ s (1)) ≥ time(σ • (δ, a)) -time(σ s ), thus for i ∈ [|σ s|Σc | + 1; time(σ t0|Σc )], if i = i -|σ s|Σc |, then time(σ t0|Σc[..i] ) = time(σ s ) + time(σ s[..i ] ) ≥ time(σ s ) + time(σ • (δ, a)) -time(σ s ) = time(σ • (δ, a)). Since time(σ • (δ, a)) ≤ time((σ • (δ, a)) |Σc[..i] ), and Π Σ (σ t0 ) |Σc Π Σ (σ • (δ, a)) |Σc , this means that σ t0 dΣ c σ • (δ, a). Finally, σ t0|Σu = σ s|Σu = σ |Σu = (σ • (δ, a)) |Σu . Thus P(σ • (δ, a)) holds.

  Thus, items 1 and 2 hold. Now, let us prove item 3. Let us consider σ ∈ tw(Σ),σ s0 , σ c = store ϕ (σ), (δ, u) ∈ R ≥0 × Σ u , σ t0 , σ d = store ϕ (σ • (δ, u)), and σ s = obs(σ s0 , time(σ • (δ, u))). Then, σ s = E ϕ (σ, time(σ • (δ, u))), and following the denition of store ϕ (Denition 7), σ s •(time(σ•(δ, u))-time(σ s ), u) σ t0 . Thus, E ϕ (σ•(δ, u), time(σ•(δ, u))) = obs(σ t0 , time(σ • (δ, u))). Since time(σ s • (time(σ • (δ, u)) -time(σ s ), u)) = time(σ • (δ, u)), it follows that σ s • (time(σ • (δ, u)) -time(σ s ), u) E ϕ (σ • (δ, u), time(σ • (δ, u))).

Proposition 4 .

 4 E ϕ is optimal in Pre(ϕ) as per Denition 4.Proof. Let us consider σ ∈ tw(Σ), (δ, a) ∈ R ≥0 × Σ such that (σ, time(σ • (δ, a))) ∈ Pre(ϕ), E an enforcement function that is compliant with respect to Σ u and Σ c , and such that E(σ, time(σ• (δ, a))) = E ϕ (σ, time(σ • (δ, a))). Let us suppose that E ϕ (σ • (δ, a), ∞) ≺ d E(σ • (δ, a), ∞).We then have to prove that there existsσ u ∈ tw(Σ u ) such that E(σ • (δ, a) • σ u , ∞) |= ϕ.Let us consider σ s = obs(E ϕ (σ, time(σ • (δ, a))), time(σ • (δ, a))). Then, since E ϕ and E are compliant, andE ϕ (σ, time(σ • (δ, a))) = E(σ, time(σ • (δ, a))), there exists σ s ∈ tw(Σ) such that E ϕ (σ • (δ, a), ∞) = σ s • σ s and σ E s ∈ tw(Σ) such that E(σ • (δ, a), ∞) = σ s • σ E s . Now, since E ϕ (σ • (δ, a), ∞) ≺ d E(σ • (δ, a), ∞), this means that σ s ≺ d σ E s .

2 .

 2 Reach(σ s ) after σ E s ∈ F G . If this does not hold, then Reach(σ s • σ E s ) ∈ F G , meaning that E(σ • (δ, a), ∞) |= ϕ.

3

 3

  E(σ •(δ, a)•σ u , ∞) |= ϕ.All that is needed is to adapt the parameters of Safe:σ s ∈ Safe(Reach(σ s , time(σ • (δ, a))), Π Σ (σ s ) -1 |Σc • Π Σ (σ • (δ, a)) |Σc ), and thus σ E s ∈ Safe(Reach(σ s , time(σ • (δ, a))), Π Σ (σ s ) -1 |Σc • Π Σ (σ • (δ, a)) |Σc), but the arguments are the same.Thus, if E is compliant, and σ ∈ tw(Σ) and (δ, a) ∈ R ≥0 × Σ are such that (σ, time(σ• (δ, a))) ∈ Pre(ϕ), E(σ, time(σ • (δ, a))) = E ϕ (σ, time(σ • (δ, a))), and E ϕ (σ • (δ, a), ∞) ≺ d E(σ • (δ, a), ∞), then there exists σ u ∈ tw(Σ u ) such that E(σ • (δ, a) • σ u , ∞) |= ϕ.

  Induction step: let us suppose that for σ ∈ tw(Σ), P(σ) holds. Let us consider (δ, a) ∈ R ≥0 × Σ, t ∈ R ≥0 , σ s0 , σ c = store ϕ (σ), σ t0 , σ d = store ϕ (σ • (δ,a)), σ s = obs(σ s0 , time(σ • (δ, a))), and c = Reach E (σ, time(σ • (δ, a))). Then, by induction hypothesis, c = nobs(σ s0 , time(σ • (δ, a))), σ c , Reach(σ s0 , time(σ • (δ, a))), time(σ • (δ, a)) -time(σ s ) .

  s0 , time(σ • (δ, a))) after (0, a) = Reach(σ s • (time(σ • (δ, a)) -time(σ s ), a)), σ b = κ ϕ (q, Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c ), and σ c = Π Σ (σ b ) -1 • (Π Σ (σ b ) • σ c ).Thus, σ b is such that σ t0 = σ s •σ b , thus c after (a/ pass-uncont(a)/a) = σ -1 s •σ t0 , σ d , Reach(σ s •(time(σ•(δ, a))-time(σ s , a))), 0 .

  output(σ • (δ, a), t) = output(σ, time(σ • (δ, a))) • (time(σ • (δ, a))time(σ s ), a) • obs(σ b , ttime(σ • (δ, a))) = σ s • (time(σ • (δ, a)) -time(σ s ), a)• obs(σ b , ttime(σ • (δ, a))) = obs(σ t0 , t)Thus, P(σ • (δ, a), t) holds.• Otherwise, a ∈ Σ c , and then rule store-cont(a) can be applied from conguration c, leading to c after(a/ store-cont(a)/ ) = σ b , σ c , Reach(σ s0 , time(σ • (δ, a))), ttime(σ s ) , with σ b = κ ϕ (Reach(σ s0 , time(σ • (δ, a))), Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c • a) + t (ttime(σ s )) and σ c = Π Σ (σ b ) -1 • (Π Σ (nobs(σ s0 , time(σ • (δ, a))))) • σ c • a.Thus, σ b is such that σ t0 = σ s • σ b , and σ c = σ d . Then, rules delay() and dump() can be applied until date t is reached, leading to Reach E (σ • (δ, a), t) = nobs(σ t0 , t), σ d , Reach(σ t0 , t), ttime(obs(σ t0 , t)) . Moreover, considering the transitions taken,output(σ • (δ, a), t) = output(σ, time(σ • (δ, a))) • obs(σ b , ttime(σ s )) = σ s • obs(σ b , ttime(σ s ))= obs(σ s • σ b , t) = obs(σ t0 , t) Thus, P(σ • (δ, a), t) holds. Thus, in both cases, P(σ • (δ, a), t) holds.

  1, the uncontrollable event Auth occurs. It has to be released immediately since it is an uncontrollable event, then ϕ t goes to l 1 . At t = 2, the uncontrollable event LockOn is received. It is also emitted instantaneously, leading ϕ t to l 2 . At t = 4, the controllable event Write occurs. It should not be emitted since it would make the system go to l 3 which is a non-accepting state. It is stored in the buer. Note that it is not necessary to store the corresponding delay, since while no other uncontrollable event occurs, it is not possible to compute an output time for Write. At time t = 5, the uncontrollable event LockO occurs. It has to be released immediately, and ϕ t goes to l 1 . Now it is possible to emit the stored action Write, but it is necessary to wait for 2 time units before. This value is associated to Write pending output (as described in [PFJ + 14]), and should be denitely released if no other uncontrollable event happens meanwhile. At t = 6, the uncontrollable event LockOn occurs, then ϕ t goes to l 2 . It is no longer possible to emit Write, which is again not associated to an output instant anymore. At time t = 7, the second Write event occurs, and it is also stored in the buer without a possibility to compute its output instant. The occurrence at t = 8 of the uncontrollable event LockO unblocks the situation, leading ϕ t to l 1 , and the two stored actions Write are again associated with

		Auth, LockO x := 0, Write x ≥ 2	Auth LockOn
		Auth		LockOn
	l 0	x := 0	l 1		l 2
	Write LockO LockOn	Write x < 2	LockO x := 0	Write
			l 3
			Σ
		Figure 3. Property ϕ t
	output delays, 2 and 0 respectively, meaning that they should be emitted at t = 10 if no other uncontrollable
	happens in the mean time.

  Then, t is the minimum number such that Safe(Reach(σ s • (δ , a), t ), buf c ) = ∅. Therefore, t ∈ T(Reach(σ s • (δ , a)), buf c ). Thus, there exists w ∈ Safe(Reach(σ s • (δ , a)) after ( , t ), buf c ) such that σ s = w + t t . Thus, σ st t ∈ Safe(Reach(σ s • (δ , a), t ), buf c ).

	Now, note that:

  Since t is the minimum date that satises this equation, ttime(σ • (δ, a)) ∈ T(Reach(σ s , time(σ • (δ, a))), buf c • a). Thus, there exists w ∈ Safe(Reach(σ s , time(σ• (δ, a))) after ( , ttime(σ • (δ, a))), buf c • a) such that σ s = (w + t ttime(σ • (δ, a))) + t (time(σ • (δ, a)) -time(σ s )). Thus, σ st (ttime(σ • (δ, a)) + time(σ • (δ, a)) -time(σ s )) = σ st (ttime(σ s )) ∈ Safe(Reach(σ s , t ), buf c • a).Let us consider t = ttime(σ s ), such that σ st t ∈ Safe(Reach(σ s , t ), buf c • a).

	Safe(Reach(σ Now,	Thus, (1) becomes:

s , t ), Π Σ (nobs(σ s0 , time(σ • (δ, a)))) • σ c • a) = ∅

  Safe(Reach(σ s , t ) after (σ st t , tt ),Π Σ (obs(σ st t , tt )) -1 • (buf c • a)) Now, since t ≥ time(σ s ), Reach(σ s , t ) after (σ st t , tt ) = Reach(σ s )after ( , ttime(σ s )) after (σ st t , tt ) = Reach(σ s ) after ( , t ) after (σ st t , tt ) = Reach(σ s ) after ((σ st t ) + t t , tt + t ) = Reach(σ s ) after (σ s , t -time(σ s )) = Reach(σ s • σ s , t)

	and
	Thus, in both cases, this means that
	nobs(σ t0 , t) -t (t -time(obs(σ t0 , t))) ∈

  and thus (2) becomes: nobs(σ t0 , t)t (ttime(obs(σ t0 , t))) ∈ Safe(Reach(σ t0 , t), Π Σ (nobs(σ t0 , t)) • σ d )

	Thus, in both cases,

nobs(σ t0 , t)t (ttime(obs(σ t0 , t))) ∈ Safe(Reach(σ t0 , t), Π Σ (nobs(σ t0 , t)) • σ d ).

  This last property holds because adding a controllable event to the buer only gives more possibilities to the EM (in the game graph, if v, w, p is winning, then v, w • c, p is also winning). This means that σ ∈ Safe(Reach(σ s0 , time(σ • (δ, a))), buf c • a), and thus, Safe(Reach(σ s0 , time(σ• (δ, a))), buf c • a) = ∅. Thus, 0 ∈ T(Reach(σ s0 , time(σ • (δ, a))), buf c • a), meaning that σ st (time(σ • (δ, a)) -time(σ s )) ∈ Safe(Reach(σ s0 , time(σ • (δ, a))), buf c • a). Let us consider t = time(σ • (δ, a)), and t = ttime(σ s ). Safe(Reach(σ s0 , t ) after (σ st t , tt ), Π Σ (nobs(σ st t , tt )) -1 • (buf c • a)) Now, if delay(σ s (1)) > ttime(σ s ) (i.e. delay((σ st t )(1)) > tt ), then nobs(σ st t , tt ) = nobs(σ s , tt + t )t t = nobs(σ s , ttime(σ s ))t tSince nobs(σ t0 , t) = nobs(σ s , ttime(σ s )), it follows that nobs(σ st t , tt ) = nobs(σ t0 , t)t t . Moreover, obs(σ st t , t-t ) = since delay(σ s (1)) > t-time(σ s ), thus, considering that obs(σ t0

	Then, following lemma 2,
	nobs(σ

st t , tt )t (tttime(obs(σ st t , tt ))) ∈

https://github.com/matthieurenard/GREP

calculated with cloc (https://github.com/AlDanial/cloc)

We patched TiPEX to retrieve the times as we do in our tool, only modifying it to get times properly, and did not change the behaviour inside the part that is being measured.

For some properties, running TiPEX was too long to run it as many times as GREP.

and Π Σ (nobs(σ t0 , t))

In particular, this means that Reach(σ t0 , t) after nobs(σ t0 , t)t (ttime(obs(σ t0 , t))) ∈ F G . Since Reach(σ t0 , t) after nobs(σ t0 , t)t (ttime(obs(σ t0 , t))) = Reach(obs(σ t0 , t)) after ( , ttime(obs(σ t0 , t))) after nobs(σ t0 , t)t (ttime(obs(σ t0 , t)))

= Reach(obs(σ t0 , t)) after (nobs(σ t0 , t)t (ttime(obs(σ t0 , t)))) + t (ttime(obs(σ t0 , t)))

= Reach(obs(σ t0 , t)) after nobs(σ t0 , t) = Reach(obs(σ t0 , t) • nobs(σ t0 , t)) = Reach(σ t0 ) this means that Reach(σ t0 ) ∈ F G , meaning that σ t0 |= ϕ.

Thus, in all cases, for any t ∈ R ≥0 , P(σ) =⇒ P(σ • (δ, a), t). This means that P(σ) =⇒ P(σ • (δ, a)).

We then have shown by induction that P(σ) holds for any σ ∈ tw(Σ). In particular, we have shown that for any (σ, t) ∈ Pre(ϕ), σ s , σ c = store ϕ (σ) =⇒ σ s |= ϕ. Thus there exists t that we can consider such that t ≥ t, that is such that for any t ≥ t , σ s = E ϕ (σ, t ).

Thus, E ϕ is sound in Pre(ϕ).

Proposition 3. E ϕ is compliant, as per Denition 3.

Proof. We have to prove that the three following properties hold: