Event-Triggered Controller Synthesis for Dynamical Systems with Temporal Logic Constraints
Dipankar Maity John S. Baras




Semantic segmentation of trajectories with agent models
    
Daisuke Ogawa, Toru Tamaki, Bisser Raytchev, Kazufumi Kaneda

Hiroshima University

Higashi-Hiroshima, Hiroshima 739-8527 Japan

















    December 30, 2023
=====================================================================================================================================================

empty
empty



In this work, we propose an event-triggered control framework for dynamical systems with temporal logical constraints.
Event-triggered control methodologies have proven to be very efficient in reducing sensing, communication and  computation
costs. When a continuous feedback control is replaced with an event-triggered strategy, the corresponding state trajectories 
also differ. In a system with logical constraints, such small deviation in the trajectory might lead to  unsatisfiability of the
logical constraints. In this work, we develop an approach where we ensure that the event-triggered state trajectory is confined within
an ϵ tube of the ideal trajectory associated with the continuous state feedback. At the same time, we will ensure satisfiability of the
logical constraints as well. 
Furthermore, we show that the proposed method works for delayed systems as long as the delay is bounded by a certain quantity.




§ INTRODUCTION

Present control systems are typically a large network of heterogeneous components sharing some common resources and information, and with coordinated cooperation, they aim to achieve desired performance.  These kinds of  highly complex systems are ubiquitous in cyber-physical-systems (CPS), and also referred as networked-CPS. In many CPS, the controller synthesis is subjected to many logical constraints that arise due to presence of logical variables and reasoning among the subsystems. 

Recent studies on controller synthesis with linear temporal logic (LTL) have paved a way to design controllers for large complex systems with safety, synchronisation, and other logical constraints <cit.>. 

Novel formulations and efficient computational approaches have been proposed to mathematically formulate specifications such as trajectory sequencing, synchronization etc. 
Temporal logics such as linear temporal logic (LTL), computational tree logic (CTL), developed for model checking, have been widely accepted by the robotics community for the purpose of motion planning 
<cit.>, <cit.>. Development of sophisticated model checking tools such as SPIN 
and NuSMV 
made it easier to synthesize controllers for such systems. As an alternative approach controller synthesis has been done using mixed integer linear programming <cit.>. 

Another challenge for the large connected CPS is that computation of the control law requires continuous sensing (often times distributed) and transmitting the sensed signals to the controllers. Consequently, the performance of such systems is generally determined by the availability of sensing power, bandwidth for continuous transmission and resources for fast computation. Therefore it will be beneficial if  the same (with little tolerance) performance can be achieved with lesser intensive sensing and computing tasks.

To circumvent the problem of limited communication bandwidth or computing resources or sensing capability, researchers have developed techniques that require intermittent communications only at certain discrete time instances to perform the same task with minor performance degradation. These control methodologies are known in many forms e.g.  event-triggered, self-triggered  or periodic control <cit.>, <cit.>. These control strategies do not require the state information x(t) for all time t, rather they sample  x(t) intermittently depending on the systems' performance criterion <cit.>, <cit.>. These  techniques have proven to be efficient for large scale inter-connected systems to reduce communication and sensing operations.

In this work, we study the temporal logic based controller synthesis problem in an event-triggered framework. We consider a controller synthesis problem for a given control affine nonlinear system and the objective is to design an event triggered controller for that system with logical constraints. We assume the logical constraints can be represented using temporal logic and its propositional calculus. 

Existing literature results show that the trajectory of an event triggered system deviates from the nominal system as a consequence of limited communication <cit.>, <cit.>. Although, the continuous feedback system satisfies the logical constraints, now with an event triggered controller we have no guarantee that the logical constraint over the event-triggered trajectory will be satisfied as well. 

We show that suitably modifying the given logical constraints, and creating  stricter constraints will make the event-triggered trajectory satisfy the original logical constraint provided we can synthesize a continuous controller to satisfy the stricter constraint. The stricter logical constraint is often times known as  robust logical constraint <cit.> since any  perturbed trajectory (within some ϵ bound) will still satisfy the constraint. We adopt this notion of robustness in this work. In the next stage, we design an event-triggered controller ensuring that the event-triggered controller confines the trajectory within an ϵ-tube around the actual trajectory. Further, we show the effects of delay (in transmitting the measurement to the controller) on the performance. The analysis shows that if the delay is bounded by a certain quantity, which depends on the physical parameters of the plant and the controller, then the delayed system will be able to perform similar to the delay-free system without further modification in design.

In Section <ref>, we formally describe the problem and our two-step approach towards the problem. Section <ref> provides preliminary background on the temporal logic and construction of ϵ-robust logic formulae. We design an event triggered controller for this problem in Section <ref> and study the effects of delay on such an event triggered controller. Finally, we illustrate the application of our framework using two examples in Section <ref>. 



§ PROBLEM FORMULATION
 
Let us consider the input-affine nonlinear state space model as given in (<ref>). 

    ẋ =f_0(t,x)+∑_i=1^m f_i(t,x)· u_i 
    
       x(t_0)=x_0.

where x(t) ∈𝒳⊆ℝ^n, u_i(t) ∈ℝ is the i-th control input. The trajectory of the dynamical system starting at t_0 under application of some control u=[u^1,⋯,u^m] is denoted as x^u,x_0[t_0]. Similarly the trajectory starting from any arbitrary point (t,x) is represented as x^u,x[t]. The objective of this work is to design an event-triggered controller u(·) that ensures satisfiability of a temporal logical constraints (φ). 


By x^u,x_0[t_0]φ we denote that the trajectory of the dynamics (<ref>) under input u satisfies the logical constraint φ. Similarly, x^u,x_0[t_0]φ denotes that the trajectory does not satisfy the logical constraint. In this work we focus on the real time linear temporal logics <cit.>, <cit.> which have been proven to be very effective for expressing logical constraints in dynamical systems <cit.>. 
 In the following, we formally pose the problem that we aim to solve in this work.
 
 
Given an input-affine dynamics (<ref>) and a logical constraint (φ) on the trajectory of the system, design an event-triggered framework to generate the control u(t) such that the event-triggered trajectory satisfies φ, i.e. 

    find       u
    
    subject to      u∈𝒰^e 
    
       ẋ =f_0(t,x)+∑_i=1^m f_i(t,x)· u_i 
    
        x^u,x_0[t_0]φ

 
where 𝒰^e denotes the set of event based control strategies. 
In this work we do not impose any restriction on the event-triggered framework other than the exclusion of Zeno behavior <cit.>. We provide sufficient conditions which, if satisfied, ensure that the trajectory of the designed event-triggered system will satisfy the logical constraint φ. 

While temporal logic can express various types of logical constraints (see Section <ref>), it comes with a cost that verifying whether a trajectory satisfies the logical constraints is Pspace-complete <cit.>. Therefore synthesis of a controller is a hard problem in its own right, and synthesis of an event-based controller is harder for obvious reasons. However, there are some proposed techniques which can generate a (feedback) controller that satisfies the temporal logic constraints, see for example <cit.>, <cit.>.

Therefore, we divide the original problem into two subproblems: Problem <ref> and Problem <ref>.
 
Given the dynamics (<ref>), design a feedback controller u_i(t)=γ_i(t,x(t)) such that x^γ,x_0[t_0]φ^ϵ.
 
where φ^ϵ is another logical constraint  derived from φ.  φ^ϵ is a stricter constraint than φ in the sense that x^γ,x_0[t_0]φ^ϵ implies ξ[t_0]φ^ϵ for all piecewise continuous curves ξ(·) : [t_0, +∞)→ℝ^n such that sup_t∈ [t_0, +∞)x(t)-ξ(t)≤ϵ. In the following sections we will explicitly explain how φ^ϵ is related to  φ for a given ϵ≥ 0.
 
 
For all ϵ>0, given the dynamics (<ref>) and a feedback control γ(t,x(t)), design an event-triggered controller γ^e(t,x(τ_k)) such that the trajectory of the event-triggered system x^γ^e, x_0[t_0] remains within an ϵ neighborhood of the ideal trajectory associated with the feedback closed-loop system. As ϵ→ 0, γ^e(t,·)→γ(t,·) pointwise ∀ t.
 

Therefore, in this two step approach, we first design a feedback controller for satisfying the ϵ-strict constraint φ^ϵ (for some ϵ>0). In the next stage we use an event-triggering mechanism which provides sufficient condition(s) for ensuring that the trajectory of the event-triggered system will be in an ϵ neighborhood of the actual feedback trajectory pointwise, i.e. x_e(t)-x(t)≤ϵ (x_e is the event-triggered trajectory and x is the ideal feedback trajectory) for all t. In Figure <ref>, we present our schematic for event-triggered controller synthesis using the proposed two-step approach. From this point onward, we will suppress the control and initial state in denoting a trajectory when these are apparent from the context i.e. we will represent x^u,x_0[t_0] as x[t_0] etc. 







 

§ PROPOSITIONAL TEMPORAL LOGIC
 
Like other families of propositional logic, temporal logic over the reals also requires a set of propositional variables Π={π_1,π_2,⋯,π_n}. Associated with each propositional variable π_i, there is a labelling function ℒ_i: 𝒳→{0,1} which denotes whether the proposition π_i  is true at some point in 𝒳. Therefore, Π  divides 𝒳 into subsets and assigns π_i with each of the subsets. A formula of a propositional logic is defined over a Boolean signal and in our case, ℒ_i(·) maps the ℝ^n valued signal (x(t)) to a Boolean signal. For example, π_1 could be associated with the ball of radius 1 at the origin of 𝒳=ℝ^2. Then ℒ_1(s)=1 for all x ∈ B_0(1) and 0 otherwise, where  B_x(δ)={y∈𝒳 | y-x_2≤δ} is a ball of radius δ centered at x.  Note that it is not necessary that the regions associated with π_i are non-overlapping. We will use the notation π_i ≅𝒳_i (⊆𝒳) to denote ℒ_i(x)=1 for all x∈𝒳_i and ℒ_i(x)=0 for all x∈𝒳∖𝒳_i (basically the indicator function of the set 𝒳_i). At this point, it should be noted that any algebraic constraint on x of the form G(x) ≤ 0 could be associated with a proposition π such that π≅{x ∈𝒳 |  G(x) ≤ 0}. 

However, the power of temporal logic is beyond capturing these algebraic constraints. Let us first provide an informal overview of the capability of the logic and then formally state the syntax and semantics  of the logic. The RTL (Temporal Logic over Reals) <cit.> formulae are built on the propositional variables Π with the use of usual logical operators  (negation), ∨ (conjunction) and ∧ (disjunction), and some special temporal operators e.g. U (until),  (eventually),  (always) and other operators that could be derived from the mentioned operators. For example, the formula π (read as “Eventually Always in π") where π≅𝒳_i, when satisfied by a trajectory of the dynamics (<ref>), means that eventually the trajectory enter the region 𝒳_i and stay there for all future times. Similarly, (π_1 ∧π_2 ∧π_3)Uπ_4 states the rule that region 𝒳_4 must be reached   while avoiding regions 𝒳_i for i=1,2,3 (π_j ≅𝒳_j). Although the satisfaction of the formula tells us that the state trajectory will reach 𝒳_4,  it does not provide any interval of time within which it will reach the destination. This limitation can easily be circumvented by the traditional augmentation of a new state x_n+1=t.

Adding an extra equation ẋ_n+1=1 with x_n+1(t_0)=t_0 in the dynamics (<ref>), we can pose time dependent constraints as well. In this case, the augmented space is 𝒳× [t_0,T) (T could be +∞ for an infinite horizon problem). The formula (π_1 ∨π_2) where π_1 ≅{(x,t) |  x∈𝒳, t_0≤ t < 6 } and π_2 ≅{(x,t) |  x∈𝒳_i, 5≤ t } requires the trajectory to enter the region 𝒳_2 no earlier than t=5 and the trajectory should remain  within 𝒳_2 for all t ∈ [6,∞). The formula also mentions that the trajectory will be in 𝒳_1 when it is not in 𝒳_2. Therefore, with this state-space augmentation, all the properties related to the timing aspect of a trajectory of the system (<ref>) can be expressed. 

 

 
 The syntax of RTL formulas are defined according to the following grammar rules:
 

 ϕ ::= ⊤ |  π  | ϕ  |  ϕ∨ϕ | ϕ𝐔ϕ | ϕ𝐑ϕ
 
 
 
 where π∈Π,
⊤ and (=⊤) are the Boolean constants true and false respectively.  𝐑 symbolizes the  Release operator.
Other temporal logic operators  can be represented using the grammar in definition <ref> e.g. eventually (φ=⊤Uφ), always (φ =  (φ)) etc. 

If x[t_0] denotes a trajectory starting at time t_0, the semantics of the grammar in Definition <ref> is given as follows:

 The semantics of any formula ϕ over the trajectory x[t_0] is recursively defined as:

 x[t_0] π iff ℒ_π(x(t_0))=1

 x[t_0] π iff ℒ_π(x(t_0))=0

 x[t_0] ϕ_1∨ϕ_2 iff x[t_0] ϕ_1 or x[t_0] ϕ_2

 x[t_0] ϕ_1∧ϕ_2 iff x[t_0] ϕ_1 and x[t_0] ϕ_2

 x[t_0] ϕ_1𝐔ϕ_2 iff ∃ s≥ t_0 s.t. x[s] ϕ_2 and 
 ∀ t_0 ≤ s'<s,   x[s'] ϕ_1.

 x[t_0] ϕ_1𝐑ϕ_2 iff ∀ s≥ t_0  x[s] ϕ_2 or ∃ s' s.t. t_0 ≤ s'<s,   x[s'] ϕ_1. 




More details on RTL grammar and semantics can be found in <cit.>, <cit.>.  




 §.§ Construction of ϵ-Robust Formula


As described in Section <ref>, the motivation behind constructing an ϵ-robust formula φ^ϵ is that any trajectory satisfying the stricter formula φ^ϵ is robust in the sense that any perturbed trajectory with less than ϵ perturbation will also satisfy the original constraint φ. 


The idea is as follows: if the trajectory needs to visit a region π_i(≅𝒳_i), then we push the boundary of 𝒳_i inwards by amount ϵ and denote this new set (and proposition) by 𝒳_i^ϵ (π_i^ϵ). Similarly if the trajectory needs to avoid some region π_j (≅𝒳_j) then the boundary of 𝒳_j is expanded outwards by an amount ϵ. 

The RTL syntax presented in Definition (<ref>) is in negative normal form (NNF) <cit.>, and this enables us to detect which regions must be avoided by noting the presence of the negation () operator immediately before the corresponding propositions π_i. 

Note that, by our definition π_i ≅𝒳_i and π_i ≅𝒳∖𝒳_i.



In a given metric space (𝒳,ρ) the open ball centered at x ∈𝒳 of radius r is defined as B_x(r)={y ∈𝒳 | ρ(x,y)<r}. Let ϵ>0 be a given parameter, then the ϵ-contraction of the set 𝒴⊆𝒳 is denoted by 𝒴^ϵ={y∈𝒴 |  B_y(ϵ)⊆𝒴}.

Similarly, the ϵ-expansion of the set is denoted by 𝒴^-ϵ={x∈𝒳 | ∃ y∈𝒴, x ∈ B_y(ϵ)}.



For a RTL formula φ, the ϵ-robust formula is constructed as follows:

1) replace each π_i (≅𝒳_i), which is not preceded by any negation, by π_i^ϵ where π_i^ϵ≅𝒳_i^ϵ.

2) any π_j that is preceded by a negation () should be replaced by π_j^-ϵ≅𝒳_j^-ϵ∪ (𝒳∖𝒳^ϵ). When 𝒳=𝒳^ϵ for all finite ϵ >0 (e.g. 𝒳=ℝ^n),  π_j^-ϵ≅𝒳_j^-ϵ.

In a similar way one can define ϵ-robust formulas over the space 𝒳× [t_0,T). However, for this work we will restrict ourselves to the robustness only in 𝒳 space.

 
Let the 

trajectory x[t_0] satisfies the RTL formula φ^ϵ for some ϵ>0. Then for all δ≤ϵ and for any curve y(·):[t_0,T)→𝒳 such that sup_t ρ(x(t),y(t)) ≤δ, y[t_0]φ.


The above proposition can be proved inductively; interested readers may see <cit.> for a proof.


In order to construct a  π_i^ϵ from π_i, 𝒳_i must have a non-empty interior. 


Let us define the radius of a set 𝒳_i in the following way r(𝒳_i)=sup{r | ∃ x∈𝒳_i, B_x(r)⊆𝒳_i }.
Therefore for each π_i, π_i^ϵ is well defined for  ϵ≤ r(𝒳_i), for ϵ > r(𝒳_i), π_i^ϵ≅∅. 
For the subsequent section we will implicitly assume that  min_i{r(𝒳_i)}>0  and moreover, each of these sets, 𝒳_i is a polyhedron.

Therefore, to solve problem <ref>, our goal will be to design a controller that satisfies the robust RTL formula φ^ϵ. The power of using these temporal logic formulae is that each formula can be represented by an equivalent (Büchi) automaton. Satisfaction of an RTL formula is equivalent to finding a path from the initial state to one of the accepting states of the automaton. The construction of such automata can be done automatically using the available tools SPIN and NuSMV <cit.>, <cit.>. The dynamics (<ref>) can be represented as a finite transition system (FTS), where the transitions are performed by selecting the control u. Thus, the dynamics constraint and logical constraint in (<ref>) can jointly be represented by forming a product of the automata and the FTS. More detail on such construction and controller synthesis can be found in our earlier work <cit.>. To keep the paper short, we spare the details here, however, interested reader may see, for example, <cit.>, <cit.>. 












































§ EVENT TRIGGERED CONTROLLER SYNTHESIS
 
In the previous section it is presented how the control inputs can be generated for the dynamics (<ref>) so that the trajectory of the system satisfies the logical constraint φ^ϵ for some ϵ>0. This section will focus on designing an event-triggered controller  that will replace the feedback controller designed to satisfy φ^ϵ  in such a way that the trajectory of the event-triggered system will remain within ϵ distance of the ideal feedback trajectory.

Let us denote the controller u(t)=γ(x(t)) that achieves the satisfaction of  φ^ϵ. The closed-loop dynamics are:

    ẋ =f_0(t,x) +∑_i=1^m f_i(t,x)γ_i(x)
       x(t_0)=x_0
 
Let x[t_0] denote the trajectory of the above closed loop system. 
We make the following assumptions on the system (<ref>).
 
(A1) γ_i(·) and for all t, f_i(t,·)  are Lipschitz functions with Lipschitz constants L_γ^i,
L_f^i respectively, for all i=0,1,2,⋯, m. 

(A2) 

 For all i=1,2⋯,m and ∀ t, f_i(t,x)γ_i(x) and f_0(t,x) are continuously differentiable functions w.r.t x with continuous first derivative.





In event-triggered framework, the controller is designed to be:

    γ_i^e(t)= γ_i(x(t_k))     ∀ t ∈ [t_k,t_k+1)

where t_ks are the event-triggering times. An event-generator needs to be designed that will produce the t_k in certain way that is explained in the following. 

Let us denote the event-triggered closed loop system as x_e(t) and the corresponding trajectory as x_e[t_0]. Thus,

    ẋ_e= f_0(t,x_e)+∑_i=1^mf_i(t,x_e)γ^e_i(x_e(t_k))
       x_e(t_0)=x_0.

Let us define the error e(t)=x(t)-x_e(t).
 
Note that the event-triggered controller γ_i^e(t,·) for all t is an approximation of the ideal feedback controller γ_i(t,·) by piecewise constant functions. Therefore, designing  the γ_i at first makes the problem tractable for generating the event-triggered controller. 

The dynamics of e(t) is given as:

    ė =F(t,x)-F(t,x_e)+∑_i=0^mf_i(t,x_e)(γ^e_i(x_e(t_k))-γ_i(x_e(t))) 
        e(t_0)=0,

where F(t,x)=f_0(t,x) +∑_i=1^m f_i(t,x)γ_i(x)
 
y(t) is exponentially stable with

    ẏ= A(t)y

where A(t)=∂ F(t,x)/∂ x|_x=x(t) and  x(t) is the trajectory of (<ref>).  

We can write, 

    ė= A(t)e+f̃(t,x_e,e)e+δ(t)

where f̃(t,x_e,e)e=F(t,x)-F(t,x_e)-A(t)e and δ(t)=∑_i=0^mf_i(t,x_e)(γ^e_i(x_e(t_k))-γ_i(x_e(t)))

Using Assumption <ref> (A2),

    F(t,x+h)=F(t,x)+∫_s=0^1dF(t,x+sh)dsh
 where dF(t,·): ℝ^n→ℝ^n is a linear map which is the derivative of  the map F(t,·): ℝ^n→ℝ^n. Selecting h=x_e-x=-e, we obtain:

    F(t,x_e)=F(t,x)-∫_0^1dF(t,x-se)dse.

Therefore,

    f̃(t,x_e,e)=∫_s=0^1dF(t,x_e(t)+(1-s)e(t))ds-A(t).
 
Also f̃(t,x_e,0)=0. 


Since ẏ=A(t)y is the linearization of the system  ė=A(t)e+f̃(t,x_e,e)e around e=0, we can say that ė=A(t)e+f̃(t,x_e,e)e is locally exponentially stable due to Assumption <ref>. As a consequence of the Lyapunov converse theorem <cit.>, we have a (local) quadratic Lyapunov function that satisfies:

    c_1e^2 ≤ V(t,e)    ≤ c_2e^2
    ∂ V/∂ t +∂ V/∂ e(A(t)+f̃(t,x_e,e))e   ≤ -c_3e^2
    ∂ V/∂ e   ≤ c_4e
  


 
For all t,

    e(t)_2≤c_4/2c_1∫_t_0^te^-(t-s)c_3/2c_2δ(s)_2ds




A detailed proof of this can be found in our earlier work <cit.>. The proposition is due to the BIBO (bounded input bounded output) stability of an exponential stable system.



Note that at each t_k, δ(t_k)=0. We can bound δ(t) to ensure a bound on e(t). 



 Without computing x(t) real-time, e(t) can be bounded by observing the signal δ(t) which depends only on x_e. Moreover, due to the Lipschitz assumptions on f_i(t,·) and γ_i(·), it is sufficient to only monitor the difference signal x(t)-x(t_k).

From (<ref>), we have the sufficiency condition that sup_tδ(t)≤ϵ_1= c_1c_3/c_2c_4ϵ ensures sup_te(t)≤ϵ.

We propose the following event-trigger function:

    g(t)= c_1c_3/c_2c_4ϵ-δ(t).

An event is generated whenever g(t)≤ 0 and the state value at that time (x(t_k)) is sent to the controller. The set of triggering times is denoted by 𝒯 ={t_1,t_2,⋯ ,t_k,⋯} such that g(t_k)=0 and g(t)<0 otherwise.

There could be other event-triggering functions that can also ensure bounded error e(t). In this paper, we consider (<ref>) to carry out the analysis further and to perform the simulations.


 
For all t, 

    δ(t)≤αx_e(t)-x_e(t_k)^2+β(t)x_e(t)-x_e(t_k).

for some α,β(t)>0.  t_k is the latest triggering time at time t. 



We have δ(t)=∑_i=1^mf_i(t,x_e)(γ^e_i(x_e(t_k))-γ_i(x_e(t))).
By rearranging,

    δ(t)=∑_i=1^mf_i(t,x_e(t_k))(γ^e_i(x_e(t_k))-γ_i(x_e(t)))+
       ∑_i=1^m(f_i(t,x_e(t))-f_i(t,x_e(t_k)))(γ^e_i(x_e(t_k))-γ_i(x_e(t)))

Using the Lipschitz continuity assumption in Assumption <ref>, we can write:

    δ≤   (x_e(t_k))-(x_e(t))∑_i=1^mL^i_γf_i(t,x_e(t_k))+
       (x_e(t_k))-(x_e(t))^2∑_i=1^mL^i_γ L^i_f.

Now we define:

α=∑_i=1^mL^i_γ L^i_f and β(t)=∑_i=1^mL^i_γf_i(t,x_e(t_k)).



In <cit.> a different bound on δ was derived. There it was shown that: 


    δ(t)≤κ(t) (x_e(t_k))-(x_e(t)).

κ(t)=max_i{L^i_γ}sup_x∈Ω∑_i=1^m f_i(t,x). Where the trajectory x(t) of (<ref>) is bounded in the domain Ω^ϵ.

Comparing (<ref>) with (<ref>), we notice that the former is bounded linearly w.r.t. (x_e(t_k))-(x_e(t)) whereas the later is bounded by a quadratic form of (x_e(t_k))-(x_e(t)). In most of the practical applications ϵ≪ 1 and hence (x_e(t_k))-(x_e(t)) is required to keep smaller than ϵ (see Proposition <ref>). Therefore, (x_e(t_k))-(x_e(t))^2 can be bounded by (x_e(t_k))-(x_e(t)) with proper coefficient. Furthermore, the presence of sup operator over the whole domain Ω^ϵ in (<ref>) implies that  κ(t) ≥β(t) (in general κ(t) ≫β(t)). Therefore, (<ref>) could be a better approximation of δ(t).



[sufficiency] 
For all t, 

    x_e(t)-x_e(t_k)≤ϵ_1/ϵ_1 +β^2(t)/4αβ(t)/4α

 ensures e(t)≤ϵ, for ϵ_1=c_2c_4/c_1c_3ϵ. 



From (<ref>), αx_e(t)-x_e(t_k)^2+β(t)x_e(t)-x_e(t_k)≤ϵ_1 implies δ≤ϵ_1.

Therefore, 

    x_e(t)-x_e(t_k)≤√(β(t)^2+4αϵ_1)-β(t)/2α

implies δ≤ϵ_1. 
Using the fact 
    ln(1+x)≥x/1+x
 for all x≥ 0, one can verify

    √(β(t)^2+4αϵ_1)≥β(t)+2αβ(t)ϵ_1/(β(t)^2+4αϵ_1).

Thus, 
    x_e(t)-x_e(t_k)≤β(t)ϵ_1/(β(t)^2+4αϵ_1)

ensures δ≤ϵ_1=c_2c_4/c_1c_3ϵ.

Proposition <ref> ensures that δ≤ϵ_1=c_2c_4/c_1c_3ϵ implies e(t)≤ϵ.


As a comparison, in <cit.>, the sufficient condition equivalent to Proposition <ref> was x_e(t)-x_e(t_k)≤ϵ_1/κ(t). If 
    ϵ_1< β(κ-β)/4α
 the sufficiency condition in Proposition <ref> is relaxed than its counterpart in <cit.>.

 The following lemma ensures that the proposed event-triggering mechanism excludes Zeno behavior.


The inter-trigger time τ_k=t_k-t_k-1  is bounded from below, i.e. inf_k τ_k ≥α >0. This ensures that within a finite interval [t_0,T) there will be a finite number of triggerings.


The lemma can be proved following the approach of <cit.>; we omit it due to space limitation.
 

If there exists ϵ>0 and controllers γ_i(·) such that the closed-loop trajectory x[t_0]φ^ϵ, then the event triggered trajectory x_e[t_0] φ where events are generated whenever g(t)≤ 0.
 
 
The proof follows directly from Proposition (<ref>) where y[t_0]=x_e[t_0] and we have ensured sup_tρ(x(t),x_e(t))=sup_te(t)≤ϵ. 
 
 

 §.§ Implication of Delays

 
 In this section we study the scenario when the sampled state x(t_k) arrives to the controller at time t_k+Δ_k where Δ_k is the delay in the channel at time t_k. The aim of this section is to find a bound on the the delays so that the proposed event-triggered strategy still ensures that e(t)≤ϵ for all time t.
 
 In order to study that we start with the sufficiency condition x_e(t)-x_e(t_k)≤ h(ϵ) which ensures e(t)≤ϵ. Here h(ϵ) is β(t)ϵ_1/(β(t)^2+4αϵ_1) (or ϵ_1/κ(t) by <cit.>).
 
Let the delays at triggering times  t_k-1 and t_k be Δ_k-1, Δ_k. Thus for all t∈ [t_k-1+Δ_k-1,t_k+Δ_k) the requirement is

    x_e(t)-x_e(t_k-1)≤ h(ϵ)

Now,

    x_e(t)-   x_e(t_k-1)≤
       ∫_t_k-1^tf_0(s,x)+∑_i=1^mf_i(s,x)γ_i^e(x(t_k-1))ds 
    ≤   ∫_t_k-1^t(lx_e(s)-x_e(t_k-1)+p(s))ds

where l=L^0_f+∑_i=1^mL^i_fγ^e_i(x(t_k-1)) and p(s)=f_0(s,x(t_k-1))+∑_i=1^mf_i(s,x(t_k-1))γ_i^e(x(t_k-1)).

Therefore,

    x_e(t)-   x_e(t_k-1)≤(∫_t_k-1^tp(s)ds)e^l(t-t_k-1)


Let T_k=inf_t{t>t_k-1| (∫_t_k-1^tp(s)ds)e^l(t-t_k-1)=h(ϵ)}. 

Therefore we must have T_k≥ t_k+Δ_k and t_k≥ t_k-1+Δ_k-1.
Thus, 
    Δ_k+Δ_k-1≤ T_k-t_k-1

From the definition of T_k, 

    (∫_0^T_k-t_k-1p(s+t_k-1)ds)e^l(T_k-t_k-1)=h(ϵ)=ϵ̅

It is trivial to verify the above equation has unique solution for T_k-t_k-1 whenever ϵ̅≥ 0, and let us denote this solution by T_k-t_k-1=w̃(ϵ̅) for some function w̃ which satisfies the differential equation:

    dw̃(r)/dr   =1/rl+e^lw̃p(w̃+ t_k-1)
    w̃(0)   =0 .

When f_i does not depend explicitly on time, then p(s)=p and for this special case, 

    w̃(ϵ̅)=1/lW(lϵ̅/p)

where W(·) is the Lambert W function. 

From (<ref>)  one can verify that for all r>0, w̃(r)>0. Moreover using comparison lemma <cit.>, one can show for (<ref>) that 

    w̃(r)≥1/lW(lr/p_m)
 where p_m=supp(w̃+t_k-1).
Using the concavity property of W(·) along with W(0)=0,  for all 0 ≤ r≤ r_m

    w̃(r)≥W(lr_m/p_m)/lr_m r
. 

Thus, for ϵ̅_m≥ϵ̅=h(ϵ), 

    sup_k{Δ_k+Δ_k-1}≤W(lϵ̅_m/p_m)/lϵ̅_m h(ϵ)

ensures that e(t)≤ϵ. Thus, (<ref>) states the sufficient condition for delays under which the proposed event trigger mechanism will be able to  ensure e(t)≤ϵ. 









§ EXAMPLES AND SIMULATIONS
 


 §.§ Example 1

 Let us consider the following nonlinear system: 
  
    [ ẋ_1; ẋ_2 ]=-[ sin(x_1);      x_2 ]+[ -x_2;  x_1 ]u

 where x_1(0)=0, x_2(0)=1.
We consider the region π_1 ≅𝒳_1=B_0(0.1)⊂ℝ^2. 
The constraint (requirement) is to guide the state of the system within B_0(0.1)  and keep the trajectory within that ball for all future times.
The logical constraint is represented by  π_1.  To proceed, we consider the ϵ-robust formula π_1^ϵ with  ϵ=0.05. Therefore, 𝒳_1^ϵ=B_0(0.05).

We chose the controller u=-x_2 that achieves the property that x[0]π_1^ϵ (use the Lyapunov function V=x_1^2+x_2^2 to verify).  

At this stage we need to design an event triggering mechanism that will ensure that the event triggered system will follow the actual trajectory x[t_0]. The event triggered system dynamics is given by:

    [ ẋ_1; ẋ_2 ]=-[ sin(x_1);      x_2 ]-[ -x_2;  x_1 ]x_2(t_k)

 The initial condition is given as (0,1).
One can check that M̅_i, L^i_γ defined in Proposition <ref> have value 1. In Figure <ref>, the error signal is shown  along with the triggering instances. From Figure <ref> we note that only  9 samples are needed to achieve the task. This requires drastically reduced communication and sensing when compared to the continuous time feedback system. The trajectories of the ideal and even-triggered systems, and the ϵ-tube are shown in Figure <ref>.
















 §.§ Example 2

In this example we consider a robotic motion planning task with temporal sequencing and obstacle avoidance. The robot dynamics considered here is a unicycle model as:

    [  ẋ;  ẏ; θ̇ ] = [ cosθ; sinθ;    0 ]v +
    [ 0; 0; 1 ]w

where x,y∈ℝ^2 is the physical position  and θ∈ [0,360^o) is the heading angle. 
The task is given as follows:

    φπ_2 ∧ (π_2 Uπ_1) ∧π_3

where π_1,π_2 and π_3 corresponds to three circular regions as shown (denoted by R_1, R_2 and R_3) in Figure <ref>. The RTL formula defines the task of avoiding R_2 until reaching R_1 and eventually reaching R_2, and during the whole time the trajectory should avoid R_3.
 We adopt a potential function based approach <cit.> to generate the control laws for navigating the robot. 

As presented in previous sections, we expand and contract the appropriate regions while synthesizing the control.
The region R_3 has been expanded by ϵ=0.25 (the dashed boundary around R_3 shows the expansion in Figure <ref>) while R_1 was contracted and R_2 has been both expanded and contracted (since both π_2 and π_2 are present), however, we do not explicitly show them in Figure  <ref>. 
In figure <ref>, we show the triggering instances for this problem. 






§ CONCLUSION

In this work, we have proposed a framework for integrating the event-triggered controller synthesis and logic based controller synthesis. Our solution is based on composition of two independent controller synthesis framework.
It is also noteworthy that not any pair of logic-based-controller and event-trigger-controller has this unique composability property.
We have derived an explicit event triggering mechanism to bound the trajectory within an ϵ-tube. With the notion of robust logic constraints, the resulting trajectory finally satisfies the logical constraint. 
Simulation results show the significant reduction in communicating the state value for  updating the controller. This reduces the communication and computation costs. 























ieeetr



