Scheduling with Timed Automata

In the previous section, a simple chemical production process has been introduced and formally described by the means of RTN extended by places. The solution of the above problem is a straightforward task and can be performed without 

A very popular scheduling framework is based on mixed-integer programming. Herein, the scheduling problem is modeled in terms of variables and algebraic inequalities and solved by mathematical optimization techniques. In opposition to this well-established framework, a different approach is advocated in the paper by Alur and Dill [8] on timed automata (TA). 

TA are used to model and analyze dynamic systems with discrete and timed behavior. One of their strengths is the easy modeling in a decomposed fashion as a set of often small and individually acting automata. Time in TA is modeled in a very natural way by a set of clocks that simply measure the time between events. This is a major difference to MIP techniques, where time and dynamic components are described in a rather artificial way by providing variables and inequalities for every point of time within a discretized time horizon. In addition to the advantages in modeling, TA serve as a computational model which can be analyzed by techniques for reachability analysis. These techniques are widely used in the context of verification, in which the objective is to detect possible undesired (bad or forbidden) behaviors [9-11]. The success of these techniques was pushed by the availability and increasing performance of tools for TA, e.g., Uppaal [9, 10, 12, 13]. 

Following the above observations, the process model can be formulated by TA. For formal definitions of the syntax and semantics of TA, see [15]. TA are used to model the individual resources by resource automata and to describe timing constraints by place automata. The former are used to start and to finish tasks which are uniquely assigned to resources, the latter establish timing constraints of places. 

Passive components (e.g., materials in storage tanks) can be described by shared variables denoted by Vi. vUv. The production and consumption of materials can be represented by actions, which either increase or decrease the value of the shared variables. The term shared refers to the fact that these variables can be manipulated by any automaton in the model. 

---

Abdeddaim, Y. (2002) Scheduling with Timed Automata. Dissertation, VERIMAG, Institut National Polytechnique de Grenoble. 

To clarify the reason why different circadian schedules of 5-FU delivery have distinct cytotoxic effects, we used the cell cycle automaton model to determine the time evolution of the fraction of cells in S phase in response to different patterns of circadian drug administration, for a cell cycle variability of 15%. The results, shown in Fig. 10.5, correspond to the case considered in Fig. 10.4, namely, entrainment of a 22-h cell cycle by the circadian clock. The data for Fig. 10.5a clearly indicate why the circadian schedule with a peak at 4 a.m. is the least toxic. The reason is that the fraction of cells in S phase is then precisely in antiphase with the circadian profile of 5-FU. Since 5-FU only affects cells in the S phase, the circadian delivery of the anticancer drug in this case kills but a negligible amount of cells. 

---