Franck Cassez

Claire Pagetti

Olivier Roux Irccyn

A Timed Extension for AltaRica

Keywords: AltaRica, Semantics, Timed Automata

In this paper we present a timed extension of the AltaRica formalism. Following previous works, we first extend the semantics of AltaRica with time and define timed components and timed nodes. Moreover we lift the priority features of AltaRica to the timed case. We obtain a timed version of AltaRica, called Timed AltaRica. Finally we give a translation of a Timed AltaRica specification into a usual timed automaton. These are the semantic foundations of a high-level hierarchical language for the specification of timed systems.

Introduction

Context. The development of complex and safety-critical systems requires the use of formal methods and tools for system design and specification. In the case of discrete systems the so-called reactive languages [1,[START_REF] Halbwachs | The synchronous data-flow programming language LUSTRE[END_REF][START_REF] Le Guernic | Programming real-time applications with Signal[END_REF][START_REF] Cassez | Compilation of the Electre reactive language into finite transition systems[END_REF] have been used for almost a decade to specify industrial systems. They give a rigourous and elegant basis for the structured development of reactive systems with the use of composition and hierarchical specifications for instance. On those specifications such techniques like model-checking can be applied to check for some properties on the designed systems.

The need for a counterpart specification language in the case of timed specifications arose recently as timing information can now be dealt with while verifying a system with tools like UPPAAL [START_REF] Pettersson | UPPAAL2k[END_REF], CMC [START_REF] Laroussinie | CMC: A tool for compositional model-checking of real-time systems[END_REF], KRONOS [START_REF] Bozga | Kronos: A model-checking tool for real-time systems[END_REF] or HyTech [START_REF] Henzinger | HYTECH: A model checker for hybrid systems[END_REF]. We give here the theoretical foundations of such a high-level Address for correspondence: Franck Cassez, IRCCyN, BP 92101, 1 rue de la Noë, 44321 Nantes Cedex 3, France specification language for timed systems. We extend the AltaRica [START_REF] Point | Altarica -constraint automata as a description language[END_REF][START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF][START_REF] Arnold | The AltaRica formalism for describing concurrent systems[END_REF] formalism with timing features.

AltaRica is a high-level specification formalism that allows one to specify constraint automata [START_REF] Point | Altarica -constraint automata as a description language[END_REF] with the following features:

• a component has its own variables (internal or external), plus some others it can only read (flow variables) that are shared by the others;

• components can be defined hierarchically and composed together by a general synchronization mechanism. Such a general component is called a node. One can express broadcast communication, give priority among some transitions, etc.

Moreover AltaRica has an unambiguous semantics [START_REF] Arnold | The AltaRica formalism for describing concurrent systems[END_REF][START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF] defined in terms of (interfaced) transition systems. From this semantic model, it is possible to compile AltaRica to lower level formalisms for different verification purposes: fault-trees to perform reliability analysis [START_REF] Griffault | The AltaRica language[END_REF], Petri nets, Markov graphs or finite state automata (that can be analysed with the tool MEC [START_REF] Arnold | Construction and analysis of transition systems with MEC[END_REF][START_REF] Arnold | An experience with MEC in a real industrial project[END_REF][START_REF] Vincent | Conception et réalisation d'un vérificateur de modèles AltaRica[END_REF][START_REF] Griffault | The mec 5 model checker[END_REF] for instance).

Nevertheless one cannot specify real-time constraints in AltaRica and of course this becomes crucial when some timing information contributes to the modelling and correctness of the system. Moreover there is no real high-level specification language for timed and hybrid systems. This makes AltaRica a good candidate to fill this gap. Once the language has been extended with timing constraints, we can take advantage of the work carried out these last years about timed systems: it is now well-known how to deal with the verification of timed automata [START_REF] Alur | A theory of timed automata[END_REF] and hybrid automata [START_REF] Henzinger | The theory of hybrid automata[END_REF][START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF] and many efficient tools are now available [START_REF] Henzinger | HYTECH: A model checker for hybrid systems[END_REF][START_REF] Bozga | Kronos: A model-checking tool for real-time systems[END_REF][START_REF] Bengtsson | New generation of UPPAAL[END_REF]. This adds a new feature to the AltaRica toolbox.

Our Contribution. Our work consists in extending the AltaRica formalism with real-time constraints and define a timed version of AltaRica called Timed AltaRica. We thus extend the theoretical foundations of AltaRica: we enhance the semantic model of AltaRica, the interfaced transition system (ITS), into timed interfaced transition system (TITS) and give the semantics of Timed AltaRica in terms of TITS. We proceed by shifting all the theoretical results obtained for AltaRica (e.g. interface bisimulation homomorphism, rewriting of a node into a component, . . . ) to the timed case: this is important as it gives Timed AltaRica good compositional properties that are needed in practice. Finally we present an algorithm to compile Timed AltaRica specifications into timed automata (which can be then analyzed with UPPAAL [START_REF] Pettersson | UPPAAL2k[END_REF]).

Outline of the paper. In the next section, we remind the basics about AltaRica and introduce a running example: the Train-Gate-Controller example. Section 3 is the core of the paper and presents Timed AltaRica the timed extension of AltaRica. In sections 4 and 5 we respectively give (i) the algorithm for translating Timed AltaRica components into timed automata and (ii) an example of the use of priorities for timed specifications. We conclude by some perspectives in section 6.

The proofs of the theorems are given in the appendices (pages 1035-1042).

An Overview of the AltaRica Language

In this section we recall some basics of AltaRica [START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF][START_REF] Arnold | The AltaRica formalism for describing concurrent systems[END_REF] and give an example of an AltaRica specification:the train-gate-controller [START_REF] Bérard | Systems and Software Verification. Model-Checking Techniques and Tools[END_REF]. In this example, the aim is to keep the gate closed when a train is in a critical section. We will use three AltaRica components to model the system and describe how they synchronize.

Specifying Reactive Systems in AltaRica

A specification in AltaRica is a node. A node is a hierarchical description. It can be built from sub-nodes and so on. A node that contains no sub-nodes is a component. A node is basically composed of:

• the variables definitions (type, range, . . . ), and events definitions,

• the transition relation,

• the initial constraint and global constraint. etat=0 |-approach -> 7:

etat := 1, n := 1; 8:

etat=1 |-in -> etat := 2; 9:

etat=2 |-exit -> etat := 0, n := 0; 10: init 11:

etat:=0, n:=0; 12: assert 13:

N=n; 14: edon

Components

In the example of Fig. 1, we define a component1 train to model the behaviour of a train in two equivalent manners in order to ease the understanding: an AltaRica description (see Fig. 1(a)) and a standard automaton (see Fig. 1(b)). A train is either Far of the critical section, or Before or On meaning it is respectively near or inside the critical zone. In the AltaRica specification, the variable etat (line 4) ranging in [0, 2] represents the locations Far, Before, On of the train. The events of the component TRAIN are approach, in and exit (line 3). We also use a state variable n (line 4) to denote that the train is in {Before, On}. Initially the component is in configuration etat=0,n=0,N=0 (line 11), written (0, 0, 0) for short. When a transition occurs the values of the state variables change accordingly as well as the value of the flow variable in order to satisfy the assertion (line 13). For instance, when event approach occurs in (0, 0, 0) the configuration (1, 1, 1) is reached.

Interfaces

The component's state variables are not visible from outside of the component. Their scope is thus the component itself just as for usual programming languages. To allow sharing of information and synchronization on variables of other components one can use flow variables. Flow variables can be read by other nodes. The part of the component which is visible by other components is called the interface.

It consists in the events of the components and the flow variables.

The flow variable N is in the interface of the node TRAIN (line 2). This means that other nodes can read it and use the value of N. The value of the flow variable N is constrained to be equal to n at anytime (see the assert line 13) and the purpose of N is to make the value of n available outside.

Assume another node for the controller is given by the AltaRica specification of Fig. 2(a). A transition of the form etat = 1 |-approach -> ; (line 9) means that approach does not bring about any change in the state variables values (but not this is a deadlock!). In the component CONTROLLER the purpose of the flow variable N (referred to as CONTROLLER.N from now on) is to count the total number of trains in the region {Before, On} (if we assume there are many train components). Depending on the value of the flow CONTROLLER.N the controller will make the gate go up on an exit signal (if the value is 1, line 8) or will leave the gate closed if CONTROLLER.N > 1 (line 7).

The value of CONTROLLER.N may change on any discrete transition and be assigned any integer as no assertion constrains this flow in the node CONTROLLER. Apart from the events listed in the component's events section (line 3), we assume a special discrete event for synchronization purposes. This event is enabled in any configuration and does not change the values of variables of type state. Nevertheless flow variables can be updated on transitions with values satisfying the assertion. As the assertion of the node CONTROLLER is implicitely true the variable CONTROLLER.N may be assigned any integer value on an transition. This somewhat strange behavior will become clear when we introduce hierarchical nodes and constraints among flows of different nodes (see assert line main-assert on Fig. 3).

As for the node GATE (Fig. 2(b)) it consists in receiving orders from the controller (events Go_up and Go_down) and after a while2 to actually go up or down (events up and down).

Hierarchy and Synchronization

As emphasized in the introduction, one can describe a system by composing and building new nodes from sub-nodes. For example we can define a node Main (see Fig. 3) specifying the train-gate-controller with two trains. Indeed nodes can be instantiated and used as templates to build higher-level nodes. The node of Fig. 3 is composed of four instantiated sub-nodes (t1, t2, g and c, see Fig. 3, lines 2-5) which interact in two ways: flow coordination and synchronization of events. The synchronization constraint (after keyword sync, lines 6-14) reads as follows: if a component does not appear in a synchronization vector, it is assumed to do the action. Note that events up and down are not synchronized and thus they will be assumed to be synchronized with transitions of the other components. Finally the global assertion, line 15, constrains the flow variables so that N of the node MAIN is always equal

1: node CONTROLLER 2:
flow N : [0,p]; 3: event approach, exit, Go_up, Go_down; to the number of trains on the critical section. A joint move of the components t1,t2,g,c can be <t1.approach,t2.approach,c.approach> (see line 7) in which case the variable c.N will be updated on the move of component c to satisfy the assertion of node MAIN i.e. c.N=t1.N+t2.N. This is why we need to have the possibility to update flow variables on transitions. Anyway a meaningful specification should be such that all flow variables are constrained at least in the outermost node. Note that some constraints could be unsatisfiable: for instance if we add t1.N=2+t2.N to the assert line, this clearly can not be satisfied and the resulting system has no configuration. It is also possible to constrain the state space: if we use t1.N=t2.N we impose that the two trains issue approach at the same time and leave the critical section at the same time (event exit). This is due to the fact that no configuration with t1.N not equal to t2.N is satisfiable hence no transition with only one approach event can be fired.

Formal Semantics of AltaRica

The semantics of AltaRica specifications is given by Interfaced Transition Systems. For a detailed presentation of these notions the reader is referred to [START_REF] Arnold | The AltaRica formalism for describing concurrent systems[END_REF][START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF].

Interfaced Transition Systems Definition 2.1. (Interfaced Transition system [10])

An interfaced transition system (ITS) is a tuple A = E, F, S, π, T with:

1. E = E + ∪ {ε} is a finite set of events such that ε ∈ E + ; 2. F is a set of flow values;
3. S is the set of states; 4. π : S → 2 F associates to each state s in S all the admissible flow values in s. We assume ∀s ∈ S, π(s) = ∅.

5.

T ⊆ S × F × E × S is the transition relation and satisfies:

(a) (s, f, e, s ) ∈ T ⇒ f ∈ π(s) (b) ∀s ∈ S, ∀f ∈ π(s), (s, f, ε, s) ∈ T A configuration of an ITS is a pair (s, f ) ∈ S × F such that f ∈ π(s)
. Every tuple (s, f, e, s ) ∈ T corresponds to the set of transitions ((s, f ), e, (s , f )) between configurations s.t. f ∈ π(s ).

Remark 2.1. In AltaRica, if a transition (s, f, e, s ) is firable then there exists a configuration (s , f ) (as item 4 of Def. 2.1 assumes π(s) is not empty for s ∈ S). This remark will carry over timed ITS. The set F may be considered as a set of properties (or observations) associated to the states by the mapping π. Also note that T is a shorthand for the explicit transition relation T between configurations with

T ⊆ S × F × E × S × F and (s, f, e, s , f ) ∈ T ⇐⇒ (s, f, e, s ) ∈ T ∧ f ∈ π(s ).

Priorities

In AltaRica we can constrain the behaviours of a system by giving priorities to some transitions when more than one is possible. For instance, this concept is classical in scheduling [START_REF] Sifakis | Compositional specification of timed systems[END_REF]. Formally, a priority relation < is a strict partial order over the events. A transition labelled e can be fired from a configuration (s, f ) if it is maximal, i.e. no other transition e such that e < e is firable in (s, f ).

Definition 2.2. (Priority relation [10])

A priority relation over E is a strict partial order over E such that ∀v ∈ E + , v < ε and ε < v (with

E + = E \ {ε}).

Definition 2.3. (Priority Restriction Operator)

Let A = E, F, S, π, T be an ITS and < a priority relation over E. We define the priority restriction operator for the transition relation T ⊆ S × F × E × S and the priority relation < by: (s, f, e, s ) ∈ T < ⇐⇒ (s, f, e, s ) ∈ T ∧ ∀e ∈ E , (∃s ∈ S | (s, f, e , s ) ∈ T ) =⇒ e < e .

Formulas and Expressions

We consider hereafter the expressions E(X) built over the variables in a set X. These expressions can be either integer terms, boolean terms etc. The only thing we assume is that the variables in X take their values in a set D. A valuation ν of a set of variables X is a mapping ν : X → D and the set of valuations of X is denoted D X . The value of an expression e ∈ E(X) in the context ν : X → D is denoted e(ν). Given a set E(X) we can define the set F(X) of first order formulas over E(X) using some suitable predicates (e.g. ≤, = in the case of integer expressions) and the existential and universal quantifiers. For f ∈ F(X) we denote free(f ) the set of free variables in f . We assume that tt (true) and ff (false) which are predicates of arity 0 belong to F(X). In the sequel we often omit the base set X when we use F(X) as only the free variables used in a formula f ∈ F(X) are relevant.

The interpretation f of a formula f ∈ F(X) with free(f ) ⊆ X is a subset of D X : f ⊆ D X . Also we have tt = D X and ff = ∅.

An assignment for the variables in X is a mapping a : X → E(X). Intuitively an assignment of the form x := y + z + 2 will be defined by a(x) = y + z + 2. Given a valuation ν : X → D, we denote by a(ν) the valuation defined by a(ν)(x) = a(x)(ν). We denote by Id the identity assignment such that ∀x, Id(x) = x. Now we define an abstract syntax for the AltaRica components and nodes again taken from [START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF].

AltaRica Components

AltaRica components give an abstract syntax for the basic systems (no hierarchy) introduced in the previous section.

Definition 2.4. (Component)

A component is a tuple C = V S , V F , E, A, M, < with:

1. V S , V F are finite sets for respectively state variables, flow variables, with the property of being 2 by 2 disjoint. We denote V T = V S ∪ V F ;

2. E = E + ∪ {ε} is a finite set of events and as usual ε is the empty action;

3. A ∈ F is an assertion such that free(A) ⊆ V C ; 4. M ⊆ F×E×E(V C ) V S
is a macro-transition relation such that (tt, ε, Id) ∈ M and every (g, e, a) ∈ M satisfies:

(a) g ∈ F is a guard such that free(g) ⊆ V C , (b) e ∈ E + is the event of the transition, (c) a : V S → E(V C
) is an assignment for the variables in V S , 5. < is a priority relation.

Remark 2.2. In [START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF], another set of flow variables is defined: it corresponds to unobservable flow variables that can be used as intermediary variables. We omit them in this work as they do not increase the expressiveness of the language. Indeed they can be defined as existentially quantified flow variables in the assertion of a node. Now we can define the semantics of a component to be an ITS. For the semantic definitions, we assume that all variables in V S ∪ V F have a common domain D.

Definition 2.5. (Semantics of Components)

Let C = V S , V F , E, A, M, < be a component. The semantics of C is the interfaced transition system C = E, F, S, π, T constructed in the following way:

1. F = D V F ; 2. S = {s ∈ D V S | ∃f ∈ D V F | (s, f ) ∈ A }; 3. π : S → 2 F such that π(s) = {f | (s, f ) ∈ A }; 4. T ⊆ S × F × E × S is given by T = M < with: (a) let t = (g, e, a) ∈ M , then t = {(s, f, e, s ) | (s, f ) ∈ A ∧ g ∧ s = a(s, f )}, (b) M = ∪ t∈M t .
Note that because of item 4 above the requirement π(s) = ∅ for ITS is always fulfilled.

AltaRica Nodes

A node is built from n nodes. The purpose of nodes is to give a semantics to hierarchical definitions and synchronization in AltaRica.

Definition 2.6. (Node)

A node is a tuple

N = V F , E, <, N 0 , • • • , N n , V with: 1. V F is a set of flow variables,
2. E = E + ∪ {ε} is a finite set of events, 3. < is a priority relation over E, 4. for all i ∈ [1, n], N i is a component or a node; V F i is the set of flow variables of N i and E i the set of events. We assume ∀i

= j ∈ [1, n], V F i ∩ V F j = ∅, 5
. N 0 is a special component called the control component. The set of events of N 0 is E 0 = E and the priority relation of N 0 is the empty relation. The set of flow variables of

N 0 is V F 0 = V F ∪ V F 1 ∪ V F 2 ∪ • • • ∪ V Fn , 6. V = V d ∪ V imp
is the set of specified synchronization vectors: n+1] where

• V d ⊆ E ? 0 × • • • × E ? n × 2 [0,
E ? i = E i ∪ {?e|e ∈ E i+ }; we define E i d by: e ∈ E i d if ∃ • • • , x i , • • • ∈ V d with x i ∈ E ? i ; E i d corresponds
to the set of events of node i that are synchronized; V d induces a set of synchronization vectors (see below). The last component in 2 [0,n+1] constrains the sets of "?"-events in the nodes that need to participate in the synchronization (see below).

• V imp ⊆ E 0 × • • • × E n × {∅} is the set of implicit synchronization vectors with: -ε, • • • , ε, ∅ ∈ V imp , -∀i ∈ [0, n], ∀e i ∈ E i \ E i d , ε, • • • , e i , • • • , ε, ∅ ∈ V imp .
V imp contains all the synchronization vectors with non synchronized events.

An example of how V d generates synchronization vectors can be given by the node MAIN of Fig. 3. Assume in this node, we replace the line 7by <t1.approach?,t2.approach?,c.approach> >= 1. The meaning of this new specification is that it induces the set of synchronization vectors in which more than 1 (given by the >=1 constraint) event qualified with a "?" appears. Thus <c.approach> is not an allowed vector whereas <t1.approach,c.approach>, <t2.approach,c.approach> and <t1.approach,t2.approach,c.approach> are allowed. The unfolding of the following constrained vector <t1.approach?,t2.approach?,c.approach> >= 1 contains only the three allowed vectors defined above. Note that our definition involving subsets of [0, n + 1] allows us to specify more precise vectors than the one given by the number of "?"-events that have to be present. The synchronization set V generates a set of synchronization vectors of E 0 × E 1 × • • • × E n together with a priority relation on them 3 . As already mentioned, a vector of the form <t1.approach?,t2.approach?,c.approach> >= 1 generates all the synchronization vectors containing at least one event the name of which is qualified by a "?". The priority relation for those vectors corresponds to giving priority to the one with the maximal number of "?"-events occurring in the vector: in the previous case <t1.approach,c.approach> and <t2.approach,c.approach> are both strictly lower (have less priority) than the 3-component vector <t1.approach,t2.approach,c.approach>. In this case, each time both t1.approach and t2.approach are simultaneously enabled this priority relation imposes they are fired at the same time. Thus this specification rules out the behaviours where only one of these transitions is fired whereas the other is enabled. We do not want to constraint the system in such a way and approach events cannot be constrained in the specification. This is why we have given three distinct synchronization vectors involving event approach and they are independant from each other.

Finally, the set V imp consists of all the events that are not involved in any synchronization: they must occur on their own, hence the synchronization vectors of the form ε, • • • , e, • • • , ε (events up and down of components Gate of Fig. 2(b)).

For a formal definition of how to generate the synchronization vectors corresponding to V the reader is referred to [START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF]. We only need here to consider the set of synchronization vectors and the priority relation generated by V .

In the definition of the timed nodes (section 3.6) we will focus on timed features and will consider that V has been "unfolded" into the set of synchronization vectors V it generates and the priority relation < e

V it induces, i.e. we will use

V ⊆ E 0 × E 1 × • • • × E n and < e V instead of V .
There is a fundamental result about nodes: they can be rewritten (syntactically) into components that preserve their semantics [START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF].

Theorem 2.1. ([10, 11])

If N is an AltaRica node, C N its rewriting into a component (as defined in [START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF]), then N and C N are bisimilar.

In the next section we focus on extending ITS, AltaRica components and nodes with time. We define our timed extension on these objects. Also we show that the results obtained in the untimed case [START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF][START_REF] Arnold | The AltaRica formalism for describing concurrent systems[END_REF] still hold (e.g. Theorem 2.1).

Timed Extension of AltaRica

Our aim is to build a timed extension of AltaRica, which means we need to keep the framework defined for the untimed case: ITS, priorities and components. First we extend ITS into Timed ITS (see Def. 3.1) and define timed priorities. Then we add timing constraints to components (i.e. clock variables) and give the semantics of timed components into TITS. Finally we define timed nodes, give their semantics and prove that they can be syntactically rewritten into an equivalent (timed bisimilar) component.

Preliminaries about Timed Systems

Before defining Timed AltaRica we recall some basics about timed systems [START_REF] Larsen | Compositional and Symbolic Model-Checking of Real-Time Systems[END_REF]. More precisely we use the framework of timed automata [START_REF] Alur | A theory of timed automata[END_REF] and the associated usual notations. The real-valued variables will be clocks: a clock is a positive real valued variable, and it evolves at a constant rate w.r.t. physical time.

Clock valuations and assignments.

A clock valuation for the clocks in a set X is a mapping v : X → R ≥0 that assigns a positive real value to each clock in X. A clock assignment is a mapping a : X → E(X). For decidability reasons, we will restrict the allowed assignment expressions in section 4.4 to simple assignments given by table 2, page 1030. We denote by A(X) the set of clock assignments. As defined in subsection 2.2.3, for a clock valuation v and an assignment a, we denote a(v) the clock assignment a(v)(x) = a(x)(v). For t ∈ R ≥0 the clock valuation v+t is defined by ∀x ∈ X, (v+t

)(x) = v(x) + t.
The set of clock constraints B(X) over a set X of clocks is defined inductively by:

g := x r| x -y r |g ∧ g |g ∨ g (1)
with x, y ∈ X, ∈ {<, <, >, ≥, =}, r ∈ Q. Also we denote by B C (X) the subset of B(X) that defines convex clock constraints. A clock constraint g is a particular formula and evaluates either to tt or ff : g ⊆ R X ≥0 and g(ν) = tt ⇐⇒ ν ∈ g .

Timed Transition Systems and Timed

Automata. A timed transition system [23] (TTS) is a tuple (Q, E, Q 0 , →), where Q is set of locations, E is the set of actions, Q 0 is the set of initial states, →⊆ Q × (E ∪ R ≥0 ) × Q. A timed automaton [17] is a tuple (L, L 0 , E, X, I, T ) such that L is a (finite) set of locations, X is a finite set of clocks, L 0 is s.t. L 0 ⊆ L × R X ≥0 is a predicate that defines the set of initial states, E is a finite set of actions, T ⊆ L × (B(X) × E × A(X)) × L is the transition relation, I : L → B C (X) is the invariant constraint.
The semantics of a timed automaton (L, L 0 , E, X, I, T ) is given by a TTS

(L × R X ≥0 , E, Q 0 , →) where Q 0 = L 0 and ∀(l, v) ∈ L × R X ≥0 the transition relation → is defined by: i) discrete steps of the form (l, v) e -→ (l , v ) if ∃(l, g, e, a, l ) ∈ T, such that g(v) = tt, v = a(v), v ∈ I(l ) , ii) continuous steps of the form (l, v) δ -→ (l, v ), δ ∈ R ≥0 if ∀δ ≤ δ, v + δ ∈ I(l) .
A very useful result about timed automata (actually updatable timed automata [START_REF] Bouyer | Are timed automata updatable ?[END_REF]) is that reachability is decidable [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Bouyer | Are timed automata updatable ?[END_REF] for this class of timed systems. Hence automatic verification tools have been designed to analyse timed automata, and among them UPPAAL [START_REF] Pettersson | UPPAAL2k[END_REF], KRONOS [START_REF] Bozga | Kronos: A model-checking tool for real-time systems[END_REF] and CMC [START_REF] Laroussinie | CMC: A tool for compositional model-checking of real-time systems[END_REF]. We will give in the last section a translation from a Timed AltaRica specification into a timed automaton. This will allow us to use UPPAAL [START_REF] Pettersson | UPPAAL2k[END_REF] or KRONOS [START_REF] Bozga | Kronos: A model-checking tool for real-time systems[END_REF] or CMC [START_REF] Laroussinie | CMC: A tool for compositional model-checking of real-time systems[END_REF] to check timed properties on the designed systems.

In the sequel, we define Timed Interfaced Transition Systems (TITS) that are extended TTS. The timed extension of AltaRica components are timed components that are the counter parts of timed automata: the semantics of timed components is given by TITS.

Timed Interfaced Transition Systems

Timed Interfaced Transition Systems are an extension of ITS with real-valued variables and flows.

Definition 3.1. (Timed Interfaced Transition System)

A timed interfaced transition system (in the sequel TITS) of continuous dimension (n, m) and time domain 4 T is a tuple A = E t , F t , S t , π, T with: 3. S t ⊆ S × R n is the set of states where S is the set of discrete states and R n is the set of continuous states;

1. E t = E + ∪ {ε} ∪ T where E + is a finite set of events such that ε ∈ E + ∪ T and E + ∩ T = ∅; 2. F t ⊆ F × R m is
4. π : S t → 2 Ft associates to each state q ∈ S t all the admissible flow values in q. We assume ∀q ∈ S t , π(q) = ∅.

5. T ⊆ S t × F t × E t × S t × F t is the transition relation and satisfies: (a) (q, g, e, q , g ) ∈ T ⇒ g ∈ π(q) ∧ g ∈ π(q ) (b) ∀q ∈ S t , ∀g, g ∈ π(q) we have (q, g, ε, q, g ) ∈ T (c) ∀q ∈ S t , ∀g ∈ π(q) we have (q, g, 0, q, g) ∈ T A configuration of a TITS is a pair ((s, ν), (f, µ)) ∈ S t × F t such that (f, µ) ∈ π(s, ν).
Remark 3.1. Compared to item 5 of Def. 2.1, we need to be more precise when defining the set of transitions of a TITS. Indeed we want to enforce discrete variables to remain unchanged when time elapses. Assume we define the transition relation T in the same way as it was in defined item 5 of Def. 2.1: T ⊆ S t × F t × E t × S t . Then we will not be able to leave discrete flow values unchanged during a delay transition when we define the semantics of AltaRica timed components (Def. 3.7): in the target configuration, we can only constrain the state variables in S t and not the flow variables in F t . Thus we prefer to define T over S t × F t × E t × S t × F t which enables us to refer to the source and target flow values of a transition as in item 5.(c) of Def. 3.1.

Also note the following properties: if n = 0 and m = 0 and T = {0} we obtain the definition of ITS. Indeed as pointed out in remark 2.1, we can give the definition of the transition relation of an ITS in terms of transitions between configurations. If m = 0 and we add an initial state to the TITS then we obtain the definition of TTS: F is to be interpreted as the set of atomic properties. It is possible to consider an integer time domain, T = N. Notice that in this case even if we allow only integer time steps in the TITS, the values of the clocks can be in R ≥0 . For a dense time domain T = Q ≥0 is suitable. For a continuous time domain one can take T = R ≥0 . In the following we assume the time domain is R ≥0 when we deal with Timed AltaRica nodes.

Timed Bisimulations

In the sequel we will use the notion of timed bisimulations between timed systems. We define it for TITS extending the definition of interfaced bisimulation of [START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF]:

Definition 3.2. (Timed Interfaced Bisimulation) Let A 1 = E t , F t , S 1t , π 1 , T 1 and A 2 = E t , F t , S 2t , π 2 , T 2 be two TITS. A timed interfaced bisimu- lation relation for A 1 and A 2 is a relation R ⊆ S 1t × S 2t that satisfies 4 conditions: 1. ∀q 1 ∈ S 1t , ∃q 2 ∈ S 2t s.t. (q 1 , q 2 ) ∈ R and ∀q 2 ∈ S 2t , ∃q 1 ∈ S 1t s.t. (q 1 , q 2 ) ∈ R, 2. ∀(q 1 , q 2 ) ∈ R, π 1 (q 1 ) = π 2 (q 2 ), 3. ∀(q 1 , g, e, q 1 , g 1 ) ∈ T 1 , ∀q 2 ∈ S 2t such that (q 1 , q 2 ) ∈ R then ∃(q 2 , g, e, q 2 , g 2 ) ∈ T 2 s.t.
(q 1 , q 2 ) ∈ R, 4. ∀(q 2 , g, e, q 2 , g 2 ) ∈ T 2 , ∀q 1 ∈ S 1t such that (q 1 , q 2 ) ∈ R then ∃(q 1 , g, e, q 1 , g 1 ) ∈ T 1 s.t.

(q 1 , q 2 ) ∈ R.

Two TITS are timed bisimilar iff there exists a timed interfaced bisimulation relation on their set of states.

In the sequel we use the term timed bisimulation instead of timed interfaced bisimulation. Like in the untimed case, an interfaced bisimulation can be expressed as an homomorphism between two TITS.

Definition 3.3. (Timed Interfaced Bisimulation Homomorphism)

Let A 1 = E t , F t , S 1t , π 1 , T 1 and A 2 = E t , F t , S 2t , π 2 , T 2 be two TITS. A timed interfaced bisimu- lation homomorphism h : A 1 → A 2 is a mapping h : S 1t → S 2t such that: 1. h is surjective, 2. ∀q 1 ∈ S 1t , π 1 (q 1 ) = π 2 (h(q 1 )),
3. ∀(q 1 , g, e, q 1 , g 1 ) ∈ T 1 , ∃g 2 such that (h(q 1 ), g, e, h(q 1 ), g 2 ) ∈ T 2 , 4. ∀q 1 ∈ S 1t , ∀q 2 ∈ S 2t s.t. (h(q 1 ), g, e, q 2 , g 2 ) ∈ T 2 then ∃q 1 ∈ S 1t such that h(q 1 ) = q 2 and ∃g 1 ∈ π 1 (q 1 ) such that (q 1 , g, e, q 1 , g 1 ) ∈ T 1 .

We use the term timed bisimulation homomorphism as a shorthand for timed interfaced bisimulation homomorphism.

The following theorem is an extension to TITS of previous results on ITS and follows from [START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF][START_REF] Arnold | Finite transition systems[END_REF]:

: A 2 → B.
The proof is given in Appendix A.1.

Timed Priorities

In the untimed version of AltaRica, priorities among events play an important role [START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF]: they allow the easy modeling of priorities among concurrently enabled transitions. It is natural in a timed setting to try and introduce timed priorities i.e. priorities among transitions involving some timing information. Again we want to extend the existing AltaRica specification language and add timed priorities. Timed priorities in timed systems have been introduced for timed automata [START_REF] Bornot | On the composition of hybrid systems[END_REF] and a comprehensive study of timed priorities can be found in [START_REF] Bornot | On the construction of live timed systems[END_REF][START_REF] Bornot | Modeling urgency in timed systems[END_REF][START_REF] Bornot | An algebraic framework for urgency[END_REF]. The most common timed priority is urgency [START_REF] Sifakis | Compositional specification of timed systems (extended abstract)[END_REF]: basically, it says that if a transition is enabled in a timed automaton, time can not elapse and this transition must be fired immediately. Without loss of expressiveness we define urgent events: if an event in a Timed AltaRica specification is urgent then all the transitions labelled by this event are urgent. We then extend Def. 2.2 to allow priority between time labels (in T) and discrete events:

Definition 3.

(Simple Timed Priority Relation)

A simple timed priority relation < over E is a strict partial order over E ∪ {time} such that < is a priority relation over E and a strict partial order over E time

+ with E time + = E + ∪ {time} and ∀v ∈ E + , v < time.
Then a > time means5 that event a is urgent and has to be fired immediately when enabled (a semantic definition of priorities will appear later in this section in Def. 3.6). Also note that if a > time and b > a then b > time: the urgency of event a entails urgency of greater events.

This allows us to model what is called eagerness in [START_REF] Sifakis | Compositional specification of timed systems (extended abstract)[END_REF]: an eager transition is one that forbids time elapsing if it is enabled. In the papers [START_REF] Bornot | On the construction of live timed systems[END_REF][START_REF] Bornot | Modeling urgency in timed systems[END_REF] other notions of priorities are defined: (i) a delayable transition is one that can be fired when its guard is true and before a certain deadline; (ii) a lazy transition is one that has no deadline (it may or may not be fired). We will add in Def. 3.7 (time) guards into Timed AltaRica components which will enable us to define lazy transitions. It is proved in [START_REF] Bornot | Modeling urgency in timed systems[END_REF] that a delayable transition can be encoded using lazy an eager transitions. As we already know (Def. 3.4) how to define eager transitions, we are able to express the three types of priorities proposed in [START_REF] Sifakis | Compositional specification of timed systems (extended abstract)[END_REF].

More elaborate ways of prioritising transitions are given in [START_REF] Bornot | On the construction of live timed systems[END_REF]. The aim is to express priority between events when several are enabled by using timing information. It is an extension of the priority relation notion: we want to express that e < e only if e will not be enabled in some future. Intuitively, we will write e < 5 e for: the transition labelled e , if enabled within 5 time units, has priority over e. We now extend the notion of simple timed priority relation:

Definition 3.5. (Timed Priority Relation) A timed priority relation < over E is a 3-ary relation in E time + × (N ∪ {∞}) × E time +
satisfying the following conditions (we denote a 1 < k a 2 for (a 1 , k, a 2 ) ∈<):

• the binary relation < 0 is a simple timed priority relation,

• a < k b ∧ a = time =⇒ k = 0, • ∀k ∈ N, < k is a strict partial order, • a 1 < k a 2 =⇒ ∀k < k, a 1 < k a 2 .
Remark 3.2. Notice that in [START_REF] Bornot | On the construction of live timed systems[END_REF], another condition can be imposed on < (a transitivity condition). This condition is related to the building of live timed systems and is not relevant in our setting. It is aimed at preserving liveness in the systems and can then add new behaviors. We do not want to build live timed systems but only to provide a restriction operator (by giving priorities) that restricts the set of behaviors of the system. Note also we restrict the bounds to N which in theory is enough for specifying timed systems.

The static priority of AltaRica coincides with the particular timed priority where all the delays are equal to zero, i.e. k = 0.

As in section 2.2.2, we define the timed priority restriction operator.

Definition 3.6. (Timed Priority Restriction Operator)

Let A = E t , F t , S t , π, T be a TITS of continuous dimension (m, n), time domain T and < a timed priority relation over E. We define the timed priority restriction operator for the transition relation T ⊆ S t × F t × E t × S t × F t and the timed priority relation < by: (q, g, e, q , g ) ∈ T <⇔ (q, g, e, q , g )

∈ T ∧                if e = t ∈ T, ∀t ∈ T, t < t, if (q, g, t , q , g ) ∈ T
then ∀e ∈ E + , (q , g , e , q , g ) ∈ T =⇒ time < 0 e .

otherwise if (q, g, t, q , g ) ∈ T, t ∈ T, t ≤ k, then ∀e , (q , g , e , q , g ) ∈ T =⇒ e < k e .

We denote A < = E t , F t , S t , π, T < . We can lift the following theorem for ITS stated in [START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF] to TITS:

Theorem 3.2

. (Priority and Timed Bisimulation)

Let A 1 = E t , F t , S 1t , π 1 , T 1 and A 2 = E t , F t , S 2t , π 2 , T 2 be two TITS and < a timed priority relation over E. If h : A 1 -→ A 2 is a timed bisimulation homomorphism then h : A 1 < -→ A 2 < is also a timed bisimulation homomorphism.
The proof is given in appendix A.2.

Timed Components

Timed AltaRica components are the timed extensions of AltaRica components (see Def. 2.4). Our extension consists in adding clocks to AltaRica components. Hence our model is closely related to the timed automaton model. Adding real-valued variables instead of clocks is quite straightforward: the resulting model is then close to the hybrid automaton model. In this paper we focus on the timed extension and the addition of clocks. We consider the formulas F, expressions E and set of values D settled in section 2.2.3.

Definition 3.7. (Timed Component)

A timed component is a tuple

T = V S ∪ C S , V F ∪ C F , E, A, M, < with:
1. V S , V F are finite sets for respectively state variables, flow variables with the property of being disjoint. We denote V T = V S ∪ V F ; C S , C F are finite sets for respectively clock variables, real flow variables with the property of being disjoint. We denote C T = C S ∪ C F ; also we assume

V T ∩ C T = ∅;
2. E = E + ∪ {ε} where E + is a finite set of events and as usual ε is the empty action; Notice that the semantics of A is a subset of (D

3. A = A V T ∩ A C T ∈ F is an assertion such that free(A) ⊆ V T ∪ C T ; A V T ∈ F, free(A V T ) ⊆ V T . A C T = k∈K P k =⇒ I k where K is a finite set of indices, P k ∈ F, free(P k ) ⊆ V T , I k ∈ F, free(I k ) ⊆ C T and I k defines a convex region of R p if |C T | = p; 4. M ⊆ (F × B(C T )) × E × (E(V T ) V S × A(C T )) is a macro-transition relation such that every ((g, γ), e, (a, R)) ∈ M satisfies: (a) (g, γ) is a guard such that g ∈ F and free(g) ⊆ V T ; γ ∈ B(C T ); (b) e ∈ E is the event of the transition; (c) a : V S → E(V T ) is an assignment for the variables in V S . R ∈ A(C T )
V S × R n ) × (D V F × R m )
Let T = V S ∪ C S , V F ∪ C F , E, A, M, < be a timed component. Let |C S | = n and |C F | = m.
The semantics of T over the time domain T is the timed interfaced transition system T = E t , F t , S t , π, T of dimension (n, m) constructed in the following way:

1.

E t = E ∪ T, 2. F t = D V F × R m ,
S t = {(s, ν) ∈ D V S × R n ≥0 |∃(f, µ) ∈ D V F × R m | ((s, ν), (f, µ)) ∈ A }, 4. π : S t → 2 Ft such that π(q) = {(f, µ)| (q, (f, µ)) ∈ A }, 5. T ⊆ S t × F t × E t × S t × F t and T = M < with:
(a) let t = ((g, γ), e, (a, R)), define t by:

((s, ν), (f, µ), e, (s , ν ), (f , µ )) ∈ t if            ((s, ν), (f, µ)) ∈ A ∧ g ∧ γ ∧s = a(s, f ) ∧ ν = R(ν, µ) ∧ (f , µ ) ∈ π(s , ν )
with R(ν, µ) the new clock assignment after resetting the variables in R.

(b) let δ ∈ T, define δ by:

((s, ν), (f, µ), δ, (s, ν ), (f, µ )) ∈ δ if      ((s, ν), (f, µ)) ∈ A ∧ν = ν + δ ∧ ((s, ν ), (f, µ )) ∈ A ∧∀δ ≤ δ, ∃µ δ | (ν + δ , µ δ ) ∈ I(s, f ) with I(s, f ) = k∈K|(s,f )∈P k I k . (c) M = ∪ t∈M t ∪ δ∈T δ .
Remark 3.5. Note that I(s, f ) is a convex set as it is a conjunction of convex sets. We have not used this property of I(s, f ) in the semantics of components as it is not required in this definition. Anyway in the sequel we will need this assumption and this is why we have put it in Def. 3.7 of timed components. The delay transitions in the semantics of a timed components leave the "continuous" flows free to take any value as long as the invariant I(s, f ) is satisfied. This is rather permissive as the values encountered along a delay transition could even be non continuous. For instance a constraint on a flow like x ≤ Y ≤ x+2 where x is a clock and Y a continuous flow would allow Y to take any value between x and x + 2 at each time point. If we define flow to be clock we constrain the set of equations we can write in the assertion. Indeed equations like Y = 2x could not be defined with a "clock" Y . So far we stick to this permissive definition and we will tackle later which kind of flows can be "implemented" (see section 4.4).

Finally in the case C F = ∅ we obtain the definition of timed automata (again if we add an initial state); the semantics of such a timed component is then a TTS (again V F is to be interpreted as some properties or observations on each state.)

As for the untimed case we have the following lemma:

Lemma 3.1. Let T = V S ∪ C S , V F ∪ C F , E, A, M, < be a timed component and < is a timed priority priority relation. Then V S ∪ C S , V F ∪ C F , E, A, M, < = V S ∪ C S , V F ∪ C F , E, A, M, ∅ <.
The proof is straightforward from Def. 3.6 and Def. 3.8.

Timed Nodes

Timed nodes are straightforward extensions of nodes. Indeed, if we assume as stated in Def. 2.6 of a node, that the synchronization constraint is expanded, the new constraint added by the time transitions is trivial: the synchronized time transitions for n nodes are of the form (δ, δ, • • • , δ), δ ∈ T where T is the time domain and they do not need to be specified.

Definition 3.9. (Timed Node)

A timed node is a tuple

N = V F , C F , E, <, N 0 , • • • , N n , ( V , < e V ) with:
1. V F is a set of flow variables, 2. C F is the set of real flow variables,

3. E = E + ∪ {ε} is a finite set of events, 4. < is a timed priority relation over E, 5. for all i ∈ [1, n], N i is a timed component or a timed node; the interface of the node is composed of (i) V F i ∪ C F i , the set of discrete flows and real flows of N i and (ii) E i the set of events of N i .

We assume ∀i

= j ∈ [1, n], V F i ∩ V F j = C F i ∩ C F j = ∅, 6
. N 0 is a special timed component called the control component. The set of events of this node is E 0 = E and the priority relation of N 0 is the empty relation. The set of (discrete) flow variables of

N 0 is V F 0 = V F ∪ V F 1 ∪ V F 2 ∪ • • • ∪ V Fn ,

and the set of real flow variables is

C F 0 = C F ∪ C F 1 ∪ C F 2 ∪ • • • ∪ C Fn , 7. V ⊆ E 0 × E 1 × • • • × E n is
Let N = V F , C F , E, <, N 0 , • • • , N n , ( V , < e
V ) be a timed node and

N i = E it , F it , S it , π i , T i of dimension (n i , m i ) for i ∈ [0, n].
The semantics of N is the timed interfaced transition system N = E t , F t , S t , π, T of dimension ( n k=0 n i , |C F |) defined by:

1.

E t = E ∪ T, 2. F t = D V F × R m , with m = |C F |,
3. for q i ∈ S it , let q = (q 0 , q 1 , • • • , q n ), then

π(q) = {(f, µ) ∈ D V F × R m | ∀i ∈ [1, n], ∃η i ∈ π i (q i ) | ((f, µ), η 1 , η 2 , • • • , η n ) ∈ π 0 (q 0 )} 4. S t = {q ∈ S 0t × S 1t × • • • × S nt | π(q) = ∅}; 5. T ⊆ S t × F t × E t × S t × F t is defined by:
(a) let < 0 be the timed priority relation defined by:

(e 0 , e 1 , • • • , e n ) < 0 (e 0 , e 1 , • • • , e n ) ⇐⇒ e 0 < e 0 (b) let e = (e 0 , e 1 , • • • , e n ) ∈ E 0 × • • • × E n ∪ {(δ, • • • , δ)}, s = (s 0 , s 1 , • • • , s n ) and s = (s 0 , s 1 , • • • , s n ). Define T N by: s, f, e, s , f ∈ T N ⇐⇒      ∃f 0 = (f, f 1 , • • • , f n ) ∈ π 0 (s 0 ) ∃f 0 = (f , f 1 , • • • , f n ) ∈ π 0 (s 0 ) ∀i ∈ [0, n], (s i , f i , e i , s i , f i ) ∈ T i (c) then T = T N < Ṽ < 0 .
We have the node version of lemma 3.1:

Lemma 3.2. Let N = V F , C F , E, <, N 0 , • • • , N n , ( V , < e V )
be a timed node and N its semantics.

Then N = V F , C F , E, ∅, N 0 , • • • , N n , ( V , < e V ) <.
The proof is straightforward from Def. 3.9 and Def. 3.10.

The semantics of nodes is compositional with respect to timed bisimulation:

Theorem 3.3. Let N = V F , C F , E, <, N 0 , • • • , N n , ( V , < e V ) and N = V F , C F , E, <, N 0 , • • • , N n , ( V , < e
V ) be two timed nodes such that ∀i ∈ [0.

.n] there is a timed homomorphism h i from N i to N i . Then there exists a timed homomorphism h from N to N .

The proof is given in appendix A.3. Timed AltaRica is a hierarchical modeling language so that each timed node can be expressed by a timed component. The timed priorities and the synchronization are directly encoded into the resulting timed component. Let N = V F ∪ C F , E, <, N 0 , • • • , N n , ( Ṽ , < Ṽ ) be a timed node, we present the construction (extending the one given in [START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF]) of a timed component E,A,M, < which has the same semantics.

C N = V S ∪ C S , V F ∪ C F ,
First we associate to each timed node a timed component defined as follows:

Definition 3.11. (Symbolic Semantics)

If N = V F ∪ C F , E, <, N 0 , • • • , N n , ( Ṽ , < Ṽ ) is a timed node, with N i = V F i ∪ C F i , E i , < i , N i 0 , • • • , N in , ( Ṽi , < Ṽi ) for 0 ≤ i ≤ n, we denote by C N = V S ∪ C S , V F ∪ C F , E
, A, M, ∅ the timed component constructed as follows:

1. ∀0 ≤ i ≤ n (a) if N i is a timed component, then we define N i = N i < i and the timed priority is syntactically encoded in N i as defined later in section 3.7.2;

(b) if N i is a timed node, then we define N i = C N i the rewriting of N i into a timed component and encode timed priority syntactically as defined in section 3.7.2;

(c) we denote

N i = V S i ∪ C S i , V F i ∪ C F i , E i , A i , M i , ∅ ; 2. V S = V S 0 ∪ • • • ∪ V Sn and C S = C S 0 ∪ • • • ∪ C Sn ; 3. A = (∃ i=1..n (V F i ∪ C F i )). i=0..n A i ;
where the notation ∃ i=1..n (W i ).φ stands for: ∀i, ∃η i ∈ W i such that φ(η i ). For ((s, ν),

(f, µ)) ∈ D V S × R C S × D V F × R C F we define: • ((s, ν), (f, µ)) ∈ A ⇐⇒ ∀i ∈ [1..n], ∃η i ∈ D V F i × R C F i s.t. ((s, ν), (f, µ), η 1 , • • • , η n )) ∈ i=0..n A i , • ∀i ∈ [1..n], ((s, ν), (f, µ), η 1 , • • • , η n )) ∈ A i ⇐⇒ ((s i , ν i ), η i ) ∈ A i .

the set of macro-transitions M ⊆ (F×B(C

T ))×E ×(E(V T ) V S ×A(C T )) is defined by M = (M < e V ) < 0
, where < 0 is the timed priority relation specified in Def. 3.10, and ((g, γ), e, (a, R)) ∈ M if and only if: The proof is given in appendix A.4.

• ∀0 ≤ i ≤ n, there is a transition ((g i , γ i ), e i , (a i , R i )) ∈ M i such that: -g = (∃ i=1..n V F i ).g 0 ∧ • • • ∧ g n , -γ = (∃ i=1..n C F i ) .γ 0 ∧ • • • ∧ γ n , • ∀x ∈ V S ∩ V S i we have a(x) = a i (x) and ∀c ∈ C S ∩ C S i we have R(c) = R i (c), • e = (e 0 , e 1 , • • • , e n ) ∈ V .

Syntactical Timed Priority

In [START_REF] Bornot | On the construction of live timed systems[END_REF] the authors show that it is possible to encode a priority relation by strengthening the guards of a component: this way one can syntactically encode the priority relation.

We tackle this problem in the timed case. Let T = V S ∪ C S , V F ∪ C F , E, A, M, ∅ be a timed component and < be a timed priority relation. We first assume 6 that < contains no urgent events i.e. ∀e ∈ E, time < e. Our aim is to compute the transition relation M < syntactically i.e. by finding new guards that define M <. We first rewrite our timed component so that we are sure that when a guard evaluates to true, the corresponding transition can indeed be fired, i.e. the resulting new state satisfies assertion A. This is done by adding weakest precondition (section 3.7.1) into the existing guards. Then we show how to encode timed priority (section 3.7.2) again by strengthening the guards. Finally we detail how urgency is handled in section 3.7.3.

Weakest Precondition

The key point is to know if a transition ((g, γ), e, (a, R)) can really be fired, and the fact that the guard evaluates to true is not sufficient: a new state can be reached from ((s, ν), (f, µ)), only if after the assignments given by (a, R) π(a(s, f ), R(ν, µ)) = ∅, i.e. there are some admissible flow values. This latter condition depends on assertion A of the timed component and can be seen as a weakest precondition.

First assume we have an untimed component (Def. 2.4). Let t = (g, e, a) be a transition of this component, and

A the assertion. For Q ⊆ S × F , we define Pre t (Q) = {(s, f ) | ∃f | (a(s, f ), f ) ∈ Q}.
Assume Pre t ( A ) can be defined by a formula φ t ∈ F, and free(φ t ) ⊆ V T . Now if we take t = (g ∧ φ t , e, a), we are sure that when g ∧ φ t evaluates to true the transition t can be fired as (s, f ) ∈ g ∧ φ t =⇒ π(a(s, f )) = ∅.

We can extend this to the timed component. For t = ((g, γ), e, (a, R)) we define Pre t (Q) = {((s , ν ), (f , µ )) | ∃f , µ | ((a(s , f ), R(ν , µ )), (f , µ )) ∈ Q}. Assume Pre t ( A ) can be written as φ t ∧ θ t with free(φ t ) ⊆ V T and free(θ t ) ⊆ C T .

Then if we define t = ((g ∧ φ t , γ ∧ θ t ), e, (a, R)), we can ensure that if the guard of t evaluates to true, t can be fired.

Now we show how to encode Pre

t ( A ) into guards of the form (g, γ) with g ∈ F, free(g) ⊆ V T and γ ∈ B(C T ). Assume A = p 1 ∧ p 2 ∧ • • • ∧ p n ∧ (q 1 =⇒ i 1 ) ∧ • • • ∧ (q l =⇒ i l ). Assume Pre t ( A ) is a conjunction of the form 7 p 1 ∧ p 2 ∧ • • • ∧ p k ∧ (q 1 =⇒ i 1 ) ∧ • • • ∧ (q m =⇒ i m ). Let P = p 1 ∧ p 2 ∧ • • • ∧ p k . We can rewrite Pre t ( A ) as 8 : J∪I=[1..m] I∩J=∅ P ∧ j∈J ¬q j ∧ r∈I q r G I,J ∧ r∈I i r Γ I,J
This is a formula of the form p=1..s G p ∧ Γ p with G p ∈ F, free(G p ) ⊆ V T and Γ p ∈ B(C T ). Now we create s transitions from t = ((g, γ), e, (a, R)) defined by:

∀p ∈ [1..s], t p = ((g ∧ G p , γ ∧ Γ p ), e, (a, R))
It remains to replace t by the t p , p ∈ [1.

.s] to build a new timed component and t can be fired in the original component if and only if one of the t p can be fired in the new component (leading to the same values for the state variables.) In the sequel we assume guards have been strengthened so that if a guard evaluates to true then the transition can actually be fired.

Encoding Timed Priority

The Simple Case. Let t = ((g, γ), e, (a, R)) ∈ M . Assume e < k e and there is only one transition t = ((g , γ ), e , (a , R )) ∈ M labelled with e . Then t can be fired from a configuration q only if (g, γ) is true in q and:

1. either g is not true in q, 2. or g is true in q and γ will not be true within k time units.

First we deal with the discrete part of the guard and split the transition t into t 1 and t 2 with:

• t 1 = ((g ∧ ¬g , γ), e, (a, R)) which corresponds to item 1 above;

• t 2 = ((g ∧g , γ), e, (a, R)) which corresponds to item 2 above although γ needs to be strengthened to meet the requirements of item 2 above.

We now show how to strengthen γ in t 2 . A useful operator was introduced in [START_REF] Bornot | Modeling urgency in timed systems[END_REF][START_REF] Bornot | An algebraic framework for urgency[END_REF] for this purpose: Definition 3.12. (Modal Operator [START_REF] Bornot | Modeling urgency in timed systems[END_REF][START_REF] Bornot | An algebraic framework for urgency[END_REF])

Let X = {x 1 , x 2 , • • • , x n }. Let ν ∈ R n and k ∈ N. Let φ ∈ B(X)
and T be the time domain. We define the (state) predicate 3 k φ by:

(3 k φ)(ν) ⇐⇒ ∃t ∈ T, t ≤ k, φ(ν + t)
Now we strengthen the guard γ in t 2 and define t 2 = ((g ∧ g , γ ∧ (¬3 k γ )), e, (a, R)). According to [START_REF] Bornot | Modeling urgency in timed systems[END_REF][START_REF] Bornot | An algebraic framework for urgency[END_REF], it is possible to eliminate the existential quantifier in 3 k γ and to obtain a quantifier-free formula (we will not get into the details and refer the reader to [START_REF] Bornot | Modeling urgency in timed systems[END_REF][START_REF] Bornot | An algebraic framework for urgency[END_REF]).

General Case. In the general case there could be p transitions

t i = ((g i , γ i ), e i , (a i , R i )) s.t. e < k 1 e 1 , • • • , e < kp e p . Then we split t into 2 p transitions t F = ((g F , γ F ), e, (a, R)) with F ⊆ [1.
.p]:

g F = g ∧ i∈[1..p]\F ¬g i ∧ i∈F g i (2
)

γ F = γ ∧ i∈F ¬3 k i γ i ( 3
)
Remark 3.7. As stated in remark 3.2, page 1014, we do not modify the invariants of the system.

According to [START_REF] Bornot | On the construction of live timed systems[END_REF], the formula 3 k γ can be written as simple formula in B(C T ). If we denote by M < the transition relation obtained by:

1. strengthening the guards by the weakest precondition for fireability as defined in section 3.7.1, Lemma 3.3 follows from Def. 3.10 and Def. 3.12. From lemma 3.1, we obtain the following corollary:

Corollary 3.1. V S ∪ C S , V F ∪ C F , E, A, M, < = V S ∪ C S , V F ∪ C F , E, A, M, ∅ <
This completes the syntactical encoding of timed priority without urgency for timed components.

Encoding Urgency

Urgency consists in preventing time elapsing when a discrete transition is enabled. In this section we assume the time domain is R ≥0 . Also we assume time determinism and denote ν -t the valuation defined by (ν -t)(x) = ν(x)-t (time non determinism is more technically involved but can be handled as well).

Our work is based on previous papers by S. Bornot, J. Sifakis and S. Tripakis [START_REF] Bornot | Modeling urgency in timed systems[END_REF][START_REF] Bornot | An algebraic framework for urgency[END_REF][START_REF] Bornot | On the construction of live timed systems[END_REF]. The authors define the notion of rising edge of a guard that plays a central role:

Definition 3.13. (Rising Edge [27]) Let X = {x 1 , x 2 , • • • , x n }, ν ∈ R n and γ ∈ B(X).
The rising edge of γ, denoted γ↑ is the predicate defined by:

γ↑ (v) = γ(v) ∧ ∃t > 0 , ∀0 < t ≤ t, ¬γ(v -t ) ∨ ¬γ(v) ∧ ∃t > 0, ∀0 < t ≤ t, γ(v + t ) (4)
We assume that each guard of a transition labelled by an urgent event is such that γ ↑ ⊆ γ . Indeed x > 10 is not a relevant guard for an urgent transition as there is no first instant at which the guard becomes true: the transition becomes urgent strictly after 10 which is a fuzzy instant and this is in contradiction with urgency. Note that in this case (x > 10) ↑ ≡ (x = 10) which gives the same rising edge as for x ≥ 10 but the latter has a first instant for which it is true. This problem is wellknown and is already discussed in [START_REF] Bornot | An algebraic framework for urgency[END_REF]. Note that in this case equation (4) of Def. 3.13 simplifies in γ ↑ (v) = γ(v) ∧ ∃t > 0 , ∀0 < t ≤ t, ¬γ(vt ) . We also assume that a guard γ of an urgent transition is convex and this implies that γ↑ is convex as well.

Urgency as an assertion

The semantics of urgency (see Def. 3.6) implies that when a transition becomes urgent (i.e. its guard is true) time elapsing is forbidden and this is the semantics proposed in [START_REF] Bornot | An algebraic framework for urgency[END_REF]. It does not imply that the urgent transition is fired. Also this notion is different from the notion of urgency in UPPAAL [START_REF] Bengtsson | New generation of UPPAAL[END_REF] which only constrains processes to synchronize on common channels (synchronized events) whenever they can.

To be more precise assume we have a component U with an urgent transition e u as defined on Fig. 6(a).

Start in configuration (s = 0, x = 0). At some point f can occur. If it occurs before x = 10 it is possible to let some time elapse until x = 10 reaching (s = 1, x = 10). At this point the urgent transition prevents time from elapsing. Anyway a new occurrence of f could occur and set s to 0 again: in this (s=1) => (10<x<=20 => Y=0) 15: edon (b) Urgency as an assertion Figure 6. Encoding Urgency configuration the urgent event e u is no more enabled and time can elapse. Thus to use our notion of urgency to force a transition to occur, one must ensure that once an urgent transition is enabled (x = 10) no other transition can disable it (to achieve this, one could change the enabling condition True of line 9 of node U to x<10).

To encode urgency, we use an additional real flow variable Y (see line 2 of Fig. 6(b)). This flow variable is assumed to be reset to 0 on each discrete transition and evolves at rate 1 (synchronous with physical time) on delay transitions. How this will be achieved will be dealt with later in this section. The syntactical encoding of urgency consists in adding a timed invariant (line 14 of node U_Y, Fig. 6(b)) to constrain time elapsing. Note that this assertion implies Y = 0 only when x > 10 (and not x ≥ 10). Intuitively, assume we reach a configuration (s = 1, x < 10). Then time can elapse from this configuration until x = 10. Indeed (s = 1, x = 10) satisfies Def. 3.6 as for each strictly preceding instant the assertion is true. From this configuration on time cannot elapse as Y > 0 and the assertion forbids it. Now if we reach (s = 1, 10 ≤ x ≤ 20) by firing a discrete transition, Y is set to 0 and time elapsing is also forbidden. This achieves urgency (in the sense that time elapsing is prevented). Some limitations of our encoding is that we do not know how to deal with urgent transitions with sharp urgent guards as x = 5. This is why we require an additional assumption on guards for urgent transitions: the (temporal) guard γ u must satisfy ∃ > 0 , ν ∈ γ u ↑ =⇒ ∀ ≤ ν + ∈ γ u . We refer to this latter property as γ u is not sharp. E,A,M,<) be a timed component where < consists in one element: e u > time (e u is urgent). Assume there is one urgent transition t u = ((g u , γ u ), e u , (a u , R u )), γ u is not sharp, and there is a flow variable Y that is reset on each discrete transition and evolving at rate 1 on delay transitions.

Correctness of the encoding

Let T = (V S ∪ C S , V F ∪ C F ,

Define the timed component

T u = (V S ∪ C S , V F ∪ C F , E, A ∧ ϕ u , M, ∅) with ϕ u def = g u =⇒ (γ u ∧ ¬(γ u ↑)) =⇒ Y = 0 .
Note that we assume Y is an invisible variable that does not belong to C F . This is just for the sake of clarity as otherwise we need to define a new notion of timed bisimilarity for timed interfaced transition systems that do not have the same sets of flow variables (remind that Def. 3.2 imposes the two systems to have the same interface). The proof is given in appendix A.5.

Implementation of the encoding

To implement our encoding and add a fresh flow variable Y , we proceed as follows:

1. create node U_Y from node U, as described by Fig. 6(b), 2. build a new node YY (Fig. 7(a)) that manages a variable Y that satisfies the assumptions we needed before: Y is reset on each discrete transition and evolves at rate 1 on delay transitions. Each discrete event of other components will be synchronized with event u of YY;

3. build a parent node UU that synchronizes U_Y and YY; this node is given in Fig. 7(b). This scheme can be carried out for multiple urgent events. We do not detail this in this paper as it is just a technical exercise. Now that we know how to encode timed priority syntactically and how to flatten a node into a component. We proceed with a translation of timed components into timed automata. This will enable us to check various timed properties.

From Timed Nodes to Timed Automata

In this section, we present a translation of Timed AltaRica specifications to timed automata [START_REF] Alur | A theory of timed automata[END_REF]. This way we can extract a timed automaton from a Timed AltaRica specification and carry out some verification of temporal properties using tools for analysing timed systems like UPPAAL [START_REF] Pettersson | UPPAAL2k[END_REF], CMC [START_REF] Laroussinie | CMC: A tool for compositional model-checking of real-time systems[END_REF] or KRONOS [START_REF] Daws | The tool KRONOS[END_REF]. Notice that thanks to theorem 3.4 we only need to define the translation for timed components. E,A,M, ∅ be a timed component with |C S | = n and |C F | = m (thanks to lemma 3.3, we can assume the timed priority relation of T is the empty relation). From Def. 3.7, the assertion of a timed component consists in two parts:

From Timed AltaRica Components to Timed Automata

Let T = V S ∪ C S , V F ∪ C F ,
• A V T which gives a constraint on the discrete variables,

• A C T which associates a time invariant to a predicate on the discrete variables.

Thus we write A C T = p j=1 (P j =⇒ I j ) with free(P j ) ⊆ V T and free(I j ) ⊆ C T . As we want to build a timed automaton (which is timed bisimilar to the original node) from a timed component, we need to define the locations of this timed automaton. They are built from the assertion on the discrete variables, and must be labelled with a timed invariant. We define the translation of a timed component with no flow variables and explain later how we deal with components with flow variables.

We write

G L = [1..p] as a shorthand for G, L ⊆ [1..p], G ∩ L = ∅, G ∪ L = [1..p] i.e. G
Let T = V S ∪C S , V F ∪C F , E, A, M, ∅ be a timed component with V F = C F = ∅. Let A = A V T ∧A C T with free(A V T ) ⊆ V T , A C T = p j=1 (P j =⇒ I j ) and free(P j ) ⊆ V T and free(I j ) ⊆ C T . Given G ⊆ [1..p], L ⊆ [1.
.p], we define:

r L G = ∧ j∈G P j ∧ ∧ j∈L ¬P j (5)
l L G = A V T ∧ r L G (6)
The timed automaton 9 A(T ) = (L, L 0 , E, X, I, T ) associated with T is defined by:

• L = {l L G | G L = [1..p] ∧ l L G =
∅} is the set of locations 10 , • L 0 = L is the set of initial states (actually in real Timed AltaRica specifications, a set of initial states is given as in the example of Fig. 5(b); assume this set is defined by a predicate init then L 0 = init),

• E is the set of events,

• X = C T is the set of clocks,
• the invariant I is defined by:

I(l L G ) = ∧ k∈G I k if G = ∅ tt otherwise • the transition relation T is defined by: let l L G , l L G ∈ L such that l L G ∧ g = ∅ and a( l L G ∧ g ) ∩ l L G = ∅ (
the source location intersects the discrete guard and the target location intersects the discrete part of the state space) and t = ((g, γ), e, (a, R)) ∈ M , then

(l L G , (g ∧ Pre t (l L G ) ∧ γ, e, (a, R)), l L G ) ∈ T
9 see section 3.1 for the definition of a timed automaton 10 Thus the number of locations is exponential in the number of predicates of AC T . Notice that this definition gives a partition of the set of states defined by AV T and that l L G ⊆ St × Ft.

Remark 4.1. As we have imposed that the I k denote convex sets, the invariants I(l L G ) are allowed by the definition of timed automaton (section 3.1).

In the previous definition we assume we can give constraints on the discrete variables in the guards, and allow assignments of the discrete variables on a transition, which is not formally allowed by the definition of timed automata of section 3.1, but this definition can trivially be extended to include this (timed automata of UPPAAL [START_REF] Pettersson | UPPAAL2k[END_REF] allow the use of such features). Also if we do not make any assumption on the domain of the discrete variables of a Timed AltaRica specification the number of locations may be infinite. Anyway we can define the translation of a timed component into a timed automaton (with potentially an infinite number of locations):

Theorem 4.1. Let T = V S ∪ C S , V F ∪ C F , E, A, M, ∅ be a timed component with V F = C F = ∅.
Then T and A(T ) are timed bisimilar.

The proof is given in appendix A.6.

The Train Example

We now apply the previous translation to the train example of Fig. 8. The flow variable N is first assumed to be a state variable (line 5) and an assignment is given for N on lines 10-12. We assume that this enables us to get rid of the assertion on N (i.e. line 16 is commented out). Table 1 gives the locations and invariants of the corresponding timed automaton.

The next step consists in computing the graph structure: the result for the train component of Fig. 8 is given on Fig. 9. Notice that we compute an abstract timed automaton in the sense that discrete variables are not interpreted: as a result the number of locations of the timed automaton where the discrete variables are interpreted might be larger than the number of locations of this abstract timed automaton, even could be infinite.

G L r L G l L G I(l L G ) ∅ {1, 2} etat = 0 etat = 0 tt {1} {2} etat = 1 etat = 1 t ≤ 30 {2} {1} etat = 2 etat = 2 t ≤ 20 {1, 2} ∅ ff ff -

Discussion of our Translation

The assumption that flow variables become clock state variables of the timed component means that the flows evolution rates and resets must follow the evolution rules of a clock in a timed automaton. This imposes restriction on the type of equations one can write in the assert part of a Timed AltaRica program. We will not go into details about it and the reader is referred to [START_REF] Pagetti | Extension temporisée du langage AltaRica[END_REF] for an exhaustive presentation. Nevertheless such constraints like Y = x, Y = x + 1 etc. (where Y is a flow and x a clock) can be dealt with in the translation into timed automata. More complex equations Y = 2x + y can be handled using hybrid automata [START_REF] Henzinger | The theory of hybrid automata[END_REF]. Constraints like x + 1 ≤ Y ≤ 2y + x cannot be encoded into linear hybrid automata as the slope of Y is unbounded. In the sequel we assume that only assertions of the simple type Y = x or Y = x + c, c ∈ N are used so that we can encode them into timed automata constraints. Computing the assignments of the flow variables that have become state variables is in this case easy and detailed in Table 3.

The other choices we have made can be accounted for by the following reasons:

• we do not want to have an expensive computation to produce the timed automaton; our translation scheme is easy to implement and does not require extensive computation;

• also, we do not want to deal with clocks in the translation as it is the purpose of the tools for analysing timed systems to do some computation on continuous time domains; we only perform syntactical rewriting;

• we do not want to constrain the discrete variables to be in a finite domain before doing the translation: indeed this could be the case that the variables are in a finite domain only because of the timing constraints. Thus we do not want to compute the domain of the variables in our translation. This is why the locations are predicates on the discrete variables and transitions constrain updates of these variables. Notice also that this could be the case that the timed automaton associated with a timed component has a finite bisimilar quotient whereas the untimed component has no finite bisimilar quotient (e.g. if a transition contains an update of the form x := x + 1). With our translation, we do not need to assume that the untimed component admits a finite bisimilar quotient.

Reachability Issues for Timed AltaRica Components

Timed AltaRica components are translated into timed automata as described previously. If the domain of the discrete variables is finite, we obtain a timed automaton with a finite number of discrete states. Reachability is decidable for timed component if the translation of a timed component belongs to a class of timed automata for which reachability is decidable. This problem has been extensively studied and an exhaustive set of results was given in [START_REF] Bouyer | Are timed automata updatable ?[END_REF]. We recall (see section 3.1) that the set of clock constraints B(X) over a set X of clocks is defined inductively by the grammar (see equation 1):

g := x r| x -y r |g ∧ g |g ∨ g
with x, y ∈ X, ∈ {<, <, >, ≥, =}, r ∈ Z. The set of diagonal-free constraints B df (X) is defined by the sub-grammar: g := x r|g ∧ g |g ∨ g with x ∈ X, ∈ {<, <, >, ≥, =}, r ∈ N. Table 2 gives a summary of the results in [START_REF] Bouyer | Are timed automata updatable ?[END_REF] (an assignment of the form x :< c means that x is assigned any value less than c) concerning the decidability of the reachability problem for timed automata: decidability depends on the type of guards of the automata and on the type of assignments allowed.

Deterministic Assignment

Guards in B df (X) Guards in B(X)

x := c (1) x := y (2) Decidable x := x + 1 (3) Decidable x := y + c (4) Undecidable x := x -1 (5) Undecidable Non-Deterministic Assignment Guards in B df (X) Guards in B(X) x :< c (6) Decidable x :> c (7) Decidable x : y + c (8) Undecidable y + c <: x :< y + d (9) y + c <: x :< z + d (10) Undecidable
Table 2. Decidability Results for Reachability in Timed Automata (from [START_REF] Bouyer | Are timed automata updatable ?[END_REF])

In our setting, the decidability of reachability depends on the type of guards and assignments of the timed component as well as on the type of assertions used to constrain the continuous flow variables. If we allow only assertions on the continuous flow variables of the form Y = x+c where Y is a continuous flow variable, x is a clock state variable and c ∈ N then the updating of Y on discrete transitions can be encoded as a clock assignment according to the encoding described in Table 3: in the case of nondeterministic assignments (6-10) of x we encode the assignment for Y with an -transition that occurs right after the one assigning x without any time elapsing (can be implemented by committed locations in UPPAAL for instance).

Combining Tables 2 and3 we obtain that for an assertion containing only constraints of the form Y = x + c with Y a flow variable and x is a clock variable, c ∈ N:

• if all the guards on the clock and continuous flow variables are in B df (X), reachability is decidable in case the assignments of the clock state variables are not of type ( 5) nor [START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF];

• if all the guards on the clock and continuous flow variables are in B(X), reachability is decidable only if the assignment of the clock state variables are of the form (1) or ( 2) and c = 0 (Y = x and x := y allowed).

A Case Study Using Timed Priorities

In this section we give an example of the use of time priorities in Timed AltaRica and the modeling power they give. We consider again the train-gate-controller introduced in section 2:

Type of Assignment for x Type of Assignment for Y

x := c (1) Y := c + c (1) x := y (2) Y := y + c (4) x := x + 1 (3) Y := Y + 1 (3) x := y + c (4) Y := y + c + c (4) x := x -1 (5) Y := Y -1 (5)
x • there are two tracks crossing at the gate,

:< c (6) x :> c (7) x : y + c (8) -trans. Y := x + c (4) y + c <: x :< y + d (9) y + c <: x :< z + d (10)
• the trains can come from any side on these two tracks,

• the aim is to ensure property P stating "the gate is closed when at least one train is on the near section". Also we do not want to open the gate if a train is crossing and another is going to cross in a near future (this is where the priorities will be used).

Let k ∈ N be a parameter, we fix some timed priorities among the two events approach and Go_up within a delay k. First, we translate this system in timed automata by applying the translation developed in the previous section 4. Second, we analyse the system using UPPAAL [START_REF] Pettersson | UPPAAL2k[END_REF] (note in this case we do have to instantiate k with a value in N before using the tool).

Translation of the Train-Gate-Controller into Timed Automata

The components Train-Gate-Controller have been given in Fig. 1, page 1003 and Fig. 5, page 1018.

From those components we can build timed automata using the algorithm defined in section 4.1. For this particular case of a hierarchical node with sub-components we can use an alternative way for building the timed automaton A(M ain): it is the synchronized product of the three automata obtained by translating each component into a timed automaton. The timed automata for nodes TRAIN and GATE are given in Fig. 10. The timed automaton 11 corresponding to node MAIN is given in Fig. 11. MAIN.N.

On the synchronized product of the three UPPAAL timed automata, property P is given by the UPPAAL-style property:

A[]((TRAIN1.s2 or TRAIN2.s2) imply GATE.etat==2)

We can check that P is satisfied for any fixed value of k.

Influence of Timed Priorities

Timed priorities constrain the system and one of the first questions that arises is what kind of behaviour do we forbid. The priority we have given in Fig. 5(b), page 1018 means that we do not want to raise the gate if a new train can enter the near section within less than k time units. As intended, there should be a threshold value k 0 for k such that for all k ≥ k 0 , the gate remains closed forever. We can express this as the property 12 A[](GATE.etat==2) and it is satisfied for k 0 = 40.

Another interesting problem concerns the liveness of the system. As stated in remark 3.2, page 1014, some deadlock may occur when prioritising the system. The train-gate-controller without priority is deadlock free and looses this property as soon as k > 0.

Conclusion

We have shown how to add clocks to AltaRica and build a timed extension of this formalism: Timed AltaRica. This timed extension has the same features as the untimed ones and we were able to prove all the results obtained for the untimed case:

• two timed bisimilar timed interfaced transition systems remain timed bisimilar when we apply a timed priority restriction (theorem 3.2),

• a timed component with timed priorities can syntactically be rewritten into a timed component without timed priorities and has the same semantics (lemma 3.3),

• the synchronised product (for nodes) is compositional with respect to timed bisimulation (theorem 3.3),

• a timed node can be rewritten into a timed component that has the same semantics (theorem 3.4).

Moreover we have defined a translation of timed components into usual timed automata (section 4) so that we can use tools for analysing timed automata (like UPPAAL) to carry out our verification.

Moreover the implementation of our translation called Timed AltaRica-Compiler is currently being added to the AltaRica toolbox.

Our future work is many-fold:

• complete the extension of AltaRica by adding features allowing the user to specify hybrid systems [START_REF] Henzinger | The theory of hybrid automata[END_REF]; the main problem is to deal with time priorities in this case. The work we have presented in this paper is correct for clock variables but additional work is needed for systems where variables may have arbitrary integer slopes;

• study the problem of preserving liveness when using priorities (following the framework of [START_REF] Bornot | On the construction of live timed systems[END_REF]),

• use our AltaRica-compiler on real industrial case studies,

• investigate in alternative ways of checking the correctness of Timed AltaRica specifications: this amounts to design some hierarchical model-checking algorithms taking advantage of the structure of Timed AltaRica specifications.

If part. Assume there exist two homomorphisms h 1 : A 1 -→ B and h 2 : A 2 -→ B and denote B = E t , F t , S t , π, T . Define the relation R ⊆ S 1t × S 2t by: R(s, s ) ⇐⇒ h 1 (s) = h 2 (s ) We show that R is a timed interfaced bisimulation by proving it satisfies the four points of Def. 3.2.

1. Let q 1 ∈ S 1t et s = h 1 (q 1 ) ∈ S t . Since h 2 is surjective there exists q 2 ∈ S 2t s.t. h(q 2 ) = s = h(q 1 ).

2. Let (q 1 , q 2 ) ∈ R. Then h 1 (q 1 ) = h 2 (q 2 ). By item 2 of Def. 3.3 it follows that π 1 (q 1 ) = π(h 1 (q 1 )) = π(h 2 (q 2 )) = π 2 (q 2 ).

3. Let (q 1 , g, e, q 1 , g 1 ) ∈ T 1 . By item 3 of Def. 3.3 there exists g ∈ s.t. (h 1 (q 1 ), g, e, h 1 (q 1 ), g ) ∈ T . Let q 2 ∈ S 2t s.t. (q 1 , q 2 ) ∈ R. Then h 2 (q 2 ) = h 1 (q 1 ) and by item 4 of Def. 3.3 we have i) there exists q 2 ∈ S 2t s.t. h 2 (q 2 ) = h 1 (q 1 ) i.e. (q 1 , q 2 ) ∈ R and ii) there exists g 2 ∈ π 2 (q 2 ) s.t.

(q 2 , g, e, q 2 , g 2 ) ∈ T 2 . As the two TITS A 1 and A 2 play a symmetric role we obtain both items 3 and 4 of Def. 3.2.

Only if part

The idea is as follows: there is a largest bisimulation ≡ 1 for A 1 and ≡ 2 for A 2 and those two largest bisimulations give two transition systems A 1/≡ 1 and A 2/≡ 2 that are isomorphic. Moreover each bisimulation ≡ i can be made a function and we can build two homomorphisms from these functions. The scheme is depicted in Fig. 12.

A 1 A 2 A 1/≡ 1 A 2/≡ 2 R h 1 h 2 φ Figure 12
. Building a Timed bisimulation Homomorphism Let V ⊆ X 1 × X 2 and U ⊆ X 2 × X 3 be two binary relations. We denote V.U ⊆ X 1 × X 3 the relation s.t. (q, q ) ∈ (V.U ) ⇐⇒ ∃q 2 ∈ X 2 s.t. (q, q 2 ) ∈ V and (q 2 , q ) ∈ U . For a binary relation L ⊆ X × X denote L -1 = {(q, q )|(q , q) ∈ L} and L * = ∪ n∈N L n with L 0 = Id and L i+1 = L.L i . Note that (L.L -1 ) * is an equivalence relation.

Assume A 1 and A 2 are timed bisimilar and denote R a bisimulation relation on S 1t × S 2t .

The relations ≡ 1 def = (R.R -1 ) * ⊆ S 1t × S 1t and ≡ 2 def = (R -1 .R) * ⊆ S 2t × S 2t are both equivalence relations. We define the quotient A 1/≡ 1 and A 2/≡ 2 and the functions h i : A i -→ A i/≡ i by: h i (s) = [s] ([s] denotes the equivalence class for s). It is easy to see that h i is a timed bisimulation homomorphism. Also define the mapping φ by:

φ : A 1/≡ 1 -→ A 2/≡ 2 [s] -→ [s ] ⇐⇒ (s, s ) ∈ R
φ is a (timed bisimulation) isomorphism. Now let h 1 = φ•h 1 . h 1 is a timed bisimulation homomorphism (composition of an isomorphism and homomorphism). This completes the proof.

(a, R)(q, f ) and by Def. 3.8 this means that (q 0 , q 1 , • • • , q n ), f, e, (q 0 , q 1 , • • • , q n ), f ∈ T . The converse is straightforward and we finally have (q, f ), e, (q , f ) ∈ T ⇐⇒ (q, f ), e, (q , f ) ∈ T for e = (e 0 , e 1 , • • • , e n ) with e i ∈ T.

• if e = (δ, δ, • • • , δ) with δ ∈ T the have to ensure that all long the way from q to q the time constraint (invariant) holds. This is straightforward by pointing out that if (q, f ), δ, (q , f ) ∈ T then ∀δ ≤ δ we have (q, f ), δ , (q , f ) ∈ T for some (q , f ). Then using Def. 3.8 we easily get the result that (q 0 , q 1 , • • • , q n ), f, δ, (q 0 , q 1 , • • • , q n ), f ∈ T . Again the converse holds and we end up with T = T . Assume the flow variable Y is reset on each discrete transition and evolves at rate 1 on delay transitions. Then T and T u are timed bisimilar.

Induction Step Let N = V F ∪ C F , E

Proof:

First note that as γ u is not sharp γ u ∧ ¬(γ u ↑) = ∅. Indeed for all > 0 the set W = {ν + | ν ∈ γ u ↑ and ≤ } is included in ¬(γ u ↑). Hence if γ u ∧ ¬(γ u ↑) = ∅ it must be the case that for all > 0 the set W ∩ γ u is empty and contradicts the fact that γ u is not sharp. Second γ u ∧ ¬(γ u ↑) is past-opened i.e. if ν ∈ γ u ∧ ¬(γ u ↑) then there is > 0 such that ∀ ≤ we have ν -∈ γ u ∧ ¬(γ u ↑) . This follows from the constraint that the guard of an urgent transition has a first instant for which it becomes true.

Again we assume Y is not part of the configuration of the system and it is a global variable updated by an oracle. This enables us to use our notion of timed bisimilarity (Def. 3.2). Otherwise we would have to define timed bisimilarity for timed components with different sets of (clock) flows.

M < is the transition relation of T and we denote M u the transition relation of T u .

First part: M <⊆ M u . Remark that discrete transitions are unchanged and we only need to prove that each delay transition in M < is a transition in M u . Assume (s, ν), (f, µ), δ, (s, ν ), (f, µ ) ∈ M < with δ > 0. By Def. 3.8, item 4.(c) it implies that i) (s, ν), (f, µ), δ, (s, ν ), (f, µ ) ∈ M and by Def. 3.6 that ii) ∀t < t s.t. ((s, ν), (f, µ), t , (s, ν + t ), (f, µ + t )) ∈ M , if ((s, ν + t ), (f, µ + t ), e, q , g ) ∈ M then e > time. By i) we know that ∀δ ≤ δ if ((s, ν), (f, µ), δ , q , g ) ∈ M then (q , g ) ∈ A . Now if (s, f ) ∈ g u we need to prove that (ν , µ ) ∈ ϕ u . δ > 0 implies Y > 0. Hence (γ u ∧ ¬(γ u ↑)) must be false at (s, ν ), (f, µ ). Assume it is true at (s, ν ), (f, µ ). Then as (γ u ∧ ¬(γ u ↑)) is past-opened there must be > 0 s.t. ∀ ≤ , ((s, ν -), (f, µ -)) ∈ (γ u ∧ ¬(γ u ↑)) . This contradicts ii). Thus (γ u ∧ ¬(γ u ↑)) is not satisfied for any δ ≤ δ and A ∧ ϕ u holds all along the delay transition (s, ν), (f, µ), δ, (s, ν ), (f, µ ) which implies this transition is in M u .

Second part: M u ⊆ M <. Assume (s, ν), (f, µ), δ, (s, ν ), (f, µ ) ∈ M u and δ > 0. By Def. 3.8 this means that all long the path from (s, ν), (f, µ) to (s, ν ), (f, µ ) assertion A ∧ ϕ u holds. In case (s, f ) ∈ g u clearly the transition is in M <. If (s, f ) ∈ g u then (γ u ∧ ¬(γ u ↑)) =⇒ Y = 0 must hold all along the way. Again as Y > 0 (because δ > 0) it must be the case that (γ u ∧ ¬(γ u ↑)) is false for all 0 < t ≤ δ i.e. ¬γ u ∨ γ u ↑ holds. Either ∀0 < t < δ, γ u is false and in this case no urgent transition can be fired on the way from (s, ν), (f, µ) to (s, ν ), (f, µ ) and (s, ν), (f, µ), δ, (s, ν ), (f, µ ) ∈ M <. Or γ u holds for some 0 < t < t. Then γ u ↑ must hold at t . By the fact that γ u ∧ γ u ↑ is not single we know that there is a t < t < t s.t. γ u holds at t as well as ¬(γ u ↑)). Hence Y must be equal to zero at t which cannot be the case. Hence there cannot be any t < δ s.t. t u is fireable and again (s, ν), (f, µ), δ, (s, ν ), (f, µ ) ∈ M <. This completes the proof.

Proof:

We denote T = E t , F t , S t , π, T with F t = {tt } (F t cannot be empty because of the definition of TITS) and π is constant and equal to π(q) = tt. A(T ) = (L, L 0 , E, X, I, T ) and the semantics of A(T ) is a TTS (see section 3.1) (Q, E, →). Thus it is also TITS E t , F t , S t , π , T of dimension (|X|, 0), with E t = E ∪ R ≥0 , F t = {tt }, S t = {(l, ν) | ν ∈ inv(l) }, π(q) = tt (always non empty) and T is given by →. We omit f is configuration like (s, f ) as it always amounts to (s, tt).Now we prove that T and A(T ) are timed bisimilar: as a candidate for a timed bisimulation relation we take equality of the states.

1. Let q = (s, ν) ∈ S t . We apply Def. 3.8:

(s, ν) ∈ S t ⇐⇒ (s, ν) ∈ A V T ∧ A C T ⇐⇒ s ∈ A V T ∧ (s, ν) ∈ A C T ⇐⇒ s ∈ l L G , G L = [1..p](l L G form a partition of A V T ) and ν ∈ ∩ k∈G I k ⇐⇒ s ∈ l L G ∧ ν ∈ Inv(l L G ) ⇐⇒ (s, ν) ∈ S t

Far ≡ etat = 0 Before ≡ etat = 1 On ≡ etat = 2 (Figure 1 .

 0121 Figure 1. Specification of a Train

  init etat := 0, z := 0; 15: edon (a) The Controller node GATE event Go_down, Go_up, down, up; state etat : [0,3]; trans etat=0 |-Go_up -> ; etat=0 |-Go_down -> etat := 1; etat=1 |-Go_down -> ; etat=1 |-down -> etat := 2; etat=1 |-Go_up -> etat :=3; etat=2 |-Go_down -> ; etat=2 |-Go_up -> etat := 3; etat=3 |-Go_up -> ; etat=3 |-Go_down -> etat := 1; etat=3 |-up -> etat := 0; init etat:=0; edon (b) The Gate

Figure 2 .

 2 Figure 2. AltaRica Specifications for the Controller and the Gate

Figure 3 .

 3 Figure 3. Hierarchical Node

  the set of flow values, where F is the set of discrete flow values and R m is the set of continuous flow values;

Remark 3 . 3 .

 33 Again, if T = {0}, we obtain the definition of the priority relation restriction (Def. 2.3).

Remark 3 . 4 .

 34 is the clock assignment of the transition; 5. < is a timed priority relation. Item 3 of Def. 3.7 allows us to specify constraints C between clock variables and realvalued flow variables (e.g. Y = x where Y is a flow variable and x is clock variable): it suffices to use tt =⇒ C where C ∈ F(C T ) (e.g. tt =⇒ Y = x).

Figure 4 .

 4 Figure 4. Specification of a Train as a Timed Component

Remark 3 . 6 .

 36 an expanded synchronization set together with a priority relation < e V . (see Def. 2.2). Notice that < e V is a priority relation and not a timed priority relation. This is because ( V , < e V ) expresses the discrete synchronization constraint. Example 3.2. (Hierarchical Specification of the Train-Gate-Controller) A timed version of the train-gate-controller is given in Fig. 5. Notice that the gate is a component, the train is the component given by Fig. 1, but the node MAIN embeds the CONTROLLER node and plays the role of N 0 . node GATE event Go_down, Go_up, down, up; state etat : [0,3]; y : clock; trans etat=0 |-Go_up -> ; etat=0 |-Go_down -> etat:=1, y:=0; etat=1 |-Go_down -> ; etat=1 & y <= 10 |-down -> etat:=2; etat=1 |-Go_up -> etat:=3, y:=0; etat=2 |-Go_down -> ; etat=2 |-Go_up -> etat:=3, y:=0; etat=3 |-Go_up -> ; etat=3 |-Go_down -> etat:=1, y:=0; etat=3 & y <= 10 |-up -> etat:=0; init etat:=0, y:=0; assert (etat =1) => (y <= 10); (etat =3) => (y <= 10); edon (a) The Timed Gate node MAIN flow N : [0,p]; event approach, exit, Go_up, Go_down; priorities Go_up (<,k) approach; state etat : [0,2]; z : clock; trans etat=0 |-approach -> etat:= 1, z:=0; etat=0 & N>1 |-exit -> ; etat=0 & N=1 |-exit -> etat:= 2, z:=0; etat = 1 |-approach -> ; etat = 1 |-exit -> ; etat=1 & z<=10 |-Go_down -> etat:=0; etat=2 & z <= 10 |-Go_up -> etat:=0; etat=2 |-approach -> etat:= 1, z

Figure 5 .

 5 Figure 5. Timed AltaRica Specifications for the Controller and the Gate

Theorem 2 . 1 (Theorem 3 . 4 .

 2134 see page 1009) for untimed nodes carries over to timed nodes: Let N be a timed node. Then N can be rewritten into a timed component C N such that N and C N are timed bisimilar.

2 .

 2 strengthening the guards to encode the timed priority relation as defined above in this subsection, we obtain a new timed component T <= V S ∪ C S , V F ∪ C F , E, A, M <, ∅ such that: Lemma 3.3. (Syntactical Priority) T < = T <.

Theorem 3 . 5 .

 35 T and T u are timed bisimilar.

Figure 7 .

 7 Figure 7. Hierarchical Modeling of Urgency

  and L form a partition of [1..p]. Definition 4.1. (Timed Automaton Associated with a Timed Component)

Figure 8 .

 8 Figure 8. Train Timed Component with no Flow Variables

20 t

 20 ≥ 70 ∧ etat = 0 approach (etat,n,N,t) := (1, 1, 1, 0) 20 ≤ t ≤ 30 ∧ etat = 1 in (etat,t) := (2, 0) 10 ≤ t ≤ 20 ∧ etat = 2 exit (etat,n,N,t) := (0, 0, 0, 0)

Figure 9 .

 9 Figure 9. Translation of the Train component

Figure 10 .Figure 11 .

 1011 Figure 10. Train and Gate Automata in UPPAAL

A. 5 . 5 Theorem A. 5 .

 555 , <, N 0 , • • • , N n , ( Ṽ , < Ṽ ) and assume all the N i can be rewritten into timed componentsC N i s.t. N i and C N i are timed bisimilar. Let N = V F ∪ C F , E, < , C N 0 , • • • , C N n , ( Ṽ , < Ṽ ). Then using the base step proof we conclude there exists a timed component C N that is bisimilar to N . By theorem 3.3 we also have that N and N are timed bisimilar and hence C N and N are timed bisimilar.This completes the proof. Proof of Theorem 3.Let T = (V S , C S , V F , C F , E, A, M, <) be a timed component where > consists in one element: e u > time (e u is urgent). Assume there is one urgent transition t u = ((g u , γ u ), e u , (a u , R u )) and γ u is not sharp. Define the timed componentT u = (V S , C S , V F , C F , E, A ∧ ϕ u , M, ∅) with ϕ u def = g u =⇒ (γ u ∧ ¬(γ u ↑)) =⇒ Y = 0(7)

A. 6 . 1 Theorem A. 1 .

 611 Proof of Theorem 4.LetT = V S ∪ C S , V F ∪ C F , E, A, M, ∅ be a timed component with V F = C F = ∅.Then T and A(T ) are timed bisimilar.Note that we have shifted the clock flows into the state variables of the component and we allow only flows that are clock-definable.

  Theorem 3.1. Two TITS A 1 and A 2 are timed bisimilar if and only if there exists a TITS B and two timed interfaced bisimulation homomorphisms h 1 : A 1 → B and h 2

Example 3.1. (The Train)

  In Fig.4the time features of component TRAIN appear on line 7 where a clock (state) variable t is declared; it is used to constrain the guards of the transitions (see lines 9 to 11) and on some of them t is reset; also the assertion (lines[START_REF] Griffault | The mec 5 model checker[END_REF][START_REF] Alur | A theory of timed automata[END_REF] implies that when in state etat = 1 (resp. 2) time cannot elapse after t has reached 30 (resp. 20).

	Definition 3.8. (Semantics of Timed Components)

as well as the semantics of a guard (g, γ).

Table 1 .

 1 Locations and Invariants of the Train Component

Table 3 .

 3 Encoding Flow Variable Y constrained by Y = x + c

In AltaRica the keyword node in used for components (nodes with no sub-nodes) as well as for hierarchical nodes; indeed a component is a special case of node with no sub-nodes.

We will see later how this can be made precise using timing constraints to make a timed version of the controller and the gate in Fig.5.

how this is done is defined in[START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF].

we assume 0 ∈ T and T = N or Q ≥0 or R ≥0 or {0}.

We rule out time > a as the purpose of a priority relation is to add a sort of liveness in the system by forcing some discrete actions to be taken.

Urgency is dealt with in section. 3.7.3 and requires additional assumptions and definitions.

Quantifier elimination in Pret( A ) can only be done under some conditions (e.g. the discrete domain is finite). We do not discuss this in this paper and assume we can actually find a quantifier-free expression for Pret( A ).

This expression is equivalent to the one given in[START_REF] Point | Altarica : Contribution à l'unification des méthodes formelles et de la sûreté de fonctionnement[END_REF], Def.

9.2.3 (Priorités Syntaxiques), page 85.

To deal with priority, we use the algorithms given in section 3.7 and we obtain a priority free component.

Actually to prove this property with the restricted TCTL set of UPPAAL we have to change the initial set of states to check this property.

A.2. Proof of Theorem 3.2 Theorem A.2. (Priority and Timed Bisimulation)

Let A 1 = E t , F t , S 1t , π 1 , T 1 and A 2 = E t , F t , S 2t , π 2 , T 2 be two TITS and < a timed priority relation over E. If h : A 1 -→ A 2 is a timed bisimulation homomorphism then h : A 1 < -→ A 2 < is also a timed bisimulation homomorphism.

Proof:

Let h : A 1 -→ A 2 be a timed bisimulation homomorphim. We show that h is also a timed bisimulation homomorphim from A 1 < onto A 2 <.

For points 1 and 2 of Def. 3.3 just notice that < only restricts the transition relation and does not involve the set of states and the mapping π i=1,2 . Now for point 3, let (q 1 , g, e, q 1 , g ) ∈ T 1 <, then (h(q 1 ), g, e, h(q 1 ), g ) ∈ T 2 . Assume that (h(q 1 ), g, e, h(q 1 ), g ) / ∈ T 2 <, then according to Def. 3.6 there are two possibilities:

1. either e = t ∈ T and ∃e > 0 time, t < t, (h(q 1 ), g, t , q 2 , g ) ∈ T 2 ∧ (q 2 , g , e , q 2 , g ) ∈ T 2 . Since h is an homomorphism and (h(q 1 ), g, t , q 2 , g ) and (q 2 , g , e , q 2 , g ) are in T 2 , there exists q 1 , q 1 ∈ S 1t s.t. h(q 1 ) = q 2 , h(q 1 ) = q 2 ∧ (q 1 , g, t , q 1 , g ) and (q 1 , g , e , q 1 , g ) are in T 1 . Hence (q 1 , g, e, q 1 , g ) cannot be in T 1 < which contradicts the first assumption.

2. otherwise e ∈ E + and ∃e |e < k e and ∃t ≤ k|(h(q 1 ), g, t, q 2 , g ) ∈ T 2 and (q 2 , g , e , q 2 , g ) ∈ T 2 . Since h is an homomorphism and (h(q 1 ), g, t, q 2 , g ) and (q 2 , g , e , q 2 , g ) are in T 2 , there exists q 1 , q 1 ∈ S 1t |h(q 1 ) = q 2 , h(q 1 ) = q 2 and (q 1 , g, t, q 1 , g ) and (q 1 , g , e , q 1 , g ) are in T 1 . This contradicts again the fact that (q 1 , g, e, q 1 ) ∈ T 1 <. This ends the proof of point 3.

Now let q 1 ∈ S 1t , q 2 ∈ S 2t such that (h(q 1 ), g, e, q 2 , g ) ∈ T 2 <. Then ∃q 1 ∈ S 1t |h(q 1 ) = q 2 and (q 1 , g, e, q 1 , g ) ∈ T 1 . Again assume that for all q 1 s.t. h(q 1 ) = q 2 , we have (q 1 , g, e, q 1 , g ) / ∈ T 1 <:

1. if e ∈ T, this means that ∃t 1 < t, (q 1 , g, t 1 , q 1 , g ) ∈ T 1 and ∃e > 0 time that is firable from (q 1 , g ). Then from item 4 of the Def. of homomorphism we get (h(q 1 ), g, t 1 , h(q 1 ), g ) ∈ T 2 ∧ (h(q 1 ), g , e , q 2 , g ) ∈ T 2 and it contradicts (h(q 1 ), g, e, q 2 , g ) ∈ T 2 <.

2. Otherwise e ∈ E + and there exists e ∈ E + and t ≤ k s.t. e < k e , (q 1 , g, t, q 1 , g ) ∈ T 1 and (q 1 , g , e , q 1 , g ) ∈ T 1 . It follows that (h(q 1 ), g, t, h(q 1 ), g ), (h(q 1 ), g , e , h(q 1 ), g ) ∈ T 2 which again contradicts the hypothesis (h(q 1 ), g, e, q 2 ) ∈ T 2 <. This ends the proof of point 4 and of the theorem.

A.3. Proof of Theorem 3.3 Theorem

V ) be two timed nodes such that ∀i ∈ [0.

.n] there is a timed homomorphism h i from N i to N i . Then there exists a timed homomorphism h from N to N .

Proof:

Let N i = E t , F it , S it , π i , T i and N i = E t , F it , S it , π i , T i be the TITS that give the semantics of the timed nodes. First we assume < is the empty relation.

Define h by:

We prove that h is timed bisimulation homomorphism from N to N .

1. h is obviously surjective, 2. assume m = |C F | and f = (f, µ). For π(q) we get:

3. if (q, g, e, q 1 , g ) ∈ T since < is the empty relation and by definition of T (see Def. 3.10) it follows that (h(q), g, e, h(q 1 ), g ) ∈ T , 4. let q = (q 0 , q 1 , . . . , q n ) ∈ S t and q = (q 0 , q 1 , . . . , q n ) ∈ S t s.t. (h(q), g, e, q , g ) ∈ T . Assume e = (e 0 , . . . , e n ). Then by definition of T (Def. 3.10) we have:

As each h i is an homomorphism we get: ∃q i ∈ S it s.t. h i (q i ) = q i and f i ∈ π i (q i ) and (q i , f i , e i , q i , f i ) ∈ T i . This means:

Take q = (q 0 , . . . , q n ). We have h(q ) = q and ∃f 0 ∈ π(q ) s.t. (q, g, e, q , g ) ∈ T . Now assume < is not the empty relation. Let

. With the previous proof in the case of an empty priority relation we get that there exists an homomorphism h from N ∅ to N ∅ . Applying theorem 3.2 we obtain that h is also an homomorphism from N to N . This completes the proof.

A.4. Proof of Theorem 3.4

Theorem A.4. Let N be a timed node. Then N can be rewritten into a timed component C N such that N and C N are timed bisimilar.

Proof:

We prove theorem 3.4 by induction. E,A,M, ∅ as given by Definition 3.4, and C N = E t , F t , S t , π , T .

Base

Step For the base step assume all the N i are timed components:

the priority relation is empty as we can use the syntactical encoding of timed priorities defined in section 3.7) and

We prove that N and C N are timed bisimilar. Take equality as a candidate to be a bisimulation relation.

1. checking that equality is a total relation on S t ×S t amounts to checking that ∀q ∈ S t , π(q) = π (q)

and this is done in the second point,

3. let (q 0 , q 1 , • • • , q n ), f, e, (q 0 , q 1 , • • • , q n ), f ∈ T We denote q = (q 0 , q 1 , • • • , q n ) and q = (q 0 , q 1 , • • • , q n ). Note that T i = M i as for all N i the priority relation is empty.

• if e = (e 0 , e 1 , • • • , e n ) with e i ∈ T then by Def. 3.10:

This entails that (q, f ) ∈ A . Also by Def. 3.8 ∀i ∈ [0.

.n] there exists a transition ((g i , γ i ), e i , (a i , R i )) ∈ M i s.t. (q i , f i ) ∈ A i ∧ g i ∧ γ i and q i = (a i , R i )(q i , f i ) and (q i , f i ) ∈ A i . This implies that (q , f ) ∈ A . It remains to find a transition in M s.t. the transition from (q, f ) to (q , f ) is fireable in C N . Take ((g, γ), e, (a, R)) in C N given by g

As we already mentioned (q , f ) ∈ A . Moreover (q , f ) = 2. π and π are constant and equal to tt, so they agree for each state, 3. let (s, ν) ∈ S t . Then (s, ν) ∈ S t by item 1 above. Assume ((s, ν), e, (s 1 , ν 1 )) ∈ T with e ∈ E + .

We have to prove that ((s, ν), e, (s 1 , ν 1 )) ∈ T . As ((s, ν), e, (s 1 , ν 1 )) ∈ T there is a transition t = (g, γ), e, (a, R)) ∈ M such that i) (s, ν) ∈ A ∧ g ∧ γ , ii) s 1 = a(s) and iii) ν 1 = R(ν). This implies that in A(T ) there is a transition of the form

. By i) (s, ν) satisfies g ∧ γ ∧ l L G . So in the semantics of A(T ) a transition of the form ((s, ν), e, (s , ν )) can be taken. As we use (a, R) to update the values of the state variables and (a, R) are deterministic we obtain (s , ν ) = (s 1 , ν 1 ). Now assume ((s, ν), δ, (s 1 , ν 1 )) ∈ T with δ ∈ R ≥0 . By definition (s, ν) ∈ A and (s 1 , ν 1 ) ∈ A and as we have time determinism for the flow variables ∀0 ≤ δ ≤ δ, (s, ν + δ ) ∈ I(s) with

.p] and the invariant for l L G is Inv(l L G ) = ∩ k∈G I k . Inv(l L G ) and I(s) coincides and thus ((s, ν), δ, (s 1 , ν 1 )) ∈ T .

4. the converse of item 3 above is straightforward and proved exactly as item 3.

This completes the proof.