Loïc Hélouët
email: loic.helouet@inria.fr

Robustness in Scenarios. ANR IMPRO Deliverable

This document considers robustness problems for timed scenarios. Robustness questions come from discrepancies between idealized representation of time in models and the actual measure of time and implementation of clocks in real architectures. A robustness question can usually we described as: given a set of requirements, how does architectural assumptions and imperfect time measurement affect the semantics of the specified behaviors? We propose different interpretations of time, that consider that measured time can be imprecise, that clocks are discrete, or that some time may elapse between the moment when the decision to perform an action is taken (for instance when a timer expires) and its actual execution. We then consider properties of timed scenarios such as consistency (does a specification describe at least one execution), path consistency (is it the case that for every timed run of a scenario description, there exists a consistent timed execution ?), and semantics preservation (is the behavior of the model the same with a timed semantics as without time constraints ?), and the robustness of such properties with respect to different timed semantics.

Introduction

Scenarios are a popular formalisms to design typical behaviors of distributed systems. Recently, they have been enhanced with time annotations, to allow specification of timing constraints within requirements [START_REF] Gastin | Reachability and boundedness in time-constrained MSC graphs[END_REF]. Such timing constraints can be seen as prescriptions of behaviors that an implementation of a system executing a scenario specification should enforce. However, adding time to scenarios may completely change the behavior of the modeled system. Indeed, a scenario that is executable in an untimed setting might not be executable in a timed setting, due to inconsistent constraints on occurrence dates of events.

It is well known that a real system can not implement timing issues as precisely as required within a timed model. For instance, clocks measure time with some imprecision, and launching an action that is triggered by time (for instance expiration of a timer) is not immediate, and may not be enforceable without some delay. Such situation can be painful: formal models with idealized representation of time are frequently used for verification purpose, but a successful verification of a timed system does not means that any implementation of this system will satisfy the verified property, nor that there exists an implementation with precise enough measurement of time and sufficient reactivity that preserves the verified property. This robustness problem was first formalized by Puri [START_REF] Puri | Dynamical properties of timed automata[END_REF] within the context of timed automata. Later works showed that robustness of ω-regular properties [START_REF] Bouyer | Robust model-checking of timed automata via pumping in channel machines[END_REF] can also be verified.

This report addresses robustness issues for time constrained scenarios (TC-MSCs). We first provide several notions of "realistic time". More precisely, we consider imperfect time measurement and delayed triggering. The semantics of such timed systems is given by enlarging or shrinking semantics, or assuming that durations are measured up to some imprecision. We also consider discretized semantics, i.e semantics in which events can only occur at integer dates. This is particularly useful when considering that the modeled system in implemented on an architecture with discrete clocks. We then address several formal properties of TC-MSCs. The first property is consistency: for a TC-MSC description G, is it the case that G has at least one consistent run ? The second property is path consistency : is it the case that every run of a TC-MSC has a consistent execution under realistic time semantics ? We then consider robustness of (path) consistency properties: is it the case that a (path) consistent TC-MSC is still consistent under some "'realistic"' semantics. The second robustness issue considered is untimed semantics preservation: is it the case that the untimed language of a TC-MSC graph is the same under idealized time semantics and under realistic semantics ? The last issue we consider is whether there exists some clock precision guaranteeing robustness of the above properties.

Unsurprisingly, most of robustness questions are undecidable for TC-MSCs. This comes mainly from undecidability of consistency for TC-MSCs in the general case, but also from undecidability in MSC graphs (language equivalence or inclusion , regularity,... are undecidable). Fortunately, subclasses allow to address robustness questions for a large subclass of the model. This report is organized as follows: Section 2 introduces the formalisms that will be used throughout the document, Section 3 introduces different "realistic" semantics, that consider imperfect of discretized time. Section 4 considers robustness issues (preservation of untimed language and consistency properties) under different interpretation of time when the nature and a bound on imprecision of implementation is known. Section 5 considers robustness under arbitrary precision, and section 6 concludes this work.

Preliminaries

This section describes the main models that will be used throughout the report, namely timed automata, and time constrained Message Sequence Charts. The reason to consider timed automata is twofold: first, a lot of litterature has been devoted to robustness for this model. second, we will show that most of decidable robustness issues for TC-MSCs can be brought back to a timed automaton setting.

Timed automata

Imperfection in time measurement has been extensively addressed for timed automata [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Alur | Timed automata[END_REF]. The problem of timed robustness has been first addressed by [START_REF] Puri | Dynamical properties of timed automata[END_REF] and then in many reference such as [START_REF] Bouyer | Robustness in timed automata[END_REF][START_REF] Bouyer | Robust model-checking of timed automata via pumping in channel machines[END_REF][START_REF] De Wulf | Robust safety of timed automata[END_REF][START_REF] Bouyer | Robust analysis of timed automata via channel machines[END_REF][START_REF] Bouyer | Robust model-checking of linear-time properties in timed automata[END_REF][START_REF] De Wulf | Systematic implementation of real-time models[END_REF][START_REF] Sankur | Untimed language preservation in timed systems[END_REF][START_REF] Swaminathan | A symbolic decision procedure for robust safety of timed systems[END_REF][START_REF] Swaminathan | The surprising robustness of (closed) timed automata against clock-drift[END_REF].

Let C = {x 1 , ...x n } be a finite set of clocks. We denote by Φ C the set of conjunctions of formulas of the form k ≈ x i ≈ ′ l where k, l ∈ Q + and ≈, ≈ ′ ∈ {< , ≤}. A valuation for a set of clocks is a function v that assigns a value from R to every clock. We also denote by v + d the valuation that assigns value v(c) + d to every clock c, and by v |R the valuation that assign 0 to every clock in R and v(c) to every other clock c.

A timed automaton is a tuple A = (L, C, l 0 , E, F ), where L is a set of locations, with l 0 ∈ L the initial location and F ⊆ L is a set of accepting locations, C is a set of clocks, and

E ⊂ L × Φ C × Σ × 2 C × L is a set of edges.
An edge e = (l, g, σ, R, l ′ ) shall be interpreted as follows : the automaton moves from location l to a location l ′ while execution action σ ∈ Σ as soon as the valuation of its clocks satisfies guard g. During this move, all clocks from R are reset.

A timed word over an alphabet Σ is a sequence w = (σ 0 , d 0 )(σ 1 , d 1 ), .... where each σ i is a letter from Σ, each d i ∈ R is a date representing the occurrence date of an event of type σ i , and for every i < j, d i ≤ d j . the untiming of a timed word w

= (σ 0 , d 0 )(σ 1 , d 1 ) . . . (σ n , d n ) is the word U nt(w) = σ 1 .σ 2 . . . σ n . A run of an automaton A is a sequence (l 0 , v 0 ) a0 → (l 1 , v 1 ) a1 → (l 2 , v 2 )...(l n , v n ),
where each a i is either an action σ ∈ Σ, or a value δ i from R. We distinguish timed moves, i.e., moves of the form

(l i , v i ) δi → (l i , v i+1 ) where v i+1 = v i + δ i , and discrete moves, i.e.moves of the form (l i , v i ) σ → (l i+1 , v i+1 ), such that there exists an edge (l i , g, σ, R, l i+1 ) of A such that v i |= g, v i+1 = v i |R . A run is accepting if l n ∈ F .
A timed word w = (σ 0 , d 0 )(σ 1 , d 1 ), .... is recognized by A if there exists an accepting run of A such that the sequence of letters read in the run and in w coincide (there exists a mapping f from indices of w to discrete moves of the run such that for every i < j f (i) < f (j)), and every d i is equal to the sum of elapsed durations since the beginning of the run, i.e.

d i = j<f (i) δ j .
The semantics L(A) of a timed automaton is the set of timed words recognized by A. It is well known that timed automata enjoy some nice properties: reachability of some location, emptiness of L(A), and omega-regular properties are also decidable. However, inclusion of timed languages is not decidable in general [START_REF] Alur | A theory of timed automata[END_REF]. A timed automaton recognizes timed words which dates need not be integer. The integer semantics of a timed automaton is

L int (A) = L(A)∩(Σ ×N). The untimed semantics of A is the set of words U nt(L(A)) = {U nt(w) | w ∈ L(A)}.
Proposition 1 (Integer semantics of timed automata). Let A = (L, C, l 0 , E, F ) be a timed automaton. Then one can build an automaton A int over an alphabet Σ ∪ {τ }, where τ is an unobservable letter, such that L(A int ) = L int (A).

Proof : We can design an automaton

A int = (L, C ′ , l 0 , E ′ , F ) where -C ′ = C ⊎ {c t } -E = {(l, {c t = 1}, τ, {c t }, l) | l ∈ L} ∪ {l, g ∧ c t = 1, σ, R ∪ {c t }, l ′ ) | (l, g, σ, R, l ′ ) ∈ E} ∪ {l, g ∧ c t = 0, σ, R ∪ {c t }, l ′ ) | (l, g, σ, R, l ′ ) ∈ E}
Then, one can easily prove, by induction on the length of runs that any run of A that recognizes a timed word with integer dates is also recognized by A int , and conversely that for any accepting run of A int , there exists an accepting run of A with the same sequence of observable letters and integer dates. ⊓ ⊔

Time-Constrained MSCs, HMSCs

Let R ≥0 denote the set of non-negative reals, N the set of integers and I the collection of open and closed intervals with end points in Q as well as intervals of the form [c, ∞), (c, ∞), where c ∈ Q. Throughout this report, we fix a finite set P of processes and let p, q range over P. Let Σ = {p!q, p?q | p, q ∈ P, p = q} be the communication alphabet. The letter p!q represents p sending a message to q, while p?q signifies p receiving a message sent by q. We define the map loc : Σ → P via loc(p!q) = p = loc(p?q), and call loc(a) the location of a. We define Message Sequence Charts (MSCs) and time-constrained MSCs (TC-MSCs) as usual. Definition 1. An MSC is a tuple (E, (< p ) p∈P , µ, λ). The set of events is E and λ : E→Σ labels events with letters. For each p, < p is a total order over E p = {e ∈ E | loc(λ(e)) = p}. The message function µ ⊆ E S × E R is a bijection, such that f = µ(e) implies λ(e) = p!q, λ(f ) = q?p for some p, q ∈ P, with E S = {e ∈ E | ∃p, q ∈ P, λ(e) = p!q} and E R = {f ∈ E | ∃p, q ∈ P, λ(f ) = q?p}. We require that the transitive closure ≤ of ⋖ = p∈P < p ∪µ is a partial order.

The relation ≤ reflects causal ordering of events. We will write e < f when e ≤ f and e = f . Notice that E p has a unique < p -maximal event (respectively, minimal event), which we refer to as the last (respectively, first) event of E on p. It is frequently assumed in the literature that messages exchanges in a MSC respect a FIFO ordering (messages between pairs of processes p, q are received in the same order as they are sent), but this is not needed in this report. Definition 2. A TC-MSC is a tuple (E, (< p ) p∈P , µ, λ, δ) where (E, (< p ) p∈P , µ, λ) is an MSC and δ : E × E → I is a function associating an interval δ(e, e ′ ) ∈ I to each e ⋖ e ′ .

For each pair of events e ⋖ e ′ , the interval δ(e, e ′ ) constrains the range in which the difference between the occurrence time of e ′ and the occurrence time of e can lie. For clarity, we shall refer to occurrence times as dates. A TC-MSC T defines a collection of MSCs with dates such that the relative differences of dates fulfill the constraints asserted in T . Definition 3. Let T = (E, (< p ) p∈P , µ, λ, δ) be a TC-MSC. A dated MSC generated by T is a tuple (E, (< p ) p∈P , µ, λ, d) where d : E → R + is such that for each e ⋖ e ′ , d(e ′ )d(e) is in the interval δ(e, e ′ ). In the rest of the report, we will denote by T the set of all TC-MSCs, and by D the set of all dated MSCs. We denote by D(T ) the set of dated MSCs generated by T . Remark that for a given TC-MSC T , we may have D(T ) = ∅ if the set of constraints attached to pairs of events in T are not satisfiable. We will say that a TC-MSC T is consistent if D(T ) = ∅, and inconsistent otherwise. Definition 4. Let T be a TC-MSC with n events. The language L(T ) of a TC-MSC T is the set of timed words of the form w = (a 1 , d 1 ). . . . (a n , d n ) such that there exists a dated MSC D = (E, (< p ) p∈P , µ, λ, d) ∈ D(T ), a 1 . . . a n = λ(e 1 . . . e n ) for a linear extension e 1 . . . e n of (E, ≤), and for every i ∈ 1..n, d i = d(e i ). We denote by L(T ) the set of timed words defined by T .

To capture infinite collections of TC-MSCs, we define TC-MSC graphs as in [START_REF] Akshay | Checking coverage for infinite collections of timed scenarios[END_REF][START_REF] Gastin | Reachability and boundedness in time-constrained MSC graphs[END_REF], which are finite graphs whose nodes are labeled by TC-MSCs. Each path ρ of a TC-MSC graph G induces a TC-MSC by concatenating TC-MSCs labeling nodes of ρ. Transitions of G are labeled by interval constraints, one for each process, that act as constraints on the timing between the last and first event of each process in consecutive nodes of ρ. Definition 5. A TC-MSC graph is a structure G = (N, T , Λ, n in , N fi , -→, ∆) where N is a finite non-empty set of nodes, T a finite set of TC-MSCs, Λ : N → T labels each node with a TC-MSC, n in is the initial node, N fi the set of final nodes, -→⊆ N × N is the transition relation, and ∆ is a labeling function which associates an interval ∆ p (n→n ′ ) ∈ I to each transition n→n ′ and each process p, such that ∆ p (n→n ′ ) = [0, ∞) if Λ(n) or Λ(n ′ ) has no event on process p.

A path ρ of the TC-MSC graph G is a sequence n 0 n 1 . . . n ℓ such that n 0 = n in and n i →n i+1 for i = 0, . . . , ℓ -1. The path ρ is said to be final if n ℓ ∈ N fi . For each n→n ′ , the concatenation of TC-MSCs Λ(n), Λ(n ′ ) is defined with respect to ∆(n→n ′ ), and is denoted Λ(n) • Λ(n ′ ). Roughly speaking, this consists of putting Λ(n ′ ) after Λ(n) and for every process p, attaching to the pair (e p , f p ) the constraint ∆ p (n→n ′ ), for e p the last event of Λ(n) on process p and f p the first event of Λ(n ′ ) on p. Formally, let

Λ(n) = (E, (< p ) p∈P , µ, λ, δ), Λ(n ′ ) = (E ′ , (< ′ p ) p∈P , µ ′ , λ ′ , δ ′ ). Then Λ(n) • Λ(n ′ ) = (E ′′ , (< ′′ p ) p∈P , µ ′′ , λ ′′ , δ ′′
) where E ′′ is the disjoint union of E and E ′ , < ′′ p is the transitive closure of the union of < p , < ′ p and E p ×E ′ p , and λ ′′ is given by: λ ′′ (e) = λ(e) for e ∈ E, λ ′′ (e) = λ ′ (e) for e ∈ E ′ . We also set µ ′′ (e) = µ(e) when µ(e) is defined, and µ ′′ (e) = µ ′ (e) when µ ′ (e) is defined. At last, δ ′′ is given by: δ ′′ (e, f ) = δ(e, f ) for e ⋖ f , δ ′′ (e, f ) = δ ′ (e, f ) for e⋖ ′ f . For each p, if both E p and E ′ p are nonempty, we set δ ′′ (e p , f p ) = ∆ p (n→n ′ ) for e p the last event of E p and f p the first event of E ′ p . We emphasize that by definition, ∆ p (n→n

′ ) = [0, ∞) if E p or E ′ p is empty. It follows that for n→n ′ →n ′′ , (Λ(n) • Λ(n ′ )) • Λ(n ′′ ) is the same as Λ(n) • (Λ(n ′ ) • Λ(n ′′ ))
. Thus, we unambiguously define the TC-MSC T ρ induced by a path

ρ = n 0 . . . n ℓ of G to be Λ(n 0 ) • . . . • Λ(n ℓ ).
The notions of dated MSCs and timed languages generated by a TC-MSC extends naturally to paths. A path ρ of G is called consistent if D(T ρ ) = ∅ (or equivalently, L(T ρ ) = ∅). We denote by T (G) the set of all TC-MSCs generated by G, i.e., T (G) = {T ρ | ρ is a final path of G}. We also denote by D(G) the union of all dated MSCs generated by G, that is

D(G) = {D(T ρ ) | T ρ ∈ T (G)}, and by L(G) = L(T (G)) the timed language of G. An example of a TC-MSC graph G 1 is in Figure 2. The TC-MSC T 2 is induced by path ρ = n 1 • n 2 • n 1 • n 2 • n 1 • n 3 of G 1 , i.e., T 2 = T ρ . As n 3 is final, all dated MSCs in D(T 2 ) belong to D(G 1 ).
Definition 6. A TC-MSC graph is regular(locally synchronized) iff, for every cycle ρ of G, for every pair of processes p, q that are active in ρ, the TC-MSC T ρ contains a causal dependency from p to q and another causal dependency from q to p.

The class of locally synchronized HMSCs (TC-MSC graphs without tile information) was defined in [START_REF] Muscholl | Message sequence graphs and decision problems on mazurkiewicz traces[END_REF][START_REF] Alur | Model checking of Message sequence Charts[END_REF], and lifted in [START_REF] Akshay | Model checking time-constrained scenario-based specifications[END_REF] to a timed setting. Checking if a TCMSG is locally synchronized is a co-NP-complete problem. More interestingly, timed languages of locally synchronized TC-MSC graphs can be recognized by event clock timed automata. An event clock automaton is an automaton that has one clock c a per type of action a in the alphabet of the automaton, and that resets c a every time action a is played. An interesting property of these event clock automata is that they are closed under complementation, which is not necessarily the case for timed automata in general.

Theorem 1 ( [1]

). Let G be a regular TC-MSC graph. Then one can compute a event-clock timed automaton

A G such that L(A G ) = L(G).

Different interpretation/implementations of time

The pioneering works of [START_REF] Puri | Dynamical properties of timed automata[END_REF] and [START_REF] De Wulf | Systematic implementation of real-time models[END_REF] have highlighted one weakness of timed models: the representation of time is idealized. To be more precise, time measurements assumed by most of models are supposed arbitrarily precise. This means that when a guard stipulates that event b must occur at most 10 time units after event a, the implementation of the model system has the capacity to decide whether exactly 10 time units have elapsed according to some canonical time. Supposing that some perfect clock c a is capable of measuring perfectly the time elapsed since a, one still has to consider that some time can elapse between the date at which decision to execute b is taken (when c a approaches value 10) and the actual execution of b. This delay is not necessarily constant. So deciding to execute b as soon as c a = 10 means that b could be executed later, violating the specified constraint between a and b.

Another issue is the discrete nature of time measurement. Timed automata specify guards and allow clocks to take real values. However, it might be natural to consider that clocks take integer values to model the discrete nature of clocks in computers.

Imprecision in realistic time is frequently captured by the notion of enlargement and shrinking (guards and constraints are specified up to some small variation ǫ. Puri [START_REF] Puri | Dynamical properties of timed automata[END_REF] has proved that for some models, delays can accumulate, and that even the smallest variation ǫ may change the semantics of the model, i.e. its reachable locations, or its timed and untimed languages. This can be harmful, as properties that hold under an idealized semantics might be wrong under realistic time semantics, i.e. for any implementation of the model, regardless of clocks precision.

A large literature has been devoted to robustness for timed automata [START_REF] Puri | Dynamical properties of timed automata[END_REF][START_REF] Bouyer | Robustness in timed automata[END_REF][START_REF] Bouyer | Robust model-checking of timed automata via pumping in channel machines[END_REF][START_REF] De Wulf | Robust safety of timed automata[END_REF][START_REF] Bouyer | Robust analysis of timed automata via channel machines[END_REF][START_REF] Bouyer | Robust model-checking of linear-time properties in timed automata[END_REF][START_REF] De Wulf | Systematic implementation of real-time models[END_REF][START_REF] Sankur | Untimed language preservation in timed systems[END_REF][START_REF] Swaminathan | A symbolic decision procedure for robust safety of timed systems[END_REF][START_REF] Swaminathan | The surprising robustness of (closed) timed automata against clock-drift[END_REF], and an extension of the problem for Petri nets has been proposed [START_REF] Akshay | Robustness of time petri nets under guard enlargement[END_REF]. Regardless of the considered model, robustness issues mainly consists in comparing properties and semantics of a model under the idealized time representation and under some realistic representation of time. We propose hereafter several "realistic time" semantics for TC-MSC graphs. We will denote by G α the semantics of TC-MSC graph G under semantics α, and define it as the set of dated MSCs generated by G when time follows principles of semantics α (approximate measurement, discrete time,....).

Idealized time As mentioned before, robustness issues are often brought back to comparison of a system with realistic semantics and of the same system with idealized time semantics. For TC-MSC graphs this idealized semantics of time is the standard semantics. We have

G id = {M ∈ D(T ρ ) | ρ is a final path of G} L id (G) = M∈ G id L(M )
The idealized time semantics of a time constrained MSC graph G considers that all time constraints that are described within a consistent MSC of G can be implemented. For instance, if a pair of events e, f is equipped with a constraint δ(e, f ) = [START_REF] Bouyer | Robust analysis of timed automata via channel machines[END_REF][START_REF] Bouyer | Robust analysis of timed automata via channel machines[END_REF], the idealized semantics considers that f must be executed exactly 10 time units after e. Even if the model seems sound, it is quite obvious that no hardware can implement such perfect timing. Forbidding use of singletons as time constraints does not solve the problem: the execution date of a message reception has two preceding events : the sending of a message, and the preceding event on the same process. The execution date of a reception must occur at a date satisfying a pair of constraints, and in practice can hence be reduced to a singleton, even when constraints of the form δ(e, f ) = [x, x] are forbidden. Consider for example the TC-MSC of figure 3. Constraints on dates of events are all of the form [a, b] with a < b. However, in this scenarion, the last reception on process q can only occur exactly 4 time units after process p sends the firts message to process r. discrete time semantics The discrete time semantics assumes that all events occur at integral clock values. This is still an idealized semantics of time, but it is justified by the fact that computers measure time with clocks that tick at regular intervals, and that time is hence measured as a number of ticks.

G int = {M = (E, (< p ) p∈P , µ, λ, d) ∈ D(T ρ ) | ρ is a final path of G∧∀e ∈ E, d(e) ∈ N} L int (G) = M∈ G int L(M ) One can immediately notice that G int ⊆ G id .
Imperfect measurement As already pointed out, measurement of time in computers may be imperfect. Imprecision in measurement can be due to clock imprecision, but also to the way a system is observed. Suppposing that a system is equipped by an observer that collects occurrences of events asynchronously. Observation may introduce some delay. This means that a an event can occur at precisely 10 time units, but that it might be reported as occurring a fraction of seconds earlier or later. In some contexts, one may consider that the date of an event fulfills the time constraints expressed by the specification if there is a different timing of the observed behavior that is ǫ close to a timed behavior that meets all constraints of the specification.

G ≈ǫ =    M = (E, (< p ) p∈P , µ, λ, d) ∈ D | ∃M ′ = (E, (< p ) p∈P , µ, λ, d ′ ) ∈ G id ∧∀e ∈ E, d(e) ∈ [d ′ (e) -ǫ, d ′ (e) + ǫ]    L ≈ǫ (G) = M∈ G ≈γ L(M )
One can notice that approximation in time measurement does not change the untimed semantics of TC-MSC graphs.

Proposition 2. For every TC-MSC graph G, and for every ǫ ∈ R, we have the following properties.

-G id = ∅ ⇒ G ≈ǫ -∀ρ, path of G, D(T ρ ) = ∅ ⇒ T ρ ≈ǫ = ∅ -U nt(L ≈ǫ (G)) = U nt(L(G))
Delayed/early triggering semantics As already mentioned in the introduction, enforcing an event b to occur 10 time units after event b can be enforced by a constraint δ(a, b) = [START_REF] Bouyer | Robust analysis of timed automata via channel machines[END_REF][START_REF] Bouyer | Robust analysis of timed automata via channel machines[END_REF]; In practice, such a constraint can be implemented using a timer, that is set right after the execution of a, and expires 10 time units later, enforcing execution of b. However, deciding to execute an instruction at a precise date does not mean that the instruction executes immediately, and a small delay might be needed before starting event b. That is, if b is supposed to start 10 time units after a, it may indeed start only 10 + ψ time units after a, for some small delay ψ ∈ R. This can be captured by a guard enlargement.

I ±ǫ = [max(0, a -ǫ), b + ǫ] if b = ∞ and I ψ = [max(0, a -ǫ), ∞) otherwise.
For a set of constraint δ over a set of event dates, the right enlargement of δ by ψ is the constraint δ +ψ such that δ +ψ (e, f ) = δ(e, f ) +ψ if δ(e, f ) is defined, and is undefined otherwise. The enlargement of δ by ǫ is the constraint δ ±ǫ , where δ ±ǫ (e, f ) = δ(e, f ) ±ǫ if δ(e, f ) is defined, and is undefined otherwise. Last, the right enlargement of a TCMSC T = (E, (< p ) p∈P , µ, λ, δ) by ψ is the TCMSC T +ψ = (E, (< p ) p∈P , µ, λ, δ +ψ ) and the enlargement of T by ǫ is the TCMSC

T ±ǫ = (E, (< p ) p∈P , µ, λ, δ ±ǫ ).
The semantics of a TCMSG under delayed triggering is defined as follows:

G +ψ = {M ∈ D | ∃ρ final path of G, M ∈ D(T ρ +ψ )} L +ψ (G) = M∈ G +ψ L(M )
Similarly, one can consider the semantics of a TCMSG under an eager triggering semantics, that fires events earlier that specified by guards. We define the right shrinking of an interval [a, b] (resp. [a, ∞)) by some value ψ as the interval [a, bψ] (resp. [a, i nf ty), and define T -ψ accordingly Then the early semantics of G is defined as follows:

G -ψ = {M ∈ D | ∃ρ final path of G, M ∈ D(T ρ -ψ )} L -ψ (G) = M∈ G -ψ L(M )
Enlarged semantics The effect of imperfect measurement of time also has an effect on guards. Beyond triggering effect, one may also consider that a guard, measured using a clock, is satisfied too early, or conversely too late. Hence, satisfaction of a constraint ensuring that a delay between two events should stay within an interval [a, b] might only be implemented up to an imprecision of some ǫ on the lower and upper bound. This justifies the enlarged semantics defiend as follows:

G ±ǫ = {M ∈ D | ∃ρ final path of G, M ∈ D(T ρ ±ǫ )} L ±ǫ (G) = M∈ G ±ǫ L(M )
Remarks One can immediately notice that G ≈δ and G ±δ are different notions. Indeed, if G id = ∅, then G ≈ǫ = ∅ for any value of ǫ. On the other hand, one may have G id = ∅ and G +ψ = ∅, or G ±ǫ = ∅ for some values of ψ and ǫ.

One can also remark that G id ⊂ G ≈ǫ . Furthermore, for any value of δ, we have:

G int ⊆ G id ⊆ G +ǫ ⊆ G ±ǫ
Note also that G ±ǫ and G ≈ǫ are usually uncomparable.

Robustness issues for fixed variation of time

Even when a model is designed with an idealized representation of time, and hence does not correspond exactly to the sytem that can be ectually implemented by an architecture, one can still infer properties of a possible implementation of the model. In many cases, several assumptions on the architecture and its precision are known. For instance, clocks are usually imprecise, but during the lifetime of the system, this imprecision will never exceed a threshold δ. Similarly, one can usually assume that clocks are discrete, and hence firing dates of an event usually lay around some integer value of time, ... A natural question is then to consider if there is an important difference between the behavior of the model under idealized time semantics, and the implementable behaviors, and if properties of the model are preserved within an architectural context. This is what we will call robustness question in the rest of the report.

In this section, we review several robustness issues and their decidability for TC-MSC graphs when the nature of clocks and a bound on clock imprecision is known.

Robust consistency

A first question to ask when a timed specification is designed is whether this specification describes at least one behavior. If this is not the case, then one can consider that this description does not make sense. For timed automata, the emptiness problem consists in checking whether L(A) = ∅. This can occur if guards prevent from reaching an accepting state. For TC-MSC graphs, if a TCMSC T contains an unsatisfiable constraint, then D(T ) = ∅. Similarly, when a TCMSG G contains only paths ρ such that D(T ρ ) = ∅, we have D(G) = ∅ L(G) = ∅. We will say that a TC-MSC graph is consistent iff D(G) = ∅.

The consistency problem for TC-MSC graphs is defined as follows: given a TC-MSC graph G, determine whether G id = ∅, that is, whether it has at least one consistent and final path. In [START_REF] Gastin | Reachability and boundedness in time-constrained MSC graphs[END_REF], it is shown that this problem is undecidable in general.

Theorem 2 ([15]

). The consistency problem for TC-MSC graphs is undecidable.

The proof of this theorem uses an encoding of a counter machine using constraints in TC-MSCs. Counters are encoded as difference between occurrence dates of last events on processes minus 1, and zero test obtained by enforcing that two events occur at dates that differ by exactly one time unit.

Consistency has been addressed for regular TC-MSCs [START_REF] Akshay | Checking coverage for infinite collections of timed scenarios[END_REF]. Indeed, for a regular TC-MSC graph, one can build a event clock timed automaton A G which language is the set of timed words in L( G id ), and then check if this automaton recognizes at least one timed word.

Theorem 3 ([5]

). The consistency problem is decidable for regular TC-MSC graphs.

However, the class of regular TC-MSCs is quite restrictive. Further work has shown [START_REF] Akshay | Regular set of representatives for time-constrained msc graphs[END_REF][START_REF] Akshay | Symbolically bounding the drift in time-constrained msc graphs[END_REF] that checking emptiness for TC-MSC graphs is decidable under a weaker condition on time constraints which does not impose regularity. This restriction is called drift-boundedness. In [START_REF] Akshay | Regular set of representatives for time-constrained msc graphs[END_REF][START_REF] Akshay | Symbolically bounding the drift in time-constrained msc graphs[END_REF], the authors show that one can test whether a given TC-MSC graph satisfies this condition. Definition 8. Let us fix a TC-MSC graph G. Let ρ = n 0 . . . n ℓ be a consistent path of G and M = (E, (< p ) p∈P , µ, λ, d) be a dated MSC generated by T ρ . For an integer K, we say that M is a K-drift-bounded dated MSC of ρ iff for each i = 0, . . . , ℓ, for any two events e, e ′ in Λ(n i ), it is the case that |d(e)-d(e ′ )| ≤ K. We say that ρ is K-drift-bounded iff there exists a K-drift-bounded dated MSC in D(T ρ ). We emphasize that D(T ρ ) may also contain dated MSCs which are not K-drift-bounded. We say that G is K-drift-bounded iff every consistent (but not necessarily final) path of G is K-drift-bounded.

In other words, for each consistent path ρ, we can find a dated MSC in D(T ρ ) such that the difference between the dates of any two events from the same instance of a node is at most K. Notice that we can have G id = ∅ even though G is K-drift-bounded. In fact, G is vacuously K-drift-bounded for any K if it has no consistent path.

As an example, consider the TC-MSC graph G 1 from Figure 2. G 1 is 3drift-bounded since in every timed execution, we can be sure that all events in node n 1 or n 2 can be completed within a delay of 3 time units. But if we change the constraints on the loop on n 1 from ([0, 1] r , [0, 1] s ) to ( [START_REF] Akshay | Robustness of time petri nets under guard enlargement[END_REF][START_REF] Akshay | Checking coverage for infinite collections of timed scenarios[END_REF] r , [1, 2] s ) then for any integer K, G 1 is not K-drift-bounded. Note that G 1 is not locally synchronized. In fact, we can simulate a producer-consumer protocol in which a process continuously sends messages without waiting for an acknowledgement, and obtain non-regular behaviors. Thus, this example cannot be handled by the decidability result in [START_REF] Akshay | Model checking time-constrained scenario-based specifications[END_REF].

Drift-boundedness is a practical ans sensible notion. Interpreting a node of a TC-MSC graph as a phase or a transaction of a distributed protocol, we expect any scenario labeling the node to be executable in a bounded time, say K. A protocol specified as a TC-MSC graph that is not K-drift-bounded should thus be considered as ill-formed. Indeed, while a TC-MSC graph specification is usually incomplete (as it abstracts away some events and constraints used in the actual implementation), if it is not K-drift-bounded, then every implementation of this specification will not be K-drift-bounded either.

Let us first recall the results of [START_REF] Akshay | Regular set of representatives for time-constrained msc graphs[END_REF][START_REF] Akshay | Symbolically bounding the drift in time-constrained msc graphs[END_REF]. The first result shows that K-drift boundedness is a decidable property.

Theorem 4 ([2]

). Let K ∈ N and G be a TC-MSC graph. Then checking whether G is K-drift-bounded is decidable in PSPACE.

A nice property of drift boundedness is that it allows to check for emptiness.

Theorem 5 ([2]

). Let G be a TCMSG, and let K ∈ N be an integer. Then if

G is K-drift bounded, one can check if G id = ∅.
Now that several decidability issues have been considered, we can address the question of robustness of the consistency property. Given a TCMSG G such that G id = ∅ and for a choosen α ∈ {int, ≈ ǫ, -ǫ, ±ǫ}, is it still the case that G α = ∅ ? For a given α, we will call this problem robust consistency of G w.r.t semantics α. For enlarged or approximate semantics, the answer is straightforward:

Proposition 3. If G id = ∅, then G ≈ǫ = ∅, G ±ǫ = ∅ and G +ǫ = ∅
A direct consequence of this proposition is that robust consistency is guaranteed by definition for all TC-MSC graphs, and and semantics α ∈ {≈ ǫ, +ǫ, ±ǫ}. However, a consequence of theorem 2 is that robust consistency is undecidable in general for TC-MSCs with semantics α ∈ {int, -ψ}. Theorem 6. Robust consistency is undecidable in general for TC-MSCs with semantics α ∈ {int, -ψ}.

Proof One can easily design a TC-MSC graph G with initial node n 0 that encodes a counter machine as in theorem 2. We build a new TC MSC graph G ′ by adding a trivial transition from a n 0 to a new node n labeled by a TC MSC which is satisfiable with idealized semantics, but unsatisfiable with integer semantics or -ψ semantics. Then, G ′ int = ∅ iff the TC-MSC graph G encoding the Minsky machine is consistent, which is undecidable. ⊓ ⊔ Obviously, remaining within regular TC-MSCs allows for decidability of the emptiness question for any semantics, as the realistic semantics of the TC-MSC graph G can be described by an automaton A ′ that can be computed directly from A G . Indeed, given a regular TC-MSG G and its associated automaton

A G we have L( G int ) = L(A int G ) and L( G ±ǫ ) = L(A ±ǫ G )
, where A ±ǫ is the automaton obtained by enlarging guards of A by ǫ. Similarly, one can shrink, enlarge guards, and remain in the class of times automata, for which reachability of an accepting state is decidable.

Theorem 7. The robust consistency problem is decidable for regular TC-MSC graphs, for any semantics α ∈ {int, ≈ ǫ, -ǫ, ±ǫ}.

Again, it is desirable to extend decidability of robust consistency beyond regular TC-MSC graphs.

Theorem 8. The robust consistency problem is decidable for K-drift bounded TCMSGs under integer semantics when constraints are given as integer intervals.

Proof sketch: We reuse elements of the proof of [START_REF] Akshay | Symbolically bounding the drift in time-constrained msc graphs[END_REF] that builds an automaton which non-emptiness characterizes non-emptiness of D(G). To decide nonemptiness for K-drift bounded TC-MSC graphs, one can compute an automaton that recognizes consistent accepting paths of G. These path are all K-drift bounded, and states of the automaton contain a node of the TC-MSC, plus a symbolic representation of differences between dates of last events of each process (this can be represented as a set of inequations of the form x px q ≤ n, where n is an integer where x p denotes the occurrence date of the last event on process p). Appending a TC-MSC to a path ending in a state of this form is allowed only if there exists a way to date a TCMSC with dates starting from the set of constraints given by the inequations. This can be decided as a simple linear programming problem. Accepting states are states that end on an accepting node of G. In the integer semantics, the events dates and their differences are integers, so the encoding remains valid. Deciding whether a TC-MSC can be appended to a path can be solved using integer hull techniques (see [START_REF] Schrijver | Theory of Linear and Integer Programming[END_REF]

for details). ⊓ ⊔

A remaining open question is whether decidability still holds when G has rational constraints, and for early semantics -ψ. Both cases can force TC-MSC graphs to drift (the longer a path is, the larger the difference between occurrence dates of last events on processes is), and we conjecture that this leads to undecidability.

Path Consistency

Consistency is a sanity check that guarantees that the specified set of requirements contains at least one valid execution under some time interpretation fixed by a target architecture. As already pointed out, a path ρ of a TC-MSC graph G may not allow any valid execution under its time constraints. We call such paths inconsistent paths. The consistency problem consists in checking whether at least one path of G is consistent. Now, a more precise and interesting question is whether one paths of G is inconsistent. Designing a TC-MSC graph with inconsistent accepting paths means that some behaviors that were supposed realizable in an untimed setting are not realizable due to timing constraints.

The path consistency question for a TC-MSG G consists in deciding whether there exists an accepting path ρ of G such that D(T ρ ) = ∅. We will say that G is path consistent if all its paths have a non-empty language.

We conjecture that path consistency is undecidable in general for TC-MSC graphs. However, we can show that for regular and K-drift bounded TC-MSC graphs, this property is decidable. Theorem 9. Path consistency of regular TC-MSGs is decidable.

Proof: It has been shown that one can design a timed automaton A G from any regular TC-MSC graph G. This automaton memorizes a node n of G reached while following a path ρ of G, plus a suffix of T ρ not yet executed. The automaton A G moves from one state to another by recognizing an action to be executed (minimal w.r.t ordering) in the suffix, or an action a that is executable within a TC-MSC labeling a transition t = (n, T, n ′ ), appending T \ {a} to the current suffix. To design a timed automaton, a clock is associated to pair of event and predecessors of this event in the TC-MSC graph. Untimed transitions are enriched by guards, that measure whether the constraint w.r.t. the predecessor events is satisfied, and clock resets. It has been proved in [START_REF] Akshay | Model checking time-constrained scenario-based specifications[END_REF] that this construction is sound and finite.

We can reuse this construction and design an automaton B G that performs invisible τ moves when executing actions from the suffix of states, and moves labeled by T as soon as an action is consumed from a new transition t = (n, T, n ′ ). The timed automaton B G accepts only executions ending on states with empty suffix, i.e. it recognizes sequences of transitions of G that admit at least one timed word, i.e. consistent paths. Then, one can compare the regular language of B G to the sequence of transitions allowed by G. If they differ, then G is not path consistent. ⊓ ⊔.

Theorem 10. Path consistency of K-drift bounded TCMSGs is decidable.

Proof sketch : As for the proof of theorem 8, we can reuse the the symbolic automaton of [START_REF] Akshay | Regular set of representatives for time-constrained msc graphs[END_REF]. The symbolic automaton recognizes sequences of TCMSCs with non-empty language, that is consistent paths. If these sequences of TCMSCs are the same as in the original TC-MSC graph, then all paths of G have nonempty language. Conversely, if one can reach a state of the symbolic automaton from which a transition labeleed by a TC-MSC T exists but is not allowed due to inconsistency of constaints in T and in the inequations of the symbolic state, then there is at least one inconsistent path in G.⊓ ⊔ Path consistency is a property of TC-MSC graphs, which robustness can be also considered. The path consistency robustness problem is hence defined as follows: Given an interpretation α of time, a path consistent TC-MSC graph G, is G path consistent w.r.t α semantics, i.e. is it the case that all path of G have a dated execution under semantics α ?

We know that we have the following implications:

( T ρ int = ∅) ⇒ ( T ρ id = ∅) ( T ρ id = ∅) ⇔ (∀ǫ ∈ R, T ρ ≈ǫ = ∅) ( T ρ id = ∅) ⇒ (∀ǫ ∈ R, T ρ +ǫ = ∅) ∀ǫ ∈ R, ( T ρ +ǫ = ∅) ⇒ ( T ρ ±ǫ = ∅) ∀ǫ ∈ R, ( T ρ ≈ǫ = ∅) ⇒ ( T ρ ±ǫ = ∅) ∀ǫ ∈ R, ( T ρ -ǫ = ∅) ⇒ ( T ρ id = ∅)
Hence, path consistency may change only under integer or early triggering semantics.

Theorem 11. Let G be a path consistent TC-MSC graph. Then, G is path consistent under semantics α ∈ {≈ ǫ, +ψ, ±ǫ}.

For Regular TC-MSC graphs, we can reuse the construction of A G and B G described in theorem 9, to obtain the following result.

Theorem 12. Let G be a regular path consistent TC-MSC graph. Then, one can decide if G is path consistent under any semantics α ∈ {int, ≈ ǫ, +ψ, ψ, ±ǫ}.

Proof: For α ∈ {≈ ǫ, +ψ, ±ǫ}, path consistency of G guarantees path consistency of G under α semantics. Now, if α ∈ {int, -ψ}, we can build the automaton B G as in theorem 9, that recognizes sequences of TC-MSCs of G that have a timed execution. Then, one can adapt this timed automaton to build an automaton B int G that recognizes sequences of TC-MSCs which languages contain timed words with exclusively integer dates, following the construction in Proposition 1. Similarly, one can build an automaton B α G , that recognizes sequences of TC-MSCs recognized under shrinked semantics -ψ by shrinking guards of B G . Then, G is path consistent under integer (resp. early) semantics iff

L(B G ) = L(B int G ) (resp. L(B G ) = L(B -ψ G )
). ⊓ ⊔ We conjecture that robustness of path consistency is undecidable in general for α ∈ {int, -ψ}, even for K-drift bounded TC-MSC graphs, and is decidable for K-drift bounded TC-MSC graphs with integer constraints under integer semantics.

Untimed semantics preservation

Now, path consistency only considers paths of TC-MSC graphs, and not the contents of the assembled scenarios. We would like now to address robustness issues that consider whether the language depicted by a specification changes under a different implementation of time. Of course, requiring the timed language of a specification to remain identical under change of time implementation is requiring too much, as changing the semantics relaxes of reinforces existing constraints on execution dates of events. A more reasonable approach is to require that the untimed languages, that is the logical dependencies among events remain unchanged. Definition 9. Let T = (E, (< p ) p∈P , µ, λ, δ) be a TC-MSC. The unconstrained version of T is denoted by T ∞ , and is the MSC

T ∞ = (E, (< p ) p∈P , µ, λ). For a TC-MSC graphG = (N, T , Λ, n in , N fi , -→, ∆), the unconstrained version of G is the TC-MSC graph G ∞ = (N, T , Λ ∞ , n in , N fi , -→, ∆ ∞ ), where -Λ ∞ (n) = (Λ(n)) ∞ -∆ ∞ (n, n ′ )[p] = [0, ∞)
We will say that a TC-MSC graph has a robust untimed semantics if and only if U nt(L( G id )) = U nt(L( G ∞ id )) Theorem 13. One can not decide if a TC-MSC graph G has a robust untimed semantics, even if G is K-drift bounded.

Proof sketch: This can be brought back to HMSC language inclusion problem. Take H 1 , H 2 two HMSCs with initial nodes n 1 , n 2 . It is well known that one can not decide whether L(()H 1 ) ⊆ L(()H 2 ). Not, we can build a TC-MSC graph G, with initial node n 0 , all transitions of H 1 and H 2 , and additional transitions t 1 = (n 0 , T, n 1 ) and t 2 = (n 0 , T ′ , n 2 ), where T is an inconsistent TC-MSC, and T ′ is the unconstrained version of T . Obviously, in the untimed semantics, G can recognize T , then behave as H 1 , or T ′ , and behave as H 2 . In the timed semantics, G can only take transition labeled by T ′ and behave as in H 2 . Then the untimed semantics of G is robust if and only L(H 1 ) ⊆ L(H 2 ).⊓ ⊔

The above encoding works even if G is drift-bounded. Again, one way to obtain decidability is to consider regular TC-MSC graphs. Theorem 14. One can decide if a regular TC-MSC graph G has a robust untimed semantics.

Proof: One can design the timed automaton A G , and similarly, following the construction of [START_REF] Alur | Model checking of Message sequence Charts[END_REF], for an untimed TC-MSC graph, one can design another automaton A U G recognizing U nt(L(G)). It then suffices to compare the untimed language of A G with the language of A U G .⊓ ⊔ We can derive a robustness question with respect to semantics α from this question. We will say that a TCMSG has a robust untimed semantics w.r.t a chosen semantics α if and only if U nt(L( G α )) = U nt(L( G id )).

A specification has a robust untimed semantics w.r.t. time intrepretation α if it exhibits the same behavior that the idealized semantics under time interpretation α. Obviously, changing the interpretation of time may affect constraints on valid dates, and hence timed behavior, already at the level of TC-MSCs. As already mentioned, considering integer dates or shrinking constraints allow less behaviors that in the idealized semantics. That is, for every G, we have U nt( G int ) ⊆ U nt( G id ) and U nt( G -ψ ) ⊆ U nt( G id ).

Similarly, enlargement can only result in a larger set of timed executions of a TC-MSC graph. For every G and every ǫ ∈ R, we have G id ⊆ G +ǫ ⊆ G ±ǫ , and consequently U nt( G id ) ⊆ U nt( G +ǫ ) ⊆ U nt( G ±ǫ ).

However, comparing behavior only with respect to respective dates of events does not bring a lot of information, as it is quite obvious that enlarging guards allows new behaviors. Now, it seems important to discover when time interpretation adds or remove untimed behaviors, that is modifies the logics of the specification.

Theorem 15. Robustness of TC-MSC graphs semantics w.r.t a semantics α is undecidable, even for K-drift bounded TC-MSC graphs for any α ∈ {int, +ψ, -ψ, ±ǫ}.

Proof: We can reuse the encoding of HMSC language inclusion in theorem 13, but for each α, replace TC-MSC T that is unsatisfiable by a TC MSC T α that is satisfiable under idealized time semantics, and unsatisfiable under semantics α.

The converse encoding with T α unsatisfiable under idealized time semantics, and satisfiable under semantics α proves undecidability for semantics that enlarge time constraints. ⊓ ⊔ Theorem 16. Robustness of regular TCMSG untimed languages w.r.t a semantics α is decidable.

Proof : First, we can build build an automaton A G that recognizes timed words in G id . To compare this language to G int we can design a new automaton A int that recognizes timed words with integer dates. One can then design region automata for A and A int (they recognize respectively the untimed words in G id and G int ) and then compare their language (nb: this comparison is PSPACE in the size of the automata, which can be of exponential size w.r.t. the original TC-MSC graph).

Then, it has been shown that the enlarged semantics (by a small value ǫ) of a timed automaton A is also recognized by a timed automaton A ±ǫ obtained by enlarging guards in A. Hence, to compare G id with G ±ǫ for a regular TCMSg, it suffices to build A G , enlarge it, and then compare the untimed languages of both automata.

A similar construction can be performed for delayed semantics +ψ by right enlarging of guards in A G , and for early semantics -ψ by shrinking guards in A G . ⊓ ⊔

Robustness issues for arbitrary precision

Former section considers various interpretation of timed implementation, and robustness of specifications with respect to a choice of architecture, and a known bound ǫ on imprecision of time measurement or implementation. Such parameter is not necessarily known, and in addition, improving performances and accuracy of a system may help reducing imprecision, and preserve some properties.

However, there are situations in which even the smaller imprecision may change the overall behavior and properties of a system. Consider for instance the TCMSG G 2 of Figure 4, and in particular the TC-MSC of node n 3 . Let us call d 1 the occurrence date of the message sending from p to r and d 2 the occurrence date of the message from q to r in n 3 . The TCMSC in node n 3 is realizable within a context where the difference between d 2 and d 1 is at most 2. Now, one can note that any path of this example is a sequence of nodes of the form n 1 .n k 2 .n 3 , and that after playing n 1 , the date of the last executed event on q is greater by 15 time units than the date of the last event executed by p. After every occurrence of n 2 satisfying the attached constraints, the difference between dates of the last events on p and q can only be preserved or increased. Hence, no path of G 2 generates a correct dated MSC, and G 2 is inconsistent. Now, if we enlarge all constraints by some small value ǫ, every occurrence of n 2 can be used to reduce the possible difference between the dates of the last events on p and q by 2.ǫ in ±ǫ semantics. Hence a path of the form n 1 .n 13-2.ǫ 2.ǫ

2

.n 3 admits a dated MSC. One can notice that this remark holds for any value of ǫ, but this needs not be always the case. Now a question that arises is whether there exists a precision, i.e. a value of parameter ǫ that preserves or guarantees good properties of a system. Consider for example the TC-MSC graph G 3 of Figure 5. The constraint ([0, 0.9][1, 2]) on the loop of node n 2 implies that the TC-MSC graph is not K-drift bounded, as process q tends to receive message at dates that are further from their sending date by process p at every iteration of n 2 . However, an enlargement of the constraint by 0.1 avoids this delay accumulation. Conversely, the constraint δ(n 1 , n 1 ) for the loop on node n 1 does not force G to drift, but for any small ψ the semantics G -ψ drifts, as any passage through n 1 forces process q's last event to be later with respect to process p's last event by at least ψ time units. This example shows that there are situation where the smallest enlargement or shrink of constraints may change the overall property of a TC-MSC graph with respect to consistency, path consistency, and even drift.

From a practical point of view, this means that even very accurate architectures might be unable to preserve good properties of a specification. This raises the issue of robustness problems for architectures with arbitrary precision. We can define the following problems for arbitrary precision: i) Robust consistency : Given G such that G id = ∅, and a semantics α , does there exists ǫ ∈ R, ∀0 < ǫ ′ ≤ ǫ, G α = ∅ with enlargement/right enlargement/shrink of ǫ ′ ? ii) Robust path consistency : Given G that is path consistent, and a semantics α, does there exists ǫ ∈ R, ∀0 < ǫ ′ ≤ ǫ, G α is path consistent with enlargement/right enlargement/shrink of ǫ ′ ? Of course , we consider the the semantics α ranges in {≈ ǫ, ±ǫ, -ψ, +ψ}, because the questions do not make sense for integer semantics, that is not parameterized by any value.

Theorem 17. Let G be a regular TC-MSC graph. Then one can decide the robust enlargement, robust path consistency, and robust semantics problems.

Proof sketch: As G is regular, one can compute a timed automaton A G , and an (untimed) automaton B that recognizes the untimed language of A G . Then, one can apply the techniques of [START_REF] Bouyer | Robust model-checking of timed automata via pumping in channel machines[END_REF] to check whether there exists some value ǫ satisfying the robust consistency, robust path consistency, and robust semantics requirements. We can use the timed automaton recognizing paths of G to check path consistency, and we can compare U nt(L(()A G )) with U nt(L(()A α G )), where A α G is the timed automaton built by shrinking or enlarging guards of A G . ⊓ ⊔ We already know, from theorem 15 that for a given ǫ, one can not check properties such as consistency robustness, path consistency robustness, and robustness of a TC-MSC graph w.r.t any semantics of parameter ǫ. Furthermore, there exist TC-MSC graphs for which these undecidability results hold for any value of ǫ. One can design TC-MSC graphs that are consistent under idealized semantics, and inconsistent under -ψ , for any value of ψ. One can also design TC-MSC graphs that are trivially consistent under idealized time semantics, and which consistency depends on consistency of a part of TC-MSC graph encoding runs of a Minsky machine. Last, one can design TC-MSC graphs which language is not preserved by -ψ , +ǫ , ±ǫ for any value of ǫ. Though we have G -ψ ⊆ G -ψ ′ ⊆ G id for every ψ < ψ ′ , and G id ⊆ G ±epsilon ⊆ G ±epsilon ′ for ǫ < ǫ ′ , an algorithm starting from an arbitrary value of ψ or ǫ to reach a fixpoint satisfying the checked property is not guaranteed to terminate, and at each step would have to perform and undecidable check.

Hence we have the following conjecture:

Conjecture : Robust consistency, robust path consistency and robust semantics w.r.t. semantics α ∈ {int, ≈ ǫ, -ψ, ±ǫ, +ψ} under arbitrary precision are undecidable in general for TC-MSC graphs and K-drift bounded TC-MSC graphs.

Conclusion

We summarize in the following tables the results of the paper: We consider the emptiness problem supposing that the considered idealized time TC-MSC graph is non-empty fro the emptiness problem,that is describes at least one execution and consistent for the consistency problem. First of all we consider decidability results for regular TC-MSC graphs. Let us now address decidability for non-regular TC-MSC Graphs. As for the regular case, we suppose that the considered TC-MSC is consistent (resp path consistent) when checking robust (path) consistency:

As one can notice, leaving the regular class makes most of robustness issues undecidable, except for those that are guaranteed by definition.

As future work, we would like to complete the above pictures, and answer fully the questions of path consistency for integer and early semantics, and the conjecture on robustness problems with arbitrary precision outside the class of regular TC-MSC graphs.

Fig. 1 .

 1 Fig. 1. A TC-MSC T1 and a dated MSC D1 ∈ D(T1).

Fig. 2 .

 2 Fig. 2. A TC-MSC graph G1, and a TC-MSC T2 in T (G1).

Fig. 3 .

 3 Fig. 3. A TC-MSC T3.

Definition 7 .

 7 Let I = [a, b] be an interval, and ψ, ǫ ∈ R be small constants. The right enlargement of I by ψ is the interval I +ψ = [a, b + ψ] if b = ∞ and I ψ = [a, ∞) otherwise. The enlargement of I by ǫ is the interval

Fig. 4 .

 4 Fig. 4. A TC-MSC graph G2 : Enlargement modifies the language and consistency

Fig. 5 .

 5 Fig. 5. A TC-MSC graph G3 : modification of drift by enlargement

  Fig. 6. Decidability of robustness problems for regular TC-MSC graphs w.r.t different interpretations of time.

		int	≈ ǫ	+ψ	-ψ	±ǫ
	Robust consistency	decidable non-emptiness non-emptiness decidable non-emptiness
			guaranteed	guaranteed		guaranteed
		(Thm 7) (Prop 2)	(Prop 3)	(Thm 7) (Prop 3)
	Path Consistency	decidable guaranteed	guaranteed	decidable guaranteed
		(Thm 12) (Prop 2)	(Thm 11)	(Thm 12) (Thm 11)
	semantics preservation decidable guaranteed	decidable	decidable decidable
		(Thm 16) (Prop 2)	(Thm 16)	(Thm 16) (Thm 16)
	Problems with	irrelevant guaranteed	decidable	decidable decidable
	arbitrary precision		(Prop 2)	(Thm 17)	(Thm 17) (Thm 17)

  Decidability of robustness problems for TC-MSC graphs w.r.t different interpretations of time.Fig. 8. Decidability of robustness problems for K-drift bounded TC-MSC graphs w.r.t different interpretations of time.

		int	≈ ǫ	+ψ		-ψ	±ǫ
	Robust consistency	undecidable non-emptiness non-emptiness undecidable non-emptiness
		(Thm 6)	guaranteed	guaranteed		(Thm 6)	guaranteed
			(Prop 2)	(Prop 3)			(Prop 3)
	Path Consistency	???	guaranteed	guaranteed		???	guaranteed
			(Prop 2)	(Thm 11)			(Thm 11)
	semantics preservation undecidable guaranteed	undecidable undecidable undecidable
		(Thm 15) (Prop 2)	(Thm 15)		(Thm 15) (Thm 15)
	Problems with arbitrary irrelevant guaranteed	conjectured	conjectured conjectured
	precision		(Prop 2)	undecidable undecidable undecidable
	Fig. 7. int	≈ ǫ		+ψ		-ψ	±ǫ
	Robust consistency	decidable	non-emptiness non-emptiness ???	non-emptiness
		(with integer intervals) guaranteed	guaranteed	guaranteed
		(Thm 8)	(Prop 2)	(Prop 3)	(Prop 3)
	Path Consistency	???	guaranteed	guaranteed	???	guaranteed
			(Prop 2)	(Thm 11)	(Thm 11)
	semantics preservation undecidable	guaranteed	undecidable undecidable undecidable
		(Thm 15)	(Prop 2)	(Thm 15)	(Thm 15) (Thm 15)
	Problems with arbitrary irrelevant	guaranteed	conjectured	conjectured conjectured
	precision		(Prop 2)	undecidable undecidable undecidable