Jean-Francois Kempf

Marius Bozga

Oded Maler

Performance Evaluation of Schedulers in a Probabilistic Setting

We show how to evaluate the performance of solutions to finite-horizon scheduling problems where task durations are specified by bounded uniform distributions. Our computational technique, based on computing the volumes of zones, constitutes a contribution to the computational study of scheduling under uncertainty and stochastic systems in general.

Introduction

Scheduling, the allocation of limited reusable resources over time to competing tasks, is a universal activity. It is performed routinely in domains of very different scales in terms of time, space and energy. These include the allocation of airways and runways to flights, allocating machines to different product lines in a factory, and the efficient allocation of computation and communication resources to information-processing tasks. This latter activity is becoming of prime importance in many scales, ranging from world-wide cloud computing, via the realization of multiple distributed control loops, down to mapping and scheduling tasks onto multi-core computers. In all such situations one wants to synthesize schedulers which are optimal or good in some sense, or at least to be able to compare the performance of proposed schedulers and choose the better ones. Performance and optimality of such schedulers are typically based on the quantity of work performed over time, which in the case of a finite amount of work can be expressed as termination time. Good schedules are typically associated with intensive, almost idle-free, utilization of critical bottleneck resources.

In a deterministic setting one assumes that everything is known in advance about the demand for work, including the tasks to be executed, their arrival times and the durations for which they occupy resources. In other words, once the scheduling policy itself is determined, the system admits a unique execution scenario (run, realization). Evaluating a scheduler based on this unique run is straightforward -just simulate itwhile finding an optimal scheduler for any non-trivial scheduling problem (such as jobshop) is NP-hard or worse. However, determinism is rarely the case in real life and exact duration of tasks, their arrival times and many other features may vary to large extents. Each instance in this uncontrollable space yields a different schedule and the overall evaluation of a scheduler or a scheduling policy, which can be viewed as a strategy in a two-person timed game [START_REF] Asarin | Controller synthesis for timed automata[END_REF] with uncertainty viewed as an adversary, should be based on some quantification over all possible behaviors it induces [START_REF] Maler | On optimal and reasonable control in the presence of adversaries[END_REF]. This adversarial time-optimality problem has been tackled in [START_REF] Asarin | As soon as possible: Time optimal control for timed automata[END_REF][START_REF] Abdeddaïm | Scheduling with timed automata[END_REF] using a worstcase approach on models of different types of uncertainty. In [START_REF] Asarin | As soon as possible: Time optimal control for timed automata[END_REF], using, the general model of timed game automaton [START_REF] Asarin | Controller synthesis for timed automata[END_REF] where the adversary is discrete, the following problem was proved to be decidable: synthesize a controller which is worst-case timeoptimal in the sense that the maximal (over all possible runs induced by the adversary) time to reach a goal state is minimal. In [START_REF] Abdeddaïm | Scheduling with timed automata[END_REF] the case of job-shop scheduling with uncertain task durations each ranging over a bounded interval was treated. For this problem, worst-case optimality is defined trivially by the optimal solution to a deterministic scheduling problem associated with the worst case where all tasks take their respective maximal duration. One has to define a new notion of optimality (d-future optimal strategies) to make the optimal synthesis problem meaningful, resulting in a synthesis algorithm based on value iteration over sets of clock valuations (zones) which can be seen as an offline version of some kind of model-predictive control.

The use of worst-case reasoning is to some extent a residue of the safety-critical banner under which formal verification has been argued for, but in many (if not most) real-life situations, temporal uncertainty is modeled probabilistically as a distribution over the durations of each task and scheduler quality is measured accordingly, for example by the expected completion time or by its maximum over all but a small fraction of the runs. In this paper we develop and implement a computational framework in order to compute the performance of such schedulers, modeled by automata similar in structure to those used in [START_REF] Abdeddaïm | Scheduling with timed automata[END_REF] but whose durations are probabilistic. Such automata are sufficiently rich to express stochastic variants of well-known scheduling problems such as job-shop or task-graph. Formal definitions of these duration probabilistic automata and their semantics can be found in [START_REF] Maler | On zone-based analysis of duration probabilistic automata[END_REF].

The study of continuous-time stochastic processes has been going on for many years in other branches of mathematics where simple computational questions like those we pose are not typically asked, as well as in closer domains such as probabilistic verification and performance evaluation [START_REF] Brinksma | Lectures on Formal Methods and Performance Analysis[END_REF][START_REF] Bouyer | From Qualitative to Quantitative Analysis of Timed Systems[END_REF]. A well-studied class of such processes are continuous-time Markov chains (CTMC) where durations are distributed exponentially. Such distributions are memoryless in the sense that time spent waiting for a task to terminate does not influence the distribution on the remaining time. As a result they are easy to compute with and problems such as model-checking against qualitative [START_REF] Alur | Model-checking for probabilistic real-time systems[END_REF] and quantitative [START_REF] Baier | Model-checking algorithms for continuous-time Markov chains[END_REF] temporal properties or optimal controller synthesis for finite-horizon problems [START_REF] Abdeddaïm | Scheduling with timed automata[END_REF] are well understood. This forgetfulness assumption may be realistic and useful for modeling request arrivals in queuing models, but seems inappropriate for modeling the durations of several instances of the same computational task. 1In this paper we assume task durations to be uniform over a bounded interval, which is a natural "stochastization" of the set-theoretic temporal uncertainty of timed automata. Handling such systems we find ourselves in the realm of the so-called generalized semi-Markov processes (GSMP), a class of continuous-time stochastic processes [START_REF] German | Non-markovian analysis[END_REF][START_REF] Glynn | A GSMP formalism for discrete event systems[END_REF][START_REF] Cassandras | Introduction to Discrete Event Systems[END_REF][START_REF] Kartson | Modelling with Generalized Stochastic Petri Nets[END_REF]. Similar computational studies of GSMPs include [START_REF] Alur | Bounded model checking for GSMP models of stochastic realtime systems[END_REF][START_REF] Bernadsky | Symbolic analysis for GSMP models with one stateful clock[END_REF], [START_REF] Carnevali | State-density functions over DBM domains in the analysis of non-Markovian models[END_REF][START_REF] Vicario | Using stochastic state classes in quantitative evaluation of dense-time reactive systems[END_REF] and [START_REF] Maler | On zone-based analysis of duration probabilistic automata[END_REF]. The former are concerned with verifying temporal properties for some classes of GSMPs and develop techniques to determine whether the probability of a property-violating behavior is zero. The work of [START_REF] Carnevali | State-density functions over DBM domains in the analysis of non-Markovian models[END_REF][START_REF] Vicario | Using stochastic state classes in quantitative evaluation of dense-time reactive systems[END_REF] is concerned with stochastic Petri nets for which a computational framework is developed for propagating densities in the marking graph. This work, as well as [START_REF] Maler | On zone-based analysis of duration probabilistic automata[END_REF] on duration probabilistic automata, use densities on clocks which are auxiliary state variables. At each reachable state and zone in the clock space, the distribution over clock values is maintained and used to compute the distribution after the next transition. In contrast, the approach presented in this paper works directly on the space of the duration random variables and does not use clocks explicitly. Similar ideas were developed in [START_REF] Jurdzinski | Calculating probabilities of real-time test cases[END_REF] to compute the probability of test cases in timed systems.

The rest of the paper is organized as follows. Section 2 defines single and parallel processes, their behaviors (timed and qualitative) and presents a useful coordinate transformation between durations and time stamps. Section 3 shows how to derive the timing constraints associated with a qualitative behavior when processes execute independently without resource conflicts, and how to compute the volumes of the polytopes they define. Section 4 extends the framework to the more interesting case of resource conflicts that have to be resolved by dynamic scheduling strategies and presents very preliminary experimental results. A discussion of future directions concludes the paper.

Preliminaries

We consider a composition S = P 1 || • • • ||P n of n sequential stochastic processes, each consisting of a sequence of steps. Each step has a probabilistic duration and cannot start before its predecessor terminates. We consider two execution frameworks:

1. Independent execution: all processes start simultaneously and each process starts a step as soon as its preceding step has terminated, regardless of the state of other processes; 2. Coordinated execution: the initiation of a step is controlled by a scheduler which may hold a step of one process in a waiting state until the termination of a step of another process that uses the same resource.

The second framework will allow us to compare schedulers but we start with the first because it is simpler, does not require knowledge of timed automata and hence accessible to a wider audience. On this simpler model we will develop the basic computational machinery that will allow us to compute the probabilities of different qualitative behaviors, each corresponding to an equivalence class of timed behaviors associated with a particular order in which steps of different processes terminate.

Definition 1 (Uniform Distribution). A uniform distribution inside an interval I = [a, b] is characterized by a density ψ defined as

ψ(y) = 1/(b -a) if a ≤ y ≤ b 0 otherwise
and in terms of distribution as

F (y) = y 0 ψ(τ )dτ =    0 if y < a (y -a)/(b -a) if a ≤ y ≤ b 1 if b ≤ y
Definition 2 (Process). A sequential stochastic process is a pair P = (I, Ψ ) where I = {I j } j∈K is sequence of duration intervals and Ψ = {ψ j } j∈K is a matching sequences of densities with ψ j being the uniform density over I j = [a j , b j ], indicating the duration of step j.

We consider finite processes with K = {1, . . . , k}. Probabilistically speaking, step durations can be viewed as a finite sequence of independent uniform random variables {y j } j∈K that we denote as vectors y = (y 1 , . . . , y k ) ranging over a duration space

D = I 1 × • • • × I k ⊆ R k with density ψ(y 1 , . . . , y k ) = ψ 1 (y 1 ) • • • ψ k (y k ).
Each point y in the duration space induces a unique behavior of the system written as a time-event sequence of the form

ξ y = y 1 e 1 y 2 e 2 • • • y k e k . (1)
Time event sequences are alternations between time elapses represented by real numbers and discrete events that take no time. In the case of a single process y j ∈ I j is the duration of step j and e j is the event of terminating that step. The timed language2 associated with the process consists of all the timed behaviors it may generate, namely L = {ξ y : y ∈ D}. The untimed language associated with the process is L, obtained by projecting away durations and retaining events and their order. In the case of a single process L is simply the singleton language {w} where w = e 1 e 2 • • • e k .

Mechanically speaking the process behaviors can be viewed as generated by the automaton of Fig. 1 in which being at state q j corresponds to executing step j. Each run of the automaton is associated with a point y in the duration space. Upon entering q j an auxiliary clock variable x is reset to zero and the termination transition labeled by e j is taken exactly when x = y j .

q 1 q 2 e k q k e 1 e 2 • • • Fig. 1.
An automaton view of a process.

Suppose we want to characterize the probability of a certain subset of L. For example those behaviors in which for every j the actual duration of step j it in some sub-interval I j = [a j , b j ] ⊆ I j . The total probability of these behaviors is simply the volume of the rectangle I 1 × • • • × I k divided by the volume of the whole rectangle D. Probabilities of other subsets of the language can be more interesting but harder to compute. For example, the probability that the whole process terminates before some deadline r is simply the volume of the subset of D satisfying y 1 + • • • + y k < r divided by the volume of D. Our technique is based on computing such volumes for a system of several parallel processes as described in the sequel.

It turns out to be easier to compute volumes after a coordinate transformation from the space of durations to the space of time stamps consisting of vectors t = (t 1 , . . . , t k ) where t j is the absolute occurrence time of event e j , defined as

t j = y 1 + y 2 + • • • + y j .
A behavior ξ y can thus be written also as a sequence of time-stamped events3 ξ t = (e 1 , t 1 ), (e 2 , t 2 ), . . . , (e k , t k ).

Assuming that all durations admit a positive lower bound a j > 0, all time stamps satisfy precedence constraints of the form t j < t j+1 .

Converting y to t and vice versa is done by the linear transformations t = T y and y = T t where T and T are matrices of the form

T =     1 0 0 0 1 1 0 0 1 1 1 0 1 1 1 1     T =     1 0 0 0 -1 1 0 0 0 -1 1 0 0 0 -1 1    
These matrices are lower triangular (the value of t j cannot depend on a duration y j with j > j) and their diagonal entries are equal to 1. The determinant of a triangular matrix is equal to the product of the diagonal entries which is 1 and hence the transformations are volume preserving. This means that the volume of the duration space D is equal to the volume of the time-stamp space C defined by the constraints

ϕ C : j∈K a j ≤ t j -t j-1 ≤ b j
and computing the volume of any subset C ⊆ C amounts to computing the volume of its T image D ⊆ D. Let us remark that the density of t j is the convolution of the densities ψ 1 , . . . , ψ j and its support is the Minkowski sum of I 1 , . . . , I j . The time-stamp space C and its subsets that we will encounter are defined as conjunctions of inequalities of the form x ≺ c or x -x ≺ c where ≺∈ {<, ≤, =, ≥, >} and c is an integer constant. They define polytopes which are called zones (or timed polyhedra). Zones are used extensively in the analysis of timed automata [START_REF] Henzinger | Symbolic model checking for realtime systems[END_REF][START_REF] Daws | The tool KRONOS[END_REF][START_REF] Larsen | UPPAAL in a nutshell[END_REF]. They admit an efficient representation by difference bounds matrices (DBM) [START_REF] Dill | Timing assumptions and verification of finite-state concurrent systems[END_REF] and efficient algorithms based on shortest-path to remove redundant constraints [START_REF] Cormen | Introduction to algorithms[END_REF].

Definition 3 (Process System). A process system consists of n process

S = P 1 || • • • ||P n = {(I i , Ψ i )} n i=1
We use notations P i j to refer to step j of process i and I i j = [a i j , b i j ] and ψ i j for the respective intervals and densities. To ease notation we assume all processes to have the same number k of steps. The event alphabet of the system is

Σ = {e 1 1 , e 1 2 , . . . , e n k-1 , e n k }
consisting of all the termination events of the steps of the various processes. A behavior of the system is induced by a point in the global duration space

y = (y 1 1 , y 1 2 , . . . , y n k-1 , y n k ) ∈ D = n i=1 k j=1 I i j ⊂ R nk ,
which can be transformed into a point t in the time-stamp space

t = (t 1 1 , t 1 2 , . . . , t n k-1 , t n k ) ∈ C = T D
where T is the appropriate block diagonal matrix. When all processes start simultaneously, the time stamps are taken from the same global time reference and one can view a global run as merging local runs and sorting the events according to their time stamps, as illustrated in Fig. 2. The set of all such global behaviors is denoted by

L = L 1 || • • • ||L n .
All timed behaviors that admit the same order of events are said to exhibit the same qualitative behavior. This can be formalized as an operation among the untimed the local languages. Let

L i = {e i 1 e i 2 • • • e i k }
be the untimed language associated with process P i : it consists of the unique qualitative behavior which satisfies the precedence constraints of P i . The potential qualitative behaviors of S constitute the language

L = L 1 || • • • ||L n
which is the shuffle of these languages, that is, the set of sequences consisting of one occurrence of each event in Σ and respecting the local precedence constraints for each process. Mathematically speaking, a qualitative behavior corresponds to a linear order 4which is consistent with the partial order defined by the union of the precedence relations of all the tasks. Such an order is also known as interleaving in the theory of concurrency (motivated readers might want to consult [START_REF] Diekert | The Book of Traces[END_REF] or [START_REF] Esparza | Unfoldings -A Partial-Order Approach to Model Checking[END_REF]).

We use the term qualitative behavior also for any prefix of a sequence in L. Such a prefix corresponds naturally to an incomplete run where not all processes have finished all their steps. From the standpoint of automata, qualitative behaviors correspond to paths in the transition graph of the global automaton associated with the system which is the (Cartesian) product A = A 1 || • • • ||A n of the automata associated with the individual processes as illustrated in Fig. 3. Unfortunately, these extremely important objects are not easy to draw for non-trivial dimensions. Incomplete behaviors correspond to paths not reaching the final state.

In a global state of the form (q 1 j1 , . . . , q n jn ) each process i is busy executing its step j i and there is a race between the termination transitions. The transition e i ji that will win will be the first to satisfy the condition x i = y i ji . Since x i has been reset to zero at t i ji-1 this condition will be fulfilled at time

t i ji-1 + y i ji = t i ji .
The outcomes of all these races are completely determined by the value of y, and this determines the qualitative behavior which is exhibited. Had there been no timing constraints on task durations, that is, I i j = [0, ∞), the system would be completely asynchronous and all interleavings would, in principle, be possible. When durations are bounded, some qualitative behaviors may become strictly impossible due to the arithmetics of timing constraints while others will occur at low probability. In the sequel we develop methods for computing these probabilities.

Computing Volumes

The computation of the probability of a qualitative behavior w is performed in two steps. First we associate with it a zone Z w ⊆ C consisting of all instances of t that yield this behavior. Then we integrate over this zone to find its volume.

Let ϕ C be the constraint describing the whole time-stamp space:

ϕ C : i∈N j∈K a i j ≤ t i j -t i j-1 ≤ b i j
with t i 0 = 0 for every i. The zone Z w for the qualitative behavior of Fig. 2 can be characterized by adding constraints that specify the particular order of events in w:

ϕ w : ϕ C ∧ t 1 1 < t 2 1 < t 2 2 < t 3 1 < t 2 3 < t 1 2 < t 1 3 < t 3 2 < t 3 3 .
Some of these constraints appear already in ϕ C and some are implied via transitivity by other constraints. After eliminating these redundant constraints one obtains the following description: 3 and e 2 2 in state (q 1 3 , q 2 2 ) is indicated by the dashed arrows.

ϕ w : ϕ C ∧ (t 1 1 < t 2 1 ) ∧ (t 2 2 < t 3 1 ) ∧ (t 3 2 < t 1 2 ) ∧ (t 1 3 < t 2 3 ) ∧ (t 2 3 < t 3 3 ).
As illustrated in Fig. 2, the constraints that remain in ϕ w are the inter-process constraints that are sufficient to characterize w. These constraints can be computed incrementally as we move along the prefix of a qualitative behavior. Let us follow the first two steps. Initially we have the empty word whose associated zone is C and hence its probability is 1. After the occurrence of the first event e 1 1 we know that P 1 1 terminated before P 2 1 and P 3 1 . This leads to the constraints:

ϕ e 1 1 : ϕ C ∧ (t 1 1 < t 2 1 ) ∧ (t 1 1 < t 3 1 ) (2)
After this first event we have a competition between e 2 1 , e 3 1 and e 1 2 . The winner of the race is the next event of w, e 2 1 and hence we add the constrains t 2 1 < t 3 1 and t 2 1 < t 1 2 and remove the constraint t 1 1 < t 3 1 which becomes redundant, yielding:

ϕ e 1 1 e 2 1 : ϕ C ∧ (t 1 1 < t 2 1 ) ∧ (t 2 1 < t 3 1 ) ∧ (t 2 1 < t 1 2 ).
In general whenever event e i j occurs, we add a constraint stating that t i j is smaller than the time stamps associated with all the pending events in the other processes. The incremental process is illustrated in Fig. 4.

This procedure is probabilistically correct in the following sense. For every w ∈ L the probability of all behaviors having w as a prefix is the relative volume of the corresponding zone Z w , namely, p(w) = |Z w |/|C|. This holds trivially for the empty behavior when there are no constraints. For the inductive step observe that any qualitative behavior of the form w e which extends w has to satisfy ϕ w due to causality as well as additional constraints that guarantee that e is indeed the next event to win the race. 1 and then for e 1 1 e 2 1 . The constraint t 1 1 < t 3 1 becomes redundant after the second event.

The constraints associated with all the extension of w form a partition of Z w and all the probabilistic mass p(w) is split among them, satisfying e p(w e) = p(w).

In [START_REF] Maler | On zone-based analysis of duration probabilistic automata[END_REF] a similar incremental approach that goes from a path/prefix to its successors has been developed using the clock auxiliary variables. The use of clocks required the concept of density transformers to account for the distribution of clock values before and after transitions (see also [START_REF] Alur | Bounded model checking for GSMP models of stochastic realtime systems[END_REF][START_REF] Bernadsky | Symbolic analysis for GSMP models with one stateful clock[END_REF][START_REF] Carnevali | State-density functions over DBM domains in the analysis of non-Markovian models[END_REF][START_REF] Vicario | Using stochastic state classes in quantitative evaluation of dense-time reactive systems[END_REF]). These are not needed in the clock-free approach presented here. Those acquainted with the verification of timed automata using a forward computation of the simulation/reachability graph [START_REF] Daws | The tool KRONOS[END_REF][START_REF] Larsen | UPPAAL in a nutshell[END_REF] may notice that for every w the zone Z w in the time-stamp space is empty exactly when its associated clock space zone in the reachability graph becomes empty. This suggests an alternative clock-free analysis algorithm for timed automata which is immediately applicable acyclic systems but will require more work to be adapted to the cyclic case.

Having labeled qualitative behaviors by constraints we need to compute the volume of the zones. We illustrate this procedure on a concrete example with n = 3 and k

= 1, hence D = C = I 1 1 × I 2 1 × I 3 1 , with concrete values [a 1 1 , b 1 1 ] = [2, 5], [a 2 1 , b 2 1 ] = [3, 4], and [a 3 1 , b 3 1 ] = [4, 7].
The constraints associated with all qualitative behaviors where process P 1 wins the first race are

ϕ e 1 1 : (2 ≤ t 1 1 ≤ 5) ∧ (3 ≤ t 2 1 ≤ 4) ∧ (4 ≤ t 3 1 ≤ 7) ∧ (t 1 1 < t 2 1 ) ∧ (t 1 1 < t 3 1 ).
We pick an integration order t 3 1 ≺ t 2 1 ≺ t 1 1 , that is, the inside-out order of variable elimination, and rewrite ϕ e 1 1 as

ϕ e 1 1 : (2 ≤ t 1 1 ≤ 5) ∧ (max(3, t 1 1 ) ≤ t 2 1 ≤ 4) ∧ (max(4, t 1 1 ) ≤ t 3 1 ≤ 7)
Then we split I 1 1 into maximal segments where both max(3, t 1 1 ) and max(4, t 1 1 ) are uniform. In our example [START_REF] Alur | Bounded model checking for GSMP models of stochastic realtime systems[END_REF][START_REF] Asarin | Timed regular expressions[END_REF] splits into [START_REF] Alur | Bounded model checking for GSMP models of stochastic realtime systems[END_REF][START_REF] Alur | Model-checking for probabilistic real-time systems[END_REF], [START_REF] Alur | Model-checking for probabilistic real-time systems[END_REF][START_REF] Alur | A theory of timed automata[END_REF] and [START_REF] Alur | A theory of timed automata[END_REF][START_REF] Asarin | Timed regular expressions[END_REF] and the volume of the set can be written as

dt 3 1 dt 2 1 dt 1 1 = 3 + 3 2 + 0 = 9 2
which after dividing by |C| = 9 gives a probability of 1/2 for e 1 1 winning the first race. Figure 5 illustrates two possible splits of a 2-dimensional zone into integration domains. The number of case splits and the forms of the integration domains may vary a lot depending on the chosen order. Theorem 1 (Probability of Qualitative Behaviors). Given a system of stochastic sequential processes as in Def. 3 the probability of any of its qualitative behaviors is computable.

The global termination time (makespan in the job-shop jargon) of a behavior is Θ = max{t 1 k , . . . , t n k }. For all behaviors that are qualitatively equivalent the maximum is attained by the same variable, namely t i k for any behavior whose last event is e i k . To compute the expected termination time we integrate t i k over Z w and sum up over all w:

E(Θ) = 1 |C| n i=1 w=w e i k Zw t i k .
Before moving to the coordinated execution framework let us mention some useful observations. So far we have treated qualitative behaviors in their finest granularity, taking note of the ordering between any pair of events. In many situations we are interested in sets of qualitative behaviors and their probability can often be computed more efficiently than summing up the probabilities of individual qualitative behaviors.

Suppose we want to characterize the set of all qualitative behaviors that pass through a global state q = (q 1 j1 , . . . , q n jn ). Let L i j = {e i 1 • • • e i j-1 } be the qualitative behavior of P i that leads to q i j . Then the set of qualitative behaviors that lead to q is

L(q) = L 1 j1 || • • • ||L n jn .
The constraints that characterize L(q) may forget the specific interleaving, that is, the specific order in which past events have occurred. The only constraints that are relevant are those that guarantee that the entrance of each process into its respective local state preceded the exit of all other processes from their respective states, that is,

ϕ q : ϕ C ∧ n i=1 i =i t i ji-1 < t i j i .
Thus, to compute the expected termination time it suffices to partition the set of qualitative behaviors into n classes according to the identity of the last transition, letting Z i be the zone defined by

ϕ i : ϕ C ∧ i =i t i k < t i k .
Then the expected termination time is

E(Θ) = 1 |C| n i=1 Z i t i k . (3)
A similar observation, made in the context of zone-based verification of timed automata, underlies the fact that the union of zones reached by interleavings of the same set of events is convex [START_REF] Zhao | Partial order path technique for checking parallel timed automata[END_REF][START_REF] Lugiez | A partial order semantics approach to the clock explosion problem of timed automata[END_REF][START_REF] Ben-Salah | On interleaving in timed automata[END_REF].

Conflicts and Schedulers

Now we adapt the framework to the case where steps of different processes may be at conflict due to requiring the same resource and hence cannot be executed simultaneously. Naturally, this situation is more intuitively expressed using automata, states and runs. In order not to discourage semantically challenged audience we explain the automaton-based modeling very informally. Interested readers may consult [START_REF] Abdeddaïm | Scheduling with timed automata[END_REF] for a general framework for modeling and solving scheduling problems with timed automata as well as [START_REF] Maler | On zone-based analysis of duration probabilistic automata[END_REF] for the formal definitions of duration-probabilistic automata (DPA) which is the model underlying this paper. As a running example consider a system of two processes with three steps each, admitting a resource conflict between their respective second steps P 1 2 and P 2 2 . Conflicts are modeled in automata using forbidden states in the global automaton, state (q 1 2 , q 2 2 ) in our example. To be able to prevent the automaton from entering this state 5 we refine the process model so that the initiation of step P i j does not occur automatically upon the termination of step P i j-1 . We thus modify the process automaton shown in Fig. 3 by inserting a waiting state qi j between q i j-1 and q i j . The automaton can leave this state only when it receives a start command s i j from a scheduler as illustrated in Fig. 6-(a). As long as the scheduler is not completely specified the system is open or using another terminology, admits both probabilistic and set-theoretic non-determinism. For example in state (q 1 2 , q 2 1 ) process P 1 may either start its second step (q 1 2 , q 2 1 ) → (q 1 2 , q 2 1 ) or wait until step P 2 1 terminates and let P 2 take the resource first (q 1 2 , q 2 1 ) → (q 1 2 , q2 2 ) → (q 1 2 , q 2 2 ). A scheduler resolves this type of non-determinism by telling each process in a waiting state whether to take the resource and proceed to execution or wait until the resource is taken and released by another process. 6 Once such a scheduler is defined, the set-theoretic non-determinism is eliminated and the only non-determinism that remains is the one associated with task durations and thus it becomes possible to compute probabilities. To be more precise, probabilities can be computed also for non-deterministic schedulers that make a probabilistic choice, but we do not consider them here.

e 1 1 s 1 2 e 1 2 e 1 3 s 2 2 q 2 1 q 1 1 q1 2 q 1 2 q 1 3 q 1 f q2 2 q 2 2 q 2 3 q 2 f q 1 2 q 2 2 x 1 1 := 0 e 2 2 e 2 1 e 2 1 x 2 1 := 0 s 2 2 s 2 2 s 1 2 s 1 2 (a) e 1 1 s 1 2 e 1 2 e 1 3 q 2 1 q 1 1 q1 2 q 1 2 q 1 3 q 1 f q2 2 q 2 2 q 2 3 q 2 f q 1 2 q 2 2 Z12 Z12 Z21 Z21 e 2
A scheduler is thus a mechanism which may observe the state of the system and decide whether to grant a resource to a process, possibly based on the level of progress of other processes. The most passive scheduler grants the resource to the first process whose corresponding becomes enabled. Under such a FIFO scheduling policy it is the result of the race between e 1

1 and e 2 1 which determines the resource granting decision. The automaton obtained by composing the system with such a scheduler is shown in Figure 6-(b) where we have chosen to ignore the zero-measure situation when both processes terminate exactly at the same time (alternatively this situation can be handled by assigning an arbitrary priority when this is the case).

More active schedulers interfere with the execution order by imposing additional conditions upon the start transitions. Suppose that the duration of step P 1 3 is much longer than that of P 2 3 hence it would be reasonable to give P 1 2 a priority over P 2 2 even if the latter becomes enabled earlier. This priority can have different degrees of rigidity. A strict priority scheduler allows s 2 2 only in global states where P 1 2 has terminated, a condition that we write as A 1 > q 1 2 . The automaton obtained by composing the system with such a scheduler is shown in Fig. 7. Note that strict priority schedulers make the automaton always "bypass" a conflict state from the same side.

Strict priority schedulers can be unnecessarily rigid for tasks with durations variability as they do not adapt to the actual evolution of the schedule. As an example for such adaptability consider the case where P 2 1 terminates very early so that we can start P 2 2 so that it will surely terminate before P 1 2 becomes enabled and hence will not block it. Even if this is not guaranteed with certainty, a scheduler might want to start P 2 2 if the expected delay incurred to P 1 is small. Technically, the knowledge of the relative timing of e 2 1 at decision time is encoded by the value of clock x 1 reset upon starting P 1 1 . The larger is the value of x 1 , the more we are likely to block P 1 and for a longer period. Hence the condition for issuing s 2 2 by such a state-dependent scheduler will be of the form (A 1 > q 1 2 ) ∨ (A 1 < q1 2 ∧ x 1 < d) for some constant d. The labeling of states and qualitative behaviors with constraints in order to compute volumes, probabilities and expected termination times can be extended to handle all these types of schedulers. As an illustration consider the FIFO scheduler of Fig. 6-

e 1 1 s 1 2 e 1 2 e 1 3 e 2 1 e 2 1 s 2 2 q 2 1 q 1 1 q1 2 q 1 2 q 1 3 q 1 f q2 2 q 2 2 q 2 3 q 2 f q 1 2 q 2 2 e 2 2 A 1 > q 1
2 Fig. 7. (a) A scheduler that gives strict priority to P 1 . This is realized by the condition A 1 > q 1 2 which allows P 2 2 to start only after P 1 2 terminates.

(b) which admits 4 classes of qualitative behaviors (scenarios) that correspond to the outcomes of the conflict between P 1 and P 2 on the shared resource. These scenarios are characterized by the identity of the winner (for this scheduler it depends on the relation between t 1 1 and t 2 1 ) and by whether the loser termination time is delayed (depending on whether the winner releases the resource before the loser becomes enabled). These cases are summarized in Table 1 and depicted in Fig. 6-(b).

As the alert reader might have noticed, the transformation T from the duration space to the time-stamp space is different from the independent execution framework. It can nevertheless be shown to be volume preserving along the following lines. First, one can show that after adding inter-process precedence constraints causality is preserved and there is always a rearrangement of the indices such that the transformation matrix remains lower triangular. Secondly the notion of volume preservation can be easily generalized from linear to piecewise-linear transformations.

The above analysis can be generalized to m distinct resources and to multi-party conflicts on each of them. For each resource l one can compute the set U l of all the utilization scenarios for this resource and their respective zones. A scenario corresponds to a particular order of resource utilization by conflicting steps and to the waiting delays incurred to these steps. Then the classes of potential qualitative behaviors of interest are the combinations of those, that is, U = U 1 × • • • × U m with zones defined by intersection. While this sounds like a recipe for a severe combinatorial explosion, note that many scenarios will lead to empty zones, either for logical reasons (inter-process ordering of conflicting steps is incompatible with local precedence constraints) or due winner loser delayed loser not delayed to the arithmetics of timing constraints (two conflicting tasks, one at the beginning and one at the end of their respective processes, are likely to be executed in one order). Naturally, for priority schedulers there will be less scenarios to analyze.

P 1 Z 12 a 1 1 < t 1 1 < b 1
We have implemented a prototype tool which computes expected termination times as described in this paper. As input it takes a system description consisting of processes, steps, duration intervals and conflicts as well as a definition of a scheduling policy. Then for every utilization scenario it derives the corresponding zone, using the DBM library of IF [START_REF] Bozga | IF-2.0: A validation environment for component-based real-time systems[END_REF] to normalize constraints and detect empty zones. Then it performs integration over the non-empty zones to compute probability and expected termination time. The integration uses the GNU Multiple Precision Arithmetic Library (GMP) to avoid rounding errors.

Let us describe our preliminary experiments. For each value of n from 1 to 5 and for each value of k from 1 to 40, we choose a number of conflicts (between 0 and 3) and a number of participants in each conflict (2 or 3). Each choice in this space defines a problem type for which we draw 10 concrete problems by randomly choosing the identity of the conflicting steps as well as step duration intervals of the form The experiments with n = 1 compute the volume of one zone, the time-stamp space. Applying the reverse order integration we can compute up to dimension 63 in 0.4 seconds (currently this is a limitation of our DBM library). In general integration takes place in R nk and its complexity depends on the following factors. First, the number of scenarios (orders of resource utilizations and their combinations) determines the number of zones whose volume we might need to compute, in case they are not detected beforehand to be empty. For each zone and each variable t we compute I t , the projection of the zone on t. Then we define a partial order relation between these intervals such that I t < I t if the upper bound of I t is smaller than the lower bound of I t . Then we construct a compatible linear order and integrate backwards. The chosen order determines the number of case splits but also the form of the integration domains and the polynomials obtained during integration. We experienced orders of integration that generate more splits but take less overall computation time. Since there is a lot of exploration and fine tuning ahead it is premature to report performance systematically.

To give an idea, we mention some problem types for which we managed to compute for all the test cases.These include (n, k) = (2, 12) with 2 conflicts, [START_REF] Alur | Model-checking for probabilistic real-time systems[END_REF][START_REF] Asarin | As soon as possible: Time optimal control for timed automata[END_REF] and (4, 6) with 3 binary conflicts or 2 ternary conflicts and (5, 4) with 2 binary conflicts.

Concluding Remarks

We have presented a computational technique to evaluate schedulers in a non-Markovian setting based on splitting the space of valuations of the random variables and computing volumes. To the best of our knowledge no similar computational results have been reported. We mention some future work.

1. Integration over zones is the major computational activity in our procedure and its optimization is an interesting algorithmic problem. 2. To handle larger systems one needs to develop algorithms that do not explore all classes of qualitative behaviors but restrict the exploration to a high-volume small subset of those, whenever such exists. 3. While this work solves the analysis problem it would be more challenging to synthesize optimal schedulers automatically using value iteration.

It is an open question whether such a backward iteration can be defined using the clock-free methods developed in this paper. 4. Another major challenge is to extend this framework to cyclic systems, define the appropriate performance measures and study their steady-state behavior. 5. Finally, it would be interesting to compare the analytic method developed here with statistical approaches based on random simulation. It is intriguing to see how many simulation runs are needed to approximate our results with a good confidence.

Fig. 2 .e 2 1 e 2 2 e 3 1 e 2 3 e 1 2 e 1 3 e 3 2 e 3 3

 23 Fig. 2. A global behavior w = e 1 1 e 2 1 e 2 2 e 3 1 e 2 3 e 1 2 e 1 3 e 3 2 e 3 3 obtained by merging local behaviors. The dashed line indicate the minimal set of additional inter-process constraints that characterize w.

3 Fig. 3 .e 2 1 e 2 2 e 3 1 e 2 3 e 1 2 e 1 3 e 3 2 e 3 3 .

 333 Fig. 3. The product automaton for a process system with n = 2, k = 3. The thick arrows indicate the path corresponding to the qualitative behavior w = e 1 1 e 2 1 e 2 2 e 3 1 e 2 3 e 1 2 e 1 3 e 3 2 e 3 3 . The race between e 13 and e 2 2 in state (q 1 3 , q22 ) is indicated by the dashed arrows.

2 P 3 Fig. 4 .

 234 Fig.4. Incremental constraint construction: constraints for e1 1 and then for e 1 1 e 2 1 . The constraint t 1 1 < t3 1 becomes redundant after the second event.

1 Fig. 5 .

 15 Fig. 5. Zone volume computation by splitting into integration domains in two different integration orders which yield 3 and 2 domains, respectively.

Fig. 6 .

 6 Fig. 6. (a) Two parallel processes admitting a resource conflict and their product automaton. The dashed arrows indicate start transitions which should be under the control of a scheduler while the dotted arrows indicate post-conflict start transitions; (b) The automaton resulting from composition with a FIFO scheduler and the 4 potential conflict resolution and resource utilization scenarios.

  [c-d, c+d] with c drawn uniformly in [40, 50] and d in [0, c/10]. Then we try to compute expected termination times for a FIFO scheduler with a timeout of 3 minutes per problem on an old laptop.

Table 1 .

 1 The zones corresponding to the four possible outcomes of the resource conflict of Fig.7-(b). Constraints on t 1 3 and t 2 3 are omitted.

The academic paper industry is perhaps the prime example of an application domain where this hypothesis is useful.

In the computer science tradition the term language is often used to denote a set of sequences or other objects that define dynamic behaviors.

These are the timed traces used originally in[START_REF] Alur | A theory of timed automata[END_REF] to give semantics to timed automata. More about the relation between semantic models of timed behaviors can be found in[START_REF] Asarin | Timed regular expressions[END_REF].

Since we are dealing with volumes, our neglect of the possibility of events occurring at exactly the same time and not paying too much attention to the distinction between strict and non strict inequalities is justified.

Note that we restrict ourselves to non-lazy schedulers: if they do not issue an s i j command at some point, they will not issue it later unless another process has utilized the resource. This class has been shown[START_REF] Abdeddaïm | Scheduling with timed automata[END_REF] to contain the optimal schedulers for the problems we are dealing with.

Acknowledgment This work grew out of numerous discussions with Kim Larsen and Bruce Krogh and benefitted from the constructive criticism of Eugene Asarin.


Marius Bozga
email: marius.bozga@imag.fr

Vassiliki Sfyrla
email: vassiliki.sfyrla@imag.fr

Joseph Sifakis
email: joseph.sifakis@imag.fr

Modeling Synchronous Systems in BIP

Keywords: D.1.3 [Programming Techniques]: Concurrent Programming, F.1.1 [Computation by abstract devices]: Models of Computation, F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs Languages, Theory, Verification synchronous systems, priority Petri nets, modal flow graphs, Lustre, BIP (Behavior-Interaction-Priority)

published or not. The documents may come   L'archive ouverte pluridisciplinaire

INTRODUCTION

Synchronous systems are composed of strongly synchronized parallel components. Their global behavior is characterized by runs consisting of successive computation steps. In each step, all components perform some quantum of computation. This ensures a built-in fairness between components in sharing resources, usually enforced by using static scheduling policies. Synchronous computation models are particularly adequate for hardware, real-time systems and streaming systems. Their main advantage over asynchronous computation models is efficiency and predictability (determinacy), in particular thanks to lightweight analysis techniques for deciding deadlock-freedom and timeliness.

Nonetheless, for general applications an adequate mix of synchronous and asynchronous computation is necessary for optimal use of resources e.g. GALS models [START_REF] Benveniste | Composing heterogeneous reactive systems[END_REF]. A non-trivial open problem is the design of systems consistently integrating synchronous and asynchronous subsystems e.g. one in Simulink and another in ADA. This requires in principle, the use of a common semantic model encompassing both the synchronous and the asynchronous formalism.

The BIP (Behavior, Interaction, Priority) component framework is a formalism for modeling heterogeneous componentbased systems [START_REF] Basu | Modeling heterogeneous real-time systems in BIP[END_REF]. It allows the description of systems as the composition of generic atomic components characterized by their behavior and their interfaces. It supports a system construction methodology based on the use of two families of composition operators: interactions and priorities. Interactions are used to specify multiparty synchronization between components as the combination of two protocols: rendezvous (strong symmetric synchronization) and broadcast (weak asymmetric synchronizations). Priorities between interactions are used to restrict non determinism inherent to parallel systems. They are particularly useful to model scheduling polices.

In contrast to existing formal frameworks, BIP is expressive enough to directly model any coordination mechanism between components [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF]. It has been successfully used to model complex systems including mixed hardware/software systems and complex software applications.

In this paper, we show how the basic execution mechanisms underlying synchronous data-flow systems can be modeled in BIP. We define a notion of synchronous BIP component which differs from general components in that its behavior is described by a step. Steps of components are delimited by a specific transition labeled by a port sync and executed synchronously by all components. The behavior of a component in a step is described by a safe extended priority Petri net. This is a safe Petri-net whose transitions are labeled with elements of a set of ports P and a priority order, a strict partial order ≺⊂ P × P . Furthermore, transitions may be labeled with guards and functions representing data transformations. The Petri net has a set of initial and a set of final places. When only final places are marked, a step can terminate by executing the specific transition labeled by sync. Termination of a step consists in removing the tokens from final places and putting a token in each initial place. Implicitely, the priority order requires that sync has lower priority than any other port to ensure maximal computation in a step. We define composition of synchronous components as a partial internal operation parameterized by a set of interactions. Given a set of synchronous components, we get a product component by composing their Petri nets and their priority orders.

An essential property of synchronous systems is termination of steps, in particular steps must be deadlock-free. Another requirement is confluence of computation within a step which means that the overall behavior is deterministic when system states are observed only at the end of each step. For some synchronous languages e.g. Lustre, these properties can be ensured by checking very simple sufficient conditions [START_REF] Halbwachs | The synchronous dataflow programming language lustre[END_REF].

We provide results guaranteeing deadlock-freedom and confluence for a class of synchronous systems encompassing most of the existing executable synchronous formalisms. We define the class of modal flow components where priority Petri nets are replaced by modal flow graphs. These graphs correspond to a subclass of priority Petri nets for which deadlock-freedom and confluence can be decided at low cost.

Modal flow graphs are structures expressing dependency relations between events. Similar structures [START_REF] Harel | Assert and negate revisited: Modal semantics for UML sequence diagrams[END_REF][START_REF] Nowak | Synchronous structures[END_REF][START_REF] Zhou | Causality interfaces for actor networks[END_REF] have been proposed and used in different contexts. An important difference between modal flow graphs and related formalisms is the use of three different modalities characterizing dependency between events. For a given set of ports P , a modal flow graph is a directed acyclic graph with nodes P and edges representing the union of three binary relations. Each relation expresses a different kind of causal dependency (modality) between pairs of ports p and q:

• q strongly depends on p if the execution of p must be followed by the execution of q. That is, p and q cannot be executed independently, only the sequence pq is possible.

• q weakly depends on p if the execution of p may be followed by q. That is either p can be executed alone or the sequence pq.

• q conditionally depends on p if when both p and q are executed, then q must follow p. Conditional dependency requires that if p and q occur then only the sequence pq is possible; otherwise or p or q may be independently executed.

In Figure 2, we show the modal flow graph corresponding to the Petri net of The semantics of a modal flow graph is a priority Petri net. It associates with each port a transition of the Petri net. The associated priority order is the inverse of the causality order, that is causes have higher priority than consequences.

Modal flow graphs are deadlock-free if they are well-triggered. This property expresses consistency between the three types of dependency. It also guarantees confluence under some conditions of non interference of concurrent computations.

To illustrate the results, we translate the Lustre language into synchronous BIP. The translation method follows the BIP system construction methodology and involves:

• Definition of the set of atomic components. We need atomic components for modeling flows (variables) and clocks as well as for modeling combinatorial, delay, sampling and interpolation Lustre operators. As in [START_REF] Maraninchi | 42: Programmable models of computation for a component-based approach to heterogeneous embedded systems[END_REF], atomic components have two kinds of ports: 1) data ports associated with data variables and used to input and output data between components and 2) control ports, used to enforce (partially) the control flow of computation within a step.

• Definition of the interactions between atomic components. We use two classes of interactions: 1) interactions which implement the data flow relation between data ports and 2) interactions realizing strong synchronization between control ports of components.

The translation is modular and makes explicit all the interactions needed to perform a synchronous computation in a inherently parallel (component-based) system.

Related work

Our work as a tentative to bridge the gap between synchronous and asynchronous computation, is related to approaches with similar objectives.

In [START_REF] Maraninchi | 42: Programmable models of computation for a component-based approach to heterogeneous embedded systems[END_REF], a model for synchronous components is proposed where steps are described by using automata with final states. Another similarity is the distinction between data ports and control ports. Nonetheless, the latter are activated by controllers which are specific components. The synchronous/reactive domain of the Ptolemy system-level design framework [START_REF] Eker | Taming heterogeneity -the Ptolemy approach[END_REF] allows component-based description of synchronous systems where synchronous execution is orchestrated by a director. Finally, our work has the same general objectives as [START_REF] Benveniste | Composing heterogeneous reactive systems[END_REF] which studies a compositional framework for heterogeneous reactive systems. In contrast to BIP, the framework is denotational and is based on the concept of tags marking the events of the signals of a system.

There are several differences between our work and existing results. Our work is based on operational semantics. It considers synchronous component-based systems as a particular case of the BIP framework which also encompasses general asynchronous computation. Furthermore, we believe that our framework is expressive enough to allow modular translation of synchronous languages into BIP by preserving the structure of the source, as shown for Lustre.

Modal flow graphs without data and only strong dependencies are acyclic partial orders on events. They correspond to acyclic marked graphs which are Petri nets without forward and backward conflicts. Theorem 2 generalizes wellknown results for marked graphs [START_REF] Commoner | Marked directed graphs[END_REF].

Modal flow graphs with strong dependencies and their composition operation are also similar to synchronous structures used in a study of the synchronous model of computation [START_REF] Nowak | Synchronous structures[END_REF]. This model has also some similarities with models such as modal automata [START_REF] Larsen | Modal i/o automata for interface and product line theories[END_REF] which distinguish between must and may transitions or live sequence charts [START_REF] Combes | Modeling and verification of a telecommunication application using live sequence charts and the play-engine tool[END_REF] which distinguish between hot and cold events. Nonetheless, modal flow graphs encompass three independent modalities which are all necessary for modular description of synchronous systems, as shown in the paper. Furthermore, for a reasonably general class of modal flow graphs we proposed sufficient conditions for deadlock-freedom and confluence.

Organisation of the paper

The paper is structured as follows. Synchronous components and their composition are presented in Section 2. Section 3 is the main section of the paper. It presents the sub-class of synchronous components defined by using modal flow graphs as well as sufficient conditions for deadlockfreedom and confluence. Section 4 presents the concrete application of modal flow graphs for modeling of synchronous systems. We conclude and we present future work directions in Section 5. Detailed proofs of propositions and theorems can be found in the technical report [START_REF] Bozga | Modeling synchronous systems in BIP[END_REF].

SYNCHRONOUS COMPONENTS

We present synchronous components and their semantics. The behavior of a synchronous component within a synchronous computation step is a safe extended priority Petri net with given sets of initial and final places. When only final places are marked, termination may happen by removing tokens from final places and putting tokens to initial places.

Definition 1 (synchronous component: syntax).

A synchronous component B is a tuple (X, P, N, ≺) where:

• X is a set of data variables,

• P is a set of ports p, each one labelled with a subset of variables Xp ⊆ X, the ones exported on interactions through p,

• N = (L, T, F, L0, L f ) is an extended 1-safe Petri net:
-L is a finite set of places, -T is a finite set of transitions τ labelled by (pτ , gτ , fτ ) where pτ ∈ P is the port triggered by the transition τ , gτ is the guard of τ , that is a predicate on X and fτ is the update function associated with τ , that is a state transformer defined on X,

-F ⊆ L × T ∪ T × L is the token flow relation,
-L0, L f ⊆ L are the sets of initial, respectively final places

• ≺⊆ P × P is a priority order on ports, that is a strict partial order on the set of ports.

Example 1. Figure 3 shows a synchronous BIP component that produces a tock every P ticks. At every step, it executes the tick transition and then, during the same step, it increases the local variable x by executing the update transition. Whenever x reaches the value P , the component can also execute the tock transition and reset x to 0. In this situation, the tock and update transitions are conflicting, however, the associated priorities enforce the execution of tock before update if both transitions are possible. In order to define the operational semantics for synchronous components, let us first introduce some notation. Given a Petri net N = (L, T, F, L0, L f ) the set of 1-safe markings M is the set of functions m : L → {0, 1}. Given two markings m1, m2, inclusion m1 ≤ m2 holds iff for all l ∈ L, m1(l) ≤ m2(l). Also, addition m1 + m2 is the marking m12 such that, for all l ∈ L, m12(l) = m1(l) + m2(l). Given a set of places K ⊆ L, we define its characteristic marking mK by mK(l) = 1 for all l ∈ K and mK(l) = 0 for all l ∈ L \ K. Moreover, when no confusion is possible from the context, we will simply use K to denote its characteristic marking mK . Finally, for a given transition τ , its pre-set • τ (resp. post-set τ • ) is the set of places flowing to (resp. from) that transition

• τ = {l | (l, τ ) ∈ F } (resp. τ • = {l | (τ, l) ∈ F }).
Given an expression e on variables X, we will note by use(e) the set of variables occuring in e. Given an update function f , we will note by def(f ) the set of variables defined (i.e, modified) by f . Definition 2 (synchronous component: semantics). The operational semantics of a synchronous component B = (X, P, N, ≺) with N = (L, T, F, L0, L f ) is defined as the labelled transition system S = (Q, Σ, -→) where

• Q = M×V is the set of states where M = {m : L → {0, 1}}
is the set of 1-safe markings and V = {v : X → D} is the set of valuations of variables,

• Σ = P ∪ {sync} is the set of labels, Rules R1 and R2 define moves -→0 of the behavior without priorities. Rule R1 is the usual firing rule of transitions in Petri nets extended with global data. Rule R2 defines sync transitions which denote the end of a step and the beginning of the next one. sync transitions can be executed whenever the current marking does not contain tokens in non-final places, and their effect is to restore the initial marking, while keeping the data unchanged. Rules R3 and R4 define the moves -→ of a synchronous component, by restricting -→0 with respect to priorities. Rule R3 is simply the application of the priority rule specified by the priority order ≺. Rule R4 ensures that the sync transition is executed only if no other transition can.

• - →⊆ Q × Σ × Q is the set of transitions defined by the rules in Figure 4 τ ∈ T • τ ≤ m m ′ = m -• τ + τ • gτ (v) v ′ = fτ (v) m ≤ mL f (m, v) pτ -→0 (m ′ , v ′ ) (m, v) sync ---→0 (mL 0 , v) [R1] [R2] (m, v) p -→0 (m ′ , v ′ ) (m, v) sync ---→0 (m ′ , v ′ ) ¬(∃p ′ .p ≺ p ′ ∧ (m, v) p ′ -→0) ¬(∃p.(m, v) p -→0) (m, v) p -→ (m ′ , v ′ ) (m, v) sync ---→ (m ′ , v ′ ) [R3]
Definition 3 (interaction). An interaction a is a triple (Pa, Ga, Fa) where • Pa is a set of ports, the support set of the interaction,

• Ga is the interaction guard, that is a boolean predicate defined on variables ∪p∈P a Xp exported through ports belonging to the interaction,

• Fa is an update (or transfer) function, that is a state transformer on variables ∪p∈P a Xp

We define composition parameterized by interactions as an operation of synchronous components. This operation is partial: the result of the composition is defined as a synchronous component only if the priority order associated to it is acyclic.

Definition 4 (synchronous component: composition).

Let {Bi = (Xi, Pi, Ni, ≺i)}i=1,n be a set of synchronous components defined on disjoint sets of variables and ports. Let γ be a set of interactions on ports ∪ n i=1 Pi such that each interaction uses at most one port of every component, that is for all a ∈ γ, for all i ∈ 1, n, |Pa ∩ Pi| ≤ 1. The composition γ(B1, ..., Bn) is a partial operation defining the synchronous component B = (X, P, N, ≺) where

• the set of variables is X = ∪ n i=1 Xi,
• the set of ports P is the set of interactions γ. Moreover, for each interaction a ∈ γ, its set of exported variables is Xa = ∪p∈P a Xp,

• the Petri net N = (L, T, F, L0, L f ) is obtained from the set of the Petri nets {Ni = (Li, Ti, Fi, L0i, L f i )}i=1,n as follows:

the set of places L = ∪ n i=1 Li, -the set of transitions T corresponds to sets of interacting transitions

T =  a, {τi}i∈I a ∈ γ, I ⊆ 1, n such that ∀i ∈ I.τi ∈ Ti ∧ Pa = {pτ i }i∈I ff
Moreover, for any transition τ = a, {τi}i∈I the associated port pτ is the interaction a, the guard gτ = ∧ n i=1 gτ i ∧ Ga, and the update function fτ = Fa; (⊔ n i=1 fτ i ) consists of the interaction transfer Fa, followed by local functions fτ i in arbitrary order (the order of computation is irrelevant as the data of the components are disjoint).

the token flow relation F of the net is defined as

F = {(l, a, {τi}i∈I ) | ∃j ∈ I.l ∈ • τj} ∪ ˘( a, {τi}i∈I , l) | ∃j ∈ I.l ∈ τ • j - the set of initial places L0 is ∪ n i=1 L0i, -the set of final places L f is ∪ n i=1 L f i ,
• the relation ≺ is the strict transitive closure of the relation ≺0 defined as the extension of individual priority orders ≺i to interactions:

a1 ≺0 a2 iff ∃i ∈ 1, n. ∃pi 1 ∈ Pa 1 ∩ Pi. ∃pi 2 ∈ Pa 2 ∩ Pi such that pi 1 ≺i pi 2 .
The composition is defined only if this relation is a strict partial order.

Example 2. Composition of synchronous components is illustrated in Figure 5. Two tick-tock components are composed by synchronizing the tock of the first component and the tick of the second one. The resulting component produces a tock2 every P 2 ticks.

MODAL FLOW COMPONENTS

Modal flow components are synchronous components defined by modal flow graphs, which correspond to a particular class of priority Petri nets. We define the semantics of atomic flow components as well as their composition. Example 3. In Figure 6, the tick-tock synchronous component of Figure 3, is represented as a modal flow component. The tock transition is weakly dependent on tick transition. Also, the update transition is strongly dependent on tick and conditionally dependent on tock. The only possible executions within a step are therefore tick update or tick tock update.

We use the following notation. For fixed x = s, w, c, we write p x ; q to denote (p, q) ∈ Dx. We write x ; * to denote the reflexive and transitive closure of x ;. We write p ; q to denote (p, q) ∈ Ds ∪ Dw ∪ Dc and ; * for its reflexive and transitive closure. Two ports p and q are called independent (noted p♯q) iff neither p ; * q nor q ; * p.

For fixed x = s, w, c, we denote by minx P the set of minimal ports with respect to Dx, that is minx P = {q | ¬∃p.p We introduce now the notion of well-triggered modal flow graphs. This notion ensures consistency, between the three types of dependencies, defined by the following constraints:

1. each port p has a unique minimal strong cause |{q ∈ mins P | q s ; * p}| = 1 2. each port p has exclusively either strong or weak causes.

For a port p, we denote its minimal strong cause by root(p).

Well-triggered modal flow graphs can be decomposed as shown in Figure 7. The strong dependency relation defines a set of connected subgraphs involving all the ports of the component. Each one of these subgraphs has a single root which is the common cause for its ports. Weak dependencies express triggering of the root of a subgraph by some port of another subgraph. Finally, conditional dependencies may relate ports of different subgraphs provided the acyclicity property is not violated.

We define the semantics of modal flow components which are well-triggered in terms of synchronous components. • the set of variables is X,

• the set of ports is P ; moreover, for each port p the associated set of exported variables is Xp,

• the Petri net N = (L, T, F, L0, L f ) is defined by:

the set of places L is isomorphic to the set Ds ∪ Dw ∪Dc augmented with the set of minimal ports.

That is L = {l x p,q | p x ; q} ∪ {lp | p ∈ min P }, -the set of transitions T is isomorphic to the set of ports P , that is T = {tp |p ∈ P }. Moreover, for any transition tp we associate its port p, the guard gp, and the update function fp,

the token flow relation F ⊆ L × T ∪ T × L, is constructed as follows: * for each p ∈ min P add (lp, tp) to F , * for each dependency p

x ; q add (tp, l x p,q ), (l x p,q , tq) to F , * for each conditional dependency p c ; q add (l c p,q , t root(p) ) to F , -the set of initial places L0 corresponds to minimal ports and conditional dependencies that is L0 = {lp | p ∈ min P } ∪ {l c p,q | p c ; q}, -the set of final places L f consists of all places corresponding to all but strong dependencies L f = L \ {l s p,q | p s ; q}.

• the priority order ≺= (; * ) -1 \ Id, that is p ≺ q iff q ; * p and q = p, for all p, q ∈ P .

The Petri nets representing modal flow components satisfy the following trivial properties: 1) every place has at most one incoming transition, 2) every place l c p,q corresponding to a conditional dependency belongs to a cycle, 3) initially, there is precisely one token in every cycle of the net.

Notice that the above construction rules of the Petri net enforce the three kinds of dependencies between ports. Strong and weak dependencies are obviously enforced by the net. An initial empty place lp,q between tp and tq will prevent the execution of tq before tp. Moreover, if the place is not final, the execution of tp will require the execution of tq before the end of the step. Concerning conditional dependencies p c ; q, the Petri net ensures that the execution of tq disables any further execution of t root(p) and consequently of tp.

Example 4. The tick-tock modal flow component shown in Figure 6 is well-triggered. Its semantics is defined by the tick-tock synchronous component in Figure 3.

The next result gathers some additional properties.

Proposition 1. Priority Petri nets representing modal flow graphs meet the following properties 1. Every reachable marking has at most one token in ev-

ery cycle of the net.

2. Each transition is executed at most once in every step.

3. Are 1-safe.

We are now ready to give the main results about modal flow components. In fact, contrarily to synchronous components, modal flow components can be proven deadlock-free and confluent (i.e., deterministic) by checking syntactic conditions on the underlying modal flow graph. These conditions are formally stated by the following theorem.

Theorem 2. A well-triggered modal flow component:

1. is deadlock-free if every port with strong causes has its guard true.

2. is confluent if for every pair p1, p2 of independent ports p1♯p2, their associated guarded actions are non-interfering, that is:

• Xp 1 ∩ Xp 2 = ∅ • use(gp 1 ) ∩ (Xp 2 ∪ def(fp 2 )) = ∅ • use(gp 2 ) ∩ (Xp 1 ∪ def(fp 1 )) = ∅
Sketch of proof. Intuitively, deadlock situations may occur within a step only because a port with strong dependencies cannot complete its execution. Otherwise, any step eventually completes by firing the sync transition. But, if all ports with strong causes have true guards they can always fire and complete their execution, so deadlock situations never happen. Similarly, non confluence can only result from the execution of independent ports in arbitrary order. For dependent ports, the order of execution is restricted by priorities. Therefore, if every pair of independent ports has non interfering actions then their execution commutes and consequently, steps remain confluent.

Finally, we lift composition of synchronous components to modal flow components, as follows.

Definition 7 (modal flow components: composition).

Let {B f i = (Xi, Pi, Di)}i=1,n be a set of modal flow components defined on disjoint sets of variables and ports. Let γ be a set of interactions on ports ∪ n i=1 Pi such that • each interaction uses at most one port of every component, that is for all a ∈ γ, for all i ∈ 1, n |Pa ∩ Pi| ≤ 1,

• each port belongs to at most one interaction, that is for all

p ∈ ∪ n i=1 Pi |{a | p ∈ Pa}| ≤ 1,
We define the composition γ(B f 1 , ..., B f n ) as the modal flow component B f = (X, P, D) where • the set of ports P is the set of interactions γ. Moreover, for every interaction a of γ, we define the guard ga = (∧p∈P a gp)∧Ga, the exported variables Xa = ∪p∈P a Xp and the transfer function fa = Fa; (⊔p∈P a fp),

• the set of variables X is ∪ n i=1 Xi,
• the set of dependencies D = (Ds, Dw, Dc) are inherited from atomic components, that is for every x = s, w, c we have

Dx = {(a1, a2) | ∃i ∈ 1, n.∃p1 ∈ Pa 1 ∩ Pi, p2 ∈ Pa 2 ∩ Pi such that (p1, p2) ∈ Dxi}
Notice that composition amounts to merging nodes belonging to the same interaction without changing the dependency relations. Composition is a partial operation because, its result is a valid modal flow component only if the set of derived dependencies is acyclic.

Example 5. The composition of modal flow components is illustrated in Figure 8. Three tick-tock modal flow components are composed sequentially by synchronizing the tock each component with the tick of its left neighbour and by keeping all the other transitions unchanged.

Let us observe that composition of modal flow graphs is not the same operation as composition of Petri nets. These differ because conditional dependencies do not have a local interpretation e.g., p c ; q implies that execution of tq disables further execution of t root(p) . But, the minimal strong cause root(p) of p can denote different actions within the modal flow graph of p and within the composed graph.

APPLICATIONS

To illustrate the use of modal flow graphs for modeling synchronous systems, we provide a modular translation of Lustre [START_REF] Halbwachs | The synchronous dataflow programming language lustre[END_REF] into modal flow graphs. Similar translations can be made for other synchronous languages or graphical formalisms [START_REF] Guernic | Programming real time applications with Signal[END_REF][START_REF] Campbell | Modeling and Simulation in Scilab/Scicos[END_REF].

Lustre [START_REF] Halbwachs | The synchronous dataflow programming language lustre[END_REF] is a dataflow synchronous language for programming reactive systems.

= x = E | x, • • • , x = N (E, • • • , E) E ::= x | v | op(E, • • • , E) | pre(E, v) | E when b | current E A Lustre program
is structured as a set of nodes. Each node computes output flows from input flows. Output flows are defined either directly by means of equations of the form x = E, meaning xn = En for any time instant n ≥ 0 or, as the output of other (already defined) nodes instantiated with particular inputs x, ... = N (E, ...).

The basic operators used in expressions E, are combinatorial operator (op), unit delay (pre), sampling (when) and interpolation (current). Combinatorial (memory-less) operators include usual boolean, arithmetic and relational operators. The unit delay pre operator gives access to the value of its argument at the previous time instant. For example, the expression

E ′ = pre(E, v) means E ′ 0 = v and E ′ i = Ei-1, for all i ≥ 1.
In Lustre each flow (and expression) is associated with a logical clock. Implicitely, there always exists a unique, fastest, basic clock which defines the step (or basic clock cycle) of a synchronous program. Depending on this clock, other slower clocks can be defined as the sequences of time instants where boolean flow variables take the value true. In order to define and manipulate flows operating on slower clocks, Lustre provides two additional operators. The sampling operator when, samples a flow depending on a boolean flow. The expression E ′ = E when b, is the sequence of values E when the boolean flow b is true. The expression E and the boolean flow b have the same clock, while the expression E ′ , operates on a slower clock defined by the instants at which b is true. The interpolation operator current, interpolates an expression on the clock which is immediately faster than its own clock. The expression E ′ = current E, takes the value of E at the last instant when b was true, where b is the boolean flow defining the slower clock of E.

We consider statically correct programs which satisfy the static semantics rules of Lustre [START_REF] Halbwachs | About synchronous programming and abstract interpretation[END_REF]. These rules exclude programs containing cyclic, dependent equations, recursive calls of nodes as well as combinatorial operators applied to expressions having different clocks.

We define modular translation for Lustre, first for singleclock programs and then for multi-clock programs.

Single-clock synchronous programs

The single-clock subset of Lustre is generated by using only combinatorial and unit delay operators. All flows are sampled (indexed) by the basic clock.

The translation from Lustre to modal flow graphs is modular. Each node is represented by a well-triggered modal flow component with two kinds of ports: act control ports and in/out (input/output) data ports. An act port is triggered by the basic clock and initiates the step of the node. The in (resp. out) data ports carry data input (resp. output) read (resp. produced) by the node. Additionally, modal flow graphs may contain internal ports and variables, depending on the specific computation carried by the node. The modal flow components shown in Figure 9 correspond to basic Lustre elements: flow, pre operator and combinatorial operator. The flow component whenever activated through the act port, reads a value through the in port and outputs this value through the out port in the same step. The pre component has a local variable x. Whenever it is activated through act, it outputs the current value x, then it inputs and assigns a new value to x to be used in the next step. The combinatorial component starts a step when it is triggered through the act port. Then it reads input values in some arbitrary order, performs its specific computation, and finally, produces an output value.

The modal flow component representing a single-clock Lustre node is obtained by composing a set of components by using a set of interactions defined as follow.

• components: For each input and output flow declared in the node we add a flow component. For each pre (resp. combinatorial) expression occuring within the equations, we add a pre (resp. combinatorial) component. Moreover, for each subnode called within equations we add its corresponding modal flow component.

• interactions: Interactions are of two types: control flow and data flow. A single control flow interaction realizes strong synchronization between all the act ports of all components. Data flow interactions synchronize one out port to one or more in ports. They are used to propagate data from input flow components to expression components and from expression components to output flow components or other expression components according to the syntactic structure of expressions and equations. The following theorem is a consequence of modularity of translation and of the following facts: 1) the modal flow graphs corresponding to the basic constructs of Lustre are well-triggered; 2) for statically correct Lustre programs [START_REF] Halbwachs | The synchronous dataflow programming language lustre[END_REF], composition of the basic modal flow graphs preserves welltriggeredness.

Theorem 3. Every statically correct single-clock Lustre node N is represented by a well-triggered modal flow component B f N such that:

1. it has a unique root which is an act port;

2. all its dependencies are strong;

3. it is deadlock-free and confluent;

4. simulates the micro-step Lustre semantics [START_REF] Halbwachs | About synchronous programming and abstract interpretation[END_REF] of N .

Multi-clock synchronous programs

In Figure 12, we provide two components modeling respectively the sampling and interpolation operators of Lustre. Both components have two control ports, acti and acto triggering respectively the input in and the output out data ports. For a sampling component, acto depends weakly on acti, and moreover, the output out dependends conditionally on the input in. Thus an input is always read and whenever required, an output is produced with the most recent value of the input -which is precisely the interpretation of sampling. For the interpolation component, we have the opposite: acti depends weakly on acto but out conditionally depends on in. Thus the output is always produced with the most recent value of the input. The last modal flow graph in Figure 12 describes an additional component, the derived clock component corresponding to a boolean flow b. This component is used to initiate all the computations carried on the clock b. Intuitively, it triggers the slower clock port only after its base clock act has been triggered and if the value obtained through the data input in port is true. We apply a similar modular construction method for building modal flow components for multi-clock nodes.

• components: First, we add a derived clock component for each clock (i.e, when b). Second, we add a sampling (resp. interpolation) component for each sampling (resp. interpolation) expression occuring within the equations of the node.

• interactions: The data flow interactions are the same as for the single-clock case, with the addition that data is also propagated to the input port of derived clocks. Regarding control flow interactions, we add one interaction which synchronizes all the act ports of flows and expressions sampled on the basic clock. In addition, for each derived clock component, we add an interaction which synchronizes its clock port with all act ports of flows and expressions sampled by that clock. Depending on an input value x triggered by an input clock a, the input_output node produces a corresponding output value z triggered by an output clock c, by using the most recent available value of the input.

The main node is the input_output node which interconnects the two nodes, input_handler and output_handler. The input_handler node receives at every moment the boolean value a. An integer value x is received only when a is true. The output value y is an integer produced at every moment by interpolating the value of x. The output_handler node receives at every moment a boolean c and an integer variable y. It produces an output z by sampling y when c is true. Finally, the input_output top node connects the output of the input_handler to the input of the output_handler.

Figure 13 shows the modal flow component representing the system. Its modal flow graph is obtained after composition and static simplification of the modal flow graphs of the input output node. It can be decomposed into three subgraphs with activation ports act, acta and actc corresponding respectively to the basic, when a, and when c clocks. 2. the subgraphs defined by strong dependencies are connected through weak dependencies into a tree;

3. is deadlock-free and confluent;

4. simulates the micro-step Lustre semantics [START_REF] Halbwachs | About synchronous programming and abstract interpretation[END_REF] of N

Experimental work

We have studied and implemented a translator from Lustre to BIP synchronous components which directly generates Petri nets without using modal flow graphs. The translator is currently fully operational. It takes as input Lustre programs and produces full-fledged BIP systems, that can be simulated and analyzed using the BIP toolset [START_REF] Basu | Modeling heterogeneous real-time systems in BIP[END_REF].

This first approach has important drawbacks. For the generated BIP programs it is not easy to verify properties guaranteed by construction e.g. deadlock-freedom and confluence. Moreover, the BIP compilation chain cannot easily recover the information that the system is indeed synchronous and consequently, it cannot produce optimized code. For example, experiments with concrete Lustre programs show an 600 : 1 overhead of execution time between the C code produced by the BIP compiler and executed by the BIP engine, and the flat C code produced by the Lustre compiler. Although, this overhead can be diminished to 20 : 1 by applying static composition of components in BIP [?], it still remains high.

Modal flow graphs allow coping with these drawbacks. We are now investigating the possibility to integrate directly modal flow components in BIP. Our results about confluence and deadlock-freedom of modal flow components provide syntactic conditions, easy to check automatically. Moreover, modal flow components keep all the data-flow explicit and can be used to generate efficient code, monolithic or not, as synchronous language compilers do.

CONCLUSIONS

We present a general approach for modeling synchronous component-based systems. These are systems of synchronous components strongly synchronized by a common action sync that initiates execution steps of each component. Steps are described by priority Petri nets. Priorities are instrumental for enforcing run-to-completion in the execution of a step. Modal flow graphs are introduced and used to define a particular class of Petri nets for which deadlock-freedom and confluence are met by construction provided some easy-tocheck conditions hold. This result is the generalization of existing results for classes of Petri nets without conflicts. It allows more general behavior for components given that the semantics of conditional dependencies lead to Petri nets with backward conflicts and priorities.

The definition of synchronous components as a subset of the BIP framework allows their combination with other asynchronous languages that can be translated into BIP. The proposed semantics has maximal parallelism, that is it shows only the absolutely necessary dependencies between events. Execution in a step is non deterministic. However, if the behavior is confluent then the order of execution is irrelevant. The translation of Lustre shows the interplay between data flow and control flow and allows understanding how strict synchrony can be weakened to get less synchronous computation models.

This work opens the way for studying combination of synchronous and asynchronous systems. It allows integration of synchronous systems theory in an all encompassing component framework [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF] without losing advantages such as correctness-by-construction and efficient code generation. This makes possible modeling mixed synchronous/asynchronous systems without artefacts. The meaningful integration of synchronous and asynchronous models in this framework is the subject of future work.

Figure 1 :

 1 Figure 1: Email treatment

Figure 1

 1 Figure1shows a priority Petri net describing the treatment of an email in one computation step. The sync transition is not explicitly represented. Initial places are marked with a token; final places are grayed. Transitions are enabled when their input transitions are marked and the associated condition is true. The priority order restricts choices amongst enabled transitions (ports). That is if both forward and close are enabled then forward is executed. Therefore, depending on the conditions [cond1] and [cond2], the possible execution sequences are : open read close, open read forward send1 close, open read reply write send2 close, open read (forward send1 || reply write send2) close where || is the interleaving of sequences.We define composition of synchronous components as a partial internal operation parameterized by a set of interactions. Given a set of synchronous components, we get a product component by composing their Petri nets and their priority orders.An essential property of synchronous systems is termination of steps, in particular steps must be deadlock-free. Another requirement is confluence of computation within a step which means that the overall behavior is deterministic when system states are observed only at the end of each step. For some synchronous languages e.g. Lustre, these properties can be ensured by checking very simple sufficient conditions[START_REF] Halbwachs | The synchronous dataflow programming language lustre[END_REF].We provide results guaranteeing deadlock-freedom and confluence for a class of synchronous systems encompassing most of the existing executable synchronous formalisms. We define the class of modal flow components where priority Petri nets are replaced by modal flow graphs. These graphs correspond to a subclass of priority Petri nets for which deadlock-freedom and confluence can be decided at low cost.

Figure 1 .

 1 Bold, simple and dashed arrows represent respectively strong, weak and conditional dependency relations.

Figure 2 :

 2 Figure 2: Modal flow graph for email treatment

Figure 3 :

 3 Figure 3: Tick-tock synchronous component

Figure 4 :

 4 Figure 4: Operational Semantics Rules

Figure 5 :

 5 Figure 5: Example of composition

Figure 6 :

 6 Figure 6: Tick-tock modal flow component

Figure 7 :

 7 Figure 7: Well-triggered components.

Figure 8 :

 8 Figure 8: Example of composition

  Lustre programs operate on flows of values, that are infinite sequences (x0, x1, • • • , xn, • • • ) of values at logical time instants 0, 1, • • • , n, • • • . An abstract syntax for Lustre programs is shown below. In (resp. Out) denotes the set of input (resp. output) flows of a program node. Symbols N , E, x, v, b denote respectively node names, expressions, flows, boolean flows and constant values.

  program ::= node + node ::= node N (In) (Out) equation + equation ::

  = op(x1, x2)

Figure 9 :

 9 Figure 9: Single-clock operators

Example 6 .Figure 10 :

 610 Figure 10: IntegratorThe representation of this node as a composition of modal flow components is shown inFigure 11 (top). The atomic modal flow components correspond to the pre operator, the combinatorial + operator, the input flow and the output flow. In addition to the act interaction, there are three interactions for data transfer from outputs to inputs: 1) from the input flow component to the + component, 2) from the pre component to the + component and 3) from the + operator to the output flow component and back to the pre component. The result of the composition is shown in Figure11(bottom).

Figure 11 :

 11 Figure 11: The Integrator modal flow component

Figure 12 :

 12 Figure 12: Multi-clock operators

Example 7 .

 7 Consider the following Lustre program: node input_handler(a: bool, x: int when a) returns y: int; let y = if a then current x else pre(y, 0); tel ; node output_handler(c: bool, y: int) returns z: int when c; var yc: int when c; let yc = y when c; z = yc * yc ; tel ; node input_output(a,c: bool, x: int when a) returns z: int when c; var y: int; let y = input_handler(a, x); z = output_handler(c, y); tel;

Figure 13 :Theorem 4 .

 134 Figure 13: The input/output handler The following theorem establishes the correctness of our translation. Theorem 4. Every statically correct multi-clock Lustre node N is represented by a well-triggered modal flow component B f N which: 1. has multiple (control) root act ports, one for each clock in the Lustre program, and multiple data in/out ports;