Franck Cassez De
email: franck.cassez@univ-brest.fr

Formal Semantics for Reactive GRAFCET

Keywords: semantics, GRAFCET, timed automaton, reactive languages MOTS-CLE ´S: se ´mantique, GRAFCET, automate temporise ´, langages re ´actifs

GRAFCET is a graphical formalism derived from Petri Nets and widely used to program automationapplications. So far, this formalism has not been equipped with a formal semantics: interpretation algorithms give the meaning of a GRAFCET description. Our purpose is to take advantage of the work carried out for reactive languages: these languages are given a precise behavioural semantics by means of finite-state machines; the behavioural model can then be checked for various properties. The work presented hereafter consists in equipping GRAFCET with a formal semantics to obtain a behavioural model (namely a timed automaton) that captures the metric aspect of time.

RE ´SUME

´. Nous proposons dans cet article une de ´finition du GRAFCET comme langage re ´actif : GRAFCET. On de ´finit ensuite une se ´mantique ope ´rationnelle des programmes de GRAFCET sous forme de re `gles a `la Plotkin. Cette se ´mantique inclut les temporisations qui sont traite ´es comme des variables boole ´ennes de la me ˆme manie `re que les flots d'entre ´e. On obtient ainsi un mode `le de comportement des programmes de GRAFCET qui est un automate temporise

´.

Introduction

The GRAFCET formalism [AFC 77] (Function Charts for Control Systems) is one of the first language aimed at specifying real-time applications. It is derived from Petri nets [BRA 83] from which it inherites most of its features: places are called steps, they are linked together by transitions. We adopt hereafter the terms used for transitions systems (or FSM) and a transition refers to a triple (in GRAFCET standards the term transition is used for receptivity which is the transition condition). This formalism is widely used by automation manufacturers and thus has been given a lot of attention regarding standards [COM 88] [ AFN 82] [COM 93] for example. Nevertheless the crucial point of the semantics given to a GRAFCET description (a grafcet in the sequel) has barely been tackled: many interpretations have been proposed for GRAFCET [AA 92] and many are used (this implies that GRAF-CET programs are bound to be run on particular sites with a definite interpretation and may not be interpreted "equivalently" on different sites).

Recently, this aspect of GRAFCET has benefited from the development of reactive languages [PNU 86 . This technique has many advantages as it embeddes GRAFCET into the reactive framework: simulation tools, verification tools are then available for GRAFCET programs. This is very important as GRAFCET specifications can now be verified automatically and connected to reactive languages.

Nevertheless doing so has some drawbacks: the reactive behavioural model is based on logical time and only the order of the occurrences of events matters. One of the important features of GRAFCET is the time-condition allowing the use of delays in the transition conditions. This notion can not be handled easily with reactive languages. Moreover GRAFCET is a rather complex formalism with many entities like actions associated to steps or boolean conditions with integer variables associated with transitions.

The need for a semantic model that handles such features or can be extended to cope with them is quite obvious: it enables to model all the components of the GRAFCET language and to extend the scope of the verification to quantitative aspects.

To give GRAFCET a rigourous and unambiguous interpretation, it remains to fill the gap between the language and a precise behavioural model: this is the purpose of the semantics presented in this paper.

It is not THE semantics of GRAFCET but an attempt to show the possibility to treat this formalism the same way as reactive languages and to benefit from the same advantages: formalization, determinism, verification.

In the next section we introduce the intuitive notions of reactive GRAFCET and justify the choices on particular points of GRAFCET interpretation. Section 3 is devoted to the semantics rules (SOS) and the formal characterization of our GRAFCET interpretation. In section 4 we define the behavioural timed model for GRAFCET specifications.

GRAFCET as a reactive language

A reactive system [PNU 86] [MP 93] [BB 91] is characterized by the following features (among others): it reacts to occurrences of events by issuing actions into the controlled environment, a reaction of the system has no duration: it is instantaneous, when no event occurs the system remains idle.

We will use in this article a simple version of GRAFCET with no forcing orders, macro-steps nor actions associated with the steps. GRAFCET is a graphical formalism suitable for specifying the control part of a real-time application: the word system means hereafter this control part.

Steps and Flows

A real-time application is made up of a number of activities which can be started or stopped: these activities are modelled by steps in GRAFCET. A step can be in two different states: active or idle. The scheduling of the steps depends on boolean state variables called flows. The evolution of the controlled environment is sensed through the changes of the values of the flows: the edges.

Let be the set of steps of a particular grafcet, then the set of active steps at any time is defined by the characteristic mapping

! 2 1
Similarly, if is the set of flows, the values of the flows at any time are given by " 2 2

Definition 1 A state is a pair ! " in 2 2 .

Reaction of the system

The system that controls the application specified with the GRAFCET language reacts to edges (of the flows) by starting or stopping some steps. For any set let and The system reacts to events of1 . We denote (resp.

) the starting (resp. stopping) action for a step . Then the starting and stopping action upon a reaction of the system is an element of (the set ot subsets of ).

The key issue is here to determine the next state: when we use the term output actions we mean the activations and deactivations of the steps (the usual "outputs" of a grafcet appear at another level). A reaction of the system to an event from state brings about a set of output actions and leads to a new state , which is formally written as 3

We use the subscript under the right arrow to mean that this is a reaction (this will be opposed to basic evolutions in the sequel).

Specifying a system with the GRAFCET language

A GRAFCET specification of a real-time application defines (in a graphical way) what are the actions to be activated and stopped when the values of the flows change. Remark 1 The canonical representation of a grafcet as a set of transitions is the unique one which has as many transitions as the number of edges of the graphical representation.

In the sequel a grafcet is given by the set of transitions. Graphical examples with their corresponding sets of transitions are pictured on Fig. 1.

Transition conditions

We first introduce transition conditions defined by terms over the flows and their edges. The set of transition conditions is the set of terms 3 over tt ff inductively defined by: tt ff , , (we note ¯for ),

1 2 1 2 1 2
. 2 this will be precisely defined later.

3 we assume a particular grafcet under study. With each transition condition we associate a value " in the boolean set tt ff depending upon " 2 and . The interpretation " for is defined inductively:

" tt tt, " ff ff, " tt if , ff otherwise, " " " tt , " ¯" , " 1 2 " 1 " 2 , " 1 2 " 1 " 2 .

Evolution rules

State changes are determined in GRAFCET by five evolution rules [COM 88] [DA 89]:

rule 1 the initial situation ! 0 2 defines the active steps at the first instant, rule 2 a transition is enabled if all its input steps are active; it is clearable if the two following conditions hold:

1. it is enabled, 2. the transition condition evaluates to true.

A clearable transition is immediatly cleared, rule 3 clearing a transition yields the following changes:

the input steps are stopped, the output steps are activated, rule 4 if many transitions are simultaneously clearable, they are simultaneously cleared, rule 5 if during an evolution a step must be both activated and stopped it remains activate (this is stronger than the classical rule which states this only for active steps).

Definition 3 A basic evolution is a state change obtained by applying the five evolution rules simultaneously to each transition. We denote a basic evolution from state on an occurrence of event

We do not use any subscript here to remind that this is a single evolution step.

Example 1

An example of a GRAFCET specification is given on Fig. 1.(a). with transition conditions 1 and 2 ¯. The initial state of the system is 0 ! 0 " 0 with ! 0 0 tt ! 0 1 ff, " 0 " 0 ff. In the remainding of the paper we will use the shorter notation 0 0 ¯¯(i.e. ! is replaced by ! 1 tt and for we use if " tt, ¯otherwise). A possible interpretation of GRAFCET is the without stability search (WOSS) interpretation. It consists in processing new occurrences of events immediatly after each basic evolution. Then from state 0 if event occurs the basic evolution of the system is 0 0 1 4

Remark 2 In frequently used interpretations of GRAFCET the value of the transition condition 1 would be true. In our interpretation, the value of this transition condition is ¯which evaluates to false. However it is always possible to change this interpretation and use instead of with " "

where " denotes the updated values of the flows after the edges of have occurred. The common interpretation assumes right continuity of the piecewise functions giving the values of the flows. In this case a transition condition like is equivalent to in the sense that they are true at the very same time. Our choice is left continuity of the piecewise boolean functions: we consider that the values of the boolean variables will have changed only at the next state and that they are updated during the reaction. Thus is no longer equivalent to . The term in a time condition refers to the last persistent value of the flow . As our interpretation differs from the standard ones, we will use the term GRAFCET when we consider it. The interested reader is refered to [DLR 91] for a complete discussion of this subject.

From state 1 , if no new event has occurred the transition condition 1 is now true. 1 is then a non stable state (since we can proceed further basic evolutions) and the evolution rules for the WOSS interpretation implies that clearable transitions be immediatly cleared 4 :

1 1 0 1 2 5
On the contrary if event has occurred during the basic evolution (4), the system reaches state 3 instead of state 2 :

1 1 0 1 3
Now considering the reactive assumptions stated at the beginning of this section we have: 1) a reaction takes no time: thus no changes can occur in a null duration; 2) if no changes can occur during a basic evolution the system state changes with the silent move (5) without any new occurrences of events. This is not compatible with the reactive notions and thus a basic evolution in the WOSR interpretation can not be taken as a reaction.

The intuitive semantics we are going to present in section 3 implements another interpretation of GRAFCET: the with stability search (WSS) interpretation. With this interpretation of GRAFCET new events are not taken into account before a stable state has been reached. Then, from state 0 , the basic evolutions leading to a stable state are 0 1 1 2 2 and the reaction of the system to event is 0 0 1 2 4 denotes the absence of occurrences of events ; such an evolution is unobservable.

Example 2

GRAFCET provides for time condition that can be used to delay actions and handle time units. They allow one to specify the application with a metric aspect of time that refers to the instants a step was started or stopped. A time condition is part of a transition condition: the grafcet pictured on

Figure 2. A grafcet with time condition

The intuitive semantics associated with a time condition is described on the time diagram Fig. 3: 1. at the initial instant is false, 2. step 0 is the only active step at the initial instant, 3. becomes true 1 time units after step 0 has been activated 5 ; at this date the transition condition involving is cleared and step 1 is started, step 0 is stopped, 4. becomes false 2 time units after step 0 has been stopped6 , 5. an occurrence of starts step 0 again, 6. if step 0 is started again before 2 time units have elapsed, is reset to false. The set of transition conditions of GRAFCET is extended in GRAFCET to the time conditions: transition conditions in GRAFCET are terms built as described in section 2.3.1 with replaced by . However the use of the operator (not) on time condition is forbidden (this is not for semantic reasons: one may think of introducing a new feature in GRAFCET which is the negative time condition. This amounts to considering time intervals [ALL 81] and two operators and : such a notion has already been defined in [RLG 94]).

The interpretation of the new terms is straighforwardly extended to time conditions and the new interpretation is noted " # . Finally a state is now a 3-tuple ! " # in 2 2 2 . We use for the set of states 2 2 2 in the sequel.

Synchronism and asynchronism

Time conditions are viewed as boolean variables (like flows) the changes of which depend on an external clock. This is partial view of the time conditions as the metric part is left aside. This will enable us to build an abstract behavioural model for GRAF-CET programs that will be "timed" later on. So far time conditions are particular flows.

Occurrences of events from cannot be simultaneous as in the standard GRAF-CET interpretations. But two events of may occur at the same time; moreover they sometimes do occur at the same time as in 1 1 2 , 2 1 2 for which 1 and 2 are always simultaneous. The complete treatment of these situations is defined in [CAS 95]. Then edges of time conditions variables are elements of .

Finally, events of and cannot be simultaneous: we think that time condition events are to be processed with highest priority as they can not be delayed. Moreover, once the semantic model has been timed, the notion of an external clock is useless and state changes brought about by time conditions will be silent. From now on, a reaction has the following form 7 Remark 3 In GRAFCET transition conditions may involve the activities of the steps as in GRAFCET. This is developped in [CAS 95].

Stability

On the example of Fig. 2 we see that from state 1 ¯¯there is a basic evolution to state 1 ¯¯0 1 0 ¯Īs a stable state in the sense that there are no possible basic evolutions from this state? In standard GRAFCET interpretations this state is stable only if 1 0, otherwise it is non stable. With the WSR standard interpretation and 1 0 the next move is

1 0 1 ānd if 1 0 is stable.
In GRAFCET is a stable state: to leave this state we must wait for to occur. If 1 0 then this event will occur 0 time unit after has been entered.

We will distinghish two types of unstability: intrinsic unstability which does not depend on any value (like 1 ) is called structural unstability, unstability that depends on time condition values (the previous case) is called temporal unstability.

Temporal unstability will not be treated with the semantic rules and will be a property of the timed model defined in section 4.

Dynamic semantics for GRAFCET

This section formalizes the calculus of basic evolutions and reactions. The semantics is given with conditional rules in the style of Plotkin [PLO 81]. The previous definitions will be used to calculate the steps that are to be activated and stopped on a reaction or basic evolutions. $ allows us to calculate the set of steps that must be activated and deactivated when firing a transition. If and respectively denote the input and output steps of a transition and the set of active steps in the current state of the system, $

Notations

gives the set of output events corresponding to the firing of the transition:

(resp.

) means that step is to be activated (resp. deactivated). According to rule 5, the activated steps are those which were not active in the last state. The operator extends $ to simultaneous firing of transitions. If taken independently, the firing of two transitions entail output events and , then when fired simultaneously, rule 5 applies: a step is activated if is activated by at least one of the firing, and deactivated if is not simulatneously activated.

To update the boolean variables we need the operator over 2 with value in 2 defined by : " " " ¯"

" "

Similarly we introduce and over 2 and 2 with values in 2 and 2 to update the activities of the steps and the time condition variables. Finally for ! " # , and , we use the following abbreviation ! " #

Syntax of GRAFCET

A grafcet in GRAFCET is a directed graph the edges of which are elements of . As we want to give a structural operational semantics for GRAFCET we define an abstract ambiguous grammar to describe the element of GRAFCET (the axiom is %):

% :: (8) % % (9) with . If 1 2
, 1 is the set of input steps and 2 the output steps.

Semantics

The calculus of basic evolution is formally defined by the structural operational semantics (SOS) given in Fig. 4. These rules express the five evolution rules listed in section 2.3.2.

For a grafcet , a state and an event , the basic evolution from on the occurrence of written is the only one 7 that satisfies 7 unicity and existence are discussed hereafter.

1 used for program %.

! 1 tt " # tt 1 2 ! " # $ 1 2 ! 1 tt ! " # $ 1 2 ! 1 tt 1 ! 1 tt " # ff 1 2 ! " # ! " # 1 2 1 2

Proof of Theorem 1

Completeness is obvious from the rules of Fig. 4. Determinism relies on a property of operator . In a previous version of this article [CAS 96] the claim that commutativity of the operator was sufficient to ensure determinism was wrong: this mistake has been pointed out by Charles Andre ´. We give here a correct proof for determinism.

We first establish that is associative. For this we need the following algebraic laws: This is straightforward by induction on IN.

Reaction of the system

A reaction of the system is a sequence of basic evolutions. For and , the reaction of the system to is :

where: if is infinite, and (the undefined state and undefined output event), otherwise is finite, the reaction 0 1 2 converges ; let 1 ! 1 " 1 # 1 , the steps to be activated and stopped and the updated values of the boolean time condition variables are defined using the initial and final states and 1 . The reaction is then defined to be where ! 1 " 1 # and:

! 1 1 tt ! 1 tt (started steps) ! 1 tt ! 1 1 tt (stopped steps) and # ff if , otherwise # # 1 .
This way, a step is considered to be activated (resp. stopped) if it was idle (resp. active) in and now is active (resp. idle) in . Similarly, we consider time condition to be set according to external time: the correction to the final state is defined according to what happened on the reaction and the values of the boolean time condition variables are set accordingly.

Finite state modeling of GRAFCET programs

The semantic model for GRAFCET program is given only for programs with at most one time condition (general case is in [CAS 95]). For a time condition we introduce two clock variables measures the elapsed time since the last start action on , , measures the elapsed time since the last stop action on .

Awaited events

It is clear that a way of defining a semantic model for GRAFCET programs would consist in exploring from any state all the possible transitions brought about by all the events of . In fact, not all events are possible from any state and it reduces the size of the model if we care for not introducing impossible transitions.

From a state ! " # , we define the awaited events to be

" 1 tt " 1 ff where if ! 1 tt # 1 ff , if ! 1 ff # 1 tt and otherwise.
Example For the grafcet of Fig. 2.(b), 1 . For state 5 1 ¯¯, 5 .

Liveness

The system can stay in a state as long as no edges occur. Edges for time conditions occur at definite date when and . Then staying in state ! " # entails the following inequations to hold:

if # 1 ff ! 1 tt , if # 1 tt ! 1 ff , tt otherwise.
We note the inequation associated with state . Similarly, we need where is replaced by .

Behavioural model: Timed automaton

The behavioural model for an GRAFCET program is a timed automaton [NSY 92] [AD 90]. Let , et be the sets of steps, boolean variables and time condition variables for a grafcet . The initial state of the system is defined by 0 . The behavioural model for grafcet is the timed automaton 0 where:

2 2 2 is the set of states, 0 ! 0 " 0 # 0 is defined by -! 1 0 tt 0 , ! 1 0 ff 0 -" 0 ff , -# 0 ff ,
is the set of timers of the automaton, is such that ! " # ( is the set of boolean terms [NSY 92] over the variables of ), where is defined inductively as follows:

1. , 2.

where and et and .

For the grafcet of Fig. 2.(b) we obtain the timed automaton given Fig. 5 10 . The states information is listed in Table 1. Remark 5 If 1 0 (Cf. 2.7), we move from state 5 to state 0 on an occurrence of : in this state the condition 0 1 is true if time does not pass: moving to state 1 takes no time.

Stability

Structural stability It is quite obvious that a couple is non stable if is infinite. In this case the corresponding reaction is defined as in section 3.7.

Let be a particular grafcet. An endless (undefined) reaction is possible only if state is reachable in the associated automaton . We will not discuss here the decidability of this problem [ACH 95] [KPSY 93] [RR 96b] [RR 96a]: in fact it has so far been proved decidable only for bounded reachability (i.e. reachability within a given time interval).

Temporal stability Temporal stability occurs only if there is a cycle in the automaton on which time does not progress. Checking the automaton for temporal stability then amounts to a reachability problem within a time interval of null duration. Again we refer the reader to [ACH 95] [KPSY 93] [RR 96b] [RR 96a] for a discussion on these problems.

Conclusion

The work presented in this paper differs from the ones where GRAFCET is translated in a reactive language [RR 94] [AP 92] [ML 92] since we model the metric aspect of time. The semantics given above is based on the idea of [AG 94] where the evolution rules are characterized by fixpoints 11 ; our semantics include the time conditions.

We have shown in this article that an operational semantics could be defined for GRAFCET giving this language a formal background. This semantics associates with a grafcet a timed automaton. A compiler from GRAFCET to timed automata has been written in CAML [LW 93] [WL 93]. On non trivial examples the size of the associated automaton is rather small with respect to the maximum number of possible states ( 2) as shown on Table 2. We may then think of verifying "real" grafcets with tools like VALET

Definition 2 A

 2 grafcet is a directed graph input output where the vertices are sets of steps and the edges belong with the set of transition conditions 2 . The mappings input and output are defined from to denote the input and output steps of a transition).

Figure 1 .

 1 Figure 1. Examples of grafcets

  Fig. 2.(a) has a time condition linking step 0 to step 1. A time condition is written 1 2 with 1 2 IR and (in standard GRAFCET 1 2 IN )

Figure 3 .

 3 Figure 3. Time diagram

Figure 4 .

 4 Figure 4. Operational semantics for GRAFCET

  function as the operational semantics is deterministic and complete. is an output event from. the ordered set , the function is monotonic. From the well-known Tarski's theorem [TAR 55] we deduce that the equation with has a least fixed point . As is finite with minimum element there exists IN such that . Moreover the following theorem holds :

Figure 5 .

 5 Figure 5. Timed automaton

  [RUS 96] or KRONOS[YOV 93] (although those tools can right now only handle small systems).Moreover, the model (namely a timed automaton) can be enriched to include the actions of GRAFCET to obtain a more accurate model of the system: the enriched model is then a hybrid system [ACH 95] [NOSY 93]. We then use the tool VALET [RUS 96] developped at L.A.N. (Nantes) to check properties on particular classes of hybrid

  ] [BB 91] [ER 85] [BD 91] [HCRP 91] [LLGL 91] [HAR 87]: a way to give GRAFCET a semantics is to translate GRAFCET programs to reactive programs [RR 94] [AP 92] [ML 92] (if the translation is sufficiently precise) since their semantics is formally defined [BG 91] [CPHP 87] [LBBG 86] [CR 95]

this is true if we consider that two events cannot occur simultaneously. Considering events to be in is another possible choice for which the semantics given below is always consistent.

i.e., a stopwatch is started at the time step 0 is activated and after 1 time units it ticks, step 0 being always active or not.

another stopwatch is started at the instant step 0 is stopped and after 2 time units it ticks unless step 0 has been activated during this period.

we remind the reader that the GRAFCET grammar is ambiguous.

From the previous laws we infer that which yields to and as we obtain

A similar calculus can be carried out for ending with the same result which proves that is associative. Now remark that in rule (g) of Fig. 4 the new state depends on the previous one and on and not on and written in the premisses. This ensures determinism. The commutativity (obvious) of the operator ensures that whatever the order the elements of the directed graph are listed in, the semantics of a grafcet is unique:

Structural stability

We define structural stability for a state ! " # , a grafcet and an output event , denoted inductively by :

Definition 4 A pair with is stable for a grafcet iff ( ) tt.

A pair with is non stable.

Calculus of a reaction

Definition 5 The 9 reaction from state 0 on an occurrence of event is the sequence 0 1 2 of basic evolutions from 0 such that 0 This sequence may be finite if there is a stable pair , and infinite otherwise. If the sequence is finite we write

Definition 6

The orbit of a reaction from on is the set .

Proposition 1 , contains at most one stable pair and if there is a stable pair in , this set is finite.

Proof of proposition 1

Direct from the definition 5 of a reaction. Now let . To calculate the orbit we introduce a function for a given grafcet of GRAFCET defined by : : such that The author wishes to thank Charles Andre ´for his careful reading of the many versions of the paper and the other anonymous referees for their comments which helped us to improve many parts of this work.


Sébastien Hénaff

Ina Taralova

René Lozi

Observers design for a new weakly coupled map function

In some engineering applications, such as chaotic encryption, chaotic maps have to exhibit required statistical and spectral properties close to those of random signals. However, most of the papers dealing with synchronization and observer synthesis consider maps exhibiting poor statistical and spectral properties. Moreover, most of the time these properties, however essential for the chaotic encryption, are simply neglected. Unlike these papers, in our work we present the analysis of a new ultra weakly coupled maps system introduced by Lozi. The model is a deterministic one, but exhibits spectral properties (spectrum, correlation and autocorrelation) close to those of random signals, and successfully passed all the statistical tests for closeness to random signals (NIST). Two different observers have been designed. The convergence rate has been discussed in the case of affine maps, and the conditions to decrease the convergence rate by a factor of 16 have been presented, based on the locally linear behaviour of the weakly coupled map.

I. INTRODUCTION

C HAOS has recently received a growing interest in various fields of science and engineering, and in particular, in secure communications. Pecora and Carroll were the first who synchronised chaotic systems [START_REF] Caroll | Synchronising chaotic circuits[END_REF]. Several chaotic cryptographic schemes have been proposed since [START_REF] Kocarev | Public-key encryption based on Chebyshev polynomials[END_REF], [START_REF] Fei | A secure digital signature algorithm based on elliptic curve and chaotic mappings[END_REF] and can be classified in three main categories : chaotic masking, chaotic modulation and chaotic shift keying.

In the cryptographic application, the chaotic generator must exhibit appropriate features close to those of the pseudorandom generators. These adapted properties have been studied more precisely in [START_REF] Alvarez | Some Basic Cryptographic Requirements for Chaos-Based Cryptosystems[END_REF], [START_REF] Götz | Discrete-time chaotic encryption systems -Part I. Statistical design approach[END_REF], [START_REF] Rukhin | A statistical test suite for pseudorandom numbers for cryptographic applications[END_REF].

Further researchers have then looked for finding appropriate systems testing different architectures : traditional chaotic maps (for example, the logistic map, the Hénon map [START_REF] Frey | Chaotic digital encoding: an approach to secure communication[END_REF], the generalised Hénon map) piece-wise linear map, cascaded map [START_REF] Tang | Chaotic communications using nonlinear transform pairs[END_REF] or coupled map lattice. In order to evaluate the features of the system, statistical tests developed for random number generators (RNG) can also be applied to chaotic maps, in order to gather evidence that the map generates "good" chaotic signals, i.e. having a considerable degree of randomness. To address this particular problem, different statistical tests for the systematic evaluation of the randomness of cryptographic random number generators can be applied, among which the most popular NIST (National Institute of Standards and Technology) tests.

It appears that most of the maps classically used for chaotic encryption do not pass successfully these tests, and don't exhibit the required features. However, most of the papers dealing with synchronisation and observer synthesis consider precisely these kinds of maps, highly inefficient in the context of chaotic encryption.

Unlike these models, Lozi [START_REF] Lozi | New enhanced chaotic number generators[END_REF] introduced in 2008 a new ultra weakly coupled maps system to generate pseudo-random signals which exhibits very good statistical properties. To use this system for secure communication, it must exhibit good spectral features and have to be observable. So the aim of this paper is to identify and to design an observer for the weakly coupled map system. This paper is organised as follow : after briefly presenting the system under investigation, sections three and four present the issues on parameter identifiability and system observability. Sections five and six propose and compare two different observers. Finally, a concluding section ends the paper.

II. SYSTEM DEFINITION

The N-th order function F can be written as :

X(n + 1) = F (X(n)) with X(n) = (x 1 (n), x 2 (n), . . . , x N (n)) X(n + 1) = F (X(n)) = A Λ(X(n))
where A is a N xN matrix defined by:

A =      1 -(N -1)ǫ 1 ǫ 1 . . . ǫ 1 ǫ 2 1 -(N -1)ǫ 2 . . . ǫ 2 . . . . . . . . . . . . ǫ N ǫ N . . . 1 -(N -1)ǫ N     
and Λ the tent function applied to every the components of X ∈ [-1; 1] N :

Λ(X(n)) =      Λ(x 1 (n)) Λ(x 2 (n))
. . .

Λ(x N (n))     
Since the function is piece-wise linear, it can be rewritten under a matrix form, by rewriting the tent function :

Λ(x) = 2x + 1 if x < 0 -2x + 1 else
or using the generic form :

Λ(x) = sx + 1 with : s = 2 if x < 0 -2 else
For the second order, the general system F is then governed by :

x 1 (n + 1) x 2 (n + 1) = A n x 1 (n) x 2 (n) + 1 1
where A n is :

A n = (1 -ǫ 1 )s 10 ǫ 1 s 20 ǫ 2 s 10 (1 -ǫ 2 )s 20
The rest of the paper only consider the second order system.

III. IDENTIFIABILITY

The purpose of this section is to determine if the coder can generate two identical outputs from two different encryption keys. In terms of system theory, it means that the system generates two identical outputs for two different parameter combinations. If this is the case, the base of the varying parameters has to be modified, and the parameter redundancies removed. To do so, the two outputs have to be equalized and their impact on the parameters has to be investigated.

The presented study concerns the second order system without the scaling. Let consider two second order systems systems governed by the same law :

   x 1 (n + 1) = (1 -ǫ 1 )Λ(x 1 (n)) + ǫ 1 Λ(x 2 (n)) x 2 (n + 1) = (1 -ǫ 2 )Λ(x 2 (n)) + ǫ 2 Λ(x 1 (n)) y(n) = x 1 (n)    x1 (n + 1) = (1 -ǫ1 )Λ(x 1 (n)) + ǫ1 Λ(x 2 (n)) x2 (n + 1) = (1 -ǫ2 )Λ(x 2 (n)) + ǫ2 Λ(x 1 (n)) ŷ(n) = x1 (n)
Considering the same outputs : (ŷ(n)) n = (y(n)) n , is it possible that the parameters would be different? The system is piece-wise linear, so let s ij ∈ {-2; 2} be defined by Λ(x i (n+ j)) = 1 + s ij .

s ij = -2 if x i (n + j) > 0 2 else ŷ(n) = y(n) ⇒ x1 (n) = x 1 (n) ŷ(n) = y(n) ŷ(n + 1) = y(n + 1) ⇒ (ǫ 1 -ǫ 1 )Λ(x 1 (n)) = ǫ1 Λ(x 2 (n)) -ǫ 1 Λ(x 2 (n))    ŷ(n) = y(n) ŷ(n + 1) = y(n + 1) ŷ(n + 2) = y(n + 2) ⇒ [(ǫ 1 -ǫ 1 )(1 -ǫ 1 )s 11 -ǫ1 ǫ2 ŝ21 + ǫ 1 ǫ 2 s 21 -(ǫ 1 -ǫ 1 )(1 -ǫ2 )ŝ 21 ]Λ(x 1 (n)) = ǫ 1 [-(ǫ 1 -ǫ 1 )s 11 -(1 -ǫ 2 )s 21 + (1 -ǫ2 )ŝ 21 ]Λ(x 2 (n))
Both x 1 and x 2 appear in the last. But {x 1 ; x 2 } is the state of the chaotic system, which has the property to visit the whole state space [-1; 1] 2 . In other words, to a given parameter combination {ǫ 1 , ǫ 2 , ǫ1 , ǫ2 , s 10 , s 20 , s 11 , s 21 , ŝ10 , ŝ20 , ŝ11 , ŝ21 } can be associated an infinity of states {x 1 ; x 2 }. One can consider then the independent variables Λ(x

1 (n)) et Λ(x 2 (n)).
In this case, one obtains the following system of equations :

   (ǫ 1 -ǫ 1 )(1 -ǫ 1 )s 11 -ǫ1 ǫ2 ŝ21 + ǫ 1 ǫ 2 s 21 -(ǫ 1 -ǫ 1 )(1 -ǫ2 )ŝ 21 = 0 ǫ 1 [-(ǫ 1 -ǫ 1 )s 11 -(1 -ǫ 2 )s 21 + (1 -ǫ2 )ŝ 21 ] = 0
One solution of the second equation is : ǫ 1 = 0. ǫ 1 is one of the system parameters, and this solution corresponds to a decoupled system. Therefore, this particular case is to be excluded. One obtains then the new system of equations :

   (ǫ 1 -ǫ 1 )(1 -ǫ 1 )s 11 -ǫ1 ǫ2 ŝ21 + ǫ 1 ǫ 2 s 21 -(ǫ 1 -ǫ 1 )(1 -ǫ2 )ŝ 21 = 0 -(ǫ 1 -ǫ 1 )s 11 -(1 -ǫ 2 )s 21 + (1 -ǫ2 )ŝ 21 = 0
The resolution leads to the following result:

∀(s 11 , s 21 , ŝ21 ) ∈ {-2; 2} 3 ,    s 21 = ŝ21 ⇒ {ǫ 1 , ǫ2 } = {ǫ 1 , ǫ 2 } s 11 = s 21 = -ŝ 21 ⇒ ǫ 1 = 0 et ǫ2 + ǫ 2 -ǫ1 = 0 -s 11 = s 21 = -ŝ 21 ⇒ ǫ 1 = 0 et ǫ2 + ǫ 2 + ǫ1 = 0
Knowing that the solution ǫ 1 = 0 is impossible, then the following conclusion can be drawn :

       ŷ(n) = y(n) ŷ(n + 1) = y(n + 1) ŷ(n + 2) = y(n + 2) ǫ 1 = 0 ⇒ {ǫ 1 , ǫ2 } = {ǫ 1 , ǫ 2 }
Finally, there are no redundant parameters and the whole set of parameter combinations can be used as a set of encryption keys of the coder, there are no parameters different from the one used for the encryption which could allow to decrypt the message.

IV. OBSERVABILITY

An affine system can be written as :

x(n + 1) = F (x(n)) = A.x(n) + B y(n) = Cx(n)
A second order affine system is observable if its observability matrix is a full-rank one :

O = C CA
Here, the system is piece-wise affine, therefore the observability matrix shall be different according to the region to which belong the system state. It is equal to :

O = 1 0 2(1 -ǫ 1 )s 10 2ǫ 1 s 10
which is full-rank since ǫ 1 > 0. Therefore, the system is observable.

V. LINEAR LUENBERGER OBSERVER

The system is piece-wise affine. Considering it as such, the present section identifies a piece-wise linear observer. The second order system can be rewritten using the affine form on the four domains where it is defined :

x(n + 1) = F (x(n)) = A.x(n) + B y(n) = Cx(n)    x(n + 1) = (1 -ǫ 1 )s 10 ǫ 1 s 20 ǫ 2 s 10 (1 -ǫ 2 )s 20 x(n) + 1 1 y(n) = 1 0 x(n)
The associated Luenberger system is :

x(n + 1) = Âx(n) + B + K(C x(n) -y(n))
K is a predefined gain such that the error e(n) tends to zero. Let consider x(n) and x(n) in the same region of definition. In this case, Â = A and therefore,

e(n + 1) = (A + KC)e(n)

One can identify the values of the gain K which cancel the eigenvalues of the matrix (A + KC) as a function of the affine system model. In this case, since the matrix is of second order, (A + KC) 2 = 0 therefore if the system states x and its estimate x belong to the same region of the state space twice consecutively, then the estimate shall synchronise with the original system.

Zero eigenvalues lead to the following solutions for the gain :

K =                                            2(ǫ 1 + ǫ 2 -2) 2 ǫ1 (2ǫ 2 -ǫ 2 2 -ǫ 1 ǫ 2 -1) if x(n) ∈ [-1; 0] 2 2(ǫ 2 -ǫ 1 ) 2 ǫ1 (2ǫ 2 -ǫ 2 2 + ǫ 1 ǫ 2 -1) if x(n) ∈ [0; 1] × [-1; 0] -2(ǫ 2 -ǫ 1 ) -2 ǫ1 (2ǫ 2 -ǫ 2 2 + ǫ 1 ǫ 2 -1) if x(n) ∈ [-1; 0] × [0; 1] -2(ǫ 1 + ǫ 2 -2) -2 ǫ1 (2ǫ 2 -ǫ 2 2 -ǫ 1 ǫ 2 -1) if x(n) ∈ [0; 1] 2
The zero eigenvalues assure the convergence in two iterations of the affine system if the system states remain in the same region of definition. Then the synchronisation may not take place for any states evolution.

The error of the linear system evolves following the equation :

e(n + 1) = (A + KC)e(n)

Since the matrix (A + KC) is nilpotent, if the system remains in the same domain of definition,

e(n + 2) = (A + KC) 2 e(n) = 0
In reality, the system states have a probability of 1/4 to fall twice consecutively in the same domain of definition. Considering that both systems (the original one, and the observer) start from the same region, then statistically three iterations are necessary before the trajectories converge. When the system falls consecutively into two different configurations, the equation which governs the error becomes :

e(n + 2) = (A 1 + K 1 C)(A 2 + K 2 C)e(n)
Let P 1 , P 2 be two transformation matrices which triangularise respectively the matrices (A 1 + K 1 C) and (A 2 + K 2 C), and let D 1 , D 2 be the two triangularised matrices. It comes :

e(n + 2) = P 1 D 1 P -1 1 P 2 D 2 P -1
2 e(n) As soon as P 1 = P 2 , the error e does not cancel in two iterations.

Now, the proper bases of the matrices (A + KC) are the same for the domains of definition x(n) ∈ [-1; 0] 2 and x(n) ∈ [0; 1] 2 . On the other hand, the bases are the same for the domains of definition

x(n) ∈ [0; 1] × [-1; 0] and x(n) ∈ [-1; 0] × [0; 1].
In the exemple, since the matrices D 1 and D 2 have zero eigenvalues, if

P 1 = P 2 , e(n + 2) = P 1 D 1 D 2 P -1
2 e(n) = 0 Finally, considering that the two systems are in the same domains of definition, they have one chance out of two to synchronise. Now, if one considers that the transition evolution of the two systems is independent in the domain of definition until they synchronise, they have statistically one chance out of sixteen to fall twice consecutively in the same domains of definition, which decreases the probability to synchronise at a given instant to 1/32.

Finally, two synchronisation strategies are possible : the classical one considers that the master system starts from any initial condition and follows the same law during the synchronisation. In this case, the slave system will synchronise -in average -after 32 iterations and it is governed by the equation :

x(n + 1) = F (x(n)) + B + K(C x(n) -y(n))
On the other hand, one can consider that the observer consists of several systems following different laws, each following its own law whatever the value of its state at the next iterates. A system can then be governed by the law :

S1 : x(n + 1) = Â1 x(n) + B + K 1 (C x(n) -y(n))
where A 1 et K 1 are derived from the definition of the systems related to the desired domain of definition, x(n) ∈ [-1; 0] 2 for instance. The observer systems have to cover the whole set of possible combinations of the state evolutions which allow to synchronise, i.e. four observers for a second order system. The advantage to use these systems lies in the fact that the probability that one of the forth systems synchronises with the original systems rises up to 1/2. Once synchronised, a classical observer can allow to follow the trajectory of the states of the original system.

If the classical use of a second order system leads to a synchronisation in 32 iterations in average, when the system order is increased, the synchronisation time increases exponentialy. The simultaneous use of several observers allows to divide the time for synchronisation by 16 for a second order system. The drawback is that several observer systems have to run simultaneously.

VI. ANOTHER OBSERVER

For the second order system, the autonomous system is :

   x 1 (n + 1) = (1 -ǫ 1 )Λ(x 1 (n)) + ǫ 1 Λ(x 2 (n)) x 2 (n + 1) = (1 -ǫ 2 )Λ(x 2 (n)) + ǫ 2 Λ(x 1 (n)) y(n) = x 1 (n)
With two measurements at the output y, it is possible to reconstruct the signal :

x 1 (n) = y(n) x 2 (n + 1) = ǫ 2 Λ(y(n)) -1
ǫ1 (y(n + 1) -(1ǫ 1 )Λ(y(n))) Finally, this reconstructor can identify the original state for all values, which is not the case of the first observer. Although, this method can be difficultly be applied to greater order systems.

VII. CONCLUSION

Most of the papers devoted to observer synthesis considered maps with poor statistical and spectral properties. We present here the synthesis of efficient observers for the system of weakly coupled map which satisfied all statistical (NIST) and spectral analysis tests. Two different observers have been designed. The convergence rate has been discussed in the case of affine maps, and the conditions to decrease the convergence rate by a factor of 16 have been presented, based on the locally linear behaviour of the weakly coupled map. The design and analysis of higher order map observers is currently under investigation.


B Bérard

F Cassez

S Haddad

Didier Lime
email: didier@cs.aau.dk

O H Roux

When are Timed Automata weakly timed bisimilar to Time Petri Nets ?

Keywords: Time Petri Nets, Timed Automata, Weak Timed Bisimilarity

In this paper, we compare Timed Automata (TA) with Time Petri Nets (TPN) with respect to weak timed bisimilarity. It is already known that the class of bounded TPNs is included in the class of TA. It is thus natural to try and identify the (strict) subclass T A wtb of TA that is equivalent to TPN for the weak time bisimulation relation. We give a characterisation of this subclass and we show that the membership problem and the reachability problem for T A wtb are P SP ACEcomplete. Furthermore we show that for a TA in T A wtb with integer constants, an equivalent TPN can be built with integer bounds but with a size exponential w.r.t. the original model. Surprisingly, using rational bounds yields a TPN whose size is linear.

Introduction

Expressiveness of timed models. The idea of adding explicit time to classical models was first introduced in the seventies for Petri nets [START_REF] Merlin | A study of the recoverability of computing systems[END_REF][START_REF] Ramchandani | Analysis of asynchronous concurrent systems by timed Petri nets[END_REF]. Since then, timed models based on Petri nets and finite automata were extensively studied, and various tools were developed for their analysis. In this paper, we focus on two well known models: Timed Automata (TA) from [START_REF] Alur | A theory of timed automata[END_REF] and Time Petri Nets (TPNs) from [START_REF] Merlin | A study of the recoverability of computing systems[END_REF], where a closed time interval is associated with each transition. More precisely, we are interested in comparing the expressive power of the two models with respect to weak timed bisimulation. Recall that there are unbounded TPNs which do not admit a bisimilar TA. This is a direct consequence of the following observation: the untimed language of a TA is regular which is not necessarily the case for PNs (and thus for TPNs). On the other hand, it was proved in [START_REF] Cassez | Structural Translation of Time Petri Nets into Timed Automata[END_REF] that bounded TPNs form a subclass of the class of timed automata, in the sense that for each bounded TPN N , there exists a TA which is weakly timed bisimilar to N . A similar result can be found in [START_REF] Lime | State class timed automaton of a time Petri net[END_REF], where it is obtained by a completely different approach. In another line of work [START_REF] Haar | Equivalence of Timed State Machines and safe Time Petri Nets[END_REF], Haar, Kaiser, Simonot & Toussaint compare Timed State Machines (TSM) and Time Petri Nets. They give a translation from TSM to TPN that preserves timed languages.

Our Contribution. In this work, we consider TPNs and label-free TA, i.e. where two different edges have different labels (and no label is ε) and we give a characterisation of the subclass T A wtb of timed automata which admit a weakly timed bisimilar TPN. This non intuitive condition relates to the topological properties of the so-called region automaton associated with a TA. To prove that the condition is necessary, we introduce the notion of uniform bisimilarity, which is stronger than weak timed bisimilarity. Conversely, when the condition holds for a TA, we provide two effective constructions of bisimilar TPNs: the first one with rational constants has a size linear w.r.t. the TA, while the other, which uses only integer constants has an exponential size. From this characterisation, we will deduce that given a TA, the problem of deciding whether there is a TPN bisimilar to it, is P SP ACE-complete. Thus, we obtain that the membership problem is P SP ACE-complete. Finally we also prove that the reachability problem is P SP ACE-complete.

Outline of the paper. Section 2 recalls the semantics of TPNs and TA, and the notion of timed bisimilarity. Section 3 explains the characterisation while Section 4 is devoted to a sketch of its proof. Finally we propose some discussion in Section 5.

Time Petri Nets and Timed Automata

Notations. Let Σ be a finite alphabet, Σ * (resp. Σ ω ) the set of finite (resp. infinite) words of Σ and Σ ∞ = Σ * ∪ Σ ω . We also use Σ ε = Σ ∪ {ε} with ε (the empty word) not in Σ.

The sets N, Q ≥0 and R ≥0 are respectively the sets of natural, non-negative rational and non-negative real numbers. We write 0 for the tuple v ∈ N n such that v(k) = 0 for all 1 ≤ k ≤ n. Let g > 0 in N, we write

N g = { i g | i ∈ N}. A tuple v ∈ Q n belongs to the g-grid if v(k) ∈ N g for all 1 ≤ k ≤ n.
An interval I of R ≥0 is a Q ≥0 -interval iff its left endpoint belongs to Q ≥0 and its right endpoint belongs to Q ≥0 ∪{∞}. We set I ↓ = {x | x ≤ y for some y ∈ I}, the downward closure of I and I ↑ = {x | x ≥ y for some y ∈ I}, the upward closure of I. We denote by

I(Q ≥0 ) the set of Q ≥0 -intervals of R ≥0 .
Timed Transition Systems and Equivalence Relations. Timed transition systems describe systems which combine discrete and continuous evolutions. They are used to define and compare the semantics of TPNs and TA.

A Timed Transition System (TTS) is a transition system S = (Q, q 0 , →), where Q is the set of configurations, q 0 ∈ Q is the initial configuration and the relation → consists of either delay moves q d -→ q , with d ∈ R ≥0 , or discrete moves q a -→ q , with a ∈ Σ ε . Moreover, we require standard properties for the relation →: Time-Determinism: if q d --→ q and q d --→ q with d ∈ R ≥0 , then q = q , 0-delay: q 0 --→ q, Additivity: if q d --→ q and q d --→ q with d, d ∈ R ≥0 , then q d+d ----→ q and Continuity: if q d --→ q , then for every d and d in R ≥0 such that d = d + d , there exists q such that q d --→ q d ---→ q . With these properties, a run of S can be defined as a finite or infinite sequence of moves

ρ = q 0 d0 -→ q 0 a0 -→ q 1 d1 -→ q 1 a1 -→ • • • q n dn -→ q n .
. . where discrete actions alternate with durations. We also write this run as q d0a0...dn...

-------→ q . The word Untimed(ρ) in Σ ∞ is obtained by the concatenation a 0 a 1 . . . of labels in Σ ε (so empty labels disappear), and

Duration(ρ) = |ρ| i=0 d i .
It is well-known that the notion of weak timed bisimilarity is central among equivalence relations between timed systems. From a TTS, we define the relation

→ >⊆ Q × (Σ ∪ R ≥0 ) × Q for a ∈ Σ and d ∈ R ≥0 by: -q d -→ > q iff ∃ ρ = q w -→ q with Untimed(ρ) = ε and Duration(ρ) = d, -q a -→ > q iff ∃ ρ = q w -→ q with Untimed(ρ) = a and Duration(ρ) = 0. Definition 1 (Weak Timed Bisimilarity). Let S 1 = (Q 1 , q 1 0 , → 1 ) and S 2 = (Q 2 , q 2
0 , → 2 ) be two TTS and let ≈ be a binary relation over

Q 1 × Q 2 .
We write q ≈ q for (q, q ) ∈ ≈. The relation ≈ is a weak timed bisimulation between S 1 and S 2 iff q 1 0 ≈ q 2 0 and for all a ∈ Σ ∪ R ≥0 -if q 1 a -→ > 1 q 1 and q 1 ≈ q 2 then ∃q 2 a -→ > 2 q 2 such that q 1 ≈ q 2 ; -conversely, if q 2 a -→ > 2 q 2 and q 1 ≈ q 2 then ∃q 1 a -→ > 1 q 1 such that q 1 ≈ q 2 . Two TTS S 1 and S 2 are weakly timed bisimilar, written S 1 ≈ W S 2 , if there exists a weak timed bisimulation relation between them.

Strong timed bisimilarity would require similar properties for transitions labeled by a ∈ Σ ∪ R ≥0 , but with a -→ instead of a -→ >. Thus it does not take into account the possibility of splitting a run while keeping the global duration. In the rest of the paper, we abbreviate weak timed bisimilarity by bisimilarity and we explicitly name other equivalences when needed. Time Petri Nets. Introduced in [START_REF] Merlin | A study of the recoverability of computing systems[END_REF], and studied more recently in [START_REF] Pezzé | Time Petri Nets: A Primer Introduction[END_REF], Time Petri Nets (TPNs) associate a (closed) time interval with each transition. Definition 2 (Labeled Time Petri Net). A Labeled Time Petri Net N over Σ ε is a tuple (P, T, Σ ε , • (.), (.)

• , M 0 , Λ, I) where P is a finite set of places, T is a finite set of transitions with P ∩ T = ∅, • (.) ∈ (N P ) T is the backward incidence mapping, (.)

• ∈ (N P ) T is the forward incidence mapping, M 0 ∈ N P is the initial marking, Λ : T → Σ ε is the labeling function and I : T → I(Q ≥0 ) associates with each transition a closed firing interval.

A TPN N is a g-TPN if for all t ∈ T , the interval I(t) has its bounds in N g . We also use • t (resp. t • ) to denote the set of places

• t = {p ∈ P | • t(p) > 0} (resp. t • = {p ∈ P | t • (p) > 0})
as it is common is the literature.

A marking M of a TPN is a mapping in N P , with M (p) the number of tokens in place p. A transition t is enabled in a marking M iff M ≥ • t. We denote by En(M ) the set of enabled transitions in M . An enabled transition t can be fired if the time elapsed since it was last enabled belongs to the interval I(t), its firing resulting in the new marking M = M -• t + t • . A valuation ν is a mapping in (R ≥0 ) En(M ) , where ν(t) represents the time elapsed since transition t was last enabled. It remains to define when a transition t is newly enabled, i.e. when the value ν(t) is reset. In this paper, we choose persistent atomic semantics, which is slightly different from the classical semantics [START_REF] Berthomieu | Modeling and verification of time dependent systems using time Petri nets[END_REF][START_REF] Aura | A causal semantics for time Petri nets[END_REF], but equivalent when the net is bounded [START_REF] Bérard | Comparison of the Expressiveness of Timed Automata and Time Petri Nets[END_REF]. The predicate is defined by: ↑enabled(t , M, t) = t ∈ En(M -• t + t • ) ∧ (t ∈ En(M )), which amounts to consider that the firing of a transition is performed in an atomic step, the transition currently fired behaving like the other transitions.

The set ADM(N ) of (admissible) configurations consists of the pairs (M, ν) such that ν(t) ∈ I(t) ↓ for each transition t ∈ En(M ). Thus time can progress in a marking only up to the minimal endpoint of the intervals for all enabled transitions. Definition 3 (Semantics of TPN). The semantics of a TPN N = (P, T, Σ ε , • (.), (.)

• , M 0 , Λ, I) is a TTS S N = (Q, q 0 , →) where Q = ADM(N ), q 0 = (M 0 , 0)

and → is defined by: -either a delay move (M, ν)

d --→ (M, ν + d) iff ∀t ∈ En(M ), ν(t) + d ∈ I(t) ↓ ,
-or a discrete move (M, ν)

Λ(t) ---→ (M -• t + t • , ν ) where ∀t ∈ En(M -• t + t • ), ν (t ) = 0 if ↑enabled(t , M, t) and ν (t ) = ν(t) otherwise, iff t ∈ En(M ) is such that ν(t) ∈ I(t).
We simply write (M, ν) w -→ to emphasise that a sequence of transitions w can be fired. If Duration(w) = 0, we say that w is an instantaneous firing sequence. A net is said to be k-bounded if for each reachable configuration (M, ν) and for each place p, M (p) ≤ k. Timed Automata. First defined in [START_REF] Alur | A theory of timed automata[END_REF], the model of timed automata (TA) associates a set of non negative real-valued variables called clocks with a finite automaton.

Let X be a finite set of clocks. We write C(X) for the set of constraints over X, which consist of conjunctions of atomic formulas of the form x h for x ∈ X, h ∈ Q ≥0 and ∈ {<, ≤, ≥, >}.

Definition 4 (Timed Automaton). A Timed Automaton

A over Σ ε is a tuple (L, 0 , X, Σ ε , E, Inv) where L is a finite set of locations, 0 ∈ L is the initial location, X is a finite set of clocks, E ⊆ L × C(X) × Σ ε × 2 X × L
is a finite set of edges and Inv ∈ C(X) L assigns an invariant to each location. An edge e = , γ, a, R, ∈ E represents a transition from location to location with guard γ and reset set R ⊆ X. We restrict the invariants to conjunctions of terms of the form x h for x ∈ X, h ∈ N and ∈ {<, ≤}.

When we need to consider label-free automata, we simply assume that each edge has a unique label, different from ε.

A valuation v is a mapping in R X ≥0 . For a valuation v and d ∈ R ≥0 , the valuation v + d is defined by (v + d)(x) = v(x) + d for each clock x, and for R ⊆ X, the valuation v[R → 0] maps each variable in R to the value 0 and agrees with v over X \ R. Constraints of C(X) are interpreted over valuations: we write v |= γ when the constraint γ is satisfied by v.

Definition 5 (Semantics of TA). The semantics of a TA

A = (L, 0 , X, Σ ε , E, Inv) is a TTS S A = (Q, q 0 , →) where Q = L × (R ≤0 ) X , q 0 = ( 0 , 0) and → is defined by: -either a delay move ( , v) d --→ ( , v + d) iff v + d |= Inv( ), -or a discrete move ( , v) e -→ ( , v ) iff there exists some e = ( , γ, a, R, ) ∈ E s.t. v |= γ, v = v[R → 0] and v |= Inv( ).
Elementary zones of a TA. Recall [START_REF] Alur | A theory of timed automata[END_REF] that, if m is the maximal constant appearing in atomic formulas x c of A, an equivalence relation with finite index can be defined on clock valuations, leading to a partition of (R ≥0 ) X , with the following property: two equivalent valuations have the same behaviour under progress of time and reset operations, with respect to the constraints. Note that a partition using any K ≥ m would have the same property. Also, the construction can be extended to a g-grid, by taking all constants of the form i g , 0 ≤ i ≤ K•g instead of {0, 1, . . . , m}. Finally, taking K = +∞ (as depicted in Figure 1 on the left) leads to a similar structure except for the fact that the partition is infinite. In this paper, the elements of the partition are called elementary zones and we consider a slight variation for their definition: we take a constant K ≥ m + 1 and with each clock x ∈ X, we associate an interval in the set

{{0}, ]0, 1[, {1}, . . . , {K- 1}, ]K -1, K[, [K, +∞[}, instead of keeping {K} separately.
As usual, we also specify the ordering on the fractional parts for all clocks x such that x < K. Such a partition is represented in Figure 1 (on the right) for the set of two clocks X = {x, y} and K = 3. For this example, elementary zones Z 1 and Z 2 are described by the constraints:

Z 1 : (2 < x < 3) ∧ (1 < y < 2) ∧ (0 < f rac(y) < f rac(x)) and Z 2 : (x ≥ 3) ∧ (1 < y < 2).
If Z and Z are elementary zones, Z is a time successor of Z, written Z ≤ Z , if for each valuation v ∈ Z, there is some d ∈ R ≥0 such that v + d ∈ Z . For each elementary zone Z, there is at most one elementary zone such that (i) Z is a time successor of Z, (ii) Z = Z and (iii) there is no time successor Z such that Z ≤ Z ≤ Z . When it exists, this elementary zone is called the immediate successor of Z and is denoted by succ(Z).

A characterisation of TA bisimilar to TPNs

Regions of a timed automaton. Since our results are mainly based on the region automaton, we recall its definition [START_REF] Alur | A theory of timed automata[END_REF]. For a TA A, the region automaton R(A) is a finite automaton, with states of the form ( , Z), where is a location of A and Z an elementary zone of (R ≥0 ) X , for a constant K and a granularity g.

We call region a pair ( , Z) as above. The regions of R(A) are built inductively from the initial one ( 0 , 0) by the following transitions over the set of labels

{succ} ∪ Σ ε : ( , Z) succ ---→ ( , succ(Z)) if succ(Z) |= Inv( ) and ( , Z) a -→ ( , Z ) if there is a transition ( , γ, a, R, ) ∈ E such that Z |= γ and Z = Z[R → 0],
with Z |= Inv( ). Thus, only reachable regions appear in R(A). A region ( , Z) is said to be maximal in R(A) with respect to if no succ-transition is possible from (l, Z).

We now give a definition which distinguishes time-closed and time-open regions. It is equivalent to the original one but more convenient for our proofs and it fits both cases, wether K is finite or infinite. Definition 6 (Regions of an automaton w.r.t. the g-grid and constant K). A time-closed (description of a) region r is given by: r the location of r, -min r ∈ N X g with ∀x, min r (x) ≤ K, the minimal vector of the topological closure of r, -ActX r = {x ∈ X | min r (x) < K} the subset of relevant clocks, -the number size r of different fractional parts for the values of relevant clocks in the N ActXr g grid, with 1 ≤ size r ≤ M ax(|ActX r |, 1) and the onto mapping ord r : X → {1, . . . , size r } giving the ordering of the fractional parts. By convention, ∀x ∈ X \ ActX r , ord r (x) = 1.

Then r = {( r , min r + δ) | δ ∈ R X ≥0 ∧ ∀x, y ∈ ActX r [ord r (x) = 1 ⇔ δ(x) = 0] ∧ δ(x) < 1/g ∧ [ord r (x) < ord r (y) ⇔ δ(x) < δ(y)]}
A time-open (description of a) region r is defined with the same attributes (and conditions) as the time-closed region by:

r = {( r , min r + δ + d) | d ∈ R >0 ∧ ∀x ∈ ActX r , δ(x) + d < 1/g}.
The set [X] r is the set of equivalence classes of clocks w.r.t. their fractional parts, i.e. x and y are equivalent iff ord r (x) = ord r (y).

Remark that min r / ∈ r except if there is a single class of clocks relative to r (for instance if the corresponding zone is a singleton). In the sequel, the topology of the regions is implicitly derived from the one of its associated zone. We note r, the topological closure of r: it is a finite union of regions and from the definition, min r is the minimum vector of r.

Of course, when K = +∞, the part about relevant clocks, for which the value is less than K, can be omitted (since ActX r = X). While the case K = +∞ results in an infinite partition, it makes some proofs simpler, because the extremal case where a clock value is greater than K is avoided. This hypothesis can be lifted afterward.

Furthermore when K = +∞, a region admits a single description whereas when K is finite, some regions admit both time-open and time-closed descriptions (for instance a region associated with zone Z 2 in fig. 1). Note that time elapsing leads to an alternation of time-open regions (where time can elapse) and timeclosed ones (where no time can elapse). Reachability. For a reachable region r of R(A), not all configurations of r are reachable. Nevertheless, by induction on the reachability relation inside R(A), it can be shown that every configuration is quasi-reachable in the following sense: For any reachable region r, there is a region reach(r) w.r.t. the 1-grid and constant K = ∞ such that (i) reach(r) ⊂ r, (ii) each configuration of reach(r) is reachable and (iii) if reach(r) is a time-open region then r admits a time-open description else r admits a time-closed description.

As a consequence, we have: ∀x ∈ ActX r , min reach(r) (x) = min r (x) and ∀x ∈ X \ ActX r , min reach(r) (x) ≥ K and ord r restricted to ActX r is identical to ord reach(r) .

Consider the relation R defined by

(l, v) R (l, v ) iff ∀x ∈ X, v (x) = v(x) ∨ (v(x) ≥ K ∧ v (x) ≥ K).
Then R is a strong timed bisimulation relation. From the previous observations, we note that each configuration of a reachable region is strongly time bisimilar to a reachable configuration of this region. Thus speaking about reachability of regions is a slight abuse of notations.

We can now state our main results.

Theorem 1 (Characterisation of TA bisimilar to some TPN). Let A be a (label-free) timed automaton and R(A) its region automaton w.r.t. the 1-grid and a constant K strictly greater than any constant occurring in the automaton, then A is weakly timed bisimilar to a time Petri net iff for each region r of R(A) and for each edge e from A, (a) Every region r such that r ∩ r = ∅ is reachable

(b) ∀( r , v) ∈ r, if ( r , v) e -→ then ( r , min r ) e -→ (c) ∀( r , v) ∈ r, if ( r , min r ) e -→ then ( r , v) e -→.
Furthermore, if these conditions are satisfied then we can build a 1-bounded 2-TPN bisimilar to A whose size is linear w.r.t. the size of A and a 1-bounded 1-TPN bisimilar to A whose size is exponential w.r.t. the size of A. We denote by T A wtb the corresponding subclass of timed automata.

Theorem 2 (Complexity results). Given a (label-free) timed automaton A, deciding whether there is a TPN weakly timed bisimilar to A is P SP ACEcomplete. The reachability problem for the class T A wtb is P SP ACE-complete.

The characterisation of Theorem 1 is closely related to the topological closure of reachable regions: it states that any region intersecting the topological closure of a reachable region is also reachable and that a discrete step either from a region or from the minimal vector of its topological closure is possible in the whole topological closure. Consider the two TA A 0 and A 1 in Figure 2. The automaton A 0 admits a bisimilar TPN whereas A 1 does not. Indeed, the region r = {( 1 , x = 1 ∧ 0 < y < 1} is reachable. The guard of edge c is true in min r = ( 1 , (1, 0)) whereas it is false in r.

0 x ≤ 1 1 x ≤ 1 l2 x ≤ 1, a, ∅ x = 1, b, {y} x ≥ 1 ∧ y ≤ 0, c, ∅ A0 : 0 x ≤ 1 1 x ≤ 1 l2 x ≤ 1, a, {y} x ≥ 1 ∧ y ≤ 0, c, ∅ A1 :
Fig. 2. Two automata with different behaviour w.r.t bisimulation with a TPN

The next section is devoted to a sketch of the proof of Theorem 1. Some additional formal proofs are given in the Appendix. The complete proofs can be found in [START_REF] Bérard | Comparison of the Expressiveness of Timed Automata and Time Petri Nets[END_REF]. [START_REF] Bérard | Comparison of the Expressiveness of Timed Automata and Time Petri Nets[END_REF] Proof of Theorem 1

Necessary condition

From bisimulation to uniform bisimulation. As a first step, we prove that when a TPN and a TA are bisimilar, this relation can in fact be strengthened in what we call uniform bisimulation. We first need a lemma which points out the effect of time granularity on the behaviour of TPN. The proof is in the Appendix. Lemma 1. Let (M, ν) and (M, ν + δ) be two admissible configurations of a g-TPN with ν, δ ∈ R En(M ) ≥0

. Let w be an instantaneous firing sequence, then:

(i) (M, ν) w -→ implies (M, ν + δ) w -→ (ii) If ν ∈ N g En(M ) and δ ∈ [0, 1/g[ En(M ) then (M, ν + δ) w -→ implies (M, ν) w -→
Lemma 2 is the central point for the proof of necessity. It shows that bisimulation implies uniform bisimulation for the g-grid with K = ∞. Uniform bisimulation means that given a reachable region, one can exhibit first a configuration of the net bisimilar to the minimal point of the region and secondly a mapping from the enabled transitions of this configuration to the clocks of the automaton such that for any configuration inside the topological closure of this region one obtains a bisimilar configuration of the net using this mapping. Roughly speaking, a unique mechanism is used for every configuration of the topological closure of the region to obtain a bisimilar configuration of the net.

Lemma 2 (From bisimulation to uniform bisimulation). Let A be a timed automaton bisimilar to some g-TPN N via some relation R and let R(A) be the region automaton of A w.r.t. the g-grid and the constant K = ∞. Then:

-if a region r belongs to R(A) then r also belongs to R(A); -for each reachable region r, there exist a configuration of the net (M r , ν r ) with ν r ∈ N En(Mr) g and a mapping φ r : En(M r ) → [X] r such that:

• If r is time-closed, then for each δ ∈ R X ≥0 such that ( r , min r + δ) ∈ r, ( r , min r + δ) R (M r , ν r + proj r (δ)), • If r is time-open, then for each δ ∈ R X ≥0 , d ∈ R ≥0 such that ( r , min r + δ + d) ∈ r, ( r , min r + δ + d) R (M r , ν r + proj r (δ) + d),
where proj r (δ)(t) = δ(φ r (t)).

Proof. First note that the choice of a particular clock x in the class φ r (t) is irrelevant when considering the value δ(x). Thus the definition of proj r is sound. The proof is an induction on the transition relation in the region automaton. The basis case is straightforward with {(l 0 , 0)} and {(M 0 , 0)}. The induction part relies on lemma 1, with 4 cases, according to the incoming or target region and to the nature of the step: In order to complete the proof, we successively show that if the conditions are satisfied by the g-grid and K = ∞, they also hold for the 1-grid and K = ∞, and finally that they are satisfied by the 1-grid and the usual finite constant. This is done by Lemmas 3 and 4, stated and proved in the Appendix.

Sufficient condition

Starting from a TA A satisfying the conditions of Theorem 1, we build a 2-TPN bisimilar to A. We describe the construction and give the proof of correctness in the Appendix. We do not present here the construction of a 1-TPN, which can be found in [START_REF] Bérard | Comparison of the Expressiveness of Timed Automata and Time Petri Nets[END_REF].

For this construction, all edges are weighted by 1. Omitted labels for transitions stand for ε. A firing interval [0, 0] is indicated by a blackened transition and intervals [0, ∞[ are omitted. A double arrow between a place p and a transition t indicates that p is both an input and an output place for t.

W.l.o.g. we assume that an invariant never forbids to enter a state (by adding constraints to the input transitions). We then remark that x < c occurring in an invariant of A may be safely omitted. If it would forbid the progress of time in some configuration, then the associated region would be a maximal timeopen region r. Due to condition (a), r is reachable but since r is time-open, r ∩ succ(r) = ∅, so that succ(r) is reachable which contradicts the maximality of r. Clock constraints. The atomic constraints associated with a clock x are arbitrarily numbered from 1 to n(x) where n(x) is the number of such conditions. When x ≤ h occurs in at least one transition and in at least one invariant, we consider it as two different conditions. Then we add places (Rtodo x i ) i≤n(x)+1 for the reset operations.

We build a subnet for each atomic constraint x h occurring in a transition of the TA, and one for each condition x ≤ h occurring in an invariant. Figure 3 below shows the subnets corresponding to x < h (with h > 0) on the left and x ≤ h on the right. Since constant 1 2 appears in interval bounds, the resulting TPN is a 2-TPN.

• T x<h F x<h change x<h [h -1 2 , h -1 2 ] Rtodo x i Rtodo x i+1 reset 1 x<h reset 2 x<h • T x≤h F x≤h change x≤h [h + 1 2 , h + 1 2 ] Rtodo x i Rtodo x i+1 reset 1 x≤h reset 2
x≤h Fig. 3. The subnets for x < h (with h > 0) and x ≤ h

Locations and edges. With each location of the automaton, we associate an eponymous place . The place is initially marked iff the location is the initial one. The invariant Inv( ) is tested with the subnets corresponding to its Rtodo

x 1 n(x 1 )+1 Rtodo x 2 n(x 2 )+1 Rtodo x 2 1

Rtodo

x n(e) 1

Rtodo

x n(e) n(x n(e) )+1

f iree, a atomic constraints. To simulate an edge ( , γ, a, R, ), we must test the atomic constraints from γ = γ 1 ∧. . .∧γ m(e) , using the places corresponding to true in the associated subnets, and reset successively all the clocks in R = {x 1 , . . . , x n(e) } by instantaneous transitions. This is done by the subnet in Figure 4.

Conclusion

In this paper, we considered the (semantic) subclass T A wtb of labeled-free TA such that a timed automaton A is in T A wtb if and only if there is a TPN N weakly timed bisimilar to A. We obtained a characterisation of this class, based on the region automaton associated with A. To prove that our condition is necessary, we introduced the notion of uniform bisimulation between TA and TPNs.

For the sufficiency, we proposed two constructions. From this characterisation, we have proved that for the class T A wtb , the membership problem and the reachability problem are P SP ACE-complete. The techniques introduced here also lead to a similar characterisation for TA with diagonal constraints and to a simpler one for TA without strict or diagonal constraints (see [START_REF] Bérard | Comparison of the Expressiveness of Timed Automata and Time Petri Nets[END_REF]), the complexity results being unchanged. These techniques also give some insight for use of the region automaton in order to obtain expressivity results.

From (M r , ν r + proj r (δ)), the sequence w leads to some (M , ν ) bisimilar to ( r , min r + δ )). We now show how to define M r , ν r and φ r . First M r = M . Second, ν r (t) = ν r (t) for transitions t always enabled during the firing sequence and ν r = 0 otherwise. At last, φ r is obtained from φ r as follows. Let t be a transition newly enabled during the firing sequence, then φ r (t) is associated to the class of index 1. Let t be a transition always enabled during the firing sequence. There are three cases to consider for φ r (t): either there is a x ∈ φ r (t) not reset, then φ r (t) = |x] r otherwise φ r (t) is the class of maximal index which precedes φ r (t) and contains a clock not reset or else the class of index 1. The two last affectations are sound since it means that whatever the value of δ(t) fulfilling the order between classes, the firing sequence w leads to bisimilar configurations (as being bisimilar to the same configuration of the automaton). Case b. The case where r is a time-open region is handled in a similar way.

Let ( r , min r +δ 0 + d 0 ) be some element of r. Suppose that ( r , min

r +δ 0 + d 0 ) e -→ ( , v + δ 0 ) with ∀x ∈ R(e), v (x) = δ 0 (x) = 0, ∀x / ∈ R(e), v (x) = min r (x) ∧ δ 0 (x) = δ 0 (x) + d 0 .
Then in N there is a firing sequence (M r , ν r + proj r (δ 0 ) + d 0 ) w -→ labeled by e. Due to lemma 1, this firing sequence is also fireable from any (M r , ν r + proj r (δ) + d) bisimilar to ( r , min r + δ + d) ∈ r. By bisimilarity, ( r , min r +δ + d) e -→ for any ( r , min r + δ + d) ∈ r. Let r be the region including (l , v + δ 0 ), then any configuration of r is reachable by this discrete step. Note that l r = l and min r = v . From (M r , ν r +proj r (δ)+d), the sequence w leads to some (M , ν ) bisimilar to (l r , min r + δ )). We now show how to define M r , ν r and φ r . First M r = M . Second, ν r (t) = ν r (t) for transitions t always enabled during the firing sequence and ν r = 0 otherwise. At last, φ r is obtained from φ r as follows. Let t be a transition newly enabled during the firing sequence, then φ r (t) is associated to the class of index 1. There are three cases to consider for φ r (t): either there is a x ∈ φ r (t) not reset, then φ r (t) = |x] r otherwise φ r (t) is the class of maximal index which precedes φ r (t) and contains a clock not reset or else the class of index 1. The two last affectations are sound since it means that whatever the value of δ(t) fulfilling the order between classes, the firing sequence w leads to bisimilar configurations (as being bisimilar to the same configuration of the automaton).

-→. ( r , v r + δ) is bisimilar to (M r , ν r + proj r (δ)). Thus ( r , min r + δ) e -→ (l , min r + δ) d -→ (l , min r + δ + d).
Then this region can be reached via a discrete step into a time-closed region followed by a time step. So we do not need to examine this case.

A.3 Lemmas 3 and 4

We may safely assume that any atomic constraint related to a clock x occurring in the invariant of a location is added to the guard of each incoming transition which does not reset x.

Lemma 3 (about the conditions and the grid). Let A be a timed automaton, K = ∞ and g > 0 in N. If conditions (a),(b),(c) are satisfied by the region automaton associated with the g-grid, then they are satisfied by the region automaton associated with the 1-grid.

B Proof of the first construction of Theorem 1

We decompose the reachable configurations (and markings) into intermediate ones (some W i e is marked) and permanent ones (some is marked). An easy induction shows that in permanent configurations (M, ν) the enabled timed transitions relative to a clock are "synchronised": ν(change c ) = ν(change c ) = ν(reach c ) as soon as c, c , c relates to the same clock x. We define ν(x) as this common value if at least one such transition is enabled and otherwise ν(x) = K(x) where K(x) is the maximal value relative to clock x occurring in the net N . Furthermore from any intermediate configuration (M, ν), the behaviour of the net is quasi-deterministic until it reaches a permanent configuration: there are only firing sequences (i.e. no time step) and some of them lead to permanent configurations. Furthermore these permanent configurations (say (M next , ν next )) have the same marked place and the same values ν next (x).

It is also obvious that once some f ire e is fired, the construction ensures the existence of a "resetting" sequence which re-initialises the widgets associated to the clocks to be reset. Bisimulation relation. We now define the relation R between reachable configurations of the automaton A and the net N . Let us define ( , v)R(M, ν) iff:

-either M is a permanent marking and M ( ) is marked and if ν(x) < K(x) then v(x) = ν(x) else v(x) ≥ K(x). -or M is an intermediate marking leading to some permanent (M next , ν next ) and ( , v)R(M next , ν next ). This definition is sound due to the common features of the different (M next , ν next ).

It remains to prove that R is a bisimulation, which is done in the next lemma.

Lemma 5. The relation R defined above is a weak timed bisimulation.

Proof. We first consider moves from A. If c = [x ≥ a] then v(x) ≥ a which implies ν(x) ≥ a and that T x≥a is marked (eventually with the help of σ ). If c = [x > a] then let r be the region to which ( , v) belongs. min r (x) = v(x) . Using condition (b), (l, min r ) e -→. Thus v(x) ≥ min r (x) ≥ a + 1 which implies ν(x) ≥ a + 1 and that T x>a is marked (eventually with the help of σ ). If c = [x ≤ a] then v(x) ≤ a which implies ν(x) ≤ a and that T x≤a is marked (remember that change x≤a fires when ν(x) = a + 1/2). If c = [x < a] then let r be the region to which ( , v) belongs. Then there exists ( , v 1 ) ∈ r with v 1 (x) = v(x) . Using condition (b) and then (c), (l, v 1 ) e -→. Thus v(x) ≤ v 1 (x) ≤ a -1 which implies ν(x) ≤ a -1 and that T x<a is marked (remember that change x<a fires when ν(x) = a -1/2). Thus f ire e is fireable from (M , ν ). We complete σ by the "resetting" sequence leading to a configuration bisimilar to ( , v )

If M is an intermediate marking, one fires a sequence leading to some (M next , ν next ) and performs the previous simulation. Thus we only to need to examine the case of f ire e (M is then a permanent marking). Let r be the region to which ( , v) belongs. We will show that ( , min r ) e -→. Then by condition (c), we will obtain that ( , v)

2 Fig. 1 .

 21 Fig. 1. Partitions of (R + ) 2 with K = +∞ and K = 3

  1. a time step from a time-closed region, 2. a time step from a time-open region, 3. a discrete step into a time-closed region, and 4. a discrete step into a time-open region. Detailed proofs for these cases are given in the Appendix. Proof of Necessity. The fact that conditions (a), (b) and (c) of Theorem 1 are satisfied with respect to the g-grid and constant K = ∞ is straightforward: (a) This assertion is included in the inductive assertions. (b) Let r be a reachable region, let ( r , min r + δ) ∈ r be a configuration with δ ∈ [0, 1/g[ X , then ∃(M, ν) ν ∈ N En(M ) g bisimilar to ( r , min r ) and (M, ν + δ ) with δ ∈ [0, 1/g[ En(M ) bisimilar to ( r , v + δ). Suppose that ( r , min r + δ) e -→, then (M, ν + δ ) w -→ with w an instantaneous firing sequence and label(w) = e. Now by lemma 1-b, (M, ν) w -→, thus ( r , min r ) e -→. (c) Let r be a region, and ( r , min r + δ) ∈ r with δ ∈ [0, 1/g] X thus ∃(M, ν) bisimilar to ( r , min r ) and (M, ν + δ ) with δ ∈ [0, 1/g] En(M ) bisimilar to ( r , min r + δ). Suppose that ( r , min r ) e -→, then (M, ν) w -→ with w an instantaneous firing sequence and label(w) = e. Now by lemma 1-a, (M, ν + δ ) w -→, thus ( r , min r + δ) e -→.

Fig. 4 .

 4 Fig. 4. The subnet for edge e = ( , γ = γ1 ∧ . . . ∧ γ m(e) , a, R = {x1, . . . , x n(e) }, )

4 .

 4 A discrete step into a time-open region. In order to reach a timeopen region by a discrete step, the corresponding transition must start from a time-open region and must not reset any clock. Let ( r , min r + δ + d) ∈ r and ( r , min r + δ + d) e -→ (l , min r + δ + d). Here we have used the hypothesis that no clock is reset. Then there is a firing sequence (M r , ν r + proj r (δ) + d) w -→ labeled by e. Due to the lemma 1, (M r , ν r + proj r (δ))

  w

Case 1 :

 1 ( , v) e -→ ( , v ) First, let us prove that (M, ν) σ -→ with σ labeled by e. At first, σ begins by σ which consists to fire all the change c fireable leading to some (M , ν ) (with ( , v)R(M , ν )). Now we prove that (M , ν ) f iree ---→. By definition of R, M ( ) is marked. Let c be a condition occurring in the guard of e.

Case 2 :

 2 ( , v) d -→ ( , v + d)Suppose that x ≤ a belongs to the invariant of . This means that v(x) + d ≤ a. Thus from (M, ν), we let a time d elapse interleaved with possible firings of change transitions. The stop transitions associated to will be possibly firable but only at the end of this step sequence.If M is an intermediate marking, one fires a sequence leading to some (M next , ν next ) and performs the previous simulation.Conversely, we consider moves from N . Case 3: (M, ν) t -→ (M , ν ) If t is labeled by , then by construction ( , v)R(M , ν ).

  Let c be a condition occurring in the guard of e. If c = [x ≥ a] then T x≥a is marked which implies that ν(x) ≥ a and then v(x) ≥ a, thus min r (x) = v(x) ≥ a.If c = [x > a] then then T x>a is marked which implies that ν(x) ≥ a + 1 and then v(x) ≥ a + 1 thus min r (x) = v(x) ≥ a + 1 > a If c = [x ≤ a] then T x≤a is marked which implies that ν(x) ≤ a + 1/2 and then v(x) ≤ a + 1/2 thus min r (x) = v(x) ≤ a If c = [x < a] then T x<a is marked which implies that ν(x) ≤ a -1/2 and then v(x) ≤ a -1/2 thus min r (x) = v(x) ≤ a -1 < a So ( , v) e -→ ( , v) for some ( , v ). By construction of N and definition of R, ( , v )R(M , ν ).

Case 4 :

 4 (M, ν) d -→ (M, ν + d) An intermediate marking cannot let elapse time. Thus M is a permanent marking. Let x ≤ a belonging to the invariant of

A.2 Proof of Lemma 2

Proof (of points 1, 2, 3, 4). 1. A time step from a time-closed region. Let r be a time-closed region which is not maximal and let us denote r = succ(r) the immediate time successor of r. Let ( r , min r + δ 0 ) be some item of r. ( r , min r + δ 0 ) d -→ for some d > 0. Thus (by induction hypothesis) in N there is a step sequence of (M r , ν r + proj r (δ 0 )) d0t1...tndn -------→ with all transitions labelled by and d k = d. Let d k be the first non zero elapsing of time. By application of lemma 1-b, the firing sequence t 1 . . . t k is fireable from (M r , ν r ).

Let us choose (M r , ν r ) the configuration reached by this sequence. By application of lemma 1-a, this firing sequence is also fireable from any (M r , ν r + proj r (δ)) bisimilar to ( r , min r +δ) ∈ r and it leads to (M r , ν r +proj r (δ)) (still bisimilar to ( r , min r +δ)) where φ r (resp. ν r ) is equal to φ r (resp. ν r ) for transitions always enabled during the firing sequence and φ r (resp. ν r ) is obtained by associating the class of index 1 (resp. by associating the value 0) to the transitions newly enabled. Since (M r , ν r ) let the time elapse and since N is a g-TPN, we note that ∀t ∈ En(M r ), ν r (t) + 1/g ∈ I(t) ↓ . Now let ( r , min

, this last configuration being necessarily bisimilar to ( r , min r + δ + d).

A time step from a time-open region. Let r be an time-open region and let us

For this step, we have not used the characteristics of time Petri nets.

A discrete step into a time-closed region.

Case a. We first consider the case where r is a time-closed region. Let ( r , min r +δ 0 ) be some element of r. Suppose that ( r , min r +δ 0 )

Then in N there is a firing sequence (M r , ν r + proj r (δ 0 )) w -→ labeled by e. Due to lemma 1, this firing sequence is also fireable from any (M r , ν r + proj r (δ)) bisimilar to ( r , min r + δ) ∈ r. By bisimilarity, ( r , min r +δ) e -→ for any ( r , min r + δ) ∈ r. Let r be the region including ( , v + δ 0 ), then any configuration of r is reachable by this discrete step. Note that r = l and min r = v . l. a = 0 otherwise from (M, ν), stop l must be fired and time may not elapse. Similarly since stop x≤a l is only possibly fireable from (M, ν + d), it follows that ν

C Proof of Theorem 2

The reachability problem for regions of a TA is in P SP ACE [START_REF] Alur | A theory of timed automata[END_REF]. In order to check whether the condition (a) is false we non deterministically pick a region r and a region r which intersects r and check whether r is reachable and r is not reachable. In order to check whether the condition (b) is false we non deterministically pick a region r and a edge e and check whether r is reachable and e is fireable from r and not fireable from (l r , min r ). In order to check whether the condition (c) is false we non deterministically pick a region r, a region r which intersects r and a edge e and check whether r is reachable and e is not fireable from r or r and fireable from (l r , min r ). By Savitch construction, we obtain a deterministic algorithm in P SP ACE. In order to show the P SP ACE-hardness, we use the construction given in [START_REF] Aceto | Is Your Model Checker on Time? On the Complexity of Model Checking for Timed Modal Logics[END_REF] (in appendix D) which reduces the acceptation problem for linear bounded Turing machine (LBTM) to the reachability problem for TA with restricted guards. The computed TA (called A M,w0 ) satisfies the conditions (a) and (b) but does not satisfy the condition (c). However it can be safely transformed in order to satisfy this condition by adding the invariant t ≤ 1 to any state (q, i) and the invariant t ≤ 0 to any state (i, θ, j). This intermediate automaton is now bisimilar to a TPN.

Then we transform the edges entering the end state by resetting t and at last we add an edge (end, t = 0, e, ∅, end).

If the LBTM M does not accept the word w 0 , then the state end is not reachable and A M,w0 satisfies the conditions (a),(b),(c).

If the LBTM M accepts the word w 0 , then the state end is reachable and A M,w0 does not satisfy the condition (c) (the additional edge is fireable when entering end but not after letting the time elapse). The fact that the reachability problem for the class T A -is P SP ACE-complete was proved implicitly within the proof above.