Introduction

Hybrid systems are dynamical systems combining both discrete and continuous dynamics. This type of systems arise in a large number of application areas and their analysis is a well-established tool in both academic and industry researches.

The system we want to analyse in this paper is a multistage cooking program and (qualitatively/ quantitatively) governing this kind of processes is fundamental for most professional food appliances. Professional chefs, in fact, use different heating methods to bring more flavour to the food or to control the final results. For example, they may start with a short grill for searing a steak and then continue the process at low temperature for a long time. Professional appliances allow to program a cooking cycle by setting up one or more modes, instead of setting different heating stages manually.

Lifting up our view from the single application, we want to focus on the problem of parametrically designing what we can call multistage systems, that are systems characterized by n stages, where each stage has a precise-albeit parametric-evolution law. We give multistage systems as a single hybrid automaton [2], whose states are grouped in layers and states are characterized by a continuous (parametric) evolution law. Each layer qualitatively represents a stage of the entire process and the discrete transition represents the switching instant from one stage to the next one. The underlying structure of the automaton will 102 E. Pippia, A. Bozzato, E. Tiberi, R. Furlanetto, A. Policriti be that of a Directed Acyclic Graphs (DAG) and global properties of the process will be optimized with respect to full paths in such a DAG.

A multistage system is, ultimately, a parametrized hybrid system. In the literature we can find two main classes of problems analyzed on these systems: parameter synthesis and optimal control design. Parameter synthesis is simply the problem of choosing a set of parameters in order to ensure a given property. In [9,8,7] (among many others) we can find possible approaches to solve this problem. Optimal control design is the problem of choosing the best trajectory that satisfies a given property, where with trajectory we mean a possible (full) evolution of the system. Also here we have many examples of possible approaches, such as [12,4,10]. The problem we are considering in this paper is a combination of the two: we want to select a setting of parameters suitable to obtain the best trajectory that satisfies a given property.

In the literature this problem goes under the name of optimal parameter synthesis (or safe reachability problem) and is tackled specifically in [3,5]. In [5] the authors perform optimal parameter synthesis but they are working with transient systems and not with multistage systems as in our case. In a transient system you just have the set of states (finite or infinite) and a transition relation expressed with a formula, that in [5] is a linear arithmetic formula. They use model-checking to obtain the set of all admissible solutions and they illustrate different methods to explore the solution-space in order to find the best solution. [3], instead, are addressing a scheduling problem for a reducing peak power demand of the heating system of multiple zones for a commercial building [13]. In this problem a solution is an unordered list of parameters with the associated duration. The authors are not interested in the specific stage for which we select a given parameter, for this reason they can reduce the optimal parameter synthesis to a linear optimization problem.

In this paper we propose a procedure to solve optimal parameter systhesis problem working directly on the hybrid automaton. We work on the structure of the automaton in order to reduce the optimal parameter synthesis on a multistage system to the optimal control design on an automaton with an augmented number of locations-that we will call multistage automaton. Doing this we address the optimization problem as a reachability problem and we use a backtrack strategy [1] to obtain a feasible solution in the linear case.

Definitions for Hybrid Automata

The notion of hybrid automata was introduced in [2] as a model and specification language for hybrid systems. The following definitions are standard notations of hybrid automata (see [2,6] for more details).

Definition 2.1. An Hybrid AutomatonH = Z, Z , V, E, Inc, Dyn, Act, Reset consists of the following components: Z = (Z 1 , . . . , Z k ) ∈ R k and Z = (Z 1 , . . . , Z k ) ∈ R k

are two vectors of variables; V, E is a finite directed graph: the vertices in V are called locations and the edges in E are called transitions.

Each vertex v ∈ V is labelled by two formulas: Inv(v)[Z] that is an invariant, i.e. a constraint that the variables Z must respect during their evolution;

Dyn(v)[Z, Z , t] that is the dynamic law, in particular for each v ∈ V there is a continuous function f v : R k × R ≥0 → R k such as Dyn(v)[Z, Z , t] is Z = f v (Z, t)

where the variable t represents the time of the system and range over R ≥0 .

Each edge e ∈ E is labelled by other two formulas: Act(e)[Z ] is the activation, i.e. a constraint on the activation of the edge e; Reset(e)[Z, Z ] is the reset of the variables while we are using the edge e.

Definition 2.2 (State). A state σ is a pair (v, x) considering a location v ∈ V and a valuation x ∈ R k for the variables Z such as Inv(v)[x] holds.

Definition 2.3 (Transition relations).

Let H be a hybrid automaton. We have two type of transition relations between two states σ = (v, x) and δ = (w, y):

continuous transition relation σ → t δ ⇔ v = w and there exists f : R ≥0 → R k continuous function such that x = f (0), y = f (t)

Thawing Optimization Problem

The target is to solve the optimal parameter synthesis for a multistage cooking program. The procedure we describe is very general and can be applied to every multistage system. For example, we can create a continuous "cutting-stock" problem thinking of a painting product-line of a metal tube factory, where we want to maximize the overall length of tubes produced, while keeping the paint consumption for each primary color under a supply limit threshold. As another example, we can apply our methodology to find an ordered solution for the peak power demand problem described in [13].

Here we want to focus on a special multistage heating process, the thawing process, that is the process of safely heat up a frozen foodstuff to just above 0 • C. In professional applications, the thawing process can be executed inside a specific appliance able to keep the temperature of its cavity within the range 4 • C -16 • C. We can set n different stages, namely n different temperatures of the cavity in the form of a vector T set ∈ [4, 16] n with the temperatures expressed in Celsius unit. In addition we require how long we want to keep these temperatures, so we fix another vector time set with n − 1 duration expressed in seconds. We define as thawing cycle the system obtained by specifying these parameters. A thawing cycle ends when the minimum temperature of the foodstuff reaches 0 • C.

In this process food safety becomes particularly important because the bacteria that cause food poisoning are found on the surfaces of many foods and they start growing due to the continuous arise of the temperature of these areas. There are different evolution models that take into account the bacterial growth depending on the temperature and the duration, mostly variants of the logistic evolution model or piecewise exponential growth curves obtained with empirical methods [14]. We are going to consider the easiest and the strictest constraint that we can impose. The same construction can be extended to more complex models. In summary, we want keep the maximum temperature T max of the product below a T saf e temperature of 7 • C following the codex alimentarius for fish fillet [11].

The aim is to select a thawing cycle in order to minimize the total duration of the process keeping bacterial growth under control by looking at the maximum temperature of the foodstuff.

The optimization problem described is quite general. We have a multistage system with m(m − 1) variables and we want to minimize the total time having an end condition-in the thawing case is a minimum threshold that we have to reach (T min = 0 • C)-and satisfying a constraint that in this case is a maximum threshold that we do not want to overpass (T max ≤ 7 • C).

Example 3.1 (Linear multistage system). We introduce the following simplified (linear) version of the thawing cycle. Suppose we have only 3 stages and suppose we deal with two variables x 1 , x 2 only, evolving linearly. x 1 is the minimum temperature and x 2 is the maximum temperature. Suppose T set ∈ {4, 8, 12, 16} 3 , so we have to select one of these temperature for each of the 3 stages. If we are in the stage i we select the temperature T set (i) and we have:

x 1 (t) = x 1 (0) + T set (i) 8000 t; x 2 (t) = x 2 (0) + (T set (i) − 2) 4000 • t (1)

The starting values x 1 (0) and x 2 (0) for the first stage are −18 • C (typically the freezer temperature). The starting value in the second and third stage are the last value of the previous stage. In this example choosing T set and time set we obtain a trajectory for x 1 and a trajectory for x 2 that are piecewise linear functions.

Hybrid Automaton model

A multistage system with n stages is inherently an hybrid model and the natural way to model it is with an hybrid automaton with n + 1 locations: n locations for the n stages of the system, plus an extra location for the end condition. Our strategy will consist in increasing (step by step) the number of locations of a hybrid automaton till we reach what we call a multistage automaton appropriately modeling our scenario.

Definition 4.1 (Multistage automaton).

A multistage automaton (H, K, g) consists of the following components:

K a finite set of real parameters;

H = Z, Z , V, E, Inv, Dyn, Act, Reset is an hybrid automaton;

V, E is a Direct Acyclic Graph (DAG) and V = S ∪ V ∪ E a partition of V in three not empty sets, such that s ∈ S has only outgoing edges, e ∈ E has only incoming edges, and v ∈ V has at least one outgoing edge and at least one incoming edge;

g : V → K is a labeling function; Z = (Z 1 , . . . , Z n ) ∈ R n , Z = (Z 1 , . . . , Z n ) ∈ R n and there exists a function f : R n × R ≥0 × K → R n such that Dyn(v), for v ∈ V , has the following form: Dyn(v)[Z, Z , t] ≡ (Z = f (Z, t, g(v))).

We work with the linear multistage system in the Example 3.1 to illustrate the associated multistage automaton. Set K = {k 1 , k 2 , k 3 , k 4 } = {4, 8, 12, 16}. If we fix the parameter vector T set , we can define a simple linear hybrid automaton H L = Z, Z , V, E, Inv, Dyn f , Act, Reset as in Figure 1. First of all we are going to explicit the role of the variables T set (i). These constants change the evolution of our variables but we have only a finite number of values to take into account, since the dimension of K is finite.

v 1 x 1 = x 1 + Tset(1) 8000 t x 2 = x 2 + Tset (1)t x 1 ≤ 0 ∧ x 2 ≤ 7 v 2 x 1 = x 1 + Tset(2) 8000 t x 2 = x 2 + Tset (2)t x 1 ≤ 0 ∧ x 2 ≤ 7 v 3 x 1 = x 1 + Tset(3) 8000 t x 2 = x 2 + Tset (3)t x 1 ≤ 0 ∧ x 2 ≤ 7 end x 1 = −18 x 2 = −18 x 1 = x 1 x 2 = x 2 x 1 = x 1 x 2 = x 2 x 1 ≥ 0 x 1 = x 1 x 2 = x 2

We split each stage of H L in 4 different locations, one for each possible evolution. We add also a dummy starting node to initialize the variables. What we obtain is a graph with 3 internal layers as in Figure 2. We denote by v i,j a location on layer i = 1, 2, 3 with constant k j ∈ K. Every location at layer i is connected to all the locations at layer i + 1. The layered hybrid automaton L in Figure 2 has: E) as in Figure 2;

Z = (x 1 , x 2 ), Z = (x 1 , x 2 ); (V,Reset(e)[Z, Z ] ≡ (x 1 = x 1 ∧ x 2 = x 2 ) for e ∈ E; Inv(v i,j )[Z] ≡ (x 1 ≤ 0 ∧ x 2 ≤ 7) for i = 1, 2, 3 j, k = 1, . . . , 4; Inv(v)[Z] ≡ T rue for v = s, e; Dyn(v i,j )[Z, Z , t] ≡ (x 1 = x 1 + kj 8000 t ∧ x 2 = x 2 + (kj −2) 4000 t for i = 1, 2, 3 j = 1, . . . , 4; Dyn(s)[Z, Z , t] ≡ (x 1 = −18 ∧ x 2 = −18) and Dyn(e)[Z, Z , t] ≡ (x 1 = x 1 ∧ x 2 = x 2 );

Act((v 3,j , e))[Z ] ≡ (x 1 ≥ 0) for j = 1, . . . , 4 and the activation is T rue for all the other edges.

Optimization and Multistage Systems. The Thawing Case 105 For each internal location v i,j ∈ V we can define the function g(v i,j ) = k j with k j ∈ K. It is evident by construction that the couple (L, K, g) is a multistage automaton.

If we consider the multistage automaton L in Figure 2 and we solve a reachability problem from the location s to the location e we find just a feasible solution for the optimal parameter synthesis but not the optimal one. We need to make a step ahead adding the information of the total duration. In L we know that the final duration of our system can vary from 2.5 hours to 10 hours so we can split the location end in 9 locations, one per each hour (or more if we want to refine the interval). We obtain the multistage automaton L as in Figure 3. We call e 3 the end location associated with t = 3 hours and in general e h for the end location associated with t = h hours. What we have to modify is the activation constraint adding the time bound:

s v 1,2 v 1,1 v 1,3 v 1,4 v 2,1 v 2,2 v 2,3 v 2,4 v 3,1 v 3,2 v 3,3 v 3,4 e Figure 2: Layer Hybrid Automaton L with 3 layers s v 1,2 v 1,1 v 1,3 v 1,4 v 2,1 v 2,2 v 2,3 v 2,4 v 3,1 v 3,2 v 3,3 v 3,4Act((v 3,j , e 3 ))[Z ] ≡ (x 1 ≥ 0 ∧ t ≤ 3 • 3600); Act((v 3,j , e 10 ))[Z ] ≡ (x 1 ≥ 0 ∧ 9 • 3600 < t) ; Act((v 3,j , e h ))[Z ] ≡ (x 1 ≥ 0 ∧ (h − 1) • 3600 < t ≤ h • 3600)

If the reachability problem from the location s with x 1 = −18 • C and x 2 = −18 • C to the location e 3 have a solution, we have the existence of a feasible solution for the optimal parameter synthesis with a total duration ≤ 3 hours, vice versa if the reachability problem is empty we know that if a solution exists the optimal value is greater than 3 hours. In general solving the reachability problem on the automaton L give us the existence of a feasible solution for the optimal parameter synthesis problem with a lower/upper bound to the optimal solution.

To conclude we need to be able to solve the reachability problem. In general, if the evolution are linear, we can solve the reachability problem from the set of starting states Σ S to the set of ending states Σ E using the backward approach introduced in [2, 1]. The procedure is effective and we can, for example, prove that the automaton L does not have feasible trajectories with a duration less than 6 hours, hence all the reachability problems from s to e 3 , . . . , e 6 have a negative solution.

Conclusions and future works

We showed how we can reformulate a optimal parameter synthesis problem for a class of hybrid systems that we called multistage systems. For general multistage systems we obtain a multistage automaton, a hybrid automata with a layered DAG as underlying discrete structure. The key point was to reformulate the optimization problem as a reachability problem, use the backtrack technique introduced by Alur [2, 1] to prove the existence of a feasible solution, and obtain a lower/upper-bound to an optimal solution.

True thawing is, in fact, non-linear. The graph construction presented here is applicable to the non-linear case but additional ideas are needed to solve the reachability problem in that case. A further interesting direction consists, therefore, in studying the temperature-evolution in order to approximate its law-to start-with a piece-wise linear function.