Frédéric Herbreteau

Franck Cassez

Olivier Roux

Application of Partial-Order Methods to Reactive Programs with Event Memorization

Keywords: transition systems, reactive languages, composition, partial-order methods

We are concerned in this paper with the verification of reactive systems with event memorization. The reactive systems are specified with an asynchronous reactive language Electre the main feature of which is the capability of memorizing occurrences of events in order to process them later. This memory capability is quite interesting for specifying reactive systems but leads to a verification model with a dramatically large number of states (due to the stored occurrences of events). In this paper, we show that partial-order methods can be applied successfuly for verification purposes on our model of reactive programs with event memorization.

The main points of our work are two-fold: (1) we show that the independance relation which is a key point for applying partial-order methods can be extracted automatically from an Electre program; (2) the partial-order technique turns out to be very efficient and may lead to a drastic reduction in the number of states of the model as demonstrated by a real-life industrial case study.

1 Introduction 2

Introduction

The purpose of this paper is to produce a reduced model for the verification of reactive systems [BB91, MP93, Pnu86b, PH85] with event memorization, by the means of partialorder methods [Ove81, Val91b, GW91, Pel93, HP94, God96a].

Framework. The problem originated in the definition of a semantic model of an asynchronous reactive language: Electre [PRH92, CR95]. Indeed, this language provides the user with the ability of specifying that an event can be stored in order to be processed later (if it must not be processed when it occurs). However, the transition system which gives the semantics of an Electre program has a number of states that grows exponentially with the number of the so-called memorizable events. For verification purposes, this state explosion problem prevents the user from using standard model-checking techniques [McM93,GL94].

Partial-Order Methods. Nevertheless, in recent years, partial-order methods [Ove81, Val91b, GW91, Pel93, HP94, God96a] have proved to be useful and efficient in reducing the explored state-space in a verification phase. These techniques rely upon the equivalence between interleavings of actions of a transition system. The structure of the model for the memorizing device is such that each one of its state can also be seen as the interleaving leading from the initial state towards this state. In this paper, we show how partial-order methods can be successfully applied to the verification of Electre programs (since it is specially well adapted to efficiently and reasonably take event memorization into account) leading to the production of reduced models for the memorizing device.

Outline of the Paper. We first introduce, in section 2, the specification language Electre, and the semantic model on which properties verification can be carried out. Then, section 3 gives a quick overview of the key concepts of partial-order methods that will be used in section 4. This section is the core of the paper: we give the method and algorithms for applying partial-order methods to Electre programs. Section 4 also figures out complexity issues and results that illustrate the performance of the method (more especially, an industrial case application is exhibited). Eventually, in section 5, we conclude and give some directions for future work.

2 Electre: an Asynchronous Reactive Language with Event Memorization

In this section, we sketchily introduce the Electre language and its semantic model. For a detailed presentation the reader is referred to [CR95, SFRC99]. This language has been used for the modelization and the verification of several problems. In particular, [BBRR97] and [START_REF] Boisieau | Splitting reachability analysis of hybrid automata[END_REF] presents some recent results concerning temporal verification associated to it.

The main point of this section is the event memorization since it is the most original feature of the language and, moreover, we will focus on it in section 4.

Asynchronous Features

The Electre language is based on an asynchronous assumption which is better described by the definition of its fundamental components: modules which are lasting actions, of finite but non null duration (they can be preempted and later resumed), events which gather the occurrences of signals and can be stored; two occurrences are considered to occur at distinct instants in a continuous time space.

With these basic features are associated:

properties of modules or events; modules can be non preemptible, preemptible, resumed from the last reached point or restarted from the initial point; events can be fleeting events or stored ones, operators to combine modules and events: sequence, loop, parallel structures can be built with modules; starting or preempting a module by an event. Various sorts of preempting structures can be used: exclusive or parallel.

Module-based structures (a parallel composition of several sequences of modules for instance) and event-based structures (e.g., a preemption structure with an exclusive composition of parallel preemption structures) can be built and mixed according to the syntactic rules.

In Electre, the algorithmic content of a module is abstracted away and is supposed to be some executable code written in any sequential language. Thus, an Electre program only refers to module or event identifiers and describes the temporal behavior of the system as operations on its modules: starting and preempting with respect to the occurrences of events (which can be hardware or software originated) and the special events end M for all its modules M .

The asynchronous features of the Electre language are in the language basic components: modules and events allow the developer to specify the asynchronous nature of its application. Beside this, the internal treatment of the language (compilation, execution, . . . ) is quite similar to synchronous languages [LBBG86, HCRP91, Bd91].

Partial Semantics of Electre Programs

In this subsection, we sketchily introduce the semantics of the Electre language without taking into account the memorization aspects. The model of an Electre program is a transition system that we call the control system C.

Syntax

The Electre abstract syntax is based on two sets: module identifiers Mid on the one hand, and event identifiers Eid on the other one. We also partition the set of events into two disjoint sets: E = E @ ∪ E M where E @ is the set of fleeting events and E M the set of memorizable events. There are two types of components : module structures MS and events structures ES which are inductively defined as follows1 :

• nil : NIL, • m ∈ Mid =⇒ m ∈ MS,
• e ∈ Eid =⇒ e, @e ∈ ES (one-time storage event and fleeting event),

• P ∈ MS =⇒ loop P end loop ∈ MS (repetition),

-P P ∈ MS (parallel module structure), • E ∈ ES =⇒ -E E ∈ ES (parallel event structure), -E or E ∈ ES (exclusive event structure), • P ∈ MS, E ∈ ES =⇒ -P await E ∈ MS (preemption), -E launch P ∈ ES (launching).
An Electre program is an element of {MS, NIL}: we consider hereafter that Electre programs are represented by their parse trees with nodes decorated with the type of the components (MS or ES or NIL).

Semantics

According to the semantics of the language [CR95], for any Electre program P , and any event e, we can determine the program P which is obtained after taking into account the occurrence of event e (an example of such a calculus is given in Figure 3).

The formal semantics of the complete Electre language is given in [CR95]. Here we give in Figure 1 the semantics for the subset of the language we will need in this paper. Judgements are of the form (these are conditional rewriting rules written in a SOS style):

E P i : τ → P i : τ i ∈ [1, n] E op(P 1 , . . . , P n ) : θ → op (P 1 , . . . , P n ) : θ
The rule reads as : if the P i 's of type τ rewrite in P i of type τ in the environment E, then a program built from the P i 's with the operator op(P 1 , . . . , P n ) rewrites in op (P 1 , . . . , P n ). E is the environment and θ and θ are types in {MS, ES, NIL}. E is either an event's name or a "completion of module" name i.e. end m , m ∈ Mid. The asynchronous assumption implies that E has always one element, as perception of simultaneity is not considered. By convention p nil = nil p = p and, nil await E, is written await E.

We then define a reaction of the system in the state s to the event e by the transition relation:

s e ---→ s iff {e} s : {MS, NIL} → s : {MS, NIL}
Thus, we obtain a finite transition system; each one of its states is featured by the program that has to be executed at the current time. And, since the Electre language is an asynchronous reactive language, a transition is labeled with a single event's name. The set of reactions from the intial program yields to the control transition system associated to each Electre program. As a running example, we take the program of Figure 2. The semantics of the operators are intuitively given by:

• the loop-end loop structure stands for a never-ending loop of the inner code,

• the await operator is both applied to an event structure (within braces in the example) and to a module structure as in P await E: this structure consists in waiting for an event of E which preempts the executions of the modules in P .

1. or operator:

(a) E E 1 : ES → E 1 : ES E 2 : ES → E 2 : ES E E 1 or E 2 : ES → E 1 or E 2 : ES (b) E E 1 : ES → X 1 : θ 1 E 2 : ES → E 2 : ES θ 1 ∈ {MS, NIL} E E 1 or E 2 : ES → X 1 : θ 1 (c) Symmetrical rule.
2. || operator for events: • an event structure can be built with a parallel operator ( ) meaning that its components are being concurrently waited for; as soon as one of them has occurred, the parallel event structure imposes that the other part is being waited for; the exclusive operator or can also be used to define event structure: the meaning of which is that the first occurrence of the events appearing in the structure starts the event structure and the others are no more being waited for,

(a) E E 1 : ES → E 1 : ES E 2 : ES → E 2 : ES E E 1 || E 2 : ES → E 1 || E 2 : ES (b) E E 1 : ES → P 1 : MS E 2 : ES → E 2 : ES E E 1 || E 2 : ES → P 1 || await E 2 : MS (c) Symmetrical rule. (d) E E 1 : ES → nil : NIL E 2 : ES → E 2 : ES E E 1 || E 2 : ES → E 2 : ES (
• the components of an event structure are made of events, modules and the "launch" operator; the fragment e 1 launch A means that the occurrence of e 1 launches module A.

Some reactions corresponding to the first steps of the execution of program Foo's loop structure inner code are depicted in Figure 3 (the next steps which are not figured here would be to wait for end A and end B , the events that correspond to the end of these modules). The control transition system associated with an Electre program describes the effects of the processing of the events' occurrences in all the possible states. This transition system does not describe memorization and batch processing of events.

Semantics including memorization

As we have already mentioned, there are two kinds of events: the fleeting ones (E @ ), which have an effect on the execution only when they are being waited for, since their occurrences are never stored; and the memorizable ones (E M ), which may have a postponed effect, since they are stored (at most once) if they occur when they are not being waited for. Thus, we have a partition of the set of events: E = E @ ∪ E M (and E @ ∩ E M = ∅).

Fleeting Events. The fact that the occurrence of an event is to be stored is an information given by the state of the control transition system. A fleeting event can always be taken into account immediately:

• it may bring about a change in the control system (launching a module execution, interrupting some module executions, . . . ),

• or it may be lost (since it was not being waited for), which indeed means the occurrence is taken into account (but its effect on the system is null).

Consequently, all the states of the control transition system are source states for transitions labeled by fleeting event: in every state, a fleeting event can be taken into account.

Memorizable Events. Memorized occurrences of events must be processed as soon as possible and with priority to the oldest memorized occurrence in case of conflict. The priority will be dealt with in the sequel. A memorized occurrence of an event can be taken into account in each state where a spontaneous occurrence of the same event can be taken into account. Moreover, the effect of taking into account a memorized occurrence of an event is the same as taking into account a spontaneous occurrence of the same event.

Event Memorization. The complete semantics of the language (dealing with the event memorization) imposes to add a structure for storing occurrences. Since only one occurrence of event is stored, we could include this memorization in the control state of the transition system: the drawback of this technique is that it may bring about a state explosion in the number of control states. This is why we choose to store the occurrences of events in a separate list. We use a so-called FIFFO 2 -transition system which is a transition system with a kind of FIFO-list manipulated in a special way, which we will describe hereafter. In this FIFFO-transition system, we build a transition relation defined by: 1. all the transitions of C are transitions of F , 2. with every transition s e ---→ s of C is associated a transition s e ----→ s in the FIFFOtransition system F ; this transition corresponds to taking into account a memorized occurrence of e (note that the source and target state of such a transition are the same as for the transition labeled e: this means that the effect of taking into account the stored occurrence of e is exactly the same as taking into account the occurrence of e), 3. for every state s of the control transition system, for each memorizable event which isn't the label of a transition of which s is the source, we add in the FIFFO-transition system F a transition s ⊕e ----→ s (leading to the same state, but simultaneously recording the occurrence).

Synchronization of the FIFFO-Transition System and the FIFFO-List. To reduce the explored state-space, we can isolate the FIFFO component which is the cause of the state explosion. Thus, we synchronize the reduced list (see section 3) with the control system.

First, we define the automaton for the FIFFO-list: this is straightforward and an example of an automaton for a list with two events e 1 and e 2 is given in Figure 5, page 18. Transitions labeled +e i (resp. -e i ) correspond to storing (resp. removing) event e i in the FIFFO-list. One can point out that from state e 1 e 2 a transition with label -e 2 exists although e 1 is the oldest item of the list; this is the result of the FIFFO-list management where an event is taken into account as soon as possible: if e 1 cannot be processed and e 2 can, then e 2 is dequeued. Note also the τ transition which allows the FIFFO-list to remain idle.

The synchronization of the automaton of the FIFFO-list and the FIFFO-transition system is defined by the following rules:

• if transitions labeled e i 1 , e i 2 , . . . , e i k are enabled in the FIFFO-transition system, and one of these events is the oldest occurrence in the FIFFO-list, namely e i l , then transitions labeled e i l and -e i l are synchronized in the two transition systems,

• finally, if no e/e can be synchronized,

-transitions labeled e in the FIFFO-transition system are synchronized with τ in the FIFFO-list, -transitions labeled ⊕e in the FIFFO-transition system are synchronized with transitions labeled +e in the FIFFO-list.

Remarks. Priority is given to the processing of stored events. Moreover the management of the FIFFO-list is such that the stored events are taken into account as soon as possible and in case of conflict between stored occurrences with priority to the oldest. An execution may contain successive e (resp. -e) transitions.

Independence Relation and Partial-Order Methods

Using transition systems for modelisation purpose often leads to the so-called "state-space explosion problem". However, an important feature of a lot of modelled systems (e.g.

parallel programs, communication protocols, ...) is the built-in concurrent nature. It is expressed by the sometimes irrelevant order between some of the system actions: from a given state of the transition system, whatever the order between some actions is, the reached state is always the same one. Of course, for the verification of some kinds of properties, we can get rid of this order since it is not useful (e.g., liveness, deadlocks detection, ...). But, the order remains meaningful in many other cases.

Interleavings are not the panacea. Thus one can distinguish a lot of other "cheapest" models for concurrency: partial-order models (e.g., [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF][START_REF] Mazurkiewicz | Trace theory. In Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets[END_REF]Pra86,Win86]), partial-order temporal logics (e.g., [PW84, KP86, KP87, Pen88, Pen90]), ... On the other hand, for verification purposes, one aims at reducing the number of states that must be visited and/or the number of transitions that must be explored. Several techniques have been developped in order to take advantage of the concurrency for statespace reduction: virtual coarsening of atomic actions ([Pnu86a]), nets unfoldings (e.g., [McM92,Esp94]), methods by Overman ([Ove81]), strategies for property-proving without considering all interleavings (e.g., [AFdR80, EF82, SdR89, KP92b, JZ93]), heuristics selection of interleavings (e.g., [GH85, Wes86, Hol87]), etc... More precisely, partial-order methods have been developped for verification purposes. They are intended to reduce the state-space by exploring only one of the interleavings of independent events (see definition 1). They first appeared in [Val88a, Val88b] and independently in [God91, GW92]. These methods have met a great success, and consequently have been improved and adapted in a lot of frameworks [Val91a, GW91, HGP92, GP93, Pel93, Val93, GW93, HP94, Pel94, GHP95, God96a, Pag96, GKPP99]... One can consider [START_REF] Godefroid | Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem[END_REF] as a reference on partial-order methods, as it provides a description and comparison of these methods. All of them rely upon the independence relation between the actions of a given transition system.

Dependence and Independence between the Actions of an Automaton

Partial-order methods rely upon permutables transitions in sequences of transitions. Such transitions are called independent transitions, because they neither enable nor disable each other, so the order they appear in is irrelevant.

The following definition, adapted from [KP92a], gives the conditions of independence between two actions of an automaton. Then, the interleavings on independent actions are considered to be equivalent.

Definition 1 Two actions a 1 and a 2 of an automaton are independent if the following two conditions are true (otherwise they are said to be dependent) :

1. if a 1 (a 2 ) is enabled in a state s and s a 1 ----→ s (s a 2 ----→ s ), then a 2 (a 1 ) is enabled in s iff a 2 (a 1 )

===⇒ s (commutativity of enabled independent transitions).

As we focus on interleavings of actions, and more especially, as far as we will be interested in the equivalence of interleavings of independent actions, we will use a formalism in order to represent them. Such a representation comes from the trace theory of Mazurkiewicz [START_REF] Mazurkiewicz | Trace theory. In Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets[END_REF]. A trace sould be seen as a kind of equivalence class on interleavings of independent transitions. Definition 2 Let w be a sequence of transitions t 1 t 2 . . . t i t i+1 . . . t n . A trace [w] represents all the sequences of transitions obtained from w by permuting two independent adjacent transitions:

t 1 t 2 . . . t i+1 t i . . . t n .
Finally, the partial-order methods rely upon the following property that states the equivalence of behavior between sequences belonging to the same trace [START_REF] Godefroid | Partial-order methods for temporal verification[END_REF]:

Property 1 If s w 1 ===⇒ s 1 , s w 2 ===⇒ s 2 and [w 1 ] = [w 2 ], then s 1 = s 2 .
This property justifies all the reductions that can be done by the way of partial-order methods.

Partial-Order Methods

The aim of partial-order methods is to optimize the amount of states and/or transitions explored, more especially with verification purposes in mind. Sometimes, people prefer to generate a reduced model and then model-check it (e.g., [Val91b,[START_REF] Peled | All from one, one from all: on model checking using representatives[END_REF]), others use partial-order methods during an "on-the-fly" verification (e.g., [GW91, Val93, Pel94, GPS96, WW97]).

Algorithm 1: Classical depth-first exploration of a state-space.

Stack.push(s 0 ); H := ∅ while Stack = ∅ do s := Stack.pop() if s ∈ H then H := H ∪ {s} for each t ∈ enabled(s) do s := succ t (s)
Stack.push(s ) end for end if end while 3 We write s w ===⇒ s to mean that the sequence of transitions w leads from s to s .

But, whatever the frame partial-order methods are used in, one needs to differentiate the enabled transitions of a given state: on the one hand, the dependent ones, and on the other hand the independent ones. As a matter of fact, there mainly exists two methods 4 in order to do that: the persistent-sets method [Ove81, Val91b, GW92, GP93, God96a], and the sleep-sets method [God91, God96b].

Both methods are introduced using the framework of state-space exploration as it is a very general one (it is used during "on-the-fly" verification, as well as for reduced statespace generation). Algorithm 1 pictures a classical depth-first state-space exploration.

Persistent-Sets Method

The way used in order to reduce the number of transitions which have to be visited from a state s is to select and explore a sufficient subset of them. In this first method, this subset just contains transitions which are dependent (independent ones will remain enabled in the reached states). Such a subset is called a persistent-set as it is not affected by transitions which are outside of it.

Persistent-set. We would say that a set T of enabled transitions in s is persistent whenever their occurrences cannot be affected by execution, from s, of transitions not in T . Here is a definition of persistent-sets from [GW93]: Definition 3 A set T of transitions enabled in a state s is persistent in s if and only if, for all transitions t ∈ T such that there exists a sequence:

s = s 0 t 0 → s 1 t 1 → s 2 • • • t n-1 → s n tn=t → s n+1
leading from s to t and including only transitions t i ∈ T , t is independent (see definition 1) with respect to all transitions in T .

Notice that, the set of all the enabled transitions in a state s is always persistent.

Computation. The computation of a persistent-set is performed on the static structure of the considered transition system: it does not rely on the way the state-space exploration is done. The following algorithm [START_REF] Pagani | Partial orders and verification of real-time systems[END_REF] allows one to compute a persistent-set EP associated with the reached state s.

1. EP is initialized with an enabled transition t in s: EP (s)={t}, 2. Add to EP all the transitions which could produce sequences containing a transition which is dependent with respect to t,

3. Return all the transitions of EP enabled in s. 4 One can consider the stubborn-sets method [Val88a, [START_REF] Valmari | Heuristics for lazy state generation speeds up analysis of concurrent systems[END_REF]Val91b,[START_REF] Valmari | On-the-fly verification with stubborn sets[END_REF] as a persistent-sets one. Indeed Godefroid proved that stubborn-sets are also persistent-sets in [START_REF] Godefroid | Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem[END_REF]. There also exists some other methods like faithful decompositions [START_REF] Katz | Verification of distributed programs using representative interleaving sequences[END_REF] or ample-sets [START_REF] Peled | All from one, one from all: on model checking using representatives[END_REF] that are quite similar to the persistent-sets one.

Transitions Selection Techniques. The sizes of the persistent-sets given by the previous algorithm strongly depends on the transitions selection technique informally defined in the algorithm second issue. We have been interested in three selection techniques: the Godefroid and Wolper one [START_REF] Godefroid | Using partial orders for the efficient verification of deadlock freedom and safety properties[END_REF], the Overman method [Ove81] and the algorithm of Valmari [Val91b] (the latter one computes stubborn-sets, but as we have explained above, their enabled-transitions subsets are also persistent-sets [START_REF] Godefroid | Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem[END_REF]). These three algorithms differ in the way the transitions are selected in the persistent-set EP :

[GW92] For each transition t in EP , all the transitions which are enabled in s and dependent with respect to t are added to EP . If there exists a transition dependent with respect to t which is not enabled in s, then all the enabled transitions in s are added to EP .

[Ove81] For each transition t in EP , for each transition t dependent with respect to t, all the enabled transitions of the transition system where t appears are added to EP .

[Val91b] For each enabled transition t in s which is also in EP , all the transitions which are dependent with respect to t are added to EP . For each transition t not enabled in s, but which appears in EP , all the transitions which can make t enabled in a reachable state s are added to EP .

The following example (from [START_REF] Pagani | Partial orders and verification of real-time systems[END_REF]) makes these techniques more clear:

Example 1 Assume that one wants to explore the state-space of the following system composed of 3 transition systems, and that a and d are dependent, whereas all the others are independent. We are just interested here in the persistent-sets computed for state s = (1, 1 , 1 ). Here are the results given by the three algorithms, when one first adds transition a to EP (s):

Technique [GW92] [Ove81] [Val91b] EP (s) {a, b, c, e} {a, c, e} {a, d, c} EP (s) ∩ enabled(s) {a, c}
The three previous techniques are ordered from the less to the most refined one. Of course, the more refined is the method, the greater is the cost of computation. Notice that using the smallest persistent-set is nothing more than an heuristic: it does not ensure to lead with the smallest state-space exploration.

Godefroid proved that [God96a]:

• No persistent-set computed by the algorithm of Overman is larger than all of those computed by the algorithm of Godefroid and Wolper,

• There exists a persistent-set (stubborn-set) given by the algorithm of Valmari which is smaller or equal to all of those computed by the way of the algorithm of Overman.

Selective State-Space Exploration with Persistent-sets. A persistent-set of transitions is computed in each state reached during the state-space exploration. From each one of these states, we only execute the transitions which are in its persistent-set. Such an exploration is said to be a selective state-space exploration.

Algorithm 2: Selective state-space exploration using persistent-sets. Algorithm 2 presents an algorithm taking advantage of this method where EP (s) is the persistent-set computed in state s (it is adapted from [START_REF] Pagani | Partial orders and verification of real-time systems[END_REF]).

About the Persistent-Sets Method. This method avoids to explore the whole statespace of the transition system we want to model-check. Thus, we can expect saving memory if we only produce (or explore) a reduced automaton, and saving time because we explore less paths. One can found in [START_REF] Godefroid | Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem[END_REF] a complete description of the techniques described above and a comparison of the results and the complexity. It is also shown in [START_REF] Godefroid | Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem[END_REF] that every reachable deadlock state is preserved by the method. Many other properties can be checked by considering not only one but a subset of all the interleavings that preserve them (e.g., [HGP92, Pel93, GW93, Val93, WW97]).

Sleep-Sets Method

This second method is based on the selection of independent transitions and the fact that it is sometimes not necessary to explore some transitions because they lead to states which have already been visited during the exploration.

For an example, consider the two automata of Figure 4. The first one (a) represents the state-space reached during a basic exploration, whereas the second one (b) shows a selective state-space exploration where one can avoid to fire a transition. Indeed, we assume that t 1 and t 2 are two independent transitions of an automaton, both enabled in a state 0, and we perform a depth-first exploration starting in 0. Let first execute t 1 , leading from state 0 to state 1 and then t 2 finally leading to state 3. Then, we return to state 0 where we execute t 2 . State 2 is now the current state and the transition t 1 is enabled there. But this transition leads from 2 to 3, which has already been visited. So, it is sometimes not necessary to do this twice and this is the aim of this method.

Sleep-set.

A sleep-set stores the transitions that lead to states which have already been visited [God91, Pag96]: Definition 4 A sleep-set for a state s is a set of transitions independent with respect to each other in s, which lead to states which have already been visited.

Computation.

A sleep-set is computed during the state-space exploration as it relies on the past of the current state-space exploration. Indeed, the sleep-set of a state s depends on the sleep-set of the previous state s and on the transition t which leads from s to s (s t ---→ s ). Unlike persistent-sets, sleep-sets are computed from dynamic informations. Here is a general algorithm for the computation of the sleep-set associated with a state s reached by the execution of a transition:

s t ---→ s [Pag96].
1. clear sleep(s ).

2. Add to sleep(s ) all the transitions in sleep(s) which are independent with respect to t. About the Sleep-Sets Method. Notice that the sleep-sets technique does not allow one to reduce the number of visited states, but only the number of transitions which are explored. The result is that we cannot expect any reduction in memory space, but only in time space needed for the exploration.

Add

Furthermore, this method is not suitable for reduced state-space generation, as is: for example, state 2 in Figure 4(b) becomes a deadlock state.

The sleep-sets method has been improved (e.g., conflict-sets [START_REF] Holzmann | Coverage preserving reduction strategies for reachability analysis[END_REF]) or adapted in several frameworks (e.g., [START_REF] Peled | All from one, one from all: on model checking using representatives[END_REF]).

Finally, these two techniques (persistent-sets and sleep-sets) can sometimes be used together in order to go further in the reductions. For example, Godefroid and Wolper have written an algorithm for deadlock states detection which uses both methods together [START_REF] Godefroid | Partial-order methods for temporal verification[END_REF].

Application of Partial-Order Methods to Electre

We now aim at building reduced FIFFO-lists. Therefore, we have been looking for known works dealing with partial-order methods and reduced state-space generation (e.g., [Val91b,[START_REF] Peled | All from one, one from all: on model checking using representatives[END_REF]). As we will see later, such persistent-sets based techniques are not suitable in our framework, so we have also been looking for other partial-order methods or different uses of them (e.g., [God91, GW91, Val93, Pel94, GPS96]), one of which revealed to be more accurate.

Principle of the Reduction

Let us introduce our idea with an example. Consider the Electre program Foo, in Figure 2 (page 8) whose associated FIFFO-list is pictured in Figure 5. Its transitions labeled -e represent a dequeue of e, those which are labeled +e represent an enqueue of e, and transitions labeled τ are only used for synchronization purpose (see section 2.3). This program reacts to the instances of events e 1 and e 2 , which both can be memorized once. Thus, at any time, the memorizing device has one of the following contents: (∅) (e 1 ) (e 2 ) (e 1 , e 2 ) (e 2 , e 1 ) As pictured in Figure 5, each possible content for the list corresponds to a state of its automaton. Intuitively, program Foo can take into acount both events e 1 and e 2 immediately. And both sequences e 1 e 2 and e 2 e 1 lead to the same state from the given one, as shown in Figure 3 (page 8). The order between e 1 and e 2 is therefore irrelevant, and these two events are independent with respect to each other (see definition 1).

It clearly appears that the distinction between the two interleavings e 1 , e 2 and e 2 , e 1 is not necessary nor useful for the program execution. This gives a way to reduce the FIFFO-list: one replaces its two states (e 1 , e 2 ) and (e 2 , e 1 ) by a single state representing both of them. Since e 1 and e 2 are independent, we have: [e 1 e 2 ] = {(e 1 , e 2 ) , (e 2 , e 1 )}, then, it is possible to replace both states (e 1 , e 2 ) and (e 2 , e 1 ) by their trace [e 1 e 2 ]. Figure 6 shows the reduced automaton corresponding to the transition system in Figure 5. The suppressed parts are pictured in gray and dashed lines, whereas new parts are in bigger and bolder style. Notice that the state [e 1 e 2 ] in the new automaton stands for both states (e 1 , e 2 ) and (e 2 , e 1 ) in the previous one. By the way, one state and five transitions have been removed.

Computation of the Dependence Relation for Electre Programs

Our technique relies upon the fact that some events are independent with respect to each other, and others are not. We now need to be able to establish which events are dependent of which other ones. This can be done from a dependence relation (the definition is adapted from [START_REF] Godefroid | Partial-order methods for temporal verification[END_REF]).

Definition 5 A dependence relation is a binary relation such as for any couple of events e 1 and e 2 :

• either (e 1 , e 2 ) ∈ , then e 1 and e 2 are dependent (see definition 1) with respect to each other,

• or (e 1 , e 2 ) ∈ , then e 1 and e 2 are said to be independent.

Notice that this is a symmetrical, but neither reflexive, nor transitive relation. Usually, is built reflexive, but here it is not necessary nor useful because each event appears at most once in any FIFFO-list.

A control automaton associated with an Electre program is computed by rewriting the program while taking into account the events it contains (see section 2.2.2). Then, dependence between some events will imply that taking one of them into account will disable or enable the others, or that the sequences built on these events will not lead to the same states (see definition 1). Thus, all the dependences between a program events can be computed on the control automaton. One only needs to explore this automaton and determine if definition 1 holds every time several memorizable events can be taken into account. Meanwhile, this method has an important drawback: it needs a complete exploration of the control automaton.

We have developed another method which allows one to compute the dependence relation directly from the Electre program. Consequently, it is sufficient to analyze the structures of the program as explained in the following. The dependence relation is then obtained in a linear (in the number of Electre operators appearing in the program) time complexity.

Lemma 1 describes the cases of dependence and independence between events using the structures of the Electre language. Lemma 1 Let < A >, < B > and < C > be, respectively, a module structure and two event structures. We have for the following Electre operators (see Figure 1 page 7):

1. "< A > await < B >".
All the events of < A > are dependent with respect to all the first level events5 of < B >,

2. "< B > or < C >".
All the events of < B > are dependent with respect to all the events of < C >.

Otherwise, they are independent.

Proof sketch. This lemma can be proved by induction on the rewriting rules defined for each one of the Electre operators (see Figure 1 and furthermore [CR95]).2

For any given Electre program, the dependence relation is computed according to lemma 1. Each time the Electre program corresponds to one of the cases above, we add a couple of events (a dependence) per event of < B > and per event of < C > (resp. per event of < A > and per first-level event of < B >) to the dependence relation. This is done recursively on < B > and on < C > (resp. < A >), since an Electre program is seen as its parse tree (see section 2.2.1).

Notice that the example chosen in order to illustrate our results (see program Foo in Figure 2) does not contain dependent events. We would have preferred to show an example with both dependent and independent events. But such an Electre program must contain at least three events and then, leads to a non-reduced FIFFO-list with 16 states and 97 transitions. Obviously, this automaton cannot be pictured clearly.

Building of the Reduced FIFFO-List

We now describe our method for the construction of a reduced FIFFO-list. First, we choose a partial-order method well-suited for the desired reduction. Then, we exhibit our algorithms.

Choice of a Partial-Order Method

The reduction must preserve the FIFFO-list behaviors. For example, the expected reduced FIFFO-list depicted in Figure 5 (page 18) is shown in Figure 6 (page 19). We first examine the suitability of the persistent-sets method for that purpose, then the sleep-sets one.

Building a Reduced Automaton with a Persistent-Sets Method. First, consider the persistent-sets method on the automaton of Figure 5. The reduced automaton produced by the way of the persistent-sets technique is drawn in Figure 7 Obviously, the achieved result is not what we were expecting: this reduced FIFFOlist does not allow the memorizing device to only contain an instance of event e 2 . The persistent-sets method cannot be applied in order to get the reduction we are looking for. Indeed, we only select e 1 in the persistent-set of state 0 because e 1 and e 2 are independent. This means that one does not need to take care of e 2 in this state. But we could only have to memorize e 2 . Our problem is due to the fact that the persistent-sets method preserves the traces but not the states, and as explained in section 3, it omits some behaviors whereas we need all of them.

Producing a Reduced FIFFO-List with the Sleep-Sets Method. We now try to build, the reduced FIFFO-list corresponding to the automaton of Figure 5 by the way of the sleep-sets technique.

∅, {}

(a) Initialy: the FIFFO-list is empty. Of course, the sleep-sets technique applies very well in our framework, and it gives the expected solution. Figure 8 shows the process to build the reduced FIFFO-list. It is just a kind of selective state-space exploration using the sleep-sets method (see algorithm 3) but, here, we produce the reduced automaton during its exploration. The dequeue transitions are not shown on these automata because they are not necessary for the explanation, and the sleep-sets are written between braces for each state. We see in Figure 8(e) that the sleep-set of state e 2 contains an occurrence of event e 1 . It means that there exists an already built state which is equivalent to the state we would reach by a memorization of event e 1 . So, we only need to create a transition towards this existing state, avoiding, by the way, the creation of a new state, hence the reduction. This is the principle of our algorithm.

∅, {e 1 } e 1 , {} +e 1 (b) Enqueueing e 1 . ∅,

Algorithms for the Construction of the Reduced FIFFO-List

We assume that we have got a list of events (list Evt ), each of them can be stored at most once in the memorizing device. Algorithm 4 is the general algorithm for construction of the reduced automaton. We use a queue in order to store the states that have to be treated later. It queue N extStates . The states that have already been computed are stored in a list: list States . Each one of the states is a structure containing the content of the memorizing device and a sleep-set: state = (memorizing device content, sleepset).

The main part of the algorithm is represented by the computation of the successors of a state. Algorithm 5 is devoted to this task.

For each state s:

1. First, we examine its sleep-set. For each asleep event, it consists in searching for a state equivalent to the one we would have reached by adding the event. And then, we establish a transition between them, 2. Then, we compute the successors of our state which are reached by adding the events which are neither in the sleep-set of s, nor in its memorizing device content, 3. Finally, we add the dequeueing transitions and the loops used for synchronization with the FIFFO-transition system (see section 2.3).

Complexity Issue

The most interesting characteristic of the algorithms that produce reduced transition systems is the amount of reduction they provide. Hence, we aim at expressing the complexity of our method as the number of states of the generated reduced automaton.

Theoretical Approach of Complexity. As explained in section 4.1, each state of the unreduced automaton is a p ordered outcome from a permutation of n events (p ≤ n) and each permutation of p ∈ [1, n] events between n is a state of the unreduced automaton. So the number of states of the unreduced automaton is:

N ur = n r=0 r! n r = n r=0 n! (n -r)!
Moreover, if all the program events are dependent, no reduction can be expected. In this case, in fact the worst case, the "reduced" automaton and the unreduced one are identical. Thus, the number of states in the worst case is:

N worst = N ur = n r=0 r! n r
At the opposite, when all the events are independent, the reduction is maximal. In this case, the best one, there is no matter in the event order. Thus, the complexity falls from a permutation down to a combination. Therefore, the number of states of the best-reduced automaton is given by:

N best = n r=0 n r = n r=0 n! r! × (n -r)!
The last case is the average one. Despite the combinatorial structure of the automaton and the fact that both previous cases were easy, we were not able to find an expression for the average complexity. First, notice that unlike the best and the worst cases, all the events do not behave in the same way. Each event can now only permute with the events of which it is independent. One can imagine modelling this by a number of dependent events and a number of independent ones linked to each event, but this is not sufficient because the most important difference between the best case and the worst case on the one hand, and the average case on the other hand, is the difficulty to model the order the events appear in. Example 2 shows its big importance.

Example 2

We consider the three events e 1 , e 2 , e 3 linked by the following dependence relation: = {(e 1 , e 2 ), (e 1 , e 3 )} obtained from an Electre program. The two following permutations of these three events show that, the number of their equivalent sequences of events depend on the order:

• (e 1 , e 2 , e 3 ) has an equivalent permutation: (e 1 , e 3 , e 2 ),

• rather than, (e 2 , e 1 , e 3 ) does not have any.

Overview of the Complexity on Some Examples. Since we did not manage to find an expression for the average case complexity, we now give a flavour of it. Two parameters step in our method: the number of events (all independent) and the ratio of dependence between events. So, we look at two test phases, one for each of these parameters, and we make them vary.

As our evaluation criterion is the number of suppressed states, we give in tables 1 and 2 (one per test phase) the number of states of the rough automaton, the number of states of the reduced one, and the ratio of suppressed states gathered with the Electre programs of these tests. Notice that these programs are only examples, and a lot of others, having the same characteristics (number of events and percentage of dependent events), could have been choosen and would have produced the same results.

First Test. Consider 5 Electre programs with an increasing number of independent events.

Table 1 shows both test programs and the achieved results.

Notice that the ratio of suppressed states increases quickly. This can be explained in the following way: consider a program containing the five independent events: e 1 , e 2 , e 3 , e 4 and e 5 . One can build 120 (5!) different ordered sequences containing each of these 5 events once. But all these sequences have the same trace: [e 1 e 2 e 3 e 4 e 5 ], due to the empty dependence relation. Thus, in the reduced automaton, this unique last state stands for the 120 others in the rough automaton. Second Test. Now, in order to evaluate the influence of the ratio of event dependences, consider 5 programs written in the Electre language, all of them containing the same 5 events, but having an increasing ratio of dependence: from 0% to 100%. This simply comes from:

# events

• First, a program where all the events are composed in a parallel preemption structure, making them independent, • Then, the parallelism operators ("||") are gradually replaced by exclusive operators ("or"). This increases the ratio of dependent events (see lemma 1). If all the events are dependent with respect to each other, or if there is one or no event appearing in an Electre program, then any reduction can be expected. Indeed, in these cases the computed traces contain one and exactly one sequence of events (the number of traces is equal to the number of sequences).

Results

Consider the program Foo in Figure 2 (page 8) and the FIFFO-list associated with it: the rough one (in Figure 5, page 18) and the reduced one (see Figure 6, page 19). Here, our reduction technique allows removing 1 state (20% of the total number of states) and 5 transitions.

A Real-Case Study. Nevertheless, program Foo is an academic example, and moreover, a very small but readable one. The tool implementing our method has been used during the verification phase of an embedded software dedicated to the control program of an aircraft engine.

This case study is more deeply described in [START_REF] Boisieau | Vérification et exécution d'applications temps-réel industrielles avec Electre[END_REF] from which the following main features and results were extracted. It is mainly composed of two tasks: the first one is dedicated to input/output control (IO), and the second one to computation (CMP). Both of them are divided in several programs: IO1, IO2, IO3 for the input/output control task and CMP1, CMP2 for the computer. Furthermore, their communications are handled by two tasks: IO CMP and CMP IO. Table 3 shows for each program: its number of operators, its number of events, the ratio of dependence between its events, and the number of states of its non-reduced associated FIFFO-list.

The dependence relation has been computed for each one of these programs using the method given by lemma 1. The time complexity of this method is linear in the number of Electre operators appearing in the program. Thus, despite the high number of operators appearing in these programs, the time needed for the computation of the dependence relation is negligible Unfortunately, most of the programs have strongly dependent events, more especially, one cannot expect any reduction of the FIFFO-lists associated to the programs IO2, IO3, CMP2, IO CMP and CMP IO, since all their events are dependent. But, the both programs (IO1 and CMP1) have a very low amount of dependent events (respectively 3.33% and 2.86%). So, our method has been successfully applied on these programs, and the rate of suppressed states between the unreduced automata on the one hand, and the reduced one on the other hand is amazing. We figure out the results in table 4.

Conclusion

We have shown in this paper a model of reactive applications with event memorization. This a meaningful and important feature of the asynchronous reactive language Electre. The memorizing device is itself modelled by a FIFFO-list which is bounded, since at most one occurrence of each event is stored. But it is usually far too large. We focussed on some verification issues on this model and more accurately on the reduction of the event memorization space.

Our Contribution. Due to the special structure of a FIFFO-list (each one of its state is equivalent to the interleaving which leads from the initial state to this one), we have been respectively) able to produce reduced FIFFO-lists by the means of a partial-order method. Since these techniques rely upon the equivalence of interleavings of actions, and lead to the suppression of all but one equivalent interleavings, it is quite an amazing result in our case. Indeed, we were not able to remove any state or behavior from the FIFFO-list.

Our technique uses concurrency in Electre programs as a starting point and idea for a reduction, and more especially sleep-sets method for the detection and merging of equivalent states.

Of course, the reduction does not preserve all the properties of the FIFFO-list. For example, the order between the stored events is lost, and properties such as "Is every occurrence of e 1 always preceeded by an occurrence of e 2 " can not be safely checked on the reduced model. But, this reduction preserves all the behaviors of the FIFFO-list. Furthermore, it leads to drastic reductions in the number of states as shown in the realcase study.

Future Work and Perspectives. The next step of our researches in this area lies in the proof of bisimulation between the FIFFO-transition system synchronized with the rough FIFFO-list on the one hand, and the FIFFO-transition system synchronized with the reduced FIFFO-list on the other hand. Such a result would mean that our reduction does not only preserves all the behaviors of the system, but it does not create any wrong ones.

Our technique could also be improved in order to make it possible to check some properties dealing with the order between the stored events occurrences. For example, the following property: "Is every occurrence of e 1 always preceeded by an occurrence of e 2 ", could be checked in the reduced model, if the order between the occurrences of e 1 and e 2 had been kept. We only need to specify independently from the Electre program, that e 1 and e 2 are dependent events.

Finally, one appealing question is to study the unbounded FIFFO-lists. Indeed, it is possible to endow the events with the property of unbounded memorization. It would the be challenging to try to combine the partial-order techniques with abstraction techniques, in order to deal with such FIFFO-lists.

Figure 2 :

 2 Figure 2: An Electre program.

Figure 3 :

 3 Figure 3: First transitions of the loop structure body of program Foo.

2 (

 2 b) Selective exploration (sleep-sets technique).

Figure 4 :

 4 Figure 4: Automata with two independent transitions.

2 +e 1 ,

 21 Figure 5: FIFFO-list for the events e 1 and e 2 (5 states, 21 transitions).

∅ e 1 e 2 [e 1 e 2 ]Figure 6 :

 226 Figure 6: Reduced FIFFO-list for the independent events e 1 and e 2 (4 states, 16 transitions).

[e 1 e 2

 2 (a) -where persistent-sets are written for each state between braces -together with the expected automaton in Figure 7(b). ∅, {e 1 } e 1 , {e 2 } Expected reduced FIFFO-list.

Figure 7 :

 7 Figure 7: Produced and expected FIFFO-lists (skeletons).

Figure 8 :

 8 Figure 8: Building the reduced FIFFO-list with sleep-sets method (example).

  is enabled in s (independent transitions can neither disable nor enable each other), 2. if a 1 and a 2 are enabled in s, then there is a unique state s such that both 3 s

	and s	a 2 a 1	a 1 a 2 ===⇒ s

  t to sleep(s) (memorization of the transitions which have already been executed from s).

	Selective State-Space Exploration with Sleep-sets. Algorithm 3 performs a "selec-
	tive exploration" using sleep-sets in order to optimize it. Each time a new state is reached,
	one computes the associated sleep-set. All the enabled transitions but the alseep ones are
	executed from a new state.
	compute sleep(s )
	Stack.push(s )
	end for
	end if
	end while

Algorithm 3: Selective state-space exploration using sleep-sets. Stack.push(s 0 ); H := ∅ while Stack = ∅ do s := Stack.pop() if s ∈ H then H := H ∪ {s} for each t ∈ enabled(s) sleep(s) do s := succ t (s)

  {e 1 , e 2 }

					+e 1	+e 2
					e 1 , {}	e 2 , {e 1 }
					(c) Enqueueing e 2 .
	∅, {e 1 , e 2 }	∅, {e 1 , e 2 }	∅
	+e 1	+e 2	+e 1	+e 2	+e 1	+e 2
	e 1 , {e 2 }	e 2 , {e 1 }	e 1 , {e 2 }	e 2 , {e 1 }	e 1	e 2
	+e 2		+e 2	+e 1	+e 2	+e 1
	[e 1 e 2 ], {}	[e 1 e 2 ], {}	[e 1 e 2 ]
	(d) Enqueueing e 2	(e) Enqueueing e 1	(f) Reduced FIFFO-
	(state e 1 ).		(state e 2 ): processing	list (sleep-sets tech-
			the sleep-set.		nique).

  is named Algorithm 4: Building the reduced FIFFO-list. queue N extStates .enqueue (∅, {}) list States .append(∅) while queue N extStates = ∅ do state ← queue N extStates .dequeue() list N extStates ← state.computeNextStates() for each state N ext ∈ list N extStates \ list States do queue N extStates .enqueue(state N ext ) list States .append(state N ext )

	end for
	end while

Table 1 :

 1 Ratio of suppressed states with respect to the number of events.

		Program	# states # states	%
			(rough) (reduced) reduction
	1	await e1	2	2	0%
	2	await {e1 || e2}	5	4	20%
	3	await {e1 || e2 || e3}	16	8	50%
	4	await {e1 || e2 || e3 || e4}	65	16	75%
	5	await {e1 || e2 || e3 || e4 || e5}	326	32	90%

Table 2

 2 shows the programs written to get the variation of the ratio of dependence together with the resulting numbers.

	% dependent Program	# states # states	%
	events		(rough) (reduced) reduction
	0%	await {e1 || e2 || e3 || e4 || e5}	326	32	90%
	20% (1 -4 5 ) await {e1 or {e2 || e3 || e4 || e5}} 40% (1 -3 5 ) await {e1 or e2 or {e3 || e4 || e5}} 60% (1 -2 5 ) await {e1 or e2 or e3 or {e4 || e5}}	326 326 326	40 64 130	88% 80% 60%
	100%	await {e1 or e2 or e3 or e4 or e5}	326	326	0%

Table 2 :

 2 Ratio of suppressed states with respect to the ratio of dependent events.

Table 3 :

 3 6 . Overview of the software.

	Program #Electre #Events	Ratio of	Rough FIFFO-list
		operators		dependence	#states
	IO1	60	10	3.33%	9,864,101
	IO2	12	11	100%	108,505,112
	IO3	10	9	100%	986,410
	CMP1	49	15	2.86%	3,550,000,000,000
	CMP2	14	13	100%	16,926,797,486
	IO CMP	14	13	100%	16,926,797,486
	CMP IO	12	11	100%	108,505,112

Table 4 :

 4 Reduced FIFFO-lists.

We consider a special entity nil of type NIL which stands for "nothing".

First In First Fireable Out.

The first-level events associated with a given Electre program are all the events that can immediately be taken into account.For example, in the following Electre program, "await {e 1 launch A || e 2 launch [B await e 3 ]}", e 1 and e 2 are first-level events, whereas e 3 is not.

It is not comparable to the time one would need to compute the dependence relation using a statespace exploration of the FIFFO-transition system. For example, the control transition systems associated to programs IO1 and CMP1 have got 233 states/3,359 transitions and 9,651 states/212,766 transitions

Algorithm 5: Computing the successors of a state s = (memorizing device content, sleepset) (function computeNextStates). Return the list of all the created successors states Now, we only need to describe the function "inherit" which computes the successor s of a state s, reached by a transition labeled by event e. This function first computes the memorizing device content associated with s . It only adds e to the content of s: s .memorizingDeviceContent ← s.memorizingDeviceContent ∪ {e}. Then, it computes the sleep-set of s according to the algorithm given in section 3.2.2.

Complexity Issue and Results

The structure of the unreduced FIFFO-list is specific. Each one of its states corresponds to a permutation of p events among n (p ≤ n). As a consequence, the complexity of the algorithm could seem very easy to determine, but as we will see, it is not actually the fact. Our algorithm has been implemented in Objective CAML 2.03 and the resulting tool has been used during the verification phase of an embedded software dedicated to the control program of an aircraft engine. The results are given in section 4.4.2.


Franck Cassez
email: franck.cassez@irccyn.ec-nantes.fr

⋆,⋆⋆ Alexandre David
email: adavid@cs.aau.dk

Kim G Larsen

Didier Lime
email: didier.lime@irccyn.ec-nantes.fr

Jean-François Raskin
email: jraskin@ulb.ac.be

Timed Control with Observation Based and Stuttering Invariant Strategies

In this paper we consider the problem of controller synthesis for timed games under imperfect information. Novel to our approach is the requirements to strategies: they should be based on a finite collection of observations and must be stuttering invariant in the sense that repeated identical observations will not change the strategy. We provide a constructive transformation to equivalent finite games with perfect information, giving decidability as well as allowing for an efficient on-the-fly forward algorithm. We report on application of an initial experimental implementation.

Introduction

Timed automata introduced by Alur and Dill [START_REF] Alur | A theory of timed automata[END_REF] is by now a well-established formalism for representing the behaviour of real-time systems. Since their definition several contributions have been made towards the theoretical and algorithmic characterization of this formalism. In particular, industrial mature tools supporting model-checking for timed automata now exist [START_REF] Behrmann | Uppaal 4.0[END_REF][START_REF] Behrmann | A tutorial on uppaal[END_REF].

More recently the problem of controller synthesis for timed automata based models have been considered: i.e. given a timed game automaton modelling the possible moves of an environment as well as the possible moves of a control program, the problem consists in synthesizing a strategy for the control program in order that a given control objective is met no matter how the environment behaves [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF]. Controller synthesis and time-optimal controller synthesis for timed games was shown decidable in [START_REF] Asarin | Controller Synthesis for Timed Automata[END_REF] and [START_REF] Asarin | As Soon as Possible: Time Optimal Control for Timed Automata[END_REF]. First steps towards efficient synthesis algorithms were taken in [START_REF] Altisen | Tools for controller synthesis of timed systems[END_REF][START_REF] Tripakis | On-the-Fly Controller Synthesis for Discrete and Timed Systems[END_REF]. In [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF] a truly on-the-fly algorithm based on a mixture of forward search and backwards propagation was proposed and later used as the basis for an efficient implemention in the tool Uppaal Tiga [START_REF] Behrmann | Uppaaltiga: Time for playing games![END_REF].

In all of the papers cited above it has been assumed that the controller has perfect information about the plant: at any time, the controller knows precisely in what state the environment is. In general however -e.g. due to limited sensors -a controller will only have imperfect (or partial) information about the state of the environment. In the discrete case it is well known how to handle partial observability, however for the timed case it has been shown in [START_REF] Bouyer | Timed control with partial observability[END_REF] that the controller synthesis problem under partial observability is in general undecidable. Fixing the resources of the controller (i.e. a maximum number of clocks and maximum allowed constants in guards) regains decidability [START_REF] Bouyer | Timed control with partial observability[END_REF], a result which also follows from the quotient and model construction results of [START_REF] Laroussinie | CMC: A tool for compositional model-checking of real-time systems[END_REF][START_REF] Laroussinie | From timed automata to logic -and back[END_REF].

In this paper we also deal with the problem of controller synthesis for timed games under imperfect information following the approach of [START_REF] Chatterjee | Algorithms for omegaregular games with imperfect information[END_REF][START_REF] Wulf | A lattice theory for solving games of imperfect information[END_REF]. That is, the imperfect information is given in terms of (a finite number of possible) observations to be made on the system configurations, providing the sole basis for the strategy of the controller. However, in contrast to [START_REF] Chatterjee | Algorithms for omegaregular games with imperfect information[END_REF][START_REF] Wulf | A lattice theory for solving games of imperfect information[END_REF], which is essentially turn-based in the untimed setting, we will here consider a more general framework, where in each step the controller and environment are competing. In particular, the strategy of the controller is supposed to be stuttering invariant, i.e. the strategy will not be affected by a sequence of environment or time steps unless changes in the observations occur. x := 0 x ≥ 0

x ≥ 8

x := 0

x ≥ 8

x := 0

x ≥ 8 kick?

Fig. 1. Timed Game with Imperfect Information.

To illustrate the concepts of imperfect information and stuttering invariance consider the timed game automaton in Figure 1 modelling a production system for painting a box moving on a conveyor belt. The various locations indicate the position of the box in the system: in Sensor a sensor is assumed to reveal the presence of the box, in Sensed the box is moving along the belt towards the painting area, in Paint the actual painting of the box takes place, in Piston the box may be kick?'ed off the belt leading to Off; if the box is not kicked off it ends in End. All phases are assumed to last between 8 and 10 seconds, except for the phase Sensor, which is instantaneous. The uncontrollability of this timing uncertainty is indicated by the dashed transitions between phases. The controller should now issue a single kick?'command at the appropriate moment in order to guarantee that the box will -regardless of the above timing uncertainybe kicked off the belt. However the controller has imperfect information of the position of the box in the system. In particular, the controller cannot directly observe whether the box is in the Sensed, Paint or in the Piston phase nor can the value of the clock x be observed. Still equipping the controller with its own clock y -which it may reset and test (against a finite number of predicates)it might be possible to synthesize a control strategy despite having only partial information: in fact it may be deduced that the box will definitely be in the Piston area within 20-24 seconds after being sensed. In contrast, an increased timing uncertainty where a phase may last between 6 and 10 seconds will make a single-kick? strategy impossible.

The main contributions of this paper are: (i) we show how a variant of the subset construction of [START_REF] Chatterjee | Algorithms for omegaregular games with imperfect information[END_REF][START_REF] Wulf | A lattice theory for solving games of imperfect information[END_REF] allows us to transform a timed game H with imperfect information into an equivalent game G(H) of perfect information; (ii) we show that G(H) can be effectively and symbolically computed and this implies that the control problem under imperfect information is decidable; this allows us to apply the efficient on-the-fly forward algorithm from [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF] and (iii) we report on application of an initial experimental implementation of this algorithm and a number of heuristics for minimizing the explored state-space as well as the size of the finally synthesized strategy.

The detailed proofs can be found in the extended version available from the authors web pages.

Timed Games and Observation Based Strategies

In this section, we define the timed game structures, the notion of strategies that we are interested in, and useful vocabulary for the rest of the paper. We denote R ≥0 the set of non-negative reals and R >0 = R ≥0 \ {0} and A B the set of mappings from B to A.

Timed game structures (TGS) will be defined using a timed automaton like notation. The semantics of the notation will be defined by a two-player labeled timed transition system (2-LTTS), and the games will be played on this 2-LTTS.

Definition 1 (2-LTSS).

A 2-player labeled timed transition system (2-LTTS) is a tuple (S, s 0 , Σ 1 , Σ 2 , →) where S is a (infinite) set of states, s 0 is the initial state, Σ 1 and Σ 2 are the two disjoint alphabets of actions for Player 1 and Player 2 respectively, and →⊆ S × Σ 1 ∪ Σ 2 ∪ R >0 × S is the transition relation. Given a state s ∈ S, we define enable(s) as the set of σ ∈ Σ 1 ∪ Σ 2 ∪ R >0 such that there exists s ′ and (s, σ, s ′ ) ∈→.

Let X be a finite set of real-valued variables called clocks. Let M be a natural number. We note C(X, M ) the set of constraints ϕ generated by the grammar:

ϕ ::= x ∼ k | x -y ∼ k | ϕ ∧ ϕ where k ∈ Z ∩ [0, M ],
x, y ∈ X and ∼∈ {<, ≤, =, >, ≥}. B(X, M ) is the subset of C(X, M ) generated by the following grammar:

ϕ ::= ⊤ | k 1 ≤ x < k 2 | ϕ ∧ ϕ where k, k 1 , k 2 ∈ Z ∩ [0, M ], k 1 < k 2 ,
x ∈ X, and ⊤ is the boolean constant true. In the sequel, we will restrict our attention to bounded timed automata where clock values are all bounded by a natural number M ; this does not reduce the expressive power of timed automata. Given a natural number M , an M -valuation of the variables in X is a mapping X → R ≥0 ∩ [0, M ]. We also use the notation [X → [0, M ]] for valuations and 0 for the valuation that assigns 0 to each clock. For Y ⊆ X, we denote by v[Y ] the valuation assigning 0 (resp. v(x)) for any x ∈ Y (resp. x ∈ X \ Y ). Let t ∈ R ≥0 , v be an M -valuation for the set of clocks X, if for all x ∈ X, v(x)

+ t ≤ M then v + t is the M -valuation defined by (v + t)(x) = v(x) + t for all x ∈ X. For g ∈ C(X, M ) and v ∈ (R ≥0 ∩ [0, M ]) X , we write v |= g if v satisfies g and [[g]] denotes the set of valuations {v ∈ (R ≥0 ∩ [0, M ]) X | v |= g}. An M -zone Z is a subset of (R ≥0 ∩ [0, M ]) X s.t. Z = [[g]] for some g ∈ C(X, M ).
Definition 2 (Timed Game Structure). Let M be a natural number, an Mtimed game structure (M -TGS) is a tuple H = (L, ι, X, δ, Σ 1 , Σ 2 , inv, P) where:

-L is a finite set of locations, ι ∈ L is the initial location, -X is a finite set of real-valued clocks, -Σ 1 , Σ 2 are two disjoint alphabets of actions, Σ 1 is the set of actions of Player 1 and Σ 2 the set of actions of Player 2,

-δ ⊆ (L×B(X, M )×Σ 1 ×2 X ×L)∪(L×C(X, M )×Σ 2 ×2 X ×L) is partitioned
into transitions1 of Player 1 and transitions of Player 2. inv : L → B(X, M ) associates to each location its invariant.

-P is a finite set of pairs (K, ϕ) where K ⊆ L and ϕ ∈ B(X, M ), called observable predicates.

In the definition above, each observable predicate (K, ϕ) ∈ P is a predicate over the state space of the TGS, i.e. the set L × [X → [0, M ]]. For l ∈ L and v an M -valuation of the clocks in X, we write (l, v) |= (K, ϕ) iff l ∈ K and v |= ϕ. Two pairs (l 1 , v 1 ), (l 2 , v 2 ) that satisfy the same observable predicates from P have the same observation (they can not be distinguished by our controllers). So, an observation is a function o : P → {0, 1}, or equivalently, a class of equivalent states w.r.t P. We note O the set of functions [P → {0, 1}], it is called the set of observations of the system. With each TGS H with set of observable predicates P, we associate the function γ that maps observations to classes of equivalent states, i.e. γ : O → 2 L×[X→[0,M]] , and it is defined as follows:

γ(o) =    (l, v) | (K,ϕ) | o(K,ϕ)=1 (l, v) |= (K, ϕ) ∧ (K,ϕ) | o(K,ϕ)=0 (l, v) |= (K, ϕ)    Note that the set of observations O defines a partition of the state space of the M -TGS, i.e. o∈O γ(o) = L × [X → [0, M ]], and for all o 1 , o 2 ∈ O, if o 1 = o 2 , then γ(o 1 ) ∩ γ(o 2 ) = ∅. Given (l, v) we write γ -1 (l, v) for the observation o of state (l, v), i.e. γ -1 (l, v) is the function o : P → {0, 1} s.t. ∀p ∈ P, o(p) = 1 ⇐⇒ (l, v) |= p.
We associate with any M -TGS H a semantics in the form of a (infinite state) 2-LTTS. The state space of the 2-LTTS will be composed of elements of the form (l, v) where l is a location of the TGS and v is a valuation of the clocks. In order to avoid deadlocks in the 2-LTTS, we require that our TGS are deadlock-free2 , that is, for every state (l, v) such that v |= inv(l), there exists σ ∈ Σ 2 ∪ R >0 , such that either there is a transition (l, g, σ, Y, l

′ ) ∈ δ such that v |= g and v[Y ] |= inv(l ′ ), or for all t ′ , 0 ≤ t ′ ≤ σ, v + t ′ |= inv(l).

Definition 3 (Semantics of a TGS). The semantics of an

M -TGS H = (L, ι, X, δ, Σ 1 , Σ 2 , inv, P) is a 2-LTTS S H = (S, s 0 , Σ 1 , Σ 2 , →) where: -S = {(l, v) | l ∈ L ∧ v ∈ (R ≥0 ∩ [0, M ]) X ∧ v |= inv(l)}; -s 0 = (ι, 0); -the transition relation is composed of (i) discrete transitions. For all (l 1 , v 1 ), (l 2 , v 2 ) ∈ S, for all σ ∈ Σ 1 ∪ Σ 2 , ((l 1 , v 1 ), σ, (l 2 , v 2 )) ∈→ iff there exists a transition (ℓ, g, a, Y, ℓ ′ ) ∈ δ such that ℓ = l 1 , ℓ ′ = l 2 , v 1 |= g, and v 2 = v 1 [Y ]; (ii) time transitions. For all (l 1 , v 1 ), (l 2 , v 2 ) ∈ S, for all t ∈ R >0 , there is a transition ((l 1 , v 1 ), t, (l 2 , v 2 )) ∈→ iff l 1 = l 2 , v 2 = v 1 + t, and for all t ′ , 0 ≤ t ′ < t, (l 1 , v 1 + t ′ ) ∈ S and γ -1 (l 1 , v 1 + t ′ ) = γ -1 (l 1 , v 1 ).
Remark 1. This semantics has the following important property: changes of observations can occur only during a discrete transition, or at the last point of a time delay. This is consistent with our definition of observations using constraints in B(X, M ): the form of the constraints implies that either for all t ≥ 0, (l, v)

t -→ (l, v + t), and γ -1 (l, v + t) = γ -1 (l, v), or there is a first instant t 0 > 0 s.t. (l, v) t0 -→ (l, v + t 0 ) and γ -1 (l, v + t 0 ) = γ -1 (l, v), and for all 0 ≤ t ′ < t 0 , γ -1 (l, v + t ′ ) = γ -1 (l, v).
The 2-LTTS of a TGS has no deadlock because a TGS is deadlock-free. This also implies that any state of the 2-LTTS is the source of an infinite path. As a TGS is bounded, these infinite paths contain infinitely many discrete steps and in the sequel we will consider only these type of infinite paths.

Playing with Observation Based Stuttering Invariant Strategies. In the remainder of this section, we will define the rules of the timed games that we want to consider. We start by an informal presentation and then turn to the formalization.

Player 1 and Player 2 play on the underlying 2-LTTS of a TGS as follows. Player 1 has to play according to observation based stuttering invariant strategies (OBSI strategies for short). Initially and whenever the current observation of the system state changes, Player 1 either proposes an action σ 1 ∈ Σ 1 , or the special action delay. When Player 1 proposes σ 1 , this intuitively means that he wants to play the action σ 1 whenever this action is enabled in the system. When Player 1 proposes delay, this means that he does not want to play discrete actions until the next change of observation, he is simply waiting for the next observation. Thus, in the two cases, Player 1 sticks to his choice until the observation of the system changes: in this sense he is playing with an observation based stuttering invariant strategy. Once Player 1 has committed to a choice, Player 2 decides of the evolution of the system until the next observation but respects the following rules:

1. if the choice of Player 1 is a discrete action σ 1 ∈ Σ 1 then Player 2 can choose to play, as long as the observation does not change, either (i) a discrete actions in Σ 2 ∪ {σ 1 } or (ii) let time elapse as long as σ 1 is not enabled. This entails that σ 1 is urgent, 2. if the choice of Player 1 is the special action delay then Player 2 can choose to play, as long as the observation does not change, any of its discrete actions in Σ 2 or let time pass, 3. the turn is back to Player 1 as soon as the next observation is reached.

Plays. In the following, we define plays of a game where choices of Player 1 are explicitly mentioned. A play in H is an infinite sequence of transitions in

S H , ρ H = (l 0 , v 0 )c 0 σ 0 (l 1 , v 1 )c 1 σ 1 . . . (l n , v n )c n σ n . . . , such that for all i ≥ 0, (l i , v i ) σi -→ (l i+1 , v i+1 ) and -either σ i ∈ {c i } ∪ Σ 2 , or -σ i ∈ R X >0 and ∀0 ≤ t < σ i , c i ∈ enable(l i , v i + t) (time elapses only when the choice of Player 1 is not enabled). 3 -if σ i and σ i+1 are in R X >0 then γ -1 (l i , v i ) = γ -1 (l i+1 , v i+1 ).
We write Play((l, v), H) for the set of plays in H that start at state (l, v). We write Play(H) for the initial plays that start at the initial state of H, that is the set Play((ι, 0), H).

Prefixes, Strategies, and Outcomes. A prefix of H is a prefix of a play in H that ends in a state of H. We note Pref((l, v), H) for the set of prefixes of plays in H that starts in (l, v), i.e. plays in Play((l, v), H). We note Pref(H), for prefixes of initial plays in H, i.e. prefixes of plays in Play(H).

Let ρ H = (l 0 , v 0 )c 0 σ 0 • • • (l n , v n )c n σ n • •
• be a play or a prefix of a play, ρ H (n) denotes the prefix up to (l n , v n ). In the sequel, we measure the length of a prefix by counting the number of states that appear in the prefix. For example, ρ H (n) has a length equal to n + 1. A strategy for Player 1 in H is a function λ H :

Pref(H) → Σ 1 ∪ {delay}. The outcome of a strategy λ H in H is the set of plays ρ H = (l 0 , v 0 )c 0 σ 0 (l 1 , v 1 )c 1 σ 1 . . . (l n , v n )c n σ n . . . such that l 0 = ι, v 0 = 0 and for all i ≥ 0, c i = λ H (ρ H (i))
. We note Outcome H (λ H ) this set of plays.

Consistent Plays, Choice Points and OBSI Strategies in H. We are interested in strategies for Player 1 where the choice of action can only change if the observation of the state of the system changes. Such a strategy is called an observation based stuttering invariant strategy as presented before. When Player 1 plays such a strategy, the resulting plays have the property of being consistent. This notion is defined as follows. A play

ρ H = (l 0 , v 0 )c 0 σ 0 • • • (l n , v n )c n σ n • • • is consistent iff for all i ≥ 0: γ -1 (ℓ i+1 , v i+1 ) = γ -1 (ℓ i , v i ) =⇒ c i+1 = c i .
We note Play co (H) the set of consistent plays of H, and Pref co (H) the set of prefixes of consistent plays of

H. Let ρ H = (l 0 , v 0 )c 0 σ 0 • • • (l n-1 , v n-1 )c n-1 σ n-1 (l n , v n ) ∈ Pref co (H). ρ H is a choice point if either n = 0, or n > 0 and γ -1 (l n-1 , v n-1 ) = γ -1 (l n , v n ). Note that we have that ChoicePoint(H) ⊆ Pref co (H) ⊆ Pref(H) and Play co (H) ⊆ Play(H). Let ρ H = (l 0 , v 0 )c 0 σ 0 • • • (l n , v n )c n σ n • • • be a consistent play in H. Let I = {m | ρ H (m) ∈ ChoicePoint(H)}.
The stuttering free observation Obs(ρ H ) of ρ H is the sequence in (O.Σ 1 ) ω defined by:

-if I = {n 0 , n 1 , • • • , n k } is finite, Obs(ρ H ) = γ -1 (l n0 , v n0 )c n0 • • • γ -1 (l n k , v n k )c n k (γ -1 (l n k , v n k )c n k ) ω -if I = {n 0 , n 1 , • • • , n k , • • • } is infinite, Obs(ρ H ) = γ -1 (l n0 , v n0 )c n0 γ -1 (l n1 , v n1 )c n1 • • • γ -1 (l n k , v n k )c n k • • • We call it "stuttering free" as, for all i ∈ I, γ -1 (l ni , v ni ) = γ -1 (l ni+1 , v ni+1 ) except when I is finite, but in this case, only the last observation is repeated infinitely. Let ρ H ∈ ChoicePoint(H), let I = {n 0 , n 1 , • • • , n k } be the set of indices n i such that ρ H (n i ) ∈ ChoicePoint(H). The (finite) observation of ρ H , noted Obs * (ρ H ), is γ -1 (l n0 , v n0 )c n0 • • • γ -1 (l n k , v n k )c n k γ -1 (l n k , v n k )c n k . We
(λ H ) • Obs(ρ) ↓ O ∈ W.
To conclude this section, we define the control problem OBSI-CP we are interested in: let H be a TGS with observations O, W be a stuttering closed subset of O ω , is there an OBSI winning strategy in H for W?

(OBSI-CP)

In case there is such a strategy, we would like to synthesize one. The problem of constructing a winning strategy is called the synthesis problem.

Subset Construction for Timed Games

In this section, we show how to transform a timed game of imperfect information into an equivalent game of perfect information. Let H = (L, ι, X, δ, Σ 1 , Σ 2 , inv, P) be an M -TGS and let S H = (S, s 0 , Σ 1 , Σ 2 , →) be its semantics. In this section we assume delay ∈ Σ 1 but H has no transition labeled delay.

Useful functions. Let σ ∈ Σ 1 . We define the relation σ -→ nobs by: (l, v)

σ -→ nobs (l ′ , v ′ ) if there is a prefix ρ = (ℓ 0 , v 0 )c 0 σ 0 (ℓ 1 , v 1 )c 1 σ 1 • • • (l k , v k )c k σ k (ℓ k+1 , v k+1 ) in Pref((l, v), H) with (ℓ 0 , v 0 ) = (l, v), (ℓ k+1 , v k+1 ) = (l ′ , v ′ ), ∀0 ≤ i ≤ k, c i = σ, γ -1 (ℓ i , v i ) = γ -1 (ℓ 0 , v 0 ), and γ -1 (ℓ k+1 , v k+1 ) = γ -1 (ℓ 0 , v 0 ). Notice that because of the definition of time transitions in Definition 3, if σ i ∈ R >0 and 0 ≤ i < k then γ -1 (ℓ i , v i ) = γ -1 (ℓ i+1 , v i+1 ) and if σ i ∈ R >0 and i = k, γ -1 (ℓ i , v i ) = γ -1 (ℓ i , v i + t) for all 0 ≤ t < σ i , γ -1 (ℓ i , v i ) = γ -1 (ℓ i , v i + t) and (ℓ i+1 , v i+1 ) = (ℓ i , v i + σ i ) (i.
e. σ i is the first instant at which the observation changes). By the constraints imposed by B(X, M ) this first instant always exists. We define the function Next σ (l, v) by:

Next σ (l, v) = {(l ′ , v ′ ) | (l, v) σ -→ nobs (l ′ , v ′ )} (1)
This function computes the first next states after (l, v) which have an observation different from γ -1 (l, v) when Player 1 continuously plays σ. Next is extended to sets of states as usual.

We also define the function Sink σ (•) :

L × R X ≥0 → L × R X ≥0 for σ ∈ Σ 1 : (l ′ , v ′ ) ∈ Sink σ (l, v) iff there is an (infinite) play 5 ρ = (ℓ 0 , v 0 )c 0 σ 0 (ℓ 1 , v 1 )c 1 σ 1 • • • (l k , v k ) c k σ k (ℓ k+1 , v k+1 ) • • • in S H such that: (ℓ 0 , v 0 ) = (l, v), (ℓ k+1 , v k+1 ) = (l, ′ v ′ ), ∀0 ≤ i, c i = σ, and ∀0 ≤ i, γ -1 (l i , v i ) = γ -1 (l 0 , v 0 ).
Non-Deterministic Game (of Perfect Information). The games of perfect information that we consider here are (untimed) non-deterministic games, and they are defined as follows: in each state s Player 1 chooses an action σ and Player 2 chooses the next state among the σ-successors of s. Definition 4 (Non-Deterministic Game). We define a non-deterministic game (NDG) to be a tuple G = (S, µ, Σ 1 , ∆, O, Γ ) where:

-S = S 0 ∪ S 1 is a set of states; µ ∈ S 0 is the initial state of the game; -Σ 1 is a finite alphabet modeling choices for Player 1;

-∆ ⊆ S 0 × Σ 1 × S is the transition relation;
-O is a finite set of observations; -Γ : O → 2 S \ ∅ maps an observation to the set of states it represents, we assume Γ partitions S (Γ -1 (s) = o ⇐⇒ s ∈ Γ (o)).

Definition 5 (Plays in NDG).

A play in G from s 0 is either an infinite sequence s 0 a 0 s 1 a 1 . . . s n a n . . . such that for all i ≥ 0, s i ∈ S 0 , a i ∈ Σ 1 , and (s i , a i , s n+1 ) ∈ ∆ or a finite sequence s 0 a 0 s 1 a 1 . . . s n such that all i, 0 ≤ i < n, s i ∈ S 0 , (s i , a i , s i+1 ) ∈ ∆, and s n ∈ S 1 . We note Play(s 0 , G) the set of plays starting in s 0 in G and let Play(G) = Play(µ, G). The observation of an infinite play ρ G = s 0 a 0 s 1 a 1 . . . s n a n . . . is defined by

Obs(ρ G ) = Γ -1 (s 0 )a 0 Γ -1 (s 1 )a 1 . . . Γ -1 (s n )a n . . . . If ρ G = s 0 a 0 s 1 a 1 s n-1 a n-1 . . . s n a n s n+1 is finite then Obs(ρ G ) = Γ -1 (s 0 )a 0 Γ -1 (s 1 )a 1 . . . Γ -1 (s n )a n (Γ -1 (s n+1 )a n ) ω .
A prefix in G is a finite sequence s 0 a 0 s 1 a 1 . . . s n ending in s n ∈ S 0 , such that for all i, 0 ≤ i < n, (s i , a i , s i+1 ) ∈ ∆. We let Pref(G) be the set of prefixes of G. The observation of a prefix is

Obs(ρ G ) = Γ -1 (s 0 )a 0 Γ -1 (s 1 )a 1 . . . a n Γ -1 (s n ). For any ρ G ∈ Play(G), ρ G (n) = s 0 a 0 • • • s n is the prefix up to state s n and we let |ρ G | = n to be the length of ρ G .
Remark 2. S 0 is the set of states where Player 1 has to make a choice of action. In S 1 -states, Player 1 does not have any choice. A prefix ends in an S 0 -state. Finite sequences ending in S 1 -states are not prefixes but finite plays.

Strategies and Winning Conditions for

NDG. A strategy in G is a func- tion 6 λ G : Pref(G) → Σ 1 . The outcome, Outcome G (λ G ), of a strategy λ G is the set of (finite or infinite) plays ρ G = s 0 a 0 • • • s n a n • • • s.t. s 0 = µ, ∀i ≥ 0, a i = λ G (ρ G (i)). Let ρ G be a play of G. We let Obs(ρ G ) ↓ O be the projection of Obs(ρ G ) on O. A winning condition W for G is a subset of O ω . A strategy λ G is winning for W in G iff ∀ρ G ∈ Outcome G (λ G ), Obs(ρ G ) ∈ W.
Remark 3. Strategies in NDG are based on the history of the game since the beginning: in this sense, this is a perfect information game.

Knowledge Based Subset Construction. Definition 6. Given a game H = (L, ι, X, δ, Σ 1 , Σ 2 , inv, O, γ), we construct a NDG G(H) = (S, µ, Σ 1 , ∆, O, Γ ) as follows:

-let V = {W ∈ 2 L×R X ≥0 \ ∅ | γ -1 (l, v) = γ -1 (l ′ , v ′ ) for all (l, v), (l ′ , v ′ ) ∈ W }, -S = V × {0, 1}, and we note S 0 the set V × {0} and S 1 the set V × {1}, -µ = ({(ι, 0)}, 0), -∆ ⊆ S × Σ 1 × S is the smallest relation that satisfies: ((V 1 , i), σ, (V 2 , j)) ∈ ∆ if • i = 0. A consequence is that if i = 1 (a state in S 1
) there are no outgoing transitions.

• j = 0 and

V 2 = Next σ (V 1 )∩o for some o ∈ O such that Next σ (V 1 )∩o = ∅, or • j = 1 if Sink σ (s) = ∅ for some s ∈ V 1 and V 2 = ∪ s∈V1 Sink σ (s), -Γ -1 : S → O, and Γ -1 ((W, i)) = γ -1 (v) for v ∈ W . Note that this is
well-defined as W is a set of states of H that all share the same observation.

Notice that the game G(H) is non-deterministic as there may be many transitions labeled by σ and leaving a state s to many different states with different observations. G(H) is total for S 0 states: ∀(V, 0) ∈ S 0 , ∀σ ∈ Σ 1 , σ ∈ Enabled(V ), because either there is an infinite path from some s ∈ V with the same observation or there is an infinite path with a new observation (remember that time can elapse or Player 2 can do a discrete action from any state in H). Although non-deterministic G(H) enjoys a weaker notion of determinism formalized by the following proposition:

Proposition 1. Let (V, i) be a state of G(H), σ ∈ Σ 1 and o ∈ O. There is at most one (V ′ , j) with V ′ ⊆ γ(o) s.t. ((V, i), σ, (V ′ , j)) ∈ ∆. Note also that if ((V, 0), σ, (V ′ , 0)) ∈ ∆ then Γ -1 ((V, 0)) = Γ -1 ((V ′ , 0)).
We can relate the consistent plays in H and plays in G. For that, we define the function Abs : Play co (H) → Play(G) as follows.

Definition 7 (Abs for Plays of H

). Let ρ H = (l 0 , v 0 )c 0 σ 0 (l 1 , v 1 ) . . . (l m , v m ) c m σ m . . . be in Play co (H). Let I = {j ∈ N | ρ H (j) ∈ ChoicePoint(H)}. Then Abs(ρ H ) is defined by: -if I is a finite set, let I = {j 0 , j 1 , • • • , j n }. Define Abs(ρ H ) = s 0 a 0 s 1 a 1 . . . s n
a n s n+1 by induction as follows:

1. s 0 = ({(l 0 , v 0 )}, 0), a 0 = c j0 (and j 0 = 0), 2. and for all i,

0 < i ≤ n, if s i-1 = (V, 0) then let V ′ = Next ai-1 (V ) ∩ γ -1 (v ji ), s i = (V ′ , 0) and a i = c ji . 3.
As ρ H has a finite number of choice points, it must be the case that

∀k ≥ j n , γ -1 (l k , v k ) = γ -1 (l jn , v jn ); moreover, because ρ H is consistent, ∀k ≥ j n , c k = c jn . If s n = (V, 0) we let V ′ = ∪ v∈V Sink cj n (v). V ′ must
be non empty and we define s n+1 = (V ′ , 1).

-if I is an infinite set, let I = {j 0 , j 1 , • • • , j n , • • • }. We define Abs(ρ H ) =
s 0 a 0 s 1 a 1 . . . s n a n s n+1 • • • by induction as follows:

1. s 0 = ({(l 0 , v 0 )}, 0), a 0 = c j0 (and j 0 = 0),

and for all

i ≥ 1, if s i-1 = (V, 0) then let V ′ = Next ai-1 (V ) ∩ γ -1 (v ji ), s i = (V ′ , 0) and a i = c ji .
Definition 8 (Abs for consistent prefixes). Let ρ H = (l 0 , v 0 ) . . .

(l n-1 , v n-1 ) c n-1 σ n-1 (l n , v n ) ∈ Pref co (
H) and, I = {j 0 , j 1 , • • • , j m } be the set of choice points of ρ H . Then Abs(ρ H ) = s 0 a 0 . . . s m-1 a m-1 s m with:

s 0 = ({(l 0 , v 0 )}, 0), -and for all i,

0 < i ≤ m, if s i-1 = (V i-1 , 0) then s i = (V i , 0) where V i = Next ai-1 (V i-1 ) ∩ o i , -∀0 ≤ i < m, a i = c ji .
It can be checked that Abs(ρ H ) is well-defined for consistent plays as well for prefixes. The following theorem states the correctness of our construction: Theorem 1. Let Φ be a stuttering closed subset of O ω . Player 1 has a winning strategy in G(H) for Φ iff Player 1 has an observation based stuttering invariant winning strategy in H for Φ.

Symbolic Algorithms

In this section, we show that the game G(H) is a finite game and design an efficient symbolic algorithm for reachability and safety objectives.

Given a set of states S represented as a finite union of zones, and an action c ∈ Σ 1 we can compute the sets s∈S Next c (s) and s∈S Sink c (s) as finite unions of zones. Since the clocks are bounded in our M -TGS, only a finite number of zones are computed during the computation of those operators. As a consequence, the game G(H) is finite.

To implement efficiently the computations, we use Difference Bound Matrices (DBMs), which allow efficient realisation of most set operations (inclusion, interesection, future, reset. . . ) [START_REF] Dill | Timing Assumptions and Verification of Finite-State Concurrent Systems[END_REF][START_REF] Larsen | Model-checking for real-time systems[END_REF].

Since G(H) is finite, we can apply standard control algorithms to compute the set of winning states. In particular, for reachability or safety objectives, we can use the efficient on-the-fly forward algorithm of [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF] that has been implemented in Uppaal-Tiga [START_REF] Behrmann | Uppaaltiga: Time for playing games![END_REF].

The algorithm for finite games given in [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF] can easily be tailored to solve NDGs of type G = (S, s 0 , Σ 1 , ∆, O, Γ ) with reachability objective Goal s.t. Goal ∈ O. Then, to obtain an algorithm for games of imperfect information, we replace the transition relation of G(H) in this algorithm with the definition (see Definition 6) of the transition relation of G(H) using the Next and Sink operators. This way we obtain the algorithm OTFPOR for TGS which is given Figure 2.

An important feature added to the algorithm is the propagation of losing state-sets, that is state-sets for which the reachability objective can be directly concluded not to be achievable. For reachability games, a state-set W may declared to be losing provided it is not among the Goal sets and is a deadlock. Safety games are dual to reachability games in the sense that if the algorithm concludes that the initial state is not losing it is possible to extract a strategy to avoid losing states.

Example and Experiments

In this section we report on an application of a prototype implementation of the OTFPOR algorithm. Similar to the Box Painting Production System (BPPS) from the Introduction, we want to control a system consisting of a moving belt and an ejection piston at the end of the belt. However, a complicating feature compared with BPPS is that the system can receive both light and heavy boxes. we want to avoid); those transitions are not depicted in the figure. The control objective is to avoid entering location l 7 .

To control the system, the controller can use a clock y that it can reset at any moment. The controller can also issue the order Eject! or propose to play delay, which allows for the time to elapse. The controller has an imperfect information about the state of the system and the value of the clock y. The controller gets information throughout the following observations: E: the control of the automaton is in location l 0 , l 2 , l 3 , l 5 , or l 6 ; H: the control of the automaton is in location l 1 ; L: the control of the automaton is in location l 4 ; B: the control of the automaton is in location l 7 ; 0 ≤ y < M : the value of clock y is in the interval [0, M [, M being a parameter. The observations E, H, L, and B are mutually exclusive and cover all the states of the automaton but they can be combined with the observation 0 ≤ y < M on the clock but also with its complement y ≥ M . So formally, the set of observations that the controller can receive at any time is O = {(E, 0 ≤ y < M ), (E, y ≥ M ), (H, 0 ≤ y < M ), (H, y ≥ M ), (L, 0 ≤ y < M ), (L, y ≥ M ), (B, 0 ≤ y < M ), (B, y ≥ M )}. The set of actions that the controller can choose from is Σ c = {Reset y , Eject!, delay}.

We modelled this example in our prototype and checked for controllability of the safety property A ¬B. Controllability as well as the synthesized strategy heavily depend on the choice of the parameter M , i.e. the granularity at which the clock y may be set and tested. Table 1 gives the experimental results for M ∈ {1, 0.5, 0.25, 0.2}7 . It turns out that the system is not controllabe for M = 1: a granularity of 1 is simply too coarse to determine (up to that granularity) with certainty when, say, a light box will be in l 6 and should be Eject?'ed. The differences between the guards and invariants in l 5 , l 6 and l 7 are simply too small. As can be seen from Table 1 the finer granularities yield controllability.

We report on the number of explored state-sets (state-set ) and the number of state-sets that are part of the strategy (strat ). To get an impression of the complexity of the problem of controller synthesis under partial observability we note that the the model in Figure 3 as a regular timed automaton. Table 1 reports on experiments exploiting an additional inclusion checking option in various ways: (notfi ) without on-the-fly inclusion checking, and (otfi ) with on-the-fly inclusion checking. In addition, we apply the post-processing step of inclusion checking (+post ) on the strategy and a filtering of the strategy (+filter ) on top to output only the reachable state-sets under the identified strategy. The results show that on-the-fly inclusion checking gives a substantial reduction in the number of explored state-sets -and is hence substantially faster. Both (notfi ) and (otfi ) shows that post processing and filtering reduces the size of the control strategy with a factor of approximately 100. It can also be seen that the size of the final strategy grows when granularity is refined; this is to be expected as the strategies synthesized can be seen to involve counting modulo the given granularity. More suprising is the observation that the final strategies in (notfi +post +filter ) are uniformly smaller than the final strategies in (otfi ): not performing on-the-fly inclusion checking explores more state-sets, thus having the potential for a better reduction overall.

Conclusions and Future Works

During the last five years a number of very promissing algorithmic techniques has been introduced for controller synthesis in general and controller synthesis for timed systems in particular. The contribution of this paper to the decidability and algorithmic support for timed controller synthesis under imperfect information is an important new step within this line of research. Future research includes more experimental investigation as well as search for additional techniques for minimizing the size of the produced strategies (e.g. using minimization wrt. (bi)simulation or alternating simulation). For safety objectives, we need methods to insure that the synthesized strategies do not obtain their objective simply by introducing zeno behaviour. Finally, a rewrite of the prototype as extension of Uppaal-Tiga is planned.

On x ≤ 10 Sensor

 10

Fig. 3 .

 3 Fig. 3. Timed Game for Sorting Bricks. Edges to l7 with action Eject? are omitted.

  say that a strategy λ H is an observation based stuttering invariant (OBSI) strategy if the following property holds: for all ρ H

1 , ρ H 2 ∈ Pref co (H), let n 1 be the maximal value such that ρ H 1 (n 1 ) ∈ ChoicePoint(H), let n 2 be the maximal value such that ρ H 2 (n 2 ) ∈ ChoicePoint(H), if Obs * (ρ H 1 (n 1 )) = Obs * (ρ H 2 (n 2 )) then λ H (ρ H 1 ) = λ H (ρ H 2 ). Winning Conditions and Winning Strategies. Let ρ H ∈ Play(H) s.t. Obs(ρ H ) = o 0 c 0 o 1 c 1 . . . o n c n . . . . The projection Obs(ρ H ) ↓ O over O of Obs(ρ H ) is the sequence o 0 o 1 . . . o n . . . . A winning condition W is a stuttering closed 4 subset of O ω . A strategy λ H for Player 1 is winning in H for W, if and only if, ∀ρ ∈ Outcome H

Table 1 .

 1 has 115 reachable symbolic states when viewed Number of state-sets and size of strategy obtained for different heuristics for observations 0 ≤ y < M of the clock y with M ∈ {1, 0.5, 0.25, 0.2}. The case M = 1 is not controllable.

			notfi				otfi
		state-set strat +post +filter state-set strat +post +filter
	[0, 0.2[	110953 36169 1244	70	52615 16372 841	176
	[0, 0.25[ 72829 23750 1014	60	35050 11016 697	146
	[0, 0.5[	20527 6706 561	41	10586 3460 407	88
	[0, 1[	2284	-	-	-	1651	-	-	-

Note that we impose that guards of Player 1's transitions are left closed. This ensures that, when a guard becomes true for an action owned by Player 1, there is always a first instant where it becomes true.

And more precisely, either time can elapse or Player 2 can do a discrete action from any state: thus Player 1 cannot block the game by refusing to take its actions.

Remember that delay is never enabled and if Player 1 wants to let time elapse he plays delay.

A language is stutter closed, if for any word w in the language, the word w ′ obtained from w by either adding a stuttering step (repeating a letter), or erasing a stuttering step, is also in the language.

With an infinite number of discrete transitions because of the boundedness assumption. If needed we can add the requirement that this path is non-zeno if we want to rule out zeno-runs.

Notice that S1-states have no outgoing transitions and we do not need to define a strategy for these states.

Fractional values of M are dealt with by multiplying all constants in the timed game automaton with 1 M .

⋆ Work supported by the French National Research Agency ANR-06-SETI-DOTS. ⋆⋆ Author supported by the Fonds National de la Recherche Scientifique, Belgium. ⋆ ⋆ ⋆ Author supported by the Belgian FNRS grant 2.4530.02 of the FRFC project "Centre Fédéré en Vérification" and by the project "MoVES", an Interuniversity Attraction Poles Programme of the Belgian Federal Government.

Initialization:

P assed ← {{s0}}; When receiving a light box, its speed is high and the box takes between 4 to 6 seconds to reach the zone where it can be Eject?'ed with a piston. When receiving a heavy box, the speed of the belt is slower and the box takes between 9 and 11 seconds to reach the zone where it can be Eject?'ed by the piston. The controller should command the piston so that the order to Eject? a box is given only when the box is in the right region. The system is modeled by the timed game automaton of Figure 3. The initial location of the automaton is l 0 . The system receives boxes when it is in location l 0 , if it receives a heavy box then it branches to l 1 , if it receives a light box then it branches to l 4 . The only event that is shared with the controller is the Eject? event. This event should be issued when the control of the automaton is in l 3 or l 6 (which has the effect of ejecting the box at the end of the belt), in all other locations, if this event is received then the control of the automaton evolves to location l 7 (the bad location that