Formal Synthesis of Control Strategies for Positive Monotone Systems
Sadra Sadraddini Calin Belta


Strongly Interacting Phases of Metallic Wires in Strong Magnetic Field
    Xiao-Liang Qi
    Accepted .  Received ; in original form 
======================================================================




We design controllers from formal specifications for positive discrete-time monotone systems that are subject to bounded disturbances. Such systems are widely used to model the dynamics of transportation and biological networks. The specifications are described using signal temporal logic (STL), which can express a broad range of temporal properties. We formulate the problem as a mixed-integer linear program (MILP) and show that under the assumptions made in this paper, which are not restrictive for traffic applications, the existence of open-loop control policies is sufficient and almost necessary to ensure the satisfaction of STL formulas. We establish a relation between satisfaction of STL formulas in infinite time and set-invariance theories and provide an efficient method to compute robust control invariant sets in high dimensions. We also develop a robust model predictive framework to plan controls optimally while ensuring the satisfaction of the specification. Illustrative examples and a traffic management case study are included.



Formal Synthesis and Verification, Monotone Systems, Transportation Networks.





§ INTRODUCTION







In recent years, there has been a growing interest in using formal methods for specification, verification,  and synthesis in control theory. Temporal logics <cit.> provide a rich, expressive framework for describing a broad range of properties such as safety, liveness, and reactivity. In formal synthesis, the goal is to control a dynamical system from such a specification. For example, in an urban traffic network, a synthesis problem can be to generate traffic light control policies that ensure gridlock avoidance and fast enough traffic through a certain road, for all times. 



Control synthesis for linear and piecewise affine systems from linear temporal logic (LTL) specifications was studied in <cit.>. The automata-based approach used in these works requires constructing finite abstractions that (bi)simulate the original system. Approximate finite bisimulation quotients for nonlinear systems were investigated in <cit.>. The main limitations of finite abstraction approaches are the large computational burden of discretization in high dimensions and conservativeness when exact bisimulations are impossible or difficult to construct. As an alternative approach, LTL optimization-based control of mixed-logical dynamical (MLD) systems <cit.> using mixed-integer programs was introduced in <cit.>, and was recently extended to model predictive control (MPC) from signal temporal logic (STL) specifications in <cit.>. However, these approaches are unable to guarantee infinite-time safety and the results are fragile in the presence of non-deterministic disturbances. 
 


In some applications, the structural properties of the system and the specification can be exploited to consider alternative approaches to formal control synthesis. We are interested in systems in which the evolution of the state exhibits a type of order preserving law known as monotonicity, which is common in models of transportation, biological, and economic systems <cit.>. Such systems are also positive in the sense that the state components are always non-negative. Control of positive systems have been widely studied in the literature <cit.>. Positive linear systems are always monotone <cit.>. 

In this paper, we study optimal STL control of discrete-time positive monotone systems (i.e., systems with state partial order on the positive orthant) with bounded disturbances. STL allows designating time intervals for temporal operators, which makes it suitable for describing requirements with deadlines. Moreover, STL is equipped with quantitative semantics, which provides a measure to quantify how strongly the specification is satisfied/violated. The quantitative semantics of STL can also be used as cost 
for maximization in an optimal control setting. The STL specifications in this paper are restricted to a particular form that favors smaller values for the state components. We assume that there exists a maximal disturbance element that characterizes a type of upper-bound for the evolution of the system. These assumptions are specifically motivated by the dynamics of traffic networks, where the disturbances represent the volume of exogenous vehicles entering the network and the maximal disturbance characterizes the rush hour exogenous flow.  Our optimal control study is focused on STL formulae with infinite-time safety/persistence properties, which is relevant to optimal and correct traffic control in the sense that the vehicular flow is always free of congestion while the associated delay is minimized. 



The key contributions of this paper are as follows. First, for finite-time semantics, we prove that the existence of open-loop control policies is necessary and sufficient for maintaining STL correctness. 
For the correctness of infinite-time semantics, we show that the existence of open-loop control sequences is sufficient and almost necessary, in a sense that is made clear in the paper. Implementing open-loop control policies is very simple since online state measurements are not required, which can prove useful in applications where the state is difficult to access. We use a robust MPC approach to optimal control. The main contribution of our MPC framework is guaranteed recursive feasibility, a property that was not established in prior STL MPC works <cit.>. We show via a case study that our method is applicable to systems with relatively high dimensions. 

 



   













This remainder of the paper is organized as follows. We introduce the necessary notation and background on STL in Sec. <ref>. The problems are formulated in Sec. <ref>. The technical details for control synthesis from finite and infinite-time specifications are given in Sec. <ref> and Sec. <ref>, respectively. The robust MPC framework is explained in Sec. <ref>. Finally, we introduce a traffic network model and explain its monotonicity properties in Sec. <ref>, where a case study is also presented.  






 §.§ Related Work

This paper is an extension of the conference version <cit.>, where we studied safety control of positive monotone systems. Here, we significantly enrich the range of specifications to STL, provide complete proofs, and include optimal control. 


Monotone dynamical systems have been extensively investigated  in the mathematics literature <cit.>.  
Early studies mainly focused on stability properties and characterization of limit sets for autonomous, deterministic continuous-time systems <cit.>. The results do not generally  hold for discrete-time systems, as discussed in <cit.>. In particular, attractive periodic orbits are proven to be non-existent for continuous-time autonomous systems <cit.>, but may exist for discrete-time autonomous systems. Here we present a similar result for controlled systems, where we show that a type of attractive periodic orbit exists for certain control policies.

Angeli and Sontag <cit.> extended the notion of monotonicity to deterministic continuous-time control systems and provided results on interconnections of these systems. However, they assumed monotonicity with respect to both state and controls. We do not require monotonicity with respect to controls, which enables us to consider a broader class of systems. In particular, we do not require controls to belong to a partially ordered set. 

Switching policies for exponential stabilization of switched positive linear systems were studied in  <cit.>. Stabilization is closely related to set-invariance, which is thoroughly studied in this paper. Apart from richer specifications, we can handle more complex systems. We consider hybrid systems in which the mode is either determined directly by the control input or indirectly by the state (e.g., signalized traffic networks).



Recently, there has been some interest on formal verification and synthesis for monotone systems. Safety control of cooperative systems was investigated in  <cit.>. However, these work, like <cit.>, assumed monotonicity with respect to the control inputs as well. Computational benefits gained from monotonicity for reachability analysis of hybrid systems were highlighted in <cit.>. More recently, the authors in <cit.> provided an efficient method to compute finite abstractions for mixed-monotone systems (a more general class than monotone systems). The authors in <cit.> exploited monotonicity to compute finite-state abstractions that are used for compositional LTL control. 
While the approaches in <cit.> can consider systems and specifications beyond the assumptions in this paper, they still require state-space discretization, which is a severe limitation in high dimensions. Moreover, they are conservative since the finite abstractions are often not bisimilar with the original system - whereas our approach provides a notion of (almost) completeness. Finally, as opposed to the all mentioned works, our framework is amenable to optimal temporal logic control. 




§ PRELIMINARIES




 §.§ Notation


For two integers a,b, we use (a,b) to denote the remainder of division of a by b. Given a set 𝒮 and a positive integer K, we use the shorthand notation 𝒮^K for ∏_i=1^K 𝒮. A signal is defined as an infinite sequence s=s_0s_1⋯, where s_k ∈𝒮, k ∈ℕ.  
Given s_1,s_2,⋯,s_K∈𝒮, the repetitive infinite-sequence s_1s_2 ⋯ s_K s_1 s_2 ⋯ s_K⋯ is denoted by (s_1 s_2 ⋯ s_K)^ω. The set of all signals that can be generated from 𝒮 is denoted by 𝒮^ω. We use s[k]=s_ks_k+1⋯ and s[k_1:k_2]=s_k_1s_k_1+1⋯s_k_2,  k_1 < k_2, to denote specific portions of s.
A real signal is r=r_0r_1r_2⋯, where r_k ∈ℝ^n, ∀ k ∈ℕ. A vector of all ones in ℝ^n is denoted by 1_n. We use the notation 1_n[0:K]:= 1_n ⋯ 1_n, where 1_n is repeated K+1 times.

The positive closed orthant of the n-dimensional Euclidian space is denoted by ℝ^n_+ := { x ∈ℝ^n| x_[i]≥ 0, i=1,⋯,n }, where x=(x_[1],x_[2],⋯,x_[n])^T. For a,b ∈ℝ^n, the non-strict partial order relation ≼ is defined as:
a ≼ b ⇔ b-a ∈ℝ_+^n.



[<cit.>]
A set 𝒳⊂ℝ^n_+ is a lower-set if ∀ x ∈𝒳,L(x) ⊆𝒳, where L(x):= { y ∈ℝ_+^n | y ≼ x }.

It is straightforward to verify that if 𝒳_1,𝒳_2 are lower-sets, then 𝒳_1 ∪𝒳_2 and 𝒳_1 ∩𝒳_2 are also lower-sets.
 We extend the usage of notation ≼ to equal-length real signals. For two real signals r, r, we denote r'[t_1':t_2'] ≼r[t_1:t_2], t_2-t_1=t'_2-t'_1, if r'_t'_1+k≼ r_t_1+k, k=0,1,⋯,t_2-t_1. 
Moreover, if r, r' ∈ (ℝ_+^n)^ω, we are also allowed to write  r'[t_1':t_2'] ∈ L(r[t_1:t_2]).




 §.§ Signal Temporal Logic (STL)



In this paper, STL <cit.> formulas are defined over discrete-time real signals. 
The syntax of negation-free STL is:

    φ:=  π  |  φ_1 ∧φ_2   | φ_1 ∨φ_2  | φ_1  U_Iφ_2  | F_I φ | G_I φ,
  



where π=(p(r) ≤ c) is a predicate on r∈ℝ^n, p: ℝ^n →ℝ, c ∈ℝ; ∧ and ∨ are Boolean connectives for conjunction and disjunction, respectively; U_I, F_I, G_I are the timed until, eventually and always operators, respectively, and I=[t_1,t_2] is a time interval,  t_1,t_2 ∈ℕ∪{∞}, t_2≥ t_1. When t_1=t_2, we use the shorthand notation {t_1}:=[t_1,t_1]. Exclusion of negation does not restrict expressivity of temporal properties. It can be easily shown that any temporal logic formula can be brought into negation normal form (where all negation operators apply to the predicates) <cit.>. 


We deliberately omit negation from STL syntax for laying out properties that are later exploited in the paper. For simplicity, in the rest of the paper, we will refer to negation-free STL simply as STL. 
The semantics of STL is inductively defined as:

    [                            r[t] π                                 ⇔                       p(r_t) ≤ c,;                     r[t] φ_1 ∨φ_2                                 ⇔            r[t] φ_1  ∨ r[t]  φ_2,;                    r[t]  φ_1 ∧φ_2                                 ⇔            r[t] φ_1  ∧ r[t]  φ_2,;                r[t]  φ_1  U_I φ_2                                 ⇔       ∃ t^'∈ t+I 
     s.t r[t^'] φ_2;                                   ∧ ∀ t^''∈ [t,t^'],   r[t^''] φ_1,;                      r[t]   F_I φ                                 ⇔        ∃  t^'∈ t+I  s.t. r[t'] φ,;                     r[t]    G_I φ                                 ⇔        ∀  t^'∈ t+I  s.t. r[t'] φ, ]
 
where  is read as satisfies. The language of φ is the set of all signals such that r[0] φ. The horizon of an STL formula φ, denoted by h^φ, is defined as the time required to decide the satisfaction of φ, which is recursively computed as <cit.>:

    [                             h^π=                               0,;           h^φ_1 ∧φ_2=h^φ_1 ∨φ_2=                max(h^φ_1,h^φ_2),; h^ F_[t_1,t_2]φ=h^ G_[t_1,t_2]φ=                         t_2+h^φ,;           h^φ_1  U_[t_1,t_2]φ_2=            t_2+max(h^φ_1,h^φ_2).;                                  ]


An STL formula φ is bounded if h^φ<∞. 


[<cit.>]
A safety STL formula is an STL formula in which all “until" and “eventually" intervals are bounded.



The satisfaction of φ by r[t] is decided only by r[t:t+h^φ] and the rest of the signal values are irrelevant. Therefore, instead of r[t]φ, we occasionally write r[t:t+h^φ]φ with the same meaning. 
The STL robustness score ρ(r,φ,t) ∈ℝ is a measure indicating how strongly φ is satisfied by r[t], which is recursively computed as <cit.>:

    [                           ρ(r,π,t)                                  =                         c-p(r_t) ,;                    ρ(r,φ_1 ∨φ_2,t)                                  =       max(ρ(r,φ_1,t),ρ(r,φ_2,t) ),;                    ρ(r,φ_1 ∧φ_2,t)                                  =       min(ρ(r,φ_1,t),ρ(r,φ_2,t) ),;                ρ(r,φ_1  U_I φ_2,t)                                  = t^'∈ t+Imax (  
     min (ρ(r,φ_2,t'),;                                           t”∈ [t,t']minρ(r,φ_1,t”))),;                      ρ(r, F_I φ,t)                                  =             t' ∈ t+Imax ρ(r,φ,t'),;                      ρ(r, G_I φ,t)                                  =             t' ∈ t+Imin ρ(r,φ,t').;                                    ]
 
Positive (respectively, negative) robustness indicates satisfaction (respectively, violation) of the formula.
 



Consider signal r∈ℝ^ω, where r_k=k, k ∈ℕ, and π=(r^2 ≤ 10). We have ρ(r, G_[0,3]π,0)=min(10-0,10-1,10-4,10-9)=1 (satisfaction) and ρ(r, F_[4,6]π,0)=max(10-16,10-25,10-36)=-6 (violation). 



There are minor differences between the original STL introduced in <cit.> and the one used in this paper. In <cit.>, STL was  developed as an extension of metric interval temporal logic (MITL) <cit.> for real-valued continuous-time signals. Here, without any loss of generality, we apply STL to discrete-time signals. Our STL is based on metric temporal logic (MTL) (similar to <cit.>). Thus, we allow the intervals of temporal operators to be singletons (punctual) or unbounded. It is worth to note that any STL formula in this paper can be translated into an LTL formula by appropriately replacing the time intervals of temporal operators with LTL “next" operator. However, the LTL representation of STL formulas can be very inefficient. We prefer STL for convenience of specifying requirements for systems with real-valued states. We also exploit the STL quantitative semantics. 
 





§ PROBLEM STATEMENT AND APPROACH



We consider discrete-time systems of the following form:

    x_t+1=f(x_t,u_t,w_t),

where x_t ∈𝒳 is the state, 𝒳⊂ℝ_+^n, u_t ∈𝒰 is the control input, 𝒰= ℝ^m_r×{0,1}^m_b, and w_t ∈𝒲 is the disturbance (adversarial input) at time t, t∈ℕ, 𝒲= ℝ^q_r×{0,1}^q_b. The sets 𝒰 and 𝒲 may include real and binary values. For instance, the set of controls in the traffic model developed in Sec. <ref> includes binary values for decisions on traffic lights and real values for ramp meters. These types of systems are positive as all state components are non-negative. We also assume that 𝒳 is bounded.


System (<ref>) is monotone (with partial order on ℝ^n_+) if for all x,x'∈𝒳,  x' ≼ x, we have f(x',u,w) ≼ f(x,u,w), ∀ u ∈𝒰, ∀ w ∈𝒲. 

The systems considered in this paper are positive and monotone with partial order on ℝ^n_+. For the remainder of the paper, we simply refer to systems in Definition <ref> as monotone [The term cooperative in dynamics systems theory is used specifically to refer to systems that are monotone with partial order defined on the positive orthant. We avoid using this term here as it might generate confusion with the similar terminology used for multi-agent control systems.]. 
 Although the results of this paper are valid for any general f:𝒳×𝒰×𝒲→𝒳, we focus on systems that can be written in the form of mixed-logical dynamical (MLD) systems <cit.>, which are defined in Sec. <ref>. It is well known that a wide range of systems involving discontinuities (hybrid systems), such as piecewise affine systems, can be transformed into MLDs <cit.>.





There exist w^* ∈𝒲 such that

    ∀ x∈𝒳, ∀ u∈𝒰,  f(x,u,w) ≼ f(x,u,w^*), ∀ w∈𝒲.


We denote f(x,u,w^*) by f^*(x,u) and refer to f^* as the maximal system.  
As it will be further explained in this paper, the behavior of monotone  system (<ref>) is mainly characterized by its maximal f^*. Assumption <ref> is restrictive but holds for many compartmental systems where the disturbances are additive and the components are independent. Therefore, the maximal system corresponds to the situation that every component takes its most extreme value. 
We also note that if Assumption <ref> is removed, overestimating f by some f^* such that f(x,u,w) ≼ f^*(x,u), ∀ w ∈𝒲, is always possible for a bounded f. By overestimating f the control synthesis methods of this paper remain correct, but become conservative. 











We describe the desired system behavior using specifications written as STL formulas over a finite set of predicates. We assume that each predicate π is in the following form:

    π=  ( a_π^T x ≤ b_π ),
 
where a_π∈ℝ^n_+, b_π∈ℝ_+. It is straightforward to verify that the closed half-space defined by (<ref>) is a lower-set in ℝ^n_+.  
By restricting the predicates into the form (<ref>), we ensure that a predicate remains true if the values of state components are decreased (Note that this is true for any lower set. We require linearity in order to decrease the computational complexity.). This restriction is motivated by monotonicity. For example, in a traffic network, the state is the vector representation of vehicular densities in different segments of the network. The satisfaction of a “sensible" traffic specification has to be preserved if the vehicular densities are not increased all over the network. Otherwise, the specification encourages large densities and congestion.
  


















A control policy μ:=⋃_t ∈ℕμ_t is a set of functions μ_t:𝒳^t+1→𝒰, where 
    u_t=μ_t(x_0,x_1,⋯,x_t).

 
An open-loop control policy takes the simpler form u_t=μ_t(x_0), i.e., the decision on the sequence of control inputs is made using only the initial state x_0. On the other hand, in a (history dependent) feedback control policy, u_t=μ_t(x_0,x_1,⋯,x_t), the controller implementation requires real-time access to the state and its history.

An infinite sequence of admissible disturbances is w=w_0w_1⋯, where w_k ∈𝒲, k ∈ℕ. Following the notation introduced in Sec. <ref>, the set of all infinite-length sequences of admissible disturbances is denoted by 𝒲^ω. Given an initial condition x_0, a control policy μ and w∈𝒲^ω, the run of the system is defined as the following signal: 

    x=x(x_0,μ,w):=x_0 x_1 x_2 ⋯,

where x_t+1=f(x_t,u_t,w_t), ∀ t ∈ℕ. 




Now we formulate the problems studied in this paper. In all problems, we assume a monotone system (<ref>) is given, Assumption <ref> holds, and all the predicates are in the form of (<ref>). 
 





[Bounded STL Control]

Given a bounded STL formula φ, find a set of initial conditions 𝒳_0 ⊂𝒳 and a control policy μ such that 

    x(x_0,μ,w)[0] φ, ∀w∈𝒲^ω, ∀ x_0 ∈𝒳_0.






As mentioned in the previous section, the satisfaction of φ solely depends on x[0:h^φ], where h^φ is obtained from (<ref>). The horizon h^φ can be viewed as the time when the specification ends. In many engineering applications, the system is required to uphold certain behaviors for all times. Therefore, guaranteeing infinite-time safety properties is important. 
We formulate bounded-global STL formulas in the form of 

    φ_b ∧ G_[Δ,∞]φ_g,

where φ_b, φ_g are bounded STL formulas, G_[Δ,∞] stands for unbounded temporal “always"- as defined in Sec. <ref>, and Δ≥ h^φ_b is a positive integer. Formula (<ref>) states that first, φ_b is satisfied by the signal from time 0 to Δ, and, afterwards, φ_g holds for all times. 



[Bounded-global STL Control]

Given bounded STL formulas φ_b,φ_g, Δ∈ [h^φ_b,∞), find a set of initial conditions 𝒳_0 ⊂𝒳 and a control policy μ such that

    x(x_0,μ,w)[0] φ_b ∧G_[Δ,∞]φ_g, ∀w∈𝒲^ω, ∀ x_0 ∈𝒳_0.






As a special case, we allow φ_b to be logical truth so Problem <ref> reduces to global STL control problem of satisfying G_[Δ,∞]φ_g. Note that if φ_g is replaced by logical truth, Problem <ref> reduces to  Problem <ref>. We have distinguished Problem <ref> and Problem <ref> as we use different approaches to solve them. 



It can be shown that (see Appendix) a large subset of safety STL formulas - as in Definition <ref> - can be written as 
⋁_i=1^n_ϕϕ_i,
where each ϕ_i, i=1,⋯,n_ϕ, is a bounded-global formula. Therefore, the framework for solutions to Problem <ref> can also be used for safety STL control as it leads to n_ϕ instances of Problem <ref>, where a solution to any of the instances is also a solution to the original safety STL control problem. The drawback to this approach is that n_ϕ can be very large.       


 
We avoid separate problem formulations for STL formulas containing unbounded “eventually" or “until" operators as their unbounded intervals can be safely under-approximated by bounded intervals. However, bounded under-approximation is not sound for the unbounded “always" operator. A safety formula can be satisfied (respectively, violated) with infinite-length (respectively, finite-length) signals <cit.>. 


In the presence of disturbances, feedback controllers obviously outperform open-loop controllers. We show that the existence of open-loop control policies for guaranteeing the STL correctness of monotone systems in Problem 1 (respectively, Problem 2) is sufficient and (respectively, almost) necessary. The online knowledge of state is not necessary for STL correctness. But it can be exploited for planning controls optimally. 
While our framework can accommodate optimal control versions of Problem <ref> and Problem <ref>, the focus of this paper is on robust optimal control problem for global STL formulas - of form G_[0,∞)φ, where φ is a bounded formula. These type of problems are of practical interest for optimal traffic management (as discussed in Sec. <ref>). 

We use a model predictive control (MPC) approach, which is a popular, powerful approach to optimal control of constrained systems. Given a planning horizon of length H [The MPC horizon H should not be confused with the STL horizon h^φ. ], a sequence of control actions 
 starting from time t is denoted by u_t^H:=u_0|t u_1|t⋯  u_H-1|t. Given u^H_t and x_t, we denote the predicted H-step system response by 


    x_t^H(x_t,u_t^H,w_t^H):= x_1|t x_2|t⋯ x_H|t,

 where 
x_k+1|t=f(x_k|t,u_k|t,w_k|t), k=0,1,⋯,H-1,
 x_0|t=x_t and w_t^H:=w_0|t w_1|t⋯ w_H-1|t. At each time, u^H_t is found such that it optimizes a cost function J(x_t^H,u^H_t), J:𝒳^H ×𝒰^H →ℝ, subject to system constraints. When u_t^H is computed, only the first control action u_0|t is applied to the system and given the next state, the optimization problem is resolved for u_t+1^H. Thus, the implementation is closed-loop. 

[Robust STL MPC] 

Given a bounded STL formula φ, an initial condition x_0, a planning horizon H and a cost function J(x_t^H,u^H_t), find a control policy such that  u_t=μ(x_0,⋯,x_t)=u^opt_0|t, where u_t^H,opt:=u^opt_0|t⋯ u^opt_H-1|t, and u^H,opt is the following minimizer:









    [                                        _u_t^H w^H_tmax   J(x_t^H(x_t,u_t^H,w_t^H), u_t^H ),;                                          s.t.               x(x_0,μ,w)[0] G_[0,∞]φ, ∀w∈𝒲^ω,;                                                               x_k+1=f(x_k,u_k,w_k), ∀ k ∈ℕ.;                                               ]






The primary challenge of robust STL MPC is guaranteeing the satisfaction of the global STL formula while the controls are planned in a receding horizon manner (see the constraints in (<ref>)). Our approach takes the advantage of the results from Problem <ref> to design appropriate terminal sets for the MPC algorithm such that the generated runs are guaranteed to satisfy the global STL specification while the online control decisions are computed (sub)optimally. Due to the temporal logic constraints, our MPC setup differs from the conventional one. The details are explained in Sec. <ref>.


For computational purposes, we assume that J is a piecewise affine function of the state and controls. Moreover, the cost functions in our applications are non-decreasing with respect to the state in the sense that x'_k|t≼ x_k|t, k=1,2,⋯,H ⇒ J(x_t^' H,u^H_t) ≼ J(x_t^H,u^H_t), ∀ u^H_t ∈𝒰^H. As it will become clear later in the paper, we will exploit this property to simplify the worst-case optimization problem in (<ref>) to an optimization problem for the maximal system. 

As mentioned earlier, a natural objective is maximizing STL robustness score. It follows from the linearity of the predicates in (<ref>) and max and min operators in (<ref>) that STL robustness score is a piecewise affine function of finite-length signals. We can also consider optimizing a weighted combination of STL robustness score and a given cost function. We use this cost formulation for traffic application in Sec. <ref>.















































§ FINITE HORIZON SEMANTICS


In this section, we explain the solution to Problem <ref>. First, we exploit monotonicity to characterize the properties of the solutions. Next, we explain how to synthesize controls using a mixed integer linear programming (MILP) solver.

 
 
Consider runs x and x' and an STL formula φ. If for some t,t', we have x'[t':t'+h^φ] ≼x[t:t+h^φ], then x[t] φ implies x'[t'] φ. 


Since all predicates denote lower-sets in the form of (<ref>), we have x'_t'≼ x_t⇒ a_π^T x'_t'≤ a_π^T x_t, x[t] π⇒x'[t] π. Thus, all predicates that were true by the valuations in x remain true for x'. The negation-free semantics in (<ref>) implies that without falsifying any predicate, a formula can not be falsified. Therefore, x[t] φ implies x'[t'] φ


The largest set of admissible initial conditions is defined as:

    𝒳_0^max:={ x_0 ∈𝒳 |∃μ s.t. x(x_0,μ,w) φ, ∀w∈𝒲^ω}.

The set 𝒳_0^max is a union of polyhedra. Finding the half-space representation of all polyhedral sets in 𝒳_0^max may not be possible for high dimensions. Therefore, we find a half-space representation for a subset of 𝒳_0^max. The following result states how to check whether x_0 ∈𝒳_0^max. 


 

We have x_0 ∈𝒳_0^max if and only if there exists an open-loop control sequence 
    u_0^ol,x_0 u_1^ol,x_0⋯ u_h^φ-1^ol,x_0
 
such that x^ol,x_0[0:h^φ] φ, where x^ol,x_0[0:h^φ]=x_0^ol,x_0x_1^ol⋯ x_h^φ^ol,x_0, and x_k+1^ol,x_0=f^*(x_k^ol,x_0,u_k^ol,x_0), k=0,⋯,h^φ-1, x_0^ol,x_0=x_0.


(Necessity)
Satisfaction of φ with w∈𝒲^ω requires at least one satisfying run for the maximal system, hence a corresponding control sequence exists. Denote it by u_0^ol,x_0 u_1^ol,x_0⋯,u_h^φ-1^ol,x_0.  
(Sufficiency)
Consider any run generated by the original system x_k+1=f(x_k,u_k^ol,x_0,w_k). We prove that x_k ≼ x_k^ol,x_0 , k=0,1,⋯,h^φ, by induction over k. The base case x_0 ≼ x_0^ol,x_0 is trivial (x_0=x_0^ol,x_0). The inductive step is verified from monotonicity: x_k+1=f(x_k,u_k^ol,x_0,w_k) ≼ f^*(x_0^k,u_k^k) = x^ol,x_0_k+1. Therefore, x[0:h^φ] ≼x^ol,x_0[0:h^φ], ∀w[0:h^φ-1] ∈𝒲^h^φ. It follows from Lemma <ref> that x[0:h^φ] φ, ∀w[0:h^φ-1] ∈𝒲^h^φ. 



The set 𝒳_0^max is a lower-set.


Consider any x_0' ∈ L(x_0), x_0 ∈𝒳_0^max. Let x'_k+1= f(x'_k,u_k^ol,x_0,w_k), k=0,1,⋯,h^φ-1. It follows from monotonicity that x_k' ≼ x_k^ol,x_0, k=0,1,⋯,h^φ, ∀w[0:h^φ-1] ∈𝒲^h^φ. By the virtue of Lemma <ref>, x'[0:h^φ] ≼x^x_0,ol[0:h^φ]. Therefore, we have ∀ x_0 ∈𝒳_0^max, x'_0 ∈ L(x_0) ⇒ x'_0 ∈𝒳_0^max, which indicates 𝒳_0^max is a lower-set.  



If x_0 ∈𝒳_0^max and μ^ol is the following open-loop control policy

    μ^ol_t(x_0)=u^ol,x_0_t, t=0,1,⋯,h^φ-1,
 
then x(x'_0,μ,w)[0:h^φ] φ, ∀w∈𝒲^h^φ, ∀ x'_0 ∈ L(x_0).


Follows from the proof of Corollary <ref>.

Now that we have established the properties of the solutions to Problem <ref>, we explain how to compute the admissible initial conditions and their corresponding open-loop control sequences. The approach is based on formulating the conditions in Theorem <ref> as a set of constraints that can be incorporated into a feasibility solver. We convert all the constraints into a set of mixed-integer linear constraints and use off-the-shelf MILP solvers to check for feasibility. Converting logical properties into mixed-integer constraints is a common procedure which was employed for MLD systems in <cit.>. The authors in <cit.> and <cit.> extended this technique to a framework for time bounded model checking of temporal logic formulas. A  variation of this method is explained here. 






First, the STL formula is recursively translated into a set of mixed-integer constraints. For each predicate π=(a_π^T x ≤ b_π), as in (<ref>), we define a binary variable z^π_k ∈{0,1} such that 1 (respectively, 0) stands for true (respectively, false). The relation between  z^π, robustness ρ, and x is encoded as:



    a_π^Tx - M (1-z^π) + ρ≤ b_π,


    a_π^Tx + M z^π + ρ≥ b_π.


The constant M is a sufficiently large number such that M≥max{a_π^T K, b_π}, where K ∈ℝ^n_+ is the upper bound for the state values, x_k ≼ K, k =0,1,⋯,h^φ. 
In practice, M is chosen sufficiently large such that the constraint x ≼ K is never active. Note that the largest value of ρ for which z^π=1 is b_π-a^T_π x, which is equal to the robustness of π. 

Now we encode the truth table relations. For instance, we desire to capture  1 ∧ 0=0 and 1 ∨ 0=1 using mixed-integer linear equations. Disjunction and conjunction connectives are encoded as the following  constraints:



    z= ⋀_i=1^n_z z_i  ⇒   z ≤ z_i, i=1,⋯,n_z,


    z= ⋁_i=1^n_z z_i  ⇒   z ≤∑_i=1^n_z z_i,


where z ∈ [0,1] is declared as a continuous variables. However, it only can take binary values as evident from (<ref>). 
Similarly, define z^φ_k ∈ [0,1] as the variable indicating whether x[k] φ. An STL formula is recursively translated as:






















    [                                    φ= ⋀_i=1^n_φφ_i  ⇒                             z^φ_k= ⋀_i=1^n_φ z^φ_i_k,;                                    φ= ⋁_i=1^n_φφ_i  ⇒                             z^φ_k= ⋁_i=1^n_φ z^φ_i_k,;                                            φ = G_I ψ⇒                             z^φ_k = ⋀_k^'∈ I z^ψ_k^',;                                            φ = F_I ψ⇒                             z^φ_k = ⋁_k^'∈ I z^ψ_k^',;                                   φ = ψ_1  U_I ψ_2  ⇒ z^φ_k =  ⋁_k^'∈ I ( z^ψ_2_k'∧⋀_k”∈ [k,k^'] z^ψ_1_k”). ]

Finally, we add the following constraints:

    z^φ_0=1, ρ≥ 0.
 


The set of constraints in (<ref>),(<ref>),(<ref>),(<ref>) has the following properties: 


  i) we have x[0] φ if the set of constraints is feasible;

  ii) we have x[0] φ if the set of constraints is infeasible;

  iii) the largest ρ such that the set of constraints, while “ρ≥ 0" is removed from (<ref>), is feasible is equal to ρ(x,φ,0). 
 


i) We provide the proof for (<ref>), as the case for more complex STL formulas are followed in a recursive manner from (<ref>). If z=1, we have from (<ref>) that z_i=1, i=1,⋯,n_z, which correctly encodes conjunctions.  Similarly, z=1 in (<ref>) indicates that not all z_i,i=0,⋯,n_z can be zero, or, ∃ i ∈{1,⋯,n_z } such that z_i=1, which correctly encodes disjunctions. ii) Infeasibility can be recursively traced back into (<ref>). For both (<ref>) and (<ref>), if z=1 is infeasible, it indicates that z_i=0, i=1,⋯,n_z.  iii) We also prove this statement for (<ref>) as it is the base of recursion for general STL formulas. Let z_i=(a^T_π_i x + ρ≤ b_π_i), i=1,⋯,n_z. 
Consider (<ref>) and the following optimization problem:

    [                    ρ^max= argmax                               ρ,;                             s.t. a^T_π_i x + ρ≤ b_π_i, i=1,⋯,n_z, ]

where its solution is i=1,⋯, n_zmin(b_π_i-a^T_π_i x), which is identical to the quantitative semantics for conjunction (see (<ref>)). Similarly, consider (<ref>) and the following optimization problem:   

    [                         ρ^max= argmax                                    ρ,;                                  s.t. ∃ i ∈{1,⋯,n_z}, a^T_π_i x + ρ≤ b_π_i, ]
 
where the solution is i=1,⋯, n_zmax(b_π_i-a^T_π_i x), which is identical to the quantitative semantics for disjunction.    


Our integer formulation for Boolean connectives slightly differs from the formulation in <cit.>, <cit.>, where lower bound constraints for the z's are required. For example, for translating z= ⋀_i=1^n_zz_i, it is required to add z≥∑_i=1^n_z z_i - n_z + 1 to impose a lower bound for z. However, these additional constraints become necessary only when the negation operator is present in the STL formula. Hence, they are removed in our formulation. This reduces the constraint redundancy and degeneracy of the problem. By doing so, we observed computation speed gains (up to reducing the computation time by 50%) in our case studies. Moreover, we encode quantitative semantics in a different way than <cit.>, where a separate STL robustness-based encoding is developed which introduces additional integers. 
Due to property “iii" in Proposition <ref>, our encoding does not require additional integers to capture robustness hence it is computationally more efficient.     

 


System (<ref>) is in MLD form <cit.> if written as:



    x_t+1 = A x_t + B_u u_t + B_w w_t + D_δδ_t + D_r r_t,


    E_δδ_t + E_r r_t ≼ E_x x_t  +E_u u_t + E_w w_t + e,


where δ_t ∈{0,1}^n_δ and r_t ∈ℝ^n_r are auxiliary variables and A,B_u,B_w,D_δ, D_r, E_δ, E_r, E_x, E_u, E_w, e are appropriately defined constant matrices such that (<ref>) is well-posed in the sense that given x_t,u_t,w_t, the feasible set for x_t+1 is a single point  equal to f(x_t,u_t,w_t). Introducing auxiliary variables and enforcing (<ref>) can capture nonlinear f <cit.>.  

The system equations are brought into mixed-integer linear constraints by transforming system (<ref>) into its MLD form. 
As mentioned earlier, any piecewise affine system can be transformed into an MLD. In the case studies of this paper, the construction of (<ref>) from a piecewise affine (<ref>) is not explained as the procedure is well documented in <cit.>.  

Finally, the set of constraints in Theorem <ref> can be cast as:

    {[                          x_0^ol,x_0=x_0,                       Initial condition;; x_k+1^ol,x_0=f^*(x_k^ol,x_0,u_k^ol,x_0),                      System constraints;;         z^π_k = (a_π^T x_k^ol,x_0≤ b_π),                              Predicates;;                           z^φ_0=1, ρ≥ 0,                        STL satisfaction.;                                          ].

 
 

Checking the satisfaction of the set of  constraints in (<ref>) can be formulated as a MILP feasibility problem, which is handled using powerful off-the-shelf solvers. For a fixed initial condition x_0, the feasibility of the MILP indicates whether x_0 ∈𝒳_o^max.  An explicit representation of 𝒳_o^max requires variable elimination from (<ref>), which is computationally intractable for a large MILP. 
Alternatively, we can set x_0 as a free variable while maximizing a cost function (e.g. norm of x_0) such that a large L(x_0) is obtained. Another natural candidate is maximizing ρ(x^ol,x_0,φ,0). It is worth to note that by finding a set of distinct initial conditions and taking the union of all L(x_0), we are able to find a representation for an under-approximation of 𝒳_o^max. 

MILPs are NP-complete. The complexity of solving (<ref>) grows exponentially with respect to the number of binary variables and polynomially with respect to the number of continuos variables. The number of binary variables in our framework is 𝒪 ( h^φ(n_π+m_b+q_b+n_δ) ) - n_π is the number of predicates - and the number of continuous variables is 𝒪( h^φ(n+m_r+q_r+n_r) ).  
In other words, the exponential growth builds upon the intricacy of the specification and the number of modes demonstrated by the hybrid nature of the system. However, the complexity is polynomial with respect to the dimension of the state.      



Consider the following switched system:

    x^+=e^A_uτx + A_u^-1(I-e^-A_uτ)w,

where x=(x_[1],x_[2])^T ∈ℝ_+^2, u∈𝒰 is the control input (switch), 𝒰={1,2}, and

    A_1= ( [  1  1;  1 -5 ] )
    , A_2=  ( [ -8  1;  1  2 ] ).

The (additive) disturbance w is bounded to L(w^*), where w^*=(1.5,1)^T and τ=0.1. This system is the discrete-time version of ẋ=A_u x +w with sample time τ. Both matrices are Metzler (all off-diagonal terms are non-negative hence all the elements of its exponential are positive)  and non-Hurwitz hence constant input results in unbounded trajectories.
The system is desired to satisfy the  following STL formula:

    φ= ⋁_T=0^10(F_[0,T] p_1 ∧F_{T} p_2),

where p_1= ((x_[1]≤ 1) ∧ (x_[2]≤ 5)) and p_2= ((x_[1]≤ 5) ∧ (x_[2]≤ 1)). In plain English, φ states that “within 10 time units, the trajectory visits the box characterized by p_1 first and then the box corresponding to p_2" (see Fig. <ref>).
We transformed this system into its MLD form (<ref>). We formulated the constraints in (<ref>)  as a MILP and set the cost function to maximize x_0 _∞ and used the Gurobi [] MILP solver. The solution was obtained in less than 0.05 seconds on a 3GHz Dual Core MacBook Pro. 
We obtained x_0=(2.82 2.82)^T and the following open-loop control sequence: 1 2 1 2 2 1 1 1 1 1.   By applying this control sequence, we sampled a trajectory of the original system  f with values of w drawn from a uniform distribution over L(w^*). Both the trajectories of f and f^* satisfy the specification. The results are shown in Fig. <ref>. 



            







































§ INFINITE HORIZON SEMANTICS



In this section, we provide a solution to Problem <ref>. We show that the infinite-time property in (<ref>) can be guaranteed using repetitive control sequences. First, we consider global specifications and extend the results from our previous work <cit.> in Sec. <ref>.
Next, we show how to find controls for bounded-global STL formulas (Problem <ref>) in Sec. <ref>. Solution completeness is discussed in Sec. <ref>.





 §.§ Global formulas: s-sequences and inductive invariance




Consider the global specification G_[0,∞]φ, where φ is a bounded formula. We introduce some additional notation. 



Given a bounded STL formula φ over predicates in the form (<ref>), the language realization set (LRS) <cit.> is:

    ℒ^φ:={x_0x_1⋯ x_h^φ∈𝒳^h^φ | x_0x_1⋯ x_h^φφ}.




The set ℒ^φ is a lower-set.


For all x_0x_1⋯ x_h^φ∈ℒ^φ and x'_0x'_1⋯ x'_h^φ≼ x_0x_1⋯ x_h^φ, it follows from Lemma <ref> that x'_0x'_1⋯ x'_h^φφ. Thus, x'_0x'_1⋯ x'_h^φ∈ LRS(φ) hence LRS(φ) is a lower set. 



It follows from the semantics of global operator in (<ref>) that xG_[0,∞]φ is equivalent to x[t:t+h^φ] ∈ℒ^φ, ∀ t ∈ℕ. 

 
A set Ω_ℒ^φ⊆ℒ^φ is a robust control invariant (RCI) set if: 

    [          ∀  x_0x_1⋯ x_h^φ∈Ω_ℒ^φ, ∃ u ∈𝒰,  s.t.; x_1 x_2 ⋯ x_h^φ  f(x_h^φ,u,w)  ∈Ω_ℒ^φ, ∀ w ∈𝒲. ]


Satisfaction of G_[0,∞]φ is accomplished by finding a RCI set in ℒ^φ. 

Note that unlike traditional definitions of RCI sets (e.g., <cit.>), where the set is defined in the state-space 𝒳, our RCI set is defined in an augmented form of the state-space 𝒳^h^φ. The language realization set can also be interpreted as the “safe" set in (h^φ+1)-length trajectory space.  
The maximal RCI set inside ℒ^φ provides a complete solution to the set-invariance problem. The computation of maximal RCI set requires implementing an iterative fixed-point algorithm which is computationally intensive for MLD systems and non-convex sets (see <cit.> for discussion). We use monotonicity to provide an alternative approach. The following result is a more general version of the one in <cit.>. 





Given a bounded formula φ, if there exists x^s[0:h^φ] ∈ℒ^φ, and a sequence of controls: u^s_0,⋯,u^s_T-1 - where T is a positive integer determining the length of the sequence - such that:


  * x^s[k:k+h^φ] ∈ℒ^φ, k=0,1,⋯,T, where x^s_h^φ+k+1=f^*(x^s_h^φ+k,u^s_k),

  * x^s[T:T+h^φ] ≼x^s[0:h^φ],  

then the following set is a RCI set in ℒ^φ:

    Ω_ℒ^φ:= ⋃_k=0^T-1 L(x^s[k:k+h^φ]).

 





For any x'_0x'_1⋯ x'_h^φ∈Ω_ℒ^φ, there exists i ∈{0,1⋯,T-1} such that x'_0x'_1⋯ x'_h^φ∈ L(x^s[i:i+h^φ]). 
On one hand, we have x_i+1^s⋯ x_i+h^φ^sf^*(x_i+h^φ^s,u_i^s) ∈Ω_ℒ^φ. On the other hand, we have x'_1 ≼ x_i+1^s,⋯, x'_h^φ≼ x_i+h^φ^s. By applying u_i^s, monotonicity implies 

    [                                                                f(x'_h^φ,u_i^s,w) ≼ f^*(x_i+h^φ^s,u_i^s) = x_i+1+h^φ^s, ∀ w ∈𝒲;                                                              ⇒                        x'_1 x'_2 ⋯ x'_h^φ  f(x'_h^φ,u_i^s,w) ∈;                                                                                      L(x_i+1^s x_i+2^s⋯ x_i+1+h^φ^s)),∀ w ∈𝒲. ]

And the proof is complete from the fact that x_i+1^s⋯ x_i+1+h^φ^s∈Ω_ℒ^φ for all i ∈{0,1⋯,T-1}.  



Let the conditions in Theorem <ref> hold and x[t_0:t_0+h^φ] ∈ L(x^s[0:h^φ]) for some t_0 ∈ℕ. Consider the following control sequence starting from time t_0+h^φ:

    u^s:=(u^s_0 u^s_1 ⋯ u^s_T-1)^ω,

i.e., u^s_t=u^s_(t-t_0-h^φ,T), t≥ t_0+h^φ. Let x_k+1=f^*(x_k,u_k), k=t_0+h^φ,⋯. Then we have x[t:t+h^φ] ∈Ω_ℒ^φ, ∀ t≥ t_0.


We prove by induction that x[t:t+h^φ] ∈ L(x^s[(t-t_0,T):(t-t_0,T)+h^φ]), ∀ t≥ t_0. The base case for t=t_0 is true. In order to prove the inductive step x[t+1:t+1+h^φ] ∈ L(x^s[(t+1-t_0,T):(t+1-t_0,T)+h^φ]), we need to prove that x_t+k+1≼ x^s_(t+1-t_0,T)+k, k=0,⋯,h^φ, for which we need to only prove the case for k=h^φ as previous inequalities are already assumed by induction.   
We show x_t+h^φ+1≼ x^s_(t+1-t_0,T)+h^φ through monotonicity and the induction assumption that x_t+h^φ≼ x^s_(t-t_0,T)+h^φ:

    [                                   x_t+h^φ+1               =f^*( x_t+h^φ,u^s_(t-t_0,T) );                                                ≼ f^*( x^s_(t-t_0,T)+h^φ ,u^s_(t-t_0,T));                                             = x^s_(t-t_0,T)+1+h^φ≼ x^s_(t+1-t_0,T)+h^φ. ]


Note that x^s_T+h^φ≼ x^s_h^φ. The “≼" in the last line can be replaced by “=" when (t-t_0,T)+1 ≠ T. 




We refer to the repetitive sequence of controls in (<ref>) as an s-sequence. An s-sequence is an invariance inducing open-loop control policy.   
Once the latest h^φ+1-length of system state are brought into Ω_ℒ^φ, an s-sequence keeps the h^φ+1-length trajectory of the system in Ω_ℒ^φ for all subsequent times. 
 



The computation of an s-sequence requires solving an MILP for x^s[h^φ:T] G_[0,T]φ (an instance of Problem <ref>) with an additional set of constraints in  x^s[0:h^φ] φ (again, an instance of Problem <ref>, but without the dynamical constraints. In other words, x^s[0:h^φ] does not need to be a trajectory of the maximal system), and x^s[T:T+h^φ] ≼x^s[0:h^φ] (linear constraints). We are usually interested in the shortest s-sequence since its computation requires the smallest MILP. Algorithmically, we start from T=1 and implement T T+1 until the MILP formulating the conditions in Theorem <ref> becomes feasible and an s-sequence is found. As it will be implied from results in Sec. <ref>, existence of an s-sequence is almost necessary for existence of a RCI set. 




Consider the system in Example <ref>. We wish to keep the trajectory in the set characterized by p_1 ∨ p_2, i.e., 𝒮=L((1,5)^T) ) ∪ L((5,1)^T) ). Note that this set is non-convex. We set the cost function to maximize x_0_1. The shortest s-sequence has T=5 and is: (2 1 2 1 1)^ω. The resulting trajectory satisfying the definition of s-sequence is shown in Fig. <ref> (a). The corresponding robust control invariant set is shown in Fig. <ref>. (b) (cyan region), which is characterized by the x^s_0,x^s_1,⋯,x^s_4 (red dots) that lie inside 𝒮 (green region). Note that the [0,2]×[0,2] portion of the coordinates in Fig. <ref> is shown here for a clearer representation of the details. 


 



 §.§ Bounded-global specifications: ϕ-sequences


Now we consider general bounded-global formulas - as in Problem <ref> - and generalize the paradigm used for s-sequences. We provide the key result of this section.






Given a bounded-global STL formula ϕ=φ_b ∧G_[Δ,∞]φ_g, an initial condition x_0, a control sequence u_0^ϕ⋯ u_Δ+T+h^φ_g-1^ϕ, where T is a positive integer, and a non-negative integer T_0 < T, let the following conditions hold:


  * x^ϕ[0:Δ+T+h^φ_g] φ_b ∧G_[Δ,Δ+T]φ_g,

  * x^ϕ[Δ+T:Δ+T+h^φ_g] ≼x^ϕ[Δ+T_0:Δ+T_0+h^φ_g]; 

where x_k+1^ϕ=f^*(x_k^ϕ,u_k^ϕ), k ∈ [0,Δ+T+h^φ_g-1], x_0^ϕ=x_0. Let μ^ol be the open-loop  control policy  corresponding  to the following control sequence:

    u^ϕ:=u_0^ϕ⋯ u_Δ+T_0+h^φ_g-1^ϕ(u_Δ+T_0+h^φ_g^ϕ⋯ u_Δ+T+h^φ_g-1^ϕ)^ω,

Then x(x'_0,μ^ol,w) ϕ, ∀w∈𝒲^ω, ∀ x'_0 ∈ L(x_0). Moreover, the following set is a RCI set in ℒ^φ_g:

    Ω_ℒ^φ_g:= ⋃_i=0^T-T_0-1 L(x^ϕ[Δ+T_0+i:Δ+T_0+h^φ_g+i]).



We need to prove that x(x^ϕ_0,μ^ol,w^*) ϕ, where w^*=(w^*)^ω. 
The fact that x(x'_0,μ^ol,w)[0] ϕ, ∀ x'_0 ∈ L(x_0), ∀w∈𝒲^ω, follows from monotonicity and Lemma <ref>. 
The fact that Ω_ℒ^φ_g is a RCI set follows from Theorem <ref> as (<ref>) is obtained from replacing Δ=T_0=0 in (<ref>) . It follows that (u_Δ+T_0+h^φ_g^ϕ⋯ u_Δ+T+h^φ_g-1^ϕ)^ω is an s-sequence. 
For all t≥Δ + T + h^φ_g, let

    x^ϕ_t+1=f^*(x_t^ϕ,u^ϕ_Δ+T_0+h^φ_g+(t-Δ-T_0-h^φ_g,T-T_0)).

Using Corollary <ref>, we have 
x^ϕ[k+Δ+T_0:k+Δ+T_0+h^φ_g] ∈ℒ^φ_g, ∀ k ∈ℕ, and the proof is complete. 
 









We refer to the sequence of controls in (<ref>) as a ϕ-sequence. The computation of a ϕ-sequence requires solving an MILP for x^ϕ[0:Δ+T+h^φ_g] φ_b ∧G_[Δ,Δ+T]φ_g (an instance of Problem <ref>) with an additional set of constraints in  x^ϕ[Δ+T:Δ+T+h^φ_g] ≼x^ϕ[Δ+T_0:Δ+T_0+h^φ_g] (linear constraints). Thus, similar to s-sequecnes, the computation of a ϕ-sequence is based on feasibility checking of a MILP. We have two parameters T and T_0 < T to search over. We start from T=1 and implement T T+1, while checking for all T_0 < T, until the corresponding MILP gets feasible. In Sec. <ref>, we discuss the necessity of existence of a feasible solution for some T_0,T. 


Another interpretation of a ϕ-sequence is a sequence that consists of an initialization segment of length Δ+h^φ_g to bring the latest h^φ_g states of the system into Ω_ℒ^φ_g⊆ℒ^φ_g and a repetitive segment of length T to stay in Ω_ℒ^φ_g. The repetitive segment is an s-sequence. 
Since control inputs eventually becoming periodic, the long-term behavior is expected to demonstrate periodicity, which leads to the following result based on Theorem <ref>.



The ω-limit set of the run given by (<ref>) is non-empty and corresponds to the following periodical orbit:

    (x_0^ϕ,∞ x_1^ϕ,∞⋯ x_T-T_0-1^ϕ,∞)^ω,

where
x_k^ϕ,∞:= lim_c →∞ x_k+Δ+T_0+c(T-T_0)^ϕ, k=0,⋯,T-T_0-1.

 

We show that x^ϕ_t≼ x^ϕ_t+T-T_0, ∀ t ≥Δ+T_0. Similar to the proof of Corollary <ref>, we use induction. The base case for t=Δ+T_0 is already in the second condition in Theorem <ref>. The inductive step is proven as follows:

    x^ϕ_t+1+T-T_0 =f^*( x^ϕ_t+T-T_0,u_T-T_0+t ) ≼ f^*( x^ϕ_t,u_t)=  x^ϕ_t+1,

where from (<ref>) we have 

    u_t+T-T_0=u_t=u^ϕ_t+Δ+T_0+h^φ_g+(t-Δ-T_0-h^φ_g,T-T_0).
 Thus, each component of the sequence x^ϕ_Δ+T_0+kx^ϕ_Δ+T+k x^ϕ_Δ+2T-T_0+k⋯, k=0,⋯,T-T_0, is monotonically decreasing. 
Monotone convergence theorem <cit.> explains that a lower-bounded monotonically decreasing sequence converges (in this case, all values are lower-bounded by zero). Thus, lim_c→∞ x_Δ+T_0+k+c(T-T_0)^ϕ, k=0,⋯,T-T_0, exists and the proof is complete. 






Consider the system in Example <ref>. We wish to satisfy 

    ϕ= F_[0,5] p_1 ∧ G_[5,∞)(
    F_[0,6] p_1 ∧ F_[0,6] p_2 ).

The specification is in form in (<ref>) with h^φ_b=Δ=5,h^φ_g=6. 
This specification requires that p_1 is visited at least once until t=5 and, afterwards, p_1 and p_2 are persistently visited while the maximum time between two subsequent visits is not greater than 6. We find a ϕ-sequence solving a MILP for T=7, T_0=0, while maximizing x_0 _1. The obtained ϕ-sequence is 
u^ϕ=2 2 2 2 1 2 1 1 1 1 2 (2  2  1  1  1  1  2)^ω for x_0=(12.4,0)^T. The first Δ+T+h^φ_g+1=5+7+6+1=19 time points of the trajectory of the maximal system f^* satisfying the conditions in Theorem <ref> are shown in  Fig. <ref> [Left]. A sample trajectory of f with values of w chosen uniformly from 𝒲 is also shown. Both trajectories satisfy ϕ. The limit-set of f^*, which is a 7-periodical orbit, is shown in Fig. <ref> [Right].  

 






 §.§ Necessity of Open-loop Strategies


We showed that if there exists an initial condition and a finite length control sequence such that the statements in Theorem <ref> hold, an open-loop control sequence is sufficient for satisfying of a bounded-global formula, as was formulated in Problem <ref>. In this section, we address the necessity conditions.
 
We show that the existence of open-loop control strategies for satisfying a bounded-global specifications is almost necessary in the sense that if a ϕ-sequence is not found using Theorem <ref> for large values of T, then it is almost certain that no correct control policy (including feedback policies) exists, or, if exists any, it is fragile in the sense that a slight increase in the effect of the disturbances makes the policy invalid. We characterize the necessity conditions based on hypothetical perturbations in the disturbance set. 




Suppose system (<ref>) is strongly monotone with respect to the maximal disturbance in the sense that for all ϵ>0, there exists a perturbed disturbance set 𝒲_p with maximal disturbance w^*_p such that 

    ∀ x ∈𝒳, ∀ u ∈𝒰, f(x,u,w^*) + 1_n ϵ≼ f(x,u,w_p^*).

Consider the bounded-global formula ϕ=φ_b ∧G_[Δ,∞]φ. Given ϵ>0, the disturbance set is altered to 𝒲_p such that (<ref>) holds. If there exists a control policy μ and an initial condition x_0 such that x(x_0,μ,w_p) ϕ, ∀w_p ∈𝒲_p^ω, then there exists at least one open-loop control policy μ^ol in the form of a ϕ-sequence in (<ref>) for the original system such that

    T ≤A/ϵ^n(h^φ_g+1),

where A is a constant depending on ℒ^φ_g. 


Given a bounded set 𝒞⊂ℝ^n(h^φ+1), we define the diameter d(𝒞):= inf{ d |s_1≼ s_2+d1_n(h^φ+1), ∀ s_1,s_2 ∈𝒞} (e.g., the diameter of an axis-aligned hyper-box is equal to the length of its largest side). 
Consider a partition of ℒ^φ by a finite number of cells, where the diameter of each cell is less than ϵ. The maximum number of cells required for such a partition is A/ϵ^n(h^φ_g+1), where A is a constant dependent on the shape and volume of ℒ^φ_g. A conservative upper bound on A can be given as follows. Define a^*∈ℝ_+ as

    _a/ϵ∈ℕ{x[0:h^φ_g] ≼ a 1_n[0:h^φ_g], ∀x[0:h^φ_g] ∈ℒ^φ_g}.
 

Since ℒ^φ_g is bounded and closed, a^* exists. We have ℒ^φ_g⊆ L(a^* 1_n(h^φ_g+1)). Let A be a^*^n(h^φ_g+1) - the volume of L(a^* 1_n(h^φ_g+1)), which is a hyper-box. 
Partition L(a^* 1_n(h^φ_g+1)) into N:=A/ϵ^n(h^φ_g+1) number of equally sized cubic cells with side length of ϵ. Such a partition also partitions ℒ^φ_g to at most N number of cells where the diameter of each cell is not greater than ϵ. 

Since there exists μ such that x(x_0,μ,w_p) ϕ, ∀w_p ∈𝒲_p^ω, then there exist at least one run satisfying ϕ for system x_k+1=f(x_k,u_k,w_p^*). Let x_0,⋯, x_Δ+h^φ_g+N be the first Δ+h^φ_g+N+1 time points of a such a run. We have x[k:k+h^φ_g] ∈ℒ^φ_g, k=Δ,⋯,Δ+N. Consider the sequence x[Δ:Δ+h^φ_g] x[Δ+1:Δ+1+h^φ_g] ⋯x[Δ+N:Δ+N+h^φ_g]. 
Consider a partition of ℒ^φ_g with cells that for all cells the diameter is less than ϵ. By the virtue of pigeonhole principle, there exists a cell that contains at least two time points x[k_1:k_1+h^φ_g] and x[k_2:k_2+h^φ_g], Δ≤ k_1 ≤ k_2≤Δ+N. From the assumption on the diameter of the cells we have 

    x[k_2:k_2+h^φ_g] ≼x[k_1:k_1+h^φ_g] + ϵ1_n[0:h^φ_g].
 

Now consider system x'_k+1=f(x'_k,u_k,w^*) - the original maximal system - with x'_k_1+h^φ_g=x_k_1+h^φ_g. We prove that 

    x'_k + 1_n ϵ≤ x_k, ∀ k> k_1+h^φ_g.

We use induction. The base case for k=k_1+h^φ_g+1 is verified using (<ref>): 

    [              x'_k_1+1+h^φ_g + 1_n ϵ  = f(x'_k_1+h^φ_g,u_k_1+h^φ_g,w^*) +1_n ϵ;                                      ≤      f(x'_k_1+h^φ_g,u_k_1+h^φ_g,w_p^*);                                      =                         x_k_1+1+h^φ_g. ]

The inductive step is verified using monotonicity and (<ref>): 

    [                      x'_k+1+h^φ_g+ 1_n ϵ  =          f(x'_k+h^φ_g,u_k+h^φ_g,w^*) +1_n ϵ;                                           ≤               f(x'_k+h^φ_g,u_k+h^φ_g,w_p^*);                                           ≤ f(x_k+h^φ_g,u_k+h^φ_g,w_p^*) = x_k+1+h^φ_g. ]

It immediately follows from (<ref>) that 

    x'[k_2:k_2+h^φ_g] + ϵ1_n[0:h^φ_g] ≤x[k_2:k_2+h^φ_g].

Since the lefthand of (<ref>) is the righthand of (<ref>), we have:

    x'[k_2:k_2+h^φ_g] ≤x[k_1:k_1+h^φ_g].

This is reminiscent of the conditions in Theorem <ref>. Now by defining x'_k:=x_k, k=k_1,⋯,k_1+h^φ_g-1, we conclude that  

    Ω'_ℒ^φ_g:= ⋃_k=k_1^k_2-1 L(x'[k:k+h^φ])

is a RCI set for system with adversarial disturbance set 𝒲 and (u_k_1⋯ u_k_2+h^φ_g-1)^ω is an s-sequence.   
 
Now, once again, consider the original system x'_k+1=f(x'_k,u_k,w^*) with x'_0=x_0. Monotonicity implies x'[0:k_1+h^φ_g] ≤x[0:k_1+h^φ_g]. Thus, by applying u_0,⋯,u_k_1+h^φ_g-1 and using Lemma <ref>, we have x'[0:k_1+h^φ_g] φ_b ∧G_[Δ,k_1]φ_g. Corollary <ref> implies x'[k_1+h^φ_g] G_[0,∞)φ_g if (u_k_1,⋯,u_k_2-1)^ω is applied starting from time k_1. Finally, monotonicity and  Lemma <ref> immediately indicate that x(x”_0,μ^ol,w) ϕ, ∀ x”_0 ∈ L(x_0), ∀w∈𝒲^ω, where μ^ol is the following open-loop control strategy producing the following control sequence:

    u_0⋯ u_k_1-1 (u_k_1⋯ u_k_2+h^φ_g-1)^ω,
 
which is in form of (<ref>) with k_1=Δ+T_0+h^φ_g and k_2=Δ+T. Since k_2 ≤Δ+N, we also have T ≤ N, N=A/ϵ^n(h^φ_g+1), and the proof is complete.    
 






Suppose that for all T ≤ T^max, T_0 < T, there does not exist an initial condition and a control sequence such that the conditions in  Theorem <ref> hold. Then there does not exist any solution to Problem <ref> given that the maximal disturbance is w_p^* such that (<ref>) holds with ϵ > √(T^max).  



The relation between the fragility in Theorem <ref> and the length of the ϕ-sequence suggests that by performing the search for longer ϕ-sequences (which are computationally more difficult), the bound for fragility becomes smaller, implying that a correct control policy (if exists) is close to the limits (i.e., robustness score is close to zero, or the constraints are barely satisfied in the case with maximal disturbance). In practice, the bounds in Theorem <ref> are very conservative and one may desire to find tighter bounds for specific applications. 



Consider Example <ref>. Suppose that there does not exist an s-sequence of length smaller than 144 with maximal disturbance w^*. The constant A (area in this 2D case, see proof of Theorem <ref>) of region corresponding to p_1 ∨ p_2 is 9. Therefore, 𝒮 can be partitioned into 144 equally sized square cells with side length 0.25. Note that we have ϵ^2≥ 9/T. Since the disturbances are additive, it follows that if A_u^-1(I-e^-A_u t)(w^*_p-w^*) > (0.25,0.25)^T, u=1,2, then there does not exist any control strategy μ and x_0 ∈ℝ_+^n such that x(x_0,μ,w_p) G_[0,∞](x ∈𝒮),∀w_p ∈𝒲_p^ω.
 









§ MODEL PREDICTIVE CONTROL


In this section, we provide a solution to Problem <ref>. We assume full knowledge of the history of state. As mentioned in Sec. <ref>, the cost function J is assumed to be non-decreasing with respect to the state values hence the system constraints are replaced with those of the maximal system. First, we explain the MPC setup for global STL formulas. Next, we  prove that the proposed framework is guaranteed to generate runs that satisfy the global STL specification (<ref>).

Let t≥ h^φ-1. The case of t<h^φ-1 is explained later. 
Given planning horizon H, the states that are predictable at time t using controls in u^H_t are x_1|t,x_2|t,⋯,x_H|t. Given predictions x_1|t,x_2|t,⋯,x_H|t, we need to enforce x[t-h^φ+1,t+H] G_[0,H-1]φ at time t. Notice that 

    x_|t[t-h^φ+1,t+H]:=x_t-h^φ+1⋯ x_t x_1|t⋯ x_H|t,

i.e., the first h^φ time points are actual values, the rest are predictions. Also, note that the values in x[τ:τ+h^φ] are independent of the values in x_t^H for τ≤ t-h^φ and are not fully available for τ>t+H-h^φ. Thus, [t-h^φ+1,t+H-h^φ] is the time window for imposing constraints at time t <cit.>.  
 
  






  


The MPC optimization problem is initially written as (we do not use it for control synthesis as explained shortly): 

    [                             minimize                    J(x_t^H, u_t^H ),;                                 s.t. x_k+1|t=f^*(x_k|t,u_k|t), k=0,⋯,H-1,;                                             x_|t[t-h^φ+1,t+H] G_[0,H-1]φ. ]


The set of constraints in (<ref>) requires the knowledge of x_t-h^φ+1 x_t-h^φ+2⋯ x_t. Thus, the proposed control policy requires a finite memory for the history of last h^φ states. As it will be shown in Proposition <ref>, persistent feasibility of the constraints in (<ref>) leads to fulfilling G_[0,∞]φ.  However, persistent feasibility of the MPC setup in (<ref>) is not guaranteed. We address this issue for the remainder of this section. 
  




An MPC strategy is recursively feasible if, for all t ∈ℕ, the control at time t is selected such that the MPC optimization problem at t+1 becomes feasible.     


Our goal is to modify (<ref>) such that it becomes recursively feasible. 
It is known that adding a (the maximal) RCI set acting as a terminal constraint is sufficient (and necessary) to guarantee recursive feasibility <cit.>. We add the terminal constraint x [t+H-h^φ:t+H] ∈Ω_ℒ^φ to (<ref>) to obtain:

    [                         u^H,opt_t  =        u^H_t ∈𝒰^H  J(x_t^H, u_t^H ),;                                 s.t. x_k+1|t=f^*(x_k|t,u_k|t), k=0,⋯,H-1,;                                             x_|t[t-h^φ+1,t+H] G_[0,H-1]φ,;                                                x_|t [t+H-h^φ:t+H] ∈Ω_ℒ^φ. ]





Let μ_t(x_0,⋯,x_t)=μ_t(x_t-h^φ+1,⋯,x_t)=u^H,opt_0|t, where u^H,opt=u^H,opt_0|t⋯ u^H,opt_H-1|t is given by (<ref>). If the optimization problem (<ref>) is feasible for all t ≥ h^φ-1, then x(x_0,μ,w)[0] G_[0,∞]φ, ∀w∈𝒲^ω.  


We show that x(x_0,μ,w)[0:k+h^φ] G_[0,k]φ, ∀w∈𝒲^*, ∀ k ∈ℕ, using induction over k. 
Consider (<ref>) for t=k+h^φ-1 for any k ∈ℕ. The second constraint in (<ref>) requires x_|t[k,k+h^φ] φ, or equivalently, x_k ⋯ x_k+h^φ-1 x_1|k+h^φ-1φ. By applying u^opt_0|t, monotonicity implies 
x_k+h^φ=f(x_k+h^φ-1,u^opt_0|t,w) ≼ x_1|k+h^φ-1 = f^*(x_k+h^φ-1,u^opt_0|t), ∀ w ∈𝒲. From Lemma <ref> we have x[k:k+h^φ] φ. Thus, we have shown x[k:k+h^φ] φ, ∀ k ∈ℕ, and the proof is complete.             




The MPC strategy corresponding to (<ref>) is recursively feasible. 


Suppose u_t^H=u_0|t⋯ u_H-1|t and x_t^H=x_t+1|t⋯,x_t+H-1|t is a feasible solution for (<ref>) at time t. Since Ω_ℒ^φ is a RCI set, there exist u^r∈𝒰 such that x_|t[t+H+1-h^φ:t+H+1]=x_H-h^φ+1|t x_H-h^φ+2|t⋯ x_H|t  f(x_H|t,u^r,w)  ∈Ω_ℒ^φ, ∀ w ∈𝒲. Suppose u_0|t is applied to the system. We have x_t+1=f(x_t,u_0|t,w) ≼ f^*(x_t,u_0|t)=x_1|t, ∀ w ∈𝒲. 

Now, we prove that the optimization problem at time t+1 is feasible by showing that at least one feasible solution exists. Let 
u^H_t+1=u_1|t u_2|t⋯,u_H|t u^r. We already showed that x_t+1=x_0|t+1≼ x_1|t. By induction and using monotonicity, it follows that x_k|t+1≼ x_k+1|t, k=,1,⋯,H-2.
Therefore, we have x_t-h^φ+2⋯ x_t+1 x_1|t+1⋯ x_H-1|t+1≼ x_t-h^φ+2⋯ x_1|t x_2|t⋯ x_H|t, which using Lemma <ref> establishes x_t-h^φ+2⋯ x_t+1 x_1|t+1⋯ x_H-1|t+1G_[0,H-1]φ. In order to complete the proof, it remains to show that x [t+H+1-h^φ:t+H+1]= x_H+1-h^φ|t⋯ x_H|t+1φ. This follows from invariance. Note that x_H|t+1=f^*(x_H|t,u^r). Therefore x_H+1-h^φ|t⋯⋯ x_H|t+1∈Ω_ℒ^φ, and since Ω_ℒ^φ∈ℒ^φ, we have x_H+1-h^φ|t⋯⋯ x_H|t+1φ, and the proof is complete. 


The MPC optimization problem is also converted into a MILP problem. It is computationally easier to solve  the optimization problem in (<ref>) by solving T MILPs:

    [                               u^opt,H_t =  u^H_t ∈𝒰^H,i=0,⋯,T-1   J(x_t^H, u_t^H ),;                                      s.t.      x_k+1|t=f^*(x_k|t,u_k|t), k=0,⋯,H-1,;                                                       x_|t[t-h^φ+1,t+H] G_[0,H-1]φ,;                                           x_|t [t+H-h^φ:t+H] ∈ L(x^φ,x_0[i:i+h^φ]). ]

Note that all MILPs can be aggregated into a single large MILP in the expense of additional constraints for capturing non-convexities of the terminal condition. 


Finally, consider t<h^φ. In this case, we require H≥ h^φ and replace the interval [t-h^φ+1,t+H-h^φ] with [0,t+H-h^φ]  for t<h^φ in (<ref>). 

For applications where initialization is not important in long-term (like traffic management), a simpler approach is to initialize the MPC from t=h^φ-1 and assume all previous state values are zero (hence all the past predicates are evaluated as true).  


In our previous work on STL MPC of linear systems <cit.>, we did not establish recursive feasibility. In order to recover from possible infeasibility issues, we proposed maximizing  the STL robustness score (a negative value) whenever the MPC optimization problem became infeasible. Although recursive feasibility is guaranteed here, un-modeled disturbances and initial conditions outside 𝒳_0^max can lead to infeasibility. The formalism in <cit.> can be used to recover from infeasibility with minimal violation of the specification.




§ APPLICATION TO TRAFFIC MANAGEMENT

In this section, we explain how to apply our methods to traffic management. First, the model that we use for traffic networks is explained, which is similar to the one in <cit.> but freeways are also modeled. Next, the monotonicity properties of the model are discussed. We show that there exists a congestion-free set in the state-space in which the traffic dynamics is monotone. Finally, a case study on a mixed urban and freeway network is presented. 




 §.§ Model

The topology of the network is described by a directed graph (𝒱,ℒ), where 𝒱 is the set of nodes and ℒ is the set of edges. Each l ∈ℒ represents a one-way traffic link from tail node τ(l) ∈𝒱∪∅ to head node η(l) ∈𝒱, where τ(l)=∅ stands for links originating from outside of the network. We distinguish between three types of links based on their control actuations: 1) ℒ_r: road links actuated by traffic lights, 2) ℒ_o: freeway on-ramps actuated by ramp meters, 3) ℒ_f: freeway segments which are not directly controlled.  Freeway off-ramps are treated the same way as the roads. Uncontrolled roads are also treated the same as freeways. We have ℒ_r ∪ℒ_o ∪ℒ_f=ℒ. 

Some works, e.g. <cit.>, consider control over freeway links by varying speed limits, which adds to the control power  but requires the existence of such a control architecture within the infrastructure. We do not consider this type of control actuation in this paper but it can easily be incorporated into our model by modeling freeways links the same way as on-ramps, where the speed limit becomes analogous to the ramp meter input.    

 
The number of vehicles on link l at time t is represented by x_[l],t∈ [0,c_l], which is assumed to be a continuous variable, and c_l is the capacity of l. In other words, vehicular movements are treated as fluid-like flow in our model. 
The number of vehicles that are able to flow out of l in one time step, if link l is actuated, is:

    q_[l],t:= min{x_[l],t, q̅_l, {l'  | τ(l')=η(l) }minα_l:l'/β_l:l' (c_l'-x_[l'],t) },
 
where q̅_l is the maximum outflow of link l in one time step, which is physically related to the speed of the vehicles. The last argument in the minimizer determines the minimum supply available in the downstream links of l, where α_l:l'∈ [0,1] is the capacity ratio of link l' available to vehicles arriving from  link l (typically portion of the lanes), β_l:l'∈ [0,1] is the ratio of the vehicles in l that flow into l' (turning ratio). For simplicity, we assume capacity ratios and turning ratios are constants. System state is represented by x ∈ℝ^n_+: {x_[l]}_l ∈ℒ,  where n is the number of the links in the network. The state space is
𝒳:=∏_l ∈ℒ [0,c_l].

A schematic diagram illustrating the behavior of q_[l] with respect to the state variables x_[l],x_[l']- which is known as the fundamental diagram in the traffic literature <cit.> - is shown in Fig. <ref>. The link flow drops if one (or more) of its downstream links do not have enough capacity to accommodate the incoming flow. In this case (when the last argument in (<ref>) is the minimizer), we say the traffic flow is congested. Otherwise, the traffic flow is free. 
This motivates the following definition:     

The congestion-free set, denoted by Π, is defined as the following region in the state space:

    [                                              Π:={ x∈𝒳 |min{x_[l],q̅_l}≤α_l:l'/β_l:l' (c_l'-x_[l']),;                                                                            ∀ l,l'∈ℒ, τ(l')=η(l)  }. ]



The congestion-free set is a lower-set.


Consider x ∈Π and any x'∈ L(x). For all l,l'∈ℒ, τ(l')=η(l), we have min{x'_l,q̅_l}≤min{x_[l],q̅_l} and  (c_l'-x_[l]') ≤ (c_l'-x'_l'). Therefore, min{x'_l,q̅_l}≤α_l:l'/β_l:l' (c_l'-x'_l'). Thus x'∈Π, which indicates Π is a lower-set. 

Note that Π is, in general, non-convex. The predicate (x ∈Π) can be written as a Boolean logic formula over predicates in the form of (<ref>) as:

    [ ⋀_l,l'∈ℒ, τ(l')=η(l) (  ( (x_[l]≤q̅_l) ∧ (x_[l]+ α_l:l'/β_l:l' x_[l]'≤α_l:l'/β_l:l' c_l')  );                                   ∨ 
     (q_[l]+ α_l:l'/β_l:l' x_[l]'≤α_l:l'/β_l:l' c_l')    ). ]

Notice how the minimizer in (<ref>) is translated to a disjunction in (<ref>).   








Now we explain the controls. The actuated flow of link l at time t is denoted by q⃗_[l],t, where we have the following relations:

    q⃗_[l],t= {[        s_[l],t q_[l],t,                 l ∈ℒ_r,; min{ q_[l],t, r_[l],t},                 l ∈ℒ_o,;                q_[l],t,                 l ∈ℒ_f,;                         ].

where s_[l],t∈{0,1} is the traffic light for link l, where 1 (respectively, 0) stands for green (respectively, red) light, and r_[l],t∈ℝ_+ is the ramp meter input for on-ramp l at time t. Ramp meter input limits the number of vehicles that are allowed to enter the freeway in one time step. 
In order to disallow simultaneous green lights for links l,l' (which are typically pair of links pointing toward a common intersection in perpendicular directions), we add the additional constraints  s_[l],t+s_[l]',t≤ 1. 





In simple gridded networks, as in our case study network illustrated in Fig. <ref>, it is more convenient to define phases for actuation in north-south or east-west directions that are unambiguously mapped to traffic lights for each individual link.
The evolution of the network is given by:

    x_[l],t+1=x_[l],t-q⃗_[l],t+w_[l],t+∑_l', η(l')=τ(l)β_l':lq⃗_[l'],t,
 
where w_[l],t is the number of exogenous vehicles entering link l at time t, which is viewed as the adversarial input.
The evolution relation above can be compacted into the form (<ref>):

    x_t+1=f_traffic(x_t,u_t,w_t),
 
where u_t and w_t are the vector representations for control inputs (combination of traffic lights and ramp meters) and disturbances inputs, respectively.  
Note that f_traffic represents a hybrid system which each mode is affine. The mode is determined by the control inputs and state (which determines the minimizer arguments).  
Some works consider nonlinear representations for the fundamental digram (Fig. <ref>), but they still can be approximated using piecewise affine functions.




 §.§ Monotonicity


System (<ref>) is monotone in Π.
  



Consider x',x ∈Π, x ≼ x'. We show that f_traffic(x,u,w) ≼ f_traffic(x',u,w), ∀ w ∈𝒲, ∀ u ∈𝒰. Observe in (<ref>) that we only need to verify is proving that x_[l]-q⃗_[l] is a non-decreasing function of x_[l] as all other terms are additive and non-decreasing with respect to x. Since x,x' ∈Π, the last argument in (<ref>) is never the minimizer. Thus, for all ł∈ℒ, we have x_[l]-q⃗_[l]∈{0, x_[l]-r_[l],x_[l]-c_l,x_[l]}, depending on the mode of the system and actuations, which all are non-decreasing functions of x_[l]. Thus, f_traffic is monotone in Π.   

The primary objective in our traffic management approach is finding control policies such that the state is restricted to Π, which not only eliminates congestion, but also ensures that the system is monotone hence the methods of this paper become applicable. It is  worth to note that the traffic system becomes non-monotone when flow is congested in diverging junctions, as shown in <cit.>. This phenomena is attributed to the first-in-first-out (FIFO) nature of the model.    
By assuming fully non-FIFO models, system becomes monotone in the whole state space. For a more thorough discussion on physical aspects of monotonicity in traffic networks, see <cit.>.

The maximal system in (<ref>) corresponds to the scenario where each w_l is equal to its maximum allowed value w_l^*. 










 §.§ Case Study




  §.§.§ Network


Consider the network in Fig. <ref>, which consists of urban roads (links 1-26, 27,29,31,33 and 49-53), freeway segments (links 35-48) and freeway on-ramps (links 28,30,32,34). The layout of the network illustrates a freeway passing by an urban area, which is common in many realistic traffic layouts. There are 14 intersections (nodes a-n) controlled by traffic lights. Each intersection has two modes of actuation: north-south (NS) and east-west (EW). There are four entries to the freeway (nodes o-r) that are regulated by ramp meters. We have n=53 and 𝒰=ℝ_+^4 ×{0,1}^14. Vehicles arrive from links 1,6,11,15,19,23,35,42,49 and 52. The parameters of the network are shown in Table <ref>.   
 
 
 
 







  §.§.§ Specification

As mentioned earlier, the primary objective is keeping the state in the congestion-free set. In addition, since the demand for the north-south side roads (links 49-53) is smaller than the traffic in the east-west roads, we add a timed liveness requirement for the traffic flow on links 49-53:

    ψ= ⋀_l=49,50,⋯,53 (x_[l]≥ 5) ⇒F_[0,3] (x_[l]≤ 5),

which states that “if the number of vehicles on any of the north-south side roads exceeds 5, their flow is eventually actuated within three time units ahead".  
The global specification is given as:

    ϕ=G_[0,∞] ( (x∈Π) ∧ψ).

Note that h^φ=3, φ=(x∈Π) ∧ψ. 







  §.§.§ Open-loop Control Policy

We use Theorem <ref>. The shortest ϕ-sequence that we found for this problem has T=5, T_0=0. The corresponding MILP had 2357 variables (of which 1061 were binary) and 4037 constraints [The scripts for this case study are available in ], which is solved using the Gurobi MILP solver in less than 6 seconds on a dual core 3.0 GHz MacBook Pro. The cost is set to zero in order to just check for feasibility. Even though finding an optimal solution and checking for feasibility of a MILP have the same theoretical complexity, the latter is executed much faster in practice. For instance, finding a ϕ-sequence, while minimizing or maximizing ∑_k=0^7x^ϕ_k_1 both took more than 20 minutes. Note that it is virtually intractable to attack a problem of this size (53 dimensional state) using any method that involves state-space discretization, such as the method in <cit.> (e.g., if each state-component is partitioned into 2 intervals, the finite-state problem size will be 2^53).    






Monotonicity implies that any demand set 𝒲 for which there exists a solution to Problem <ref> is a lower-set. The set corresponding to the values at the bottom of Table <ref> is one of them. Table <ref> shows results on existence of ϕ-sequences for some other demand scenarios. Computation times for solving a MILP do not demonstrate a generic behavior. For the rest of this section, the numerical examples are reported for the values in Table <ref>.    





The control values in the ϕ-sequence are shown in Table <ref>. As stated in Theorem <ref>, starting from an initial condition in L(x_0), applying the open-loop control policy (<ref>) guarantees satisfaction of the specification. 
In other words, after applying the initialization segment, the repetitive controls in Table <ref> become a fixed time-table for the inputs of the traffic lights and the ramp meters. Starting from x_0, which is a 53-dimensional vector, we apply (<ref>) using the values in Table <ref>. The trajectory of the maximal system is shown in Fig. <ref> [Top]. The traffic signals are coordinated such that the traffic flows free of congestion. The black dashed lines represent the capacity of the links, and the dashed line in the fourth figure (from the left) represents the threshold for the liveness sub-specification (ψ). It is observed that all the state values for side road links (49-53) persistently fall below the threshold. The robustness values for (x∈Π) and ψ are shown in the fifth figure. As mentioned earlier, robustness corresponds to the minimum volume of vehicles that the system is away from congestion, or violating the specification. The robustness values are always positive, indicating satisfaction.

 
 As stated in Theorem <ref>, the trajectory of the maximal system converges to a periodic orbit. 
It is worth to note that the number of vehicles on freeway links is significantly smaller than its capacity, which is attributed to the fact that the number designated for q̅ (related to the maximum speed) of freeway links is relatively large (30, as opposed to 15 for roads). Therefore, freeway links are utilized in a way that there is enough space for high speed non-congested flow.   






  §.§.§ Robust MPC

Here it is assumed that the controller has full state knowledge. We apply the techniques developed in Sec. <ref>. Using the result from the previous section, the set Ω_ℒ^φ is constructed in ℝ_+^212 (=ℝ^n(h^φ+1),n=53, h^φ=3). The cost criteria that we use in this case study is the total delay induced in the network over the planning horizon H. A vehicle is delayed by one time unit if it can not flow out of a link in one time step, which may be because of the actuation (e.g., red light) or waiting for the flow of other vehicles in the same link (i.e., we have x_[l]≥ c_l). 
We are also interested in maximizing the STL robustness score. The cost function is: 


    [ J_traffic(x^H,u^H):= - ζ ρ(x,G_[0,H-1]φ,t-h^φ+1);   +  ∑_k=0^H-1γ^k∑_l ∈ℒ (x_[l],t+k-q⃗_[l],t+k) , ]
 
where q⃗_[l], given by (<ref>), is the amount of vehicles that flow out of link l, γ is the discount factor for delays predicted in further future, and ζ is a positive weight for robustness. Notice the connection between the time window of STL robustness score in (<ref>) and MPC constraint enforcement in (<ref>).
It follows from Theorem <ref> and STL quantitative semantics (<ref>) that the cost function above is non-decreasing with respect to the state in Π. Therefore, in order to minimize the worst case cost, the maximal system is considered in the MPC optimization problem.  

Starting from zero initial conditions, we implement the MPC algorithm (<ref>) with H=3 for 40 time steps. We set ζ=1000, γ=0.5 in (<ref>). The disturbances at each time step were randomly drawn from L(w^*) using a uniform distribution. The maximum computation time for each MPC step time step was less than 0.8 seconds (less than 0.5 seconds on average). The resulting trajectory is shown in Fig. <ref> [Middle]. For the same sequence of disturbances, the trajectory resulted from applying the open-loop control policy (<ref>) (using the values in Table <ref>) is shown in Fig. <ref> [Bottom]. Both trajectories satisfy the specification. However, robust MPC has obviously better performance when costs are considered. The total delay accumulated over 40 time steps is: 

    J_40=∑_τ=0^40∑_l ∈ℒ (x_[l],τ-q⃗_[l],τ).

The cost above obtained from applying robust MPC was J_40=1843, while the one for the open-loop control policy was J_40=2299, which demonstrates the usefulness of the state knowledge in planning controls in a more optimal way. An optimal tuning of parameters η and γ requires an experimental study which is out of scope of this paper. We only remark that we usually obtained larger delays with non-zero η, which shows that including STL robustness score in the MPC cost function may be useful even though the ultimate goal is minimizing the total delay. 

It is worth to note that we also tried implementing the MPC algorithm (for the case w=(w^*)^ω, or the maximal system) without the terminal constraints, as in (<ref>). The MPC got infeasible at t=8. The violating constraints were those in x ∈Π. This observation indicates that the myopic behavior of MPC in (<ref>), when no additional constraints are considered, can lead to congestion in the network. 










 


§ CONCLUSION AND FUTURE WORK

We developed methods to control positive monotone discrete-time systems from STL specifications. We showed that open-loop control sequences are sufficient and (almost) necessary for guaranteeing the correctness of STL specifications. A robust MPC method was introduced to plan controls optimally, while guaranteeing global STL specifications. We showed the usefulness of our results on traffic management.  

Future work will focus on non-monotone systems with parametric uncertainty whose state evolution can be over-approximated in an appropriate way using monotone systems. We will develop adaptive control schemes to tune parameters automatically using the data gathered from the evolution of the system. This will eventually lead to data-driven control techniques for transportation networks with formal guarantees.          






§ APPENDIX


Let 𝕊 be the set of all STL formulas that can be written in the form:

    ϕ=⋁_i=1^n_ϕφ_b,i∧ G_[Δ_i,∞]φ_g,i,

where φ_b,i,Δ_i ≥ h^φ_b,i,φ_g,i, i=1,⋯,n_ϕ, are bounded STL formulas. Then 𝕊 is a subset of safety STL formulas that is closed under STL syntax with bounded temporal operators.   


First, a quick inspection of (<ref>) verifies that it is a safety STL formula. A predicate π is a bounded formula (with zero horizon) and is a special case of (<ref>), hence π∈𝕊.   

We also have the following property that relaxes the form in (<ref>):
For all bounded STL formulas φ_1,φ_2,  we have φ_1 ∧G_[Γ,∞)φ_2 ∈𝕊, ∀Γ∈ℕ. Proof: The case for Γ≥ h^φ_1 is already in the form (<ref>) with n_ϕ=1. If Γ< h^φ_1, we write G_[Γ,∞)φ_2 = G_[Γ,h^φ_1]φ_2 ∧G_[h^φ_1,∞)φ_2. Now, define φ_1 ∧G_[Γ,h^φ_1]φ_2 as the new bounded formula and retain the form in (<ref>) with n_ϕ=1. 

We show that 𝕊 is closed under STL syntax with bounded operators. The distributivity properties of Boolean connectives and temporal operators (see, e.g., <cit.>) imply that:
 ϕ_1 ∨ (ϕ_2 ∧ϕ_3)= (ϕ_1 ∨ϕ_2) ∧ (ϕ_2 ∨ϕ_3),
ϕ_1 ∧ (ϕ_2 ∨ϕ_3)= (ϕ_1 ∧ϕ_2) ∨ (ϕ_2 ∧ϕ_3),
F_I (ϕ_1 ∨ϕ_2)=(F_I ϕ_1) ∨ (F_I ϕ_2), and 
G_I (ϕ_1 ∧ϕ_2)=(G_I ϕ_1) ∧ (G_I ϕ_2),
where ϕ_1,ϕ_2,ϕ_3 are temporal logic formulas and I is an interval.


  * ϕ_1, ϕ_2 ∈𝕊⇒ϕ_1 ∧ϕ_2 ∈𝕊, ϕ_1 ∨ϕ_2 ∈𝕊: this result easily follows from the distributivity properties of Boolean connectives mentioned above.    



  * ϕ∈𝕊⇒F_{t}ϕ∈𝕊: we use F_{t}G_[a,b]=G_[t+a,t+b] and distributivity to have (note that F_{t}=G_{t}) 

    [                                          F_{t} (⋁_i=1^n_ϕ (φ_b,i∧G_[Γ_i,∞]φ_g,i));                                        = ⋁_i=1^n_ϕ (F_{t}φ_b,i∧G_[t+Γ_i,∞]φ_g,i). ]

Introducing F_{t}φ_b,i, i=1,⋯,n_ϕ, as new bounded STL formulas leads to the form in (<ref>).







  * ϕ∈𝕊⇒F_[a,b]ϕ∈𝕊, G_[a,b]ϕ∈𝔽: use F_[a,b]=⋁_t ∈ [a,b]F_{t} and G_[a,b]=⋀_t ∈ [a,b]F_{t} to convert temporal operators to Boolean connectives.




















  * ϕ_1,ϕ_2 ∈𝕊⇒ϕ_1U_[a,b]ϕ_2  ∈𝕊:  use the STL semantics (<ref>) to substitute the bounded “until" operator using bounded “eventually" and bounded “always" operators:

    [ ϕ_1U_[a,b]ϕ_2 = ⋁_t ∈ [a,b] (G_[a,t]ϕ_1∧F_{t}ϕ_2). ]












The “reach and stay" formula F_I G_[0,∞)φ, where φ is a bounded formula, is equivalent to ⋁_t ∈ IG_[t,∞)φ.    


What remains to show that 𝕊 is equivalent to the set of all safety STL formulas is having that ϕ∈𝕊⇒G_[Γ,∞)ϕ∈𝕊, ∀Γ∈ℕ, which is not true by restricting n_ϕ in (<ref>) to be finite. Formulas that involve nested unbounded “always" operator and can not be further simplified, such as G_[Γ',∞) (φ_1 ∨G_[Γ,∞)φ_2), are rarely encountered in applications.   









[
    < g r a p h i c s >
]Sadra Sadraddini (S' 16) 
received the B.Sc. in Mechanical Engineering and the B.Sc. in Aerospace Engineering (dual majors) in 2013 from Sharif University of Technology, Tehran, Iran. 
He is currently pursuing a degree toward Ph.D. in Mechanical Engineering at Boston University, Boston, MA. 
His research focuses on formal methods to control theory with various applications in cyber-physical systems.      


[
    < g r a p h i c s >
]Calin Belta 
 (F' 17) is a Professor in the Department of Mechanical Engineering at Boston University, where he holds the Tegan family Distinguished Faculty Fellowship. He is the Director of the BU Robotics Lab, and is also affiliated with the Department of Electrical and Computer Engineering, the Division of Systems Engineering at Boston University, the Center for Information and Systems Engineering (CISE), and the Bioinformatics Program.  
His research focuses on dynamics and control theory, with particular emphasis on hybrid and cyber-physical systems, formal synthesis and verification, and applications in robotics and systems biology.  He received the Air Force Office of Scientific Research Young Investigator Award and the National Science Foundation CAREER Award. He is a fellow of IEEE.



