Philippe Darondeau
email: darondeau@irisa.fr

Blaise Genest
email: bgenest@irisa.fr

P S Thiagarajan

Shaofa Yang

Quasi-Static Scheduling of Communicating Tasks

Keywords: Communicating machines, Quasi-static scheduling, Channel bound. 2000 MSC: 68N30

HAL is a

Introduction

The high complexity of embedded systems poses challenges for their design and verification. To tame the complexity, a possible design methodology is to use specifications that are intrinsically concurrent and asynchronous, such as data flow networks [START_REF] Buck | Scheduling dynamic dataflow graphs with bounded memory using the token flow model[END_REF], Kahn process networks [START_REF] Kahn | The Semantics of Simple Language for Parallel Programming[END_REF], and Petri nets [START_REF] Liu | Schedulability Analysis of Petri Nets Based on Structural Properties[END_REF]. To implement a large system of interactive tasks on a collection of hardware resources, one partitions the large specification into small clusters of processes and one subsequently implements each cluster independently, see e.g. [START_REF] Carmona | Synthesis of Asynchronous Hardware from Petri Nets[END_REF]. In specifications, processes communicate via buffers, that are allowed to be arbitrarily large. Clearly, in implementations, one must use a finite amount of resources, and in particular, a finite capacity for communication buffers inside each cluster. A basic problem is thus how to schedule processes properly within each cluster, considered as a separate system, so that asynchronous buffers internal to the cluster never exceed some finite bound. We model each cluster as a finite system of processes communicating via point-to-point buffers. Each process is a sequential transition system, in which non-deterministic branchings may have two origins: (i) a data-dependent internal choice made by a sequential component; (ii) a process waiting for messages on different input buffers. In the second case, the waiting process non-deterministically branches by picking up a message from one of the nonempty input buffers [START_REF] Cortadella | Quasi-static scheduling of independent tasks for reactive systems[END_REF]. The system of processes is triggered by the environment iteratively in rounds. We model the system dynamics for just one round. It is easy to lift results to multiple rounds. In each round, the environment sends a data item to one of the processes. This communication starts the computation to be done in the round. The computation finishes successfully when all processes are in their final states and all buffers are empty. Then, the system waits for the initialization of a new round by the environment. In a technical sense, buffers-which are viewed here as counters without zero tests-are deployed as over-approximations of FIFOs whereas, using FIFOs directly would make the model Turing powerful [START_REF] Brand | On Communicating Finite-State Machines[END_REF]. In the present setting, we are interested in determining a good schedule for the processes: If at some configuration the scheduler picks the process p for execution and p is at a state with several outgoing transitions, then we require that a good schedule allows all possible choices to occur. In the sequel, such schedules are referred to as quasi-static schedules. In addition, a good schedule should never prevent the system from (eventually) reaching the final state. Schedules with this property are called here valid schedules. Finally, a good schedule is required to be regular in the sense that the system under schedule should use only a bounded amount of memory for serving the request made by the environment. In particular, the schedule should enforce a uniform upper bound on the number of items stored in the buffers during the round.

We show first that it is undecidable whether a valid and regular quasi-static schedule exists. The undecidability result holds even if the system on its own is valid in that it is possible to reach the final global state from every reachable global state of the unscheduled system. Next we define the subclass of databranching systems in which the simultaneous polling on multiple input buffers is ruled out; hence the only branching allowed is local (data-dependent) branching. We show that for data-branching systems, one can effectively check whether there exists a valid and regular quasi-static schedule. This result is obtained by applying classical ideas from [START_REF] Karp | Parallel Program Schemata[END_REF] to a special scheduling policy that we define, called the canonical schedule. The canonical schedule is based on the same ideas as the normal form used for the existential boundedness of languages of message sequence charts [START_REF] Genest | On Communicating Automata with Bounded Channels[END_REF]. The crucial point is that one cannot directly apply the techniques of [START_REF] Karp | Parallel Program Schemata[END_REF] to the scheduling problem, because the canonical schedule uses zero tests on buffers. It is well known that zero tests often lead to undecidability, but fortunately this is not the case here.

Before reviewing related work, it is worth noting that our setting is strongly oriented towards round-based executions of distributed tasks. Hence it does not cater for models capturing non-terminating computations such as Kahn process networks [START_REF] Kahn | The Semantics of Simple Language for Parallel Programming[END_REF]. It is not clear at present whether our undecidability result can be extended to such settings. Quasi-static scheduling (QSS) has been studied in the past in a number of settings (see [START_REF] Kondratyev | Quasi-static scheduling of concurrent specifications[END_REF] for a survey). The early work [START_REF] Buck | Scheduling dynamic dataflow graphs with bounded memory using the token flow model[END_REF] studied dynamic scheduling of boolean-controlled dataflow graphs. As this computation model is Turing powerful, the QSS problem is undecidable for this class of systems [START_REF] Buck | Scheduling dynamic dataflow graphs with bounded memory using the token flow model[END_REF]. Later, [START_REF] Cortadella | Quasi-static scheduling of independent tasks for reactive systems[END_REF] proposed a heuristic to solve the QSS problem on a different model called the YAPI model by exploring only a subset of the infinite state space. There is however no proof that the heuristic is complete, even for a subset of YAPI models. The work [START_REF] Sgroi | Quasi-Static Scheduling of Embedded Software Using Equal Conflict Nets[END_REF] considered the QSS problem on a restricted class of Petri nets called Equal-Conflict Petri nets and showed the decidability of this problem. However the notion of schedulability used in [START_REF] Sgroi | Quasi-Static Scheduling of Embedded Software Using Equal Conflict Nets[END_REF] is much weaker than the one proposed in [START_REF] Cortadella | Quasi-static scheduling of independent tasks for reactive systems[END_REF] or the one which we propose here. Basically, under the scheduling regime defined in [START_REF] Sgroi | Quasi-Static Scheduling of Embedded Software Using Equal Conflict Nets[END_REF], only a finite number of runs can arise, hence systems with loops are not schedulable. In comparison, the system models which we consider are very close to (general) Petri Nets. Our scheduling notion is essentially the same as in [START_REF] Cortadella | Quasi-static scheduling of independent tasks for reactive systems[END_REF], but slightly modified to fit our model. Our undecidability result is harder to obtain than the similar result in [START_REF] Buck | Scheduling dynamic dataflow graphs with bounded memory using the token flow model[END_REF], since reachability is decidable for our system models. Indeed, the decidability of our quasi-static schedulability problem is stated as an open problem in [START_REF] Cortadella | Quasi-static scheduling of independent tasks for reactive systems[END_REF][START_REF] Kondratyev | Quasi-static scheduling of concurrent specifications[END_REF]. The work [START_REF] Liu | Schedulability Analysis of Petri Nets Based on Structural Properties[END_REF] considered QSS in the setting of [START_REF] Cortadella | Quasi-static scheduling of independent tasks for reactive systems[END_REF] and proposed a sufficient (but not necessary) condition for non-schedulability based on the structure of the Petri net system model. There is also previous research concerning FIFOs, proposing a semi-effective check for schedulability [START_REF] Parks | Bounded Scheduling of Process Networks[END_REF] as well as a necessary condition that implies non-schedulability [START_REF] Jard | Testing for Unboundedness of FIFO Channels[END_REF]. These cited works use methods similar to ours and [START_REF] Karp | Parallel Program Schemata[END_REF]. However these results do no establish clear-cut boundaries between the decidable and undecidable partly due to the expressiveness of unbounded FIFOs.

In the next section we present our model of systems and the quasi-static scheduling problem. Section 3 establishes the undecidability result in the general setting. Section 4 imposes the data-branching restriction and shows the decidability of the quasi-static scheduling problem under this restriction. The final section summarizes and discusses the results. This paper is a complete version of the extended abstract [START_REF] Ph | Quasi-Static Scheduling of Communicating Tasks[END_REF].

Preliminaries

Through the rest of the paper, we fix a finite set P of process names. Accordingly, we fix a finite set Ch of buffer names. To each buffer c, we associate a source process and a destination process, denoted src(c) and dst (c) respectively. We have src(c) = dst (c) for each c ∈ Ch. For each process p, we set

Σ ! p = {!c | c ∈ Ch, src(c) = p} and Σ ? p = {?c | c ∈ Ch, dst (c) = p}.
So, !c stands for the action that deposits one item into the buffer c while ?c is the action that removes one item from c. For each p, we fix also a finite set Σ cho p of choice actions. We assume that Σ cho p ∩ Σ cho q = ∅ whenever p = q. Members of Σ cho p will be used to label branches arising from the abstraction of data dependences in the "if...then...else", "switch..." and "while..." statements executed by the process p. For each p, we set Σ p = Σ ! p ∪ Σ ? p ∪ Σ cho p . Note that Σ p ∩ Σ q = ∅ whenever p = q. Finally, we fix Σ = p∈P Σ p .

A task system (abbreviated as "system" from now on) is a structure A = {(S p , s init p , -→ p , s fi p )} p∈P , where for each p ∈ P, S p is a finite set of states, s init p is the initial state, -→ p ⊆ S p × Σ p × S p is the transition relation, and s fi p is the final state. As usual, if s p ∈ S p and δ = (ŝ p , a p , ŝ′ p ) is in -→ p with ŝp = s p , then we call δ an outgoing transition of s p . We require the following conditions to be satisfied:

• For each p ∈ P and s p ∈ S p , if the set of outgoing transitions of s p is not empty, then exactly one of the following conditions holds:

-Every outgoing transition of s p is in S p × Σ cho × S p . Such a state s p is a (data-dependent) choice state.

s p has exactly one outgoing transition and this transition is a send (s p , !c, s ′ p ), where c ∈ Ch, s ′ p ∈ S p . Such a state s p is a sending state. -Every outgoing transition of s p is in S p × Σ ? p × S p . Such a state s p is a polling state.

• For each process p, the final state s fi p either has no outgoing transitions or it is a polling state.

The system works in rounds. When the first round starts, all the processes will be in their initial states and the buffers will be empty (it is easy to lift the results in the paper to any other initialization of the buffers, modeling different memory states). The first round starts when a message from the environment is received on a designated channel by a designated process (the same for each round). At the end of each round, every process will be in its final state, and all buffers will be empty. A reset operation -possibly triggered by the environment-is assumed to be performed to initiate a new round. This operation puts every process in its initial state from which the computation can start again (upon receiving a message from the environment as described above). Thus, computations belonging to different rounds will not get mixed up. We do not explicitly represent this reset operation in the system model.

For technical convenience, we do not consider multi-rate communications where multiple items can be deposited to or picked up from a buffer at one time. However, our results extend easily to multi-rate task systems. They can also be adapted to systems where several rounds can overlap (e.g. pipelines), as long as the system terminates (this rules out general Kahn process networks).

For notational convenience, we shall assume that the system is deterministic, that is for each p, for each s p ∈ S p , if (s p , a1, s1 p ), (s p , a2, s2 p ) are in -→ p , then a1 = a2 implies s1 p = s2 p . However, all our results can be extended easily to non-deterministic systems. The dynamics of a system A are defined by the transition system TS A which we describe now. A configuration of A is a pair (s, χ) where s ∈ p∈P S p and χ is a mapping that assigns to each buffer c in Ch a non-negative integer χ(c) indicating the number of items it contains. We term the members of p∈P S p as global states. We view a global state as a mapping from P to p∈P S p such that s(p) ∈ S p for each p. When no confusion arises, we write s p for s(p). The initial configuration of A is (s init , χ 0 ) where s init (p) = s init p for each p, and χ 0 (c) = 0 for every c ∈ Ch. We define TS A = (RC A , (s init , χ 0 ), =⇒ A ) where the (possibly infinite) set RC A of reachable configurations and the global transition relation =⇒ A ⊆ RC A × Σ × RC A are the least sets satisfying the following:

• (s init , χ 0 ) ∈ RC A . • Suppose (s, χ) is in RC A and let (s(p), a, s ′ p ) ∈ -→ p such that a = ?c entails χ(c) ≥ 1.
Then (s ′ , χ ′ ) ∈ RC A and ((s, χ), a, (s ′ , χ ′ )) ∈ =⇒ A , where s ′ (p) = s ′ p , s ′ (q) = s(q) for all q = p, and χ ′ is the map defined as follows:

- We define s fi as the global state given by s fi (p) = s fi p for each p. We term (s fi , χ 0 ) as the final configuration.

For a sequence σ = a 1 • • • a n-1 ∈ Σ * and two configurations (s, χ) and (s ′ , χ ′ ), we write (s, χ) σ =⇒ (s ′ , χ ′ ) whenever there exist (s i , χ i ) 1≤i≤n with (s 1 , χ 1 ) = (s, χ), (s n , χ n ) = (s ′ , χ ′ ) and for all 1 ≤ i < n, (s i , χ i ) ai =⇒ (s i+1 , χ i+1 ). We define a run of A as a sequence σ ∈ Σ * such that (s init , χ 0 ) σ =⇒ (s, χ) for some (s, χ) in RC A . We say that σ ends at configuration (s, χ), and denote this configuration by (s σ , χ σ ). We let Run(A) denote the set of runs of A. The run σ is complete iff (s σ , χ σ ) = (s fi , χ 0 ), and we denote by Run cpl (A) the set of complete runs of A.

Through the rest of this section, we fix a system A and we therefore write RC and Run cpl instead of RC A and Run cpl (A). A configuration (s, χ) in RC is valid iff there exists σ such that (s, χ) σ =⇒ (s fi , χ 0 ). A run σ is valid iff it ends at a valid configuration. We say that A is deadend-free iff every configuration in RC is valid. Note that one can effectively decide whether a given system A is deadend-free by an easy reduction to the home marking reachability problem of Petri nets [START_REF] De Frutos-Escrig | Decidability of home states in place transition systems[END_REF].

To illustrate the main concepts, we give an example taken from [START_REF] Kondratyev | Quasi-static scheduling of concurrent specifications[END_REF], slightly modified to fit our context. We consider a cluster consisting of two processes shown in Fig. 1 and Fig. 2. The two processes communicate through the FIFO channel Port. The cluster communicates with the environment, by reading n from channel Start, and by executing the commands GetData() and SendData(). Notice that there is no uniform bound on runs of this system: for all B, there is a run starting by read(Start,n = B + 1) and with B + 1 messages (in transit) in channel Port.

We abstract each round of this cluster as the system of communicating processes shown in Fig. 3. P 1 is started by receiving from the environment an integer n which it reads from buffer Start, and P 2 is started by receiving from P 1 a message which it reads from buffer Port. We abstract away the other communications with the environment. We also abstract away the data x, y, z and n, and their arithmetic handling. The for loop is then replaced with a cycle. Since we do not have FIFO channels (as they would make our model Turing complete), we replace channel Port with two buffers d (counting messages with a data content) and e (counting messages with content "end"). The initial states are A and 1 while D and 2 are final states. The sequence endfor !e ?e is a complete run. The run σ = for !d endfor !e ?e is not complete, even though s σ = (D, 2). For, we have χ σ (d) = 1 = 0. This system is not deadend-free, since the run σ cannot be extended to a complete run.

Schedules

We now define the notion of schedules and schedulability. Let (s, χ) ∈ RC be a reachable configuration of A. The action a ∈ Σ is enabled at (s, χ) iff (s, χ) a =⇒ (s ′ , χ ′ ) for some (s ′ , χ ′ ) in RC . On the other hand, the process p ∈ P is enabled at (s, χ) iff some a ∈ Σ p is enabled at (s, χ). A schedule for A is a partial function Sch from Run to P which satisfies the following conditions: Sch(σ) is defined iff some action a is enabled at (s σ , χ σ ), and if Sch(σ) = p, then p is enabled at (s σ , χ σ ). Notice that if σ is a complete run, then no action is enabled at (s σ , χ σ ) and Sch(σ) is therefore undefined (in notation, Sch(σ) = ǫ). Given a schedule Sch, we denote by Run/Sch the set of runs in agreement with

while(true) { read(Start,n); for i = 1 to n { GetData(x); send(Port,x 2
); } send(Port,"end"); } Sch and we define this set inductively as follows: first, the empty sequence ε ∈ Run/Sch; second, if σ ∈ Run/Sch, Sch(σ) = p, a ∈ Σ p and σa is a run, then σa ∈ Run/Sch. In particular, if Sch(σ) = p and σ can be extended by two alternative actions a, b of process p, then the schedule must allow both a and b. It is easy to check that this definition of a schedule is equivalent to the one given in [START_REF] Cortadella | Quasi-static scheduling of independent tasks for reactive systems[END_REF]. The schedule Sch is valid iff every run in Run/Sch can be extended to a run in Run/Sch ∩ Run cpl . Next we define RC /Sch = {(s σ , χ σ ) | σ ∈ Run/Sch}, the set of configurations reached via runs in agreement with Sch. We say that Sch is regular if RC /Sch is a finite set and Run/Sch is a regular language (in particular, the system under schedule can be implemented with finite memory). Finally, we say that A is quasi-static schedulable (schedulable for short) iff there exists a valid and regular schedule for A. The quasi-static scheduling problem is to determine, given a system A, whether A is schedulable. Again, it is easy to check that this definition of quasi-static schedulability is equivalent to the one given in [START_REF] Cortadella | Quasi-static scheduling of independent tasks for reactive systems[END_REF]. In particular, the validity of the schedule corresponds to the requirement, made in [START_REF] Cortadella | Quasi-static scheduling of independent tasks for reactive systems[END_REF], that the system can always answer a query of the environment (which is guaranteed here by reaching the final configuration).

Let us consider again the task system with two processes P 1, P 2 and two channels c, d presented earlier in this section and shown in Fig. 3. The function Sch 1 (σ) = P defined with P = P 1 if P 1 is enabled at state (s σ , χ σ ), P = P 2 otherwise, is a schedule. However, this schedule is not regular, since for all m, (for !d) m ∈ Run/Sch 1 reaches a configuration with m messages sent in the channel d, implying that this channel is not bounded. On the other hand, the function Sch 2 (σ) = P defined with P = P 2 if P 2 is enabled at state (s σ , χ σ ), P = P 1 otherwise is a valid and regular schedule. Fig. 4 shows the finite state space RC /Sch 2 which contains no deadends. In this figure, a configuration is described in the form XY αβ, where X (Y ) is the state of P 2 (P 1), and α, β denote the contents of buffer d, e respectively. Thus the system of Fig. 3 is schedulable. Notice that a valid schedule does not need to prevent infinite runs. It just must allow every run to be completed for some sequence of inputs and / or choices.

General Case and Undecidability

The goal of this section is to establish the following result.

Theorem 1. The quasi-static scheduling problem is undecidable. Moreover, this problem remains undecidable for the sub-class of systems without deadends.

Our proof consists in showing that the halting problem for deterministic twocounter machines can be uniformly reduced to the quasi-static scheduling problem. Specifically, given a deterministic two counter machine M, we shall construct a system A such that M halts iff A is schedulable. Following a standard technique used by numerous authors, some runs of A will not correspond to any run of M. Hence A will not faithfully simulate M. However such runs will be unbounded or lead to deadends, and these runs shall be avoided by the scheduler.

To ease the understanding, we shall present the construction of A in three phases and prove in each case that M halts iff A is schedulable. In the first phase, our goal is to bring out the main ingredients of the construction of A with a minimal amount of technical details. Thus, we shall allow transitions of A to deviate from the definition of systems given in Section 2. In the second phase, we modify the transitions of A given in the first phase, so that they strictly adhere to the definition of systems in Section 2. In the first and second phase, A needs not be deadend-free. In the third phase, we show that the system A constructed in the second phase can be modified to become deadend-free while strictly adhering to the definition of systems in Section 2, establishing thus the second part of the theorem.

In the first two phases A will enjoy the following two properties: first, if Sch is a valid schedule for A, then the execution of A under the schedule Sch simulates the execution of M; second, if Sch leads A to its final configuration, then the corresponding execution of M reaches the halting state. We will show that whenever M halts, there exists a valid schedule Sch that leads A to its final configuration in a finite number of steps, hence it is a valid and regular schedule and A turns out to be schedulable. We will show on the other hand that, if M does not halt, then A does not even have a valid schedule.

We now give a sketch of the coding of M by A. Let C 1 , C 2 denote the two counters of M. Let halt denote the halting state of M. We assume that, for each control state i other than halt , the behaviour of M at i is given by an instruction in one of the following forms, with j ∈ {1, 2}:

• (i, Inc(j), k): "increment C j and move to control state k".

• (i, Dec(j), k, m): "if C j > 0, then decrement C j and move to control state k; otherwise (C j = 0), move to control state m".

Thus, M either stops at halt after a finite number of steps, or runs forever without visiting halt . Naturally, we encode counters of M by buffers of A. Incrementing a counter of M amounts to sending a data item to the corresponding buffer, and decrementing a counter of M amounts to picking up a data item from the corresponding buffer. It is clear how the instruction (i, Inc(j), k) of M can be simulated. The main difficulty is to simulate the instruction (i, Dec(j), k, m). Indeed, in a system, a process can not branch to different states according to whether a buffer is empty or not. Further, when a schedule Sch selects a process p to execute, Sch has to allow all transitions of p that are enabled at the current state s p of p. However, the following observation will facilitate the simulation of an (i, Dec(j), k, m) instruction. Suppose s p is a polling state with two outgoing transitions labelled ?a, ?b, where src(a) = src(b). If, prior to selecting p, and assuming both buffers a and b are currently empty, Sch can make the buffer a nonempty (for example, by selecting src(a) to send a data item to a) while keeping b empty (for example, by not selecting src(b)), then when Sch selects p, only the ?a transition is enabled and executed, while the ?b transition is ignored.

After these explanations, we enter now the technical part of the proof of Thm. 1.

-Phase (i): Here we construct a system A whose transitions slightly deviate from the definition of systems in Section 2. In particular, we allow a final state to be not a polling state and permit the outgoing transitions of a local state to be both receive transitions and choice transitions.

The system A has five processes A, C(1), C(2), GD, GZ . Their communication architecture is illustrated in Fig. 5 where a label ch on an arrow from process p to process q represents a buffer ch with src(ch) = p and dst(ch) = q. For j = 1, 2, the number of items stored in buffer c(j) encodes the value of counter C j of M. Process A mimics the instructions of M. For instructions of the form (i, Inc(j), k), A invokes C(j) to increment c(j) by sending message

C(1) C(2) GD GZ A c(1),inc-ok(1) c(2),inc-ok(2) inc(1) inc(2)
gd gz !inc(j). For instructions of the form (i, Dec(j), k, m), A accepts to receive from both channel gd ("Guess Dec") or gz ("Guess Zero"). The valid schedule can correctly simulate the emptiness test of buffer c(j) by feeding the right channel gd or gz according to the contents of c(j). Fig. 6 displays the transition systems of GD, GZ , and C(j), j = 1, 2, where an initial state is indicated by a pointing arrow, and a final state is drawn as a double circle. Fig. 7 illustrates the transition system of A. For each (i, Inc(j), k) instruction of M, A contains the states and transitions shown in Fig. 7(i). For each (i, Dec(j), k, m) instruction of M, A contains the states and transitions shown in Fig. 7(ii), where sink is a distinguished state with no outgoing transitions. Unlabelled transitions have implicit labels in Σ cho . For the halting state of M, A contains two special transitions, shown in Fig. 7(iii), whose purpose is to empty the buffers c(1), c(2) after A has reached halt for the first time. The initial state of A is the initial state of M, and the final state of A is halt .

Let Sch be a valid schedule for A. Suppose that, according to Sch, the execution of the system A arrives at a configuration in which process A is at state i. There are two cases to consider: -Case (i): The corresponding instruction of M is (i, Inc(j), k).

It is easy to see that Sch has no choice but selecting A to execute !inc(j), then selecting C(j) three times in a row to execute ?inc(j), !c(j), !inc-ok (j), and finally selecting A to execute ?inc-ok (j). In doing so, c(j) is incremented and A moves to state k.

!inc(j) ?inc-ok(j) ?gd ?gz k m sink i halt ?c(2) ?c(j) ?c(j) ?c(1) (i) (ii) (iii) i k
-Case (ii): The corresponding instruction of M is (i, Dec(j), k, m).

Note that from state i of A, there are two outgoing transitions labelled ?gd, ?gz respectively. Consider first the case where c(j) is greater than zero. We argue that Sch has to guide A to execute only the transition ?gd in order to be valid. That is, Sch should ensure that the ?gd transition of A is enabled by selecting GD. Sch must further ensure that the ?gz transition of A is not enabled which it can do by not scheduling the process GZ . By doing so, c(j) will be decremented and A will move to state k. If on the contrary, Sch did schedule process GZ and thus enable ?gz while c(j) is greater than zero, then Sch would allow A to take the ?gz transition. Consequently, Sch would allow A to reach state m, as well as state sink . However, as sink has no outgoing transitions, the run which leads A to sink is not valid. This contradicts the hypothesis that Sch is valid. Consider now the case where c(j) is zero. Then it is easy to see that Sch has to guide A to execute only the transition ?gz. Further, after executing ?gz, A can move to state m only, since the corresponding ?c(j) transition is not enabled. Altogether, we have shown that if Sch is a valid schedule, then under this schedule, A simulates correctly M.

We claim now that M halts iff A is schedulable. To see this, suppose M halts. Then M may clearly be simulated by executing A under some valid schedule Sch that leads A to the configuration in which each process is at its final state, thus in particular A is in state halt , and all buffers except possibly c(1), c(2) are empty. In view of Fig. 7(iii) and the validity of Sch, process A will eventually also empty c(1), c(2). Moreover, it follows also from the finiteness of the run of A that Sch is regular, hence A is schedulable. Suppose now that M does not halt. Assume that Sch is a valid schedule for A. Then as explained above, Sch simulates the execution of M and thus process A can never reach its final state halt . Thus Sch is not valid, a contradiction.

-End of Phase (i)

-Phase (ii): In this phase, we modify the transitions defined for A in Phase (i) so that they strictly adhere to the definition of system in Section 2. Firstly, we change the communication architecture between the processes of A. The new architecture is displayed in Fig. 8. The transitions of GD, GZ

C(1) C(2) GZ GD A c(1),inc-ok(1) c(2),inc-ok(2) inc(1) inc (2)
gz,gz-ok make-gz gd make-gd and processes C(j), j = 1, 2, are shown in Fig. 9. Note that the final states of processes GD, GZ are now polling states. For j = 1, 2, process C(j) is constructed in the same way as in Phase (i). The state space of A is depicted in Fig. 10. For each (i, Inc(j), k) instruction of M, A contains the transitions shown in Fig. 10(i). For each (i, Dec(j), k, m) instruction of M, A contains the transitions shown in Fig. 10(ii), where sink is a distinguished state with no outgoing transitions. As in Phase (i), for the halting state of M, A contains two special transitions, shown in Fig. 10(iii). It is clear that the transitions of A now strictly adhere to the definition of systems in Section 2.

Let Sch be a valid schedule for A. As in Phase (i), we show that Sch guides A to simulate correctly the execution of M. The simulation of an (i, Inc(j), k) instruction is as in Phase (i). Now suppose that, according to Sch, the execution of the system A arrives at a configuration in which A is at state i, the corresponding instruction of M is (i, Dec(j), k, m), and each of processes GD, GZ is at its initial state. Then it is not difficult to see that Sch must first select process A twice in a row to execute !make-gd, !make-gz transitions, and thus GD, GZ become enabled. Next, suppose c(j) is greater than zero. Then as in Phase (i), Sch has to guide A to execute only the transition ?gd, and eventually, c(j) is decremented, A moves to state k, and GD, GZ return to their initial states. Now suppose that c(j) is zero, then Sch has to guide A to execute only the transition ?gz, and eventually, c(j) remains zero, A moves to state m, and GD, GZ return to their initial states.

With the observation that any valid schedule Sch guides A to simulate the execution of M, it follows from similar arguments as in Phase (i) that M halts iff A is schedulable.

-End of Phase (ii)

-Phase (iii): Finally, we modify the construction of the system A defined in Phase (ii) so that it becomes deadend-free and still, any valid and regular schedule for A simulates the execution of M. One can then show that M halts iff A is schedulable. We first explain the final construction of A, then argue that M halts iff A is schedulable, and last show that A is deadend-free. The communication architecture of A is now as shown in Fig. 11. The transitions of GD, GZ and processes C(j), j = 1, 2, are displayed in Fig. 12. The transitions of A are depicted in Fig. 13. For each (i, Inc(j), k) instruction of M, A contains the transitions shown in Fig. 13(i). For each (i, Dec(j), k, m) instruction of M, A contains the transitions shown in Fig. 13(ii), where sink is a distinguished state, present also in Fig. 13(iii). For the states sink and halt , A contains the special transitions shown in Fig. 13(iii) (where unlabelled arrows bear implicit labels in Σ cho ).

We first note that the special transitions in Fig. 13(iii) are designed in such a way that any valid and regular schedule cannot lead A to a configuration in which process A is at the state sink . To see this, suppose Sch is a valid and regular schedule for A. Assume further that according to Sch, A arrives at a configuration in which process A is at the state sink . Recall that Sch can not discrim-

C(1) C(2) GZ GD A c(1),inc-ok(1) c(2),inc-ok(2) inc(1) inc (2)
gz,gz-ok make-gz make-gd gd,gd-wrong inate between the two outgoing transitions of sink which are (data-dependent) choice transitions. Thus, Sch has to allow runs in which the transitions !inc(1), ?inc-ok(1) of Fig. 13(iii) are executed arbitarily many times, in tight interleaving with corresponding transitions ?inc(1), !c(1), !inc-ok(1) from C(1). Thus, Sch allows complete runs in which A is arbitrarily often at state sink and the size of c(1) can be arbitarily large. Consequently, Sch is not regular, a contradiction.

By the above observation that any valid and regular schedule for A drives A so as to avoid visiting sink , similar arguments as in Phase (ii) may be used to show that any valid and regular schedule for A guides A to simulate correctly the execution of M. Now, as in Phase (i), if M halts, then one can construct a valid and regular schedule which leads A to the configuration in which each process is at its final state, thus in particular A is in state halt , and all buffers except possibly c(1), c(2) are empty. Further, during the execution of A under Sch, A never visits state sink . With the special transitions shown in Fig. 13(iii), A will eventually also empty buffers c(1), c(2) under the schedule Sch. Thus A is schedulable. On the other hand, if M does not halt, then under any valid schedule of A, process A must nevertheless reach the halt state and hence visit the sink state, and therefore A does not have any valid and regular schedule. We have thus shown that M halts iff A is schedulable.

Finally, we show that the system A constructed in this final phase is deadendfree. We assume that from any control state i of M except the halting state, it is always possible to reach a control state t with a corresponding instruction of the form (t, Dec(j), k, m). This assumption can be made without any loss of generality, since one may always replace each (i, Inc(j), k) instruction by an equivalent sequence of three instructions (i, Inc(j), i ′ ), (i ′ , Inc(j), i ′′ ), (i ′′ , Dec(j), k, k) where i ′ ,i ′′ are new control states with i ′ = i ′′ .

To prove that A is deadend-free, we need to show that every run σ of the unscheduled system A can be extended to a complete run. We proceed by cases according to whether M halts or not, and in each case we consider two types of runs of A (notice that runs which are neither of type I or II are not schedulable):

Type I: Runs which simulate the execution of M so that A never visits state sink .

Type II: Runs which end at the configuration in which A is at state sink , every other process is at its initial state, and all buffers except possibly c(1), c(2) are empty.

-Case (i): M halts.

Let σ be a run of A. If σ is of type I, then in this run, process A reaches the state halt without going through the state sink , and by scheduling process A until c(1) and c(2) are empty, σ can be extended to a complete run of A. If σ is of type II, then σ can be extended to a run ending at the configuration in which A is at state halt , every other process is at its initial state, and all buffers except possibly c(1), c(2) are empty. The run σ can therefore be extended to a complete run in which process A is scheduled finally until these two buffers are also empty.

-Case (ii): M does not halt.

Let σ be a run of A. First consider the case where σ is of type I. As said above, we can assume that from any control state i of M except the halting state, it is always possible to reach a control state î whose corresponding instruction has the form (î, Dec(j), k, m). Thus, σ can certainly be extended to a run σ ′ that ends at a configuration in which A is at some state i and the corresponding instruction of M is of the form (i, Dec(j), k, m). In view of Fig. 13(ii), σ ′ can be extended further to a run σ ′′ that ends at a configuration in which A is at state sink . In view of Fig. 13(iii), σ ′′ can be extended in turn to a complete run.

For the case where σ is of type II, the same arguments as in case (i) show that σ can be extended to a complete run.

-End of Phase (iii)

With the construction of a deadend-free system A such that M halts iff A is schedulable, we have completed the proof of Thm. 1.

Data-Branching and Decidability.

The ability of a schedule to bias the choice between two receive actions (e.g. ?gd and ?gz) of the same process is crucial to our undecidability proof. This observation leads us to consider a restricted class of systems as follows.

A system A is data-branching if for each process p and for each state s p ∈ S p , if s p is a polling state, then it has exactly one outgoing transition. Thus the only branching states are those at which internal (data-dependent) choices take place. For instance, the task system shown in Fig. 3 is not data branching, since process P 2 chooses between receiving from channels d or e in state 1. However, an implementation of this system depicted in Fig. 14 is data-branching. More generaly, Kahn process networks that have a terminating semantics and in which numerical data has been abstracted away, are data-branching. This implies for such a class of restricted Kahn networks, that QSS is decidable. A similar property does not hold for the YAPI extension of Kahn networks considered in [START_REF] Cortadella | Quasi-static scheduling of independent tasks for reactive systems[END_REF].

The question arises whether the quasi-static scheduling problem for databranching systems is decidable. We show that the answer is yes. This result subsumes the similar result obtained in [START_REF] Sgroi | Quasi-Static Scheduling of Embedded Software Using Equal Conflict Nets[END_REF] for systems without loops.

Theorem 2. Given a data-branching system A, one can effectively decide whether

A is schedulable.

The rest of this section is devoted to the proof of Thm. 2. We assume throughout that A is data-branching. The proof relies crucially on the notion of a canonical schedule for A, denoted Sch ca . The canonical schedule is positional (also called memoryless in the literatute), that is, Sch ca (σ) = Sch ca (σ ′ ) whenever runs σ,σ ′ end at the same configuration. Thus, we consider Sch ca as a function from RC to P. Informally, at configuration (s, χ), if there is a p ∈ P such that p is enabled and s p is a polling or choice state, then Sch ca picks one such p. If there is no such process, then for each process p enabled at (s, χ), s p has exactly one outgoing transition (s p , !c p , s ′ p ). In this case, Sch ca picks a process p with χ(c p ) being minimal. Ties will be broken by fixing a linear ordering on P. The proof of Thm. 2 consists of two steps. Firstly, we show that A is schedulable iff Sch ca is a valid and regular schedule (Prop. 1). Secondly, we prove that one can effectively decide whether Sch ca is a valid and regular schedule (Thm. 4).

The Canonical Schedule.

We fix a total order ≤ P on P and define the canonical schedule Sch ca for A as follows. For each configuration (s, χ), let P (s,χ) enable ⊆ P be the set of processes enabled at (s, χ). We partition P (s,χ) send -min iff χ(c p ) ≤ χ(c q ) for each q ∈ P (s,χ) send , where !c p (respectively, !c q ) is the action of p (respectively, of q) enabled at (s, χ).

enable into P (s,
The canonical schedule Sch ca maps each configuration (s, χ) to the process Sch ca (s, χ) as follows. If P (s,χ)

poll ∪ P (s,χ) choice = ∅, then Sch ca (s, χ) is the least member of P (s,χ) poll ∪ P (s,χ)
choice with respect to ≤ P . Otherwise, Sch ca (s, χ) is the least member of P (s,χ) send -min with respect to ≤ P . It is straightforward to verify that Sch ca adheres to the definition of schedules. We say that a schedule Sch ′ is optimal if for every run σ in Run/Sch ′ , every channel c, and every schedule Sch, there exists a run τ ∈ Run/Sch and a channel d with χ σ (c) ≤ χ τ (d).

Proposition 1. A data-branching system A is schedulable iff Sch ca is a valid and regular schedule for A. Furthermore, Sch ca is optimal.

To facilitate the proof of Prop. 1, we introduce now an equivalence on complete runs. For σ ∈ Σ ⋆ and p ∈ P, let prj p (σ) be the sequence obtained from σ by erasing letters not in Σ p . We define the equivalence relation ∼ ⊆ Run cpl × Run cpl as follows: σ ∼ σ ′ iff for every p ∈ P, prj p (σ) = prj p (σ ′ ). We observe a useful relation between ∼ and schedules. Lemma 1. Let σ be a complete run of a data-branching system A. Suppose that Sch is a schedule of A (not necessarily valid nor regular). Then there exists a complete run σ ′ such that σ ′ ∼ σ and σ ′ ∈ Run/Sch. Proof. Let σ = τ aτ ′ , with a ∈ Σ p , τ ∈ Run/Sch, and Sch(τ ) = q = p. In particular, τ a / ∈ Run/Sch and q is enabled at (s τ , χ τ ). We show that there exists a complete run w of the form τ bτ ′′ with b ∈ Σ q (thus τ b is in agreement with Sch) and w ∼ σ. Repeating inductively this argument yields eventually the desired complete run σ ′ in agreement with Sch such that σ ′ ∼ σ. all p, prj p (σ) is a prefix of prj p (ρ), and thus that σ can be extended to some complete run ρ ′ ∼ ρ.

Assume by contradiction that σ ′ = σ, and let σ = σ ′ aσ ′′ . Let q ∈ P with a ∈ Σ q . By definition of the algorithm, prj q (σ ′ ) = prj q (ρ). As ρ is complete, the state s σ ′ q reached on process q after doing σ ′ is a final state, and in particular it is polling. As σ ′ a is a run, a =?c for some channel c with dst (c) = q. Let src(c) = p. For each letter b ∈ Σ and run ω, let # b (ω) denote the number of occurrences of letter b in sequence ω. As prj p (σ ′ ) is a prefix of prj p (ρ), we have

# !c (σ ′ ) ≤ # !c (ρ). As ρ is complete, # !c (ρ) = # ?c (ρ). As prj q (σ ′ ) = prj q (ρ), we have # ?c (ρ) = # ?c (σ ′ ). Combining them, we get # !c (σ ′ ) ≤ # ?c (σ ′ ). It means that # !c (σ ′ a) < # ?c (σ ′ a) as a =?c. Since σ ′ a is a run, # !c (σ ′ a) ≥ # ?c (σ ′ a), a contradiction.
2 Using Lemmas 1 and 2, it is easy to show that if there exists a valid schedule Sch, then the canonical schedule Sch ca is valid too. Lemma 3. A data-branching system A admits some valid schedule iff Sch ca is valid for A.

Proof.

It suffices to consider the "only if" direction. Let Sch be a valid schedule for A, and let σ be any run in Run/Sch ca . By Lemma 2, there exists a continuation τ such that στ ∈ Run cpl . By Observation 3, σ may be extended to a run in Run cpl ∩ (Run/Sch ca ), hence the canonical schedule is valid.

2 The concept of an anchored run, that we introduce now will also play a crucial role in what follows. If χ is a mapping from Ch to the non-negative integers, let max(χ) = max{χ(c) | c ∈ Ch}. For a run σ, we define the height max(σ) of the run σ by max(σ) = max{max(χ σ ′ ) | σ ′ is a prefix of σ}. We say that σ is an anchored run iff σ is non-empty and denoting σ = σ ′ a with a ∈ Σ, max(σ) > max(σ ′ ). That is, a run is anchored if the height of the run has just been strictly increased. Anchored runs in agreement with Sch ca have a special property: every action enabled concurrently with the last action of an anchored run is a send action on some buffer that holds a maximum number of items. This property may be stated precisely as follows.

Lemma 4. Let σ be an anchored run according to Sch ca , and let M = max(σ). Then σ = σ!c for some c ∈ Ch and χ σ (c) = M . Further, if a ∈ Σ is enabled at (s σ , χ σ ), then a =!d for some d ∈ Ch and moreover χ σ(d) = M -1. In particular, χ σ (c) = M -1.

We are now ready to prove Prop. 1. Proof. of Prop. 1 The if part is obvious. As for the only if part, let Sch be a valid and regular schedule for A. First, it follows from Lemma 3 that Sch ca is valid.

We prove that Sch ca is regular. We know that RC/Sch contains a finite number k of configurations. Since each action adds at most one item to one buffer, for all σ ∈ Run/Sch, max(σ) ≤ k. We will prove that for all σ ca ∈ Run/Sch ca , max(σ ca ) ≤ max(σ) ≤ k, which will imply that RC/Sch ca has a finite number of configurations. It also implies that Sch ca is optimal. Since we know that Sch ca is valid, it suffices to consider only complete runs in Run/Sch ca .

Let σ ca ∈ Run/Sch ca be a complete run. Relying on Lemma 1, let σ ∈ Run/Sch be a complete run such that σ ∼ σ ca . Suppose M ca = max(σ ca ) and M = max(σ). Pick the least prefix τ ca of σ ca such that τ ca = M ca . Thus τ ca is anchored. By Lemma 4, let τ ca = τca !c. Consider the sequence τca . For a run τ ∈ Run, we say τ is covered by τca iff for every p ∈ P, the projection prj p (τ ) of τ on (Σ p ) * is a prefix of prj p (τ ca ). Now pick τ as the least prefix of σ such that τ is not covered by τca . Such a τ exists, following the definition of ∼. Let τ = τ a where a ∈ Σ is the last letter of τ . Let p a = p such that a ∈ Σ p . We consider three cases.

-Case (i) a = !d for some d ∈ Ch.

The choice of τ implies prj pa (τ ) = prj pa (τ ca ). Thus, s τ (p a ) = s τca (p a ). And !d is enabled at configuration (s τca , χ τca ). It follows from Lemma 4 that χ τca (d) = M ca -1 (whether d = c or not). As dst(d) = p a , the choice of τ also implies prj dst (d) (τ ) is a prefix of prj dst(d) (τ ca ). Hence, we have # !d (τ ) = # !d (τ ca ) and # ?d (τ ) ≤ # ?d (τ ca ). It follows that χ τ (d) ≥ χ τca (d). Combining these observations with χ τ (d) ≤ M -1 then yields M ca ≤ M .

-Case (ii): a = ?d for some d ∈ Ch.

By the same argument as in case (i), we have s τ (p a ) = s τca (p a ). Also we have prj pa (τ ) = prj pa (τ ca ), and prj src(d) (τ ) is a prefix of prj src(d) (τ ca ). Hence, χ τ (d) ≤ χ τca . It follows that ?d is enabled at configuration (s τca , χ τca ). This contradicts that at configuration (s τca , χ τca ), the schedule Sch ca picks process src(c) with s τca (src(c)) being a sending state.

-Case (iii): a ∈ Σ cho pa . Similar to Case (ii), we obtain a contradiction by noting that a is enabled at (s τca , χ τca ). 2

Deciding Boundedness of the Canonical Schedule.

The decision procedure for the boundedness of Sch ca is similar to the decision procedure for the boundedness of Petri nets [START_REF] Karp | Parallel Program Schemata[END_REF]. We now briefly recall the outline of the classical algorithm defined in [START_REF] Karp | Parallel Program Schemata[END_REF]. First, an order ⊑ on runs is defined, such that σ ⊑ σ ′ if the following conditions hold:

• σ is a strict prefix of σ ′ .

• s σ (p) = s σ′ (p) for every p ∈ P.

• χ σ (d) ≤ χ σ ′ (d) for each d ∈ Ch.
For two runs σ, σ ′ , define σ ≡ σ ′ if (s σ , χ σ ) = (s σ ′ , χ σ ′ ), that is if both runs end at the same configuration. First, [START_REF] Karp | Parallel Program Schemata[END_REF] shows that ⊑ ∪ ≡ is a well quasi order, which implies by König's lemma that the tree of runs built inductively by extending every run σ ′ by one step unless (σ, σ ′ ) ∈ (⊑ ∪ ≡) for some run σ already present, is finite. Second, [START_REF] Karp | Parallel Program Schemata[END_REF] shows that σ ⊑ σ ′ witnesses for the unboundedness of the system. Intuitively, when σ ⊑ σ ′ and σ ′ = στ , one can iterate τ to increase at least one buffer beyond any bound.

Notice that one cannot apply directly the classical algorithm defined in [START_REF] Karp | Parallel Program Schemata[END_REF] to check the boundedness of the canonical schedule, because RC/Sch ca cannot be represented as the set of reachable markings of a Petri net. Indeed, the canonical schedule performs a zero-test when it schedules a process ready to send, because it must check that all processes ready to receive have empty input buffers. We show that one can nevertheless define a quasi order ≺ ca on runs, and build a finite tree in the same way as in [START_REF] Karp | Parallel Program Schemata[END_REF] (Proposition 2), such that σ ≺ ca σ ′ for two runs σ, σ ′ in this tree iff RC/Sch ca is not a finite set or Sch ca is not a valid schedule for A (Proposition 3).

More precisely, let the quasi order ≺ ca be defined such that σ ≺ ca σ ′ iff σ ⊑ σ ′ , both σ, σ ′ are anchored (in particular they are non empty), and both runs end with the same action, that is σ = σ!c, σ ′ = σ′ !c for some c ∈ Ch. The general intuition is as follows. If σ ≺ ca σ ′ and σ ′ = στ , then for any n, even though the anchored run σ(τ ) n is not necessarily in agreement with the canonical schedule, there exists a continuation w n such that σ(τ ) n w n ∈ Run cpl and σ(τ ) n w n ∼ ρ n for some run ρ n ∈ Run/Sch ca with height max(ρ n ) at least equal to max(σ(τ ) n ), and hence larger than n.

Notice that for σ ≺ ca σ ′ , in particular, χ σ (c) < χ σ ′ (c) since σ is a strict prefix of σ ′ and both are anchored. We show now a structural property of ≺ ca which will serve us to produce a finite coverability tree of all runs. An infinite run of A is an infinite sequence ρ in Σ ω such that every finite prefix of ρ is in Run(A). We say that an infinite run ρ agrees with Sch ca iff every finite prefix of ρ agrees with Sch ca . Proposition 2. Let ρ ∈ Σ ω be an infinite run in agreement with Sch ca . Then there exist two finite prefixes σ,σ ′ of ρ such that either σ, σ ′ end at the same configuration, or σ ≺ ca σ ′ (in which case σ, σ ′ are both anchored).

Proof. If there exists k ∈ N such that for all prefixes α of ρ, max(χ α ) ≤ k, then there is only a finite number of possible configurations reached during ρ, hence we can find two prefixes of ρ ending at the same configuration. Otherwise, max(χ α ) is unbounded, and one can extract from ρ an infinite subsequence of anchored prefixes. Since there is a finite number of buffers and a finite number of tuples of local states in Π p∈P (S p ), one can extract from ρ an infinite subsequence of anchored prefixes with the same maximal channel c ∈ Ch and the same tuple of local states s ∈ Π p∈P (S p ).

By an inductive argument on i ≤ |Ch|, one easily verifies that there exists an infinite subsequence of anchored prefixes α 0 , α 1 , • • • of ρ, such that χ α0 (c j ) ≤ χ α1 (c j ) ≤ . . . for every index 1 ≤ j ≤ i. In particular, this shows the existence of prefixes σ, σ ′ of ρ such that σ ≺ ca σ ′ .

2 Next we show that any pair of runs σ, σ ′ in Run/Sch ca such that σ ≺ ca σ ′ witnesses for the unboundedness of RC/Sch ca (or for the non-validity of Sch ca ). This requires a new argument not in [START_REF] Karp | Parallel Program Schemata[END_REF] because, even though σ ′ = στ and both σ, σ ′ agree with Sch ca , the run στ n may disagree with Sch ca for some n.

-Case (iii). b ∈ Σ cho p b . As in Case (ii), we derive a contradiction by noting that p b is enabled at (s σ , χ σ), becauses s α(p b ) = s β (p b ).

2 The set of all runs of a data-branching system under the canonical schedule Sch ca forms a possibly infinite tree (in which any data dependent choice performed by a scheduled process induces several branches). Following Karp and Miller's ideas, one may stop exploring this tree whenever coming again to a configuration already visited within some run in the tree, or reaching an anchored run σ ′ that extends a smaller anchored run σ, i.e. σ ≺ ca σ ′ . Based on this construction of a finite coverability tree, we obtain the following theorem.

Theorem 4. One can effectively determine whether Sch ca is valid and regular.

Proof. We construct inductively as follows a tree W of valid runs in agreement with Sch ca . First, ε is in W . Then, suppose that σ is in W and σa is a run in agreement with Sch ca , with a ∈ Σ. If there exists σ ′ ∈ W such that σ ′ ≺ ca σa, then we can stop the construction of W and report that either Sch ca is not regular or Sch ca is not valid, based on Prop. 3. Otherwise, we check whether there exists τ ∈ W such that τ ends at the same configuration as σa. If such a τ does not exist, then we add σa to W (otherwise we just ignore σa).

We first prove that the construction of W stops after a finite number of steps. Suppose otherwise. Then the runs in W form an infinite tree. By König's lemma, there exists an infinite sequence ρ of Σ ω such that every finite prefix of ρ is in W . Applying Prop. 2, we get that there exist two finite prefixes σ,σ ′ of ρ such that σ is a prefix of σ ′ and either σ, σ ′ end at the same configuration or σ ≺ ca σ ′ . In both cases, the construction of W is stopped after σ ′ , hence ρ is not an infinite path, a contradiction.

If the construction of W is completed without finding any two anchored runs such that σ ≺ ca σ ′ (and then reporting that Sch ca is not regular or that Sch ca is not valid), then {(s σ , χ σ ) | σ ∈ W } is exactly the set of configurations of Sch ca (RC), hence RC/Sch ca is a finite set, and we can test whether Sch ca is valid by inspecting the finite graph formed of all transitions (s σ , χ σ ) a → (s σa , χ σa ) in this set.

2 Thm. 2 is now settled by applying Prop. 1 and Thm. 4. Concerning complexity, we rely on coverability techniques which have a non primitive recursive complexity [START_REF] Karp | Parallel Program Schemata[END_REF] if the order in which paths are explored is not chosen with care. For Petri Nets, [START_REF] Rackoff | The Covering and Boundedness Problems for Vector Addition Systems[END_REF] explains that if the Karp and Miller tree is generated by exploring paths with the lowest height first, the complexity decreases to doubly exponential time, almost matching the lower bound of [START_REF] Lipton | The Reachability Problem Requires Exponential Space[END_REF]. We would need to analyze this or other orders on the paths of our coverability tree to try to obtain elementary complexity. Notice that we cannot even get a lower bound complexity because our systems are not equivalent with Petri Nets.

Algorithm run on an example

To illustrate the construction given in the proof of Thm. 4, we consider the data-branching system in Fig. 14 and display in Fig. 15 the corresponding tree W constructed in Thm. 4 (for saving space, we contracted while,endfor and endwh as whl,endf and endw). In Fig. 15, the root is indicated by a pointing arrow and each node may be identified by the sequence of labels on the incoming path. We label each node σ with the configuration at which σ ends, and we let the notation ij kl represent the configuration in which process P 2 is at state i, P 1 is at state j and buffers d,e have respective sizes k,l. A dotted arrow represents a jump to a node already constructed.

Sch ca succeeds to reach the final state 4D00 through the path (for while !d endfor ?d endwh !e ?e) but two deadend states 2D 01 and 4D 10 may also be reached. This means that Sch ca is not valid, hence by Prop. 1, no valid schedule exists for A. Moreover, (for endwh !d) ≺ ca (for endwh !d for !d). The algorithm thus stops at the configuration 3A 20 reached by (for endwh !d for !d), and depicted by a double circle. This means that the canonical schedule is not regular, and by Prop. 1, no regular and valid schedule exists for A. Notice that the runs (for endwh) and (for while) are not anchored, hence we do not have (for endwh ) ≺ ca (for endwh !d for). Recall that the model A is only an over-approximation of the real task system depicted in Fig. 3. That is, even though we have a proof that A is not schedulable, this does not imply that the real system shown on Fig. 3 is not schedulable.

The algorithm produces counterexample runs (here, we have two runs for deadends and one for unboundedness). One can try to check whether these problematic runs represent actual runs of the original (not abstracted) system or whether they are spurious runs resulting from the abstractions. If all the counterexample runs are spurious, then the real system is in fact schedulable.

Discussion

In this paper, we have considered quasi-static scheduling as introduced in [START_REF] Cortadella | Quasi-static scheduling of independent tasks for reactive systems[END_REF] and have provided a negative answer to an open question posed in [START_REF] Kondratyev | Quasi-static scheduling of concurrent specifications[END_REF]. Specifically we have shown that for the chosen class of infinite state systems, checking whether a system is quasi-static schedulable is undecidable. We have then identified the data-branching restriction, and proved that the quasi-static scheduling problem is decidable for data-branching systems. Further, our proof constructs both the schedule and the finite state behaviour of the system under schedule. An important concept used in the proof is the canonical schedule that draws much inspiration from the study of existential bounds on channels of communicating systems [START_REF] Genest | On Communicating Automata with Bounded Channels[END_REF]. In the language of [START_REF] Genest | On Communicating Automata with Bounded Channels[END_REF], our result can be rephrased as: it is decidable whether a weak FIFO data branching communicating system is existentially bounded, when all its local final states are polling states. We recall that the same problem is undecidable [START_REF] Genest | On Communicating Automata with Bounded Channels[END_REF] for strong FIFO communicating systems, even if they are deterministic and deadend free. Our abstraction policy is similar to the one used in [START_REF] Leue | A Scalable Incomplete Test for the Boundedness of UML RT Models[END_REF]. However, we use existential boundedness while [START_REF] Leue | A Scalable Incomplete Test for the Boundedness of UML RT Models[END_REF] checks whether a communicating system is universally bounded, which is an easier notion to check. Note that the canonical schedule may be easily realized in any practical context: it suffices to prevent any process from sending to a buffer that already contains the maximum number of items determined from that schedule. It is also worth recalling that these bounds are optimal (Prop. 1).

Deadends play an important role in the notion of quasi-static schedulability studied here and previously. However, quasi-static scheduling may stumble on spurious deadends due to the modelling of the task by an abstract system. The algorithm we have sketched for constructing the canonical schedule may be combined with an iterative removal of spurious deadends. A more ambitious extension is to design distributed quasi-static schedulers for inter cluster communication, where the scheduler cannot have global knowledge of each process.

  If a =!c, then χ ′ (c) = χ(c) + 1 and χ ′ (d) = χ(d) for all d = c. -If a =?c, then χ ′ (c) = χ(c) -1 and χ ′ (d) = χ(d) for all d = c. -If a ∈ Σ cho p , then χ ′ (c) = χ(c) for all c ∈ Ch.

Figure 1 :

 1 Figure 1: Process 1 of the cluster

Figure 2 : 2 Figure 3 :

 223 Figure 2: Process 2 of the cluster

Figure 4 :

 4 Figure 4: The system under schedule RC /Sch 2 .

Figure 5 :Figure 6 :

 56 Figure 5: The architecture of A

Figure 7 :

 7 Figure 7: Transitions of process A

Figure 8 :Figure 9 :

 89 Figure 8: The architecture of A in Phase (ii)

Figure 10 :

 10 Figure 10: Transitions of process A in Phase (ii)

Figure 11 :Figure 12 :

 1112 Figure 11: The architecture of A in Phase (iii)

Figure 13 :

 13 Figure 13: Transitions of process A in Phase (iii)

2 Figure 14 :

 214 Figure 14: A data-branching system.

Figure 15 :

 15 Figure 15: The tree W in Thm. 4 for the system in Fig. 14.

Acknowledgement:We would like to thank the reviewers for making constructive comments helping us to improve the readability of the paper.

 [START_REF] Brand | On Communicating Finite-State Machines[END_REF]Work done as part of the Associated Team DST. 2 Work supported by the ANR-SETI-06 DOTS. 3 Work supported by the Region Bretagne project CREATE ActiveDoc. 4 Also affiliated with IRISA/CNRS. 5 Work done while being affiliated with IRISA/INRIA.

Note that, by the completeness of the run σ, s σ q is the final state of q. It thus follows from the definition of a task system that, either s σ q has no outgoing transitions, or s σ q is a polling state. In order to show the existence of w as above, we consider two cases.

-Case (i): s τ q is a sending state or a choice state. We have s τ q = s σ q since s σ q either has no outgoing transitions or it is a polling state. So some (choice or sending) action b in Σ q should occur in τ ′ to move process q from s τ q . Let τ ′ = ρbρ ′ where ρ contains no letter of Σ q . Then one readily verifies that w = τ baρρ ′ is also a run of A and that w ∼ σ.

-Case (ii): s τ q is a polling state. Since Sch(τ ) = q, some action ?c with dst (c) = q is enabled at the configuration (s τ , χ τ ). That is, (s τ q , ?c, s q ) is an outgoing transition of s τ q and χ τ (c) > 0. We show that ?c occurs in τ ′ and thus if we write τ ′ in the form of ρ ?c ρ ′ where ρ contains no letter of Σ q , then w = τ ?c aρρ ′ is also a run of A and w ∼ σ. Since A is data-branching and s τ q is a polling state, if some action in τ ′ belongs to Σ q , then the first such action must be ?c. Towards a contradiction, suppose that there is no action of q in τ ′ , then s τ q = s σ q and there is no ?c in τ ′ (since ?c is an action of q), hence χ σ (c) ≥ χ τ (c) > 0 contradicting the fact that (s σ , χ σ ) is a final configuration. 2

Observation 3. Lemma 1 implies that a run σ in Run/Sch can be extended to a run in Run cpl /Sch iff it can be extended to a run in Run cpl . This holds for every schedule Sch (not necessarily valid nor regular), provided that the system is data-branching.

The specific power of the valid schedules is shown by the lemma below.

Lemma 2. If there exists a valid schedule Sch, then the (unscheduled) databranching system is deadend free, i.e. any run may be extended to a complete run.

Proof. Let σ be a run. Consider the following algorithm:

p end else ρ := ρa p for some a p ∈ Σ p such that ρa p ∈ Run done As Sch is valid, any run in Run/Sch may be extended to a run in Run cpl ∩ (Run/Sch), and this algorithm has at least one terminating execution, leading to a complete run ρ. Let σ ′ be the largest prefix of σ such that for each p ∈ P, prj p (σ ′ ) is a prefix of prj p (ρ). We prove now that σ ′ = σ. It implies that for However, we shall argue that if there exist two anchored runs satisfying σ ≺ ca σ ′ then for every n = 1, 2, . . ., there exists a run ρ n according to Sch ca such that either max(ρ n ) ≥ n or ρ n cannot be extended to reach a final configuration, entailing by Lemma 2 that Sch ca is not valid. Proposition 3. If there exist two anchored runs σ, σ ′ in Run an /Sch ca such that σ ≺ ca σ ′ , then either RC/Sch ca has an infinite number of configurations or Sch ca is not valid.

Proof.

Let σ ′ = στ . Fix an arbitrary integer k > 1 and consider the sequence α = στ τ . . . τ (k copies of τ ). Following the definition of ≺ ca , one verifies that α is a run of A. If α cannot be extended to a complete run, then by Lemma 2, Sch ca is not valid and this concludes the proof. Otherwise, by Lemma 1, there exists a continuation w ∈ Σ * such that αw is a complete run and αw ∼ ρ for some run ρ ∈ Run cpl ∩ (Run/Sch ca ). Let M = max(σ) and

We show below that max(ρ) ≥ M + k • (M ′ -M ) and thus Sch ca is not regular.

Though στ agrees with Sch ca , we note that α is not necessarily a prefix of ρ. Let α = α!c. Consider the sequence α. For a prefix β of ρ, recall from the proof of Prop. 1 that β is covered by α iff for every p ∈ P, prj p (β) is a prefix of prj p (α). Pick β to be the least prefix of ρ such that β is not covered by α.