Trajectory-Based Theory for Hybrid Systems

Abstract

This chapter presents a trajectory-based perspective in solving safety/ reachability analysis and synthesis problems and fault diagnosability analysis in hybrid systems. The main tool used in obtaining the results presented in this chapter is the concept of trajectory robustness, which is derived from the theory of approximate bisimulation. Trajectory robustness essentially provides a guarantee on how far the system’s state trajectories can deviate (in $L_{\infty }$ norm) as a result of initial state variations. It further leads to the possibility of approximating the set of the system’s trajectories, which is infinite, with a finite set of trajectories. This fact, in turns, allows us to pose the above problems as finitely many finite problems that can be practically solved. In addition, these finite problems can be solved in parallel.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

20.1 Note from the Author

This chapter is dedicated to Arjan van der Schaft in the occasion of his 60th birthday. The work presented here germinated from seed ideas that I developed while working as a doctoral student under Arjan’s mentorship. I was a graduate student at the Department of Applied Mathematics at the University of Twente in the period of 1999–2005. During this period, I had the fortune of being introduced to the (then) nascent field of hybrid systems, and exposed to the elegance of the behavioral systems theory. Under Arjan’s guidance, I wrote my doctoral dissertation on essentially the intersection of these two fields. In later years, while being a postdoctoral researcher at the University of Pennsylvania, I was introduced to the seminal work of Antoine Girard and George Pappas on the approximate bisimulation theory. The trajectory-based perspective of the behavioral systems theory and the notion of invariance and metrics in the space of trajectories from the approximate bisimulation theory are largely the impetus of the results presented in this paper.

20.2 Introduction

Hybrid systems are dynamical systems with interacting discrete and continuous dynamics [1]. Intuitively, one way to describe a hybrid system is to think of it as a multimodal dynamical system, where the dynamics of the continuous states depends on the discrete state of the system, which is also called the mode or the location. Because of their modeling expressivity, hybrid systems have been used in modeling of embedded systems [2–8], air traffic systems [9–14], automotive systems [15–17], electronic circuits [18–20], genetic regulatory networks [21–23], computational morphodynamics [24], and other fields.

In this chapter, we consider two types of hybrid systems, autonomous hybrid systems and control hybrid systems. More formal definitions of these systems will follow in Sect. 20.3.1. Intuitively, the autonomous hybrid systems do not admit any input. They are the hybrid systems analog of $\dot{x}=f(x)$. Hybrid control systems, on the other hand, admit both continuous and discrete control inputs. They are the hybrid systems analog of $\dot{x}=f(x,u)$. In a sense, for autonomous hybrid systems, the evolution of the states is completely determined by its initial state.¹

Research involving autonomous hybrid systems is typically of the analysis type, i.e., they are concerned with proving whether the systems have certain properties. One of the most important analysis problems in hybrid systems is the reachability/safety analysis, where the question of interest is whether the system can enter an undesirable state during its execution. Reachability/safety analysis has a lot of important practical applications, for example, in the safety analysis of air traffic systems [11, 12, 14, 25, 26], design verification for electronic circuits [18–20], design verification for synthetic biology [21, 27], and model analysis for biochemical processes [28].

Another type of analysis problems that is also studied a lot is the observability analysis (see e.g., the editorial [29]). Here, the question of interest is whether we can infer certain properties of the state trajectories by observing certain aspects thereof. An important problem of this type is fault diagnosis. The central question in fault diagnosis is whether we can infer that the state trajectory is faulty (e.g., it involves a directly unobservable fault event) from partial observation (e.g., by observing only the a part of the events in the system). Fault diagnosis for hybrid systems is an active research area, with applications in embedded control systems [30], process control [31], and others.

For hybrid control systems, there is a strong research interest involving synthesis. The synthesis part of the safety/reachability issue deals with the construction of control laws/algorithms for systems with input and controllable events, in order to achieve executions with desired properties (e.g., safety) despite uncertainties.

In this chapter, we review some results on reachability/safety analysis and synthesis and fault diagnosis for hybrid systems. The underlying theme of the results is that they are all trajectory based. That is, they make use of trajectories to represent the systems, and they are based on reasoning at the trajectory level, instead of at the system representation level.

20.3 Review of the Fundamentals

20.3.1 Hybrid Automata

Following [1], we define hybrid systems as hybrid automata. A hybrid automaton is expressed as an octuple $\mathcal {H} =(L,\mathcal {X},Init,A,\mathcal {U},E,Inv,\varSigma ),$ where:

• L is a finite set of discrete states, which are also called modes or locations.

• $\mathcal {X}$ is the continuos state space.

• $Init\subset \mathcal {X}\times L$ is the set of initial states.

• A is a finite set of transition symbols.

• $\mathcal {U}$ is the space of continuous input.

• E is the set of transitions.

• $Inv:L\rightarrow 2^{\mathcal {X}}$ defines the invariant sets of each location. For an $\ell \in L$, $Inv(\ell )$ is the set in which the continuous states must remain as long as the discrete state is $\ell$.

• $\varSigma$ assigns each location to its continuous dynamics. For each location $\ell \in L$, we define

  $$\begin{aligned} \varSigma (\ell ):\dot{x}=F_{\ell }(x),~x\in Inv(\ell ), \end{aligned}$$

  (20.1)

  if the hybrid system is autonomous, or

  $$\begin{aligned} \varSigma (\ell ):\dot{x}=F_{\ell }(x,u),~x\in Inv(\ell ),~u\in \mathcal {U}, \end{aligned}$$

  (20.2)

  if the hybrid system admits control inputs. Here we assume that for each location $F_{\ell }$ satisfies some conditions that guarantee well-posedness of the continuous dynamics.

Each transition in E is a pentuple $e=(\ell ,\ell ^{\prime },Guard,R,a)\in E$, where $\ell \in L$ is the origin of the transition, $\ell ^{\prime }\in L$ is the target location, $Guard\subset Inv(\ell )$ is the guard set of the transition, and $R:Inv(\ell )\rightarrow Inv(\ell ^{\prime })$ is the reset map. The symbol $a \in A$ is the symbol associated with the transition. The semantics of the execution of a hybrid automaton can be explained as follows: (see illustration in Fig. 20.1a). An execution trajectory of $\mathcal {H}$ is a sequence

$$\begin{aligned} (\ell _{0},x_{0},u_{0},e_{0},\varDelta _{0}),(\ell _{1},x_{1},u_{1},e_{1},\varDelta _{1}), \ldots ,(\ell _{N},x_{N},u_{N},\varnothing ,\varDelta _{N}), \end{aligned}$$

(20.3)

where for all values of i that appear here $\varDelta _{i}\in [0,\infty )$, $e_{i}\in E$, and $u_{i}:[0,\varDelta _{i}]\rightarrow \mathcal {U}$ is the input signal, if the hybrid system admits input. If the system does not admit any input, the execution trajectory is a sequence

$$\begin{aligned} (\ell _{0},x_{0},e_{0},\varDelta _{0}),(\ell _{1},x_{1},e_{1},\varDelta _{1} ), \ldots ,(\ell _{N},x_{N},\varnothing ,\varDelta _{N}). \end{aligned}$$

(20.4)

The initial state $(x_{0},\ell _{0})\in Init$. Each element of the sequence is essentially an interval of execution within which the discrete state is constant. These execution intervals can be characterized recursively as follows. For the ith interval, the value of the continuous state x(t) is given by $\xi _{i}(t)$, which satisfies $\xi _{i}(0)=x_{i}$ and the ODE given by $\varSigma (\ell _{i}).$ Within the time interval $[0,\varDelta _{i}]$, $\xi _{i}(t)\in Inv(\ell _{i})$. At time $t=\varDelta _{i},$ the transition $e_{i} =(\ell _{i},\ell _{i+1},Guard_{i},R_{i},a)$ occurs. That means $\xi _{i} (\varDelta _{i})\in Guard_{i}$ and the continuous state is reset for the next interval of execution. That is, for the $(i+1)$-st interval, the continuous state is initialized at $\xi _{i+1}(0)=x_{i+1}=R_{i}(\xi _{i}(\varDelta _{i}))$. Further, the symbol $a\in A$ is associated to the transition. If the transition is triggered externally, for example, a can be considered the discrete command that is given to the system. For the discussion in this chapter, we limit our attention to execution trajectories with finitely many intervals, and that the last interval does not terminate with a transition. Physically, the amount of time that elapses during the execution trajectory above is $\sum _{i=0}^{N}\varDelta _{i}$. Also, we only stipulate that the transitions occur when the continuous state is in the guard set of the transition. We do not stipulate (yet) whether the transitions happen spontaneously, i.e., triggered by the system’s own dynamics (example: a falling object bouncing off the floor), or they are triggered externally (example: switching gear in manual transmission).

Fig. 20.1

An illustration of (a) the execution trajectory of a hybrid automaton, b the concept of trajectory robustness

20.3.2 Trajectory Robustness

The key ingredient in our framework is the notion of trajectory robustness. With the notion of trajectory robustness, we provide a guarantee on how far the system’s state trajectories can deviate (in $L_{\infty }$ norm) as a result of initial state variations. This concept is easily extensible to treat system parameter variation, for example, by embedding the parameters as static states in the system. Therefore, although not explicitly stated, the following discussion also applies to variations in system parameter.

We construct trajectory robustness using the theory of approximate bisimulation, which was developed by Girard and Pappas [32–34]. This theory was subsequently extended to stochastic hybrid systems and trajectory-based analysis of hybrid systems [35–39]. In the following, we review the application of approximate bisimulation in establishing state trajectory robustness with respect to initial condition variation for a nonlinear dynamical system

$$\begin{aligned} \varSigma :\dot{x}=F(x),~x\in \mathcal {X}, \end{aligned}$$

(20.5)

where x is the state of the system, and $\mathcal {X}$ is the state space. Suppose that we can construct a differentiable function $\phi :\mathcal {X} \times \mathcal {X}\rightarrow \mathbb {R}$ such that

$$\begin{aligned} \phi (x,x^{\prime })\ge \left\| x-x^{\prime }\right\| ,\forall x,x^{\prime }\in \mathcal {X},\end{aligned}$$

(20.6a)

$$\begin{aligned} \frac{d\phi }{dt}=\frac{\partial \phi }{\partial x}F(x)+\frac{\partial \phi }{\partial x^{\prime }}F(x^{\prime })\le 0,\forall x,x^{\prime }\in \mathcal {X}. \end{aligned}$$

(20.6b)

Such a function $\phi (x,x^{\prime })$ is called a autobisimulation function [32–34].

Notation We denote the solution of (20.5) with initial state $x_{0}$ as $\xi (t,x_{0})$ and we define the ball

$$\begin{aligned} B_{\phi }(x,r)\triangleq \left\{ y\in \mathcal {X~}|~\phi (x,y)\le r\right\} ,~x\in \mathcal {X},~r>0. \end{aligned}$$

(20.7)

From (20.6b), we can easily conclude that the value of $\phi$ is nondecreasing along any two state trajectories of the system. From (20.6a), we can see that $\phi (x,x^{\prime })$ is an upper bound for the Euclidean distance between the two states. Then by combining these two properties, we can conclude that for all $t\ge 0$,

$$\begin{aligned}&\xi (t,x_{0}^{\prime }) \in B_{\phi }(\xi (t,x_{0}),\phi (x_{0},x_{0}^{\prime })),\end{aligned}$$

(20.8)

$$\begin{aligned}&\left\| \xi (t,x_{0})-\xi (t,x_{0}^{\prime })\right\| \le \phi (x_{0},x_{0}^{\prime }), \end{aligned}$$

(20.9)

for any initial state $x_{0}^{\prime }\in \mathcal {X}$. Please refer to Fig. 20.1b for an illustration of this concept.

Remark 20.1

The concept of trajectory robustness is very related to the concept of contraction metric developed by Lohmiller and Slotine [40]. In general, there are some differences between the two concepts. For example, autobisimulation function can also be defined as a pseudometric if we are only concerned about the divergence of the state trajectories in a certain subspace. Also, as the name suggests, bisimulation functions are originally defined to bound the divergence between the state trajectories of two different systems [33]. However, as defined in this chapter, if we also require that $\phi$ is a metric in $\mathcal {X}$, then it can be considered as a contraction metric.

The autobisimulation function $\phi$ plays an essential role in establishing trajectory robustness. If (20.5) defines a stable linear affine dynamics

$$\begin{aligned} \varSigma :\dot{x}=Ax+b,~x,b\in \mathbb {R}^{n},~A\in \mathbb {R}^{n\times n}, \end{aligned}$$

(20.10)

and A is Hurwitz, then $\phi$ can be using a quadratic Lyapunov function as follows [33, 38].

$$\begin{aligned} \phi (x,x^{\prime })=\sqrt{(x-x^{\prime })^{T}P(x-x^{\prime })}, \end{aligned}$$

(20.11)

where P is a symmetric positive definite matrix satisfying the Lyapunov Linear Matrix Inequality

$$\begin{aligned} A^{T}P+PA\preceq 0. \end{aligned}$$

(20.12)

If (20.5) defines a special class of nonlinear dynamics, the procedure above can be extended. For example, if F(x) in (20.5) is polynomial, we can search for a polynomial autobisimulation function. We refer the reader for more details on this to [39], where sum-of-squares optimization technique [41] is used for this purpose. For the discussion in this chapter, it suffices to consider the linear affine case above.

20.4 Approximation with Finite Behavior

Trajectory robustness gained from approximate bisimulation theory is a very useful tool. It allows us to approximate a dynamical system or a hybrid system with a representation that has finitely many trajectories. The main idea can be explained as follows. Consider the dynamics given by (20.5), and suppose that the system is known to have an initial state in a compact set $Init\subset \mathcal {X}$. This means, any trajectory of the system can be written as $\xi (t,x_{0}^{\prime }),$ for some $x_{0}^{\prime }\in Init$. Suppose that we have a bisimulation function $\phi$ that satisfies (20.6a), (20.6b). See the illustration in Fig. 20.2.

Fig. 20.2

Approximation of the sytem’s trajectories with a set of one trajectory (left) or finitely many trajectories (right)

If $x_{0}\in \mathcal {X}$ and $r>0$ are such that

$$\begin{aligned} Init\subset B_{\phi }(x_{0},r), \end{aligned}$$

(20.13)

then for any trajectory of the system $\xi (t,x'_{0})$, we have

$$\begin{aligned} \xi (t,x'_{0})\in B_{\phi }(\xi (t,x_{0}),r). \end{aligned}$$

(20.14)

Thus, we can think of a single trajectory $\xi (t,x_{0})$ as an approximation of the entire set of the system’s trajectories. Equation (20.14) essentially means that the accuracy of this approximation is given by r.

The idea above can be further generalized and stated as follows.

Theorem 20.2

Consider a family of initial states $x_{0,1},x_{0,2}, \ldots ,x_{0,M}\in \mathcal {X}$ and positive numbers $r_{1},r_{2}, \ldots ,r_{M}$ such that

$$\begin{aligned} Init\subset {\displaystyle \bigcup \limits _{k=1}^{M}} B_{\phi }(x_{0,k},r_{k}). \end{aligned}$$

(20.15)

For any $x_{0}^{\prime }\in Init$ there exists $k\in \{1, \ldots ,M\}$ such that

$$\begin{aligned} \xi (t,x_{0}^{\prime })\in B_{\phi }(\xi (t,x_{0,k}),r_{k}),\forall t\ge 0. \end{aligned}$$

(20.16)

The main point of this theorem is that the entire set of the system’s trajectories can be approximated by a finite set of trajectories. Again, the numbers $r_{1} ,r_{2}, \ldots ,r_{M}$ essentially define the accuracy of this approximation. The smaller they are, the approximation is more accurate but we can expect to need more balls to cover Init.

In the remainder of this section, we will discuss the extension of this idea to hybrid systems. We limit our discussion in this section to autonomous hybrid systems and leave control hybrid systems for Sect. 20.7.3. Consider a hybrid automaton $\mathcal {H}$ as defined in Sect. 20.3.1. Suppose that $L=\{\ell _{0},\ell _{1}, \ldots ,\ell _{|L|}\}$ and that for each discrete state $\ell _{i}\in L$ the continuous state dynamics

$$ \varSigma (\ell _{i}):\dot{x}=F_{\ell _{i}}(x) $$

admits an autobisimulation function $\phi _{i}$. Further, we assume that the guard sets of the transitions define the boundary of the invariant sets of the locations. Also, we assume the transitions in this system occur as soon as the continuous state hits a guard of a transition. Consider an execution trajectory of such hybrid automaton, as exemplified in (20.4). For simplicity of the discussion, let us assume that there are only two intervals, i.e., the trajectory is $(\ell _{0},x_{0},e_{0},\varDelta _{0}),(\ell _{1} ,x_{1},\varnothing ,\varDelta _{1})$. This is illustrated in Fig. 20.3. The transition $e_{0}=(\ell _{0},\ell _{1},Guard_{0},R_{0},a_0)$. We define $\overline{Guard}$ as the union of the guards of all transitions other than $e_{0}$ that start in $\ell _{0},$

$$\begin{aligned} R_{0}^{-1}\left( B_{\phi _{1}}(x_{1},r_{1})\right)&\triangleq \left\{ x\in Guard_{0}~|~R_{0}(x)\in B_{\phi _{1}}(x_{1},r_{1})\right\} ,\\ G_{0}&\triangleq Guard_{0}\backslash R_{0}^{-1}\left( B_{\phi _{1}} (x_{1},r_{1})\right) . \end{aligned}$$

We can formulate the following theorem (adapted from [38]).

Fig. 20.3

An illustration of an execution trajectory of a hybrid automaton and the concept of trajectory robustness

Theorem 20.3

Suppose that $r_{0},r_{1},\varepsilon _{0},\varepsilon _{0}^{\prime }>0$ are such that the following are true.

$$\begin{aligned}&B_{\phi _{0}}(x_{0},r_{0})\subset Init,\end{aligned}$$

(20.17a)

$$\begin{aligned}&B_{\phi _{0}}(\xi _{0}(t,x_{0}),r_{0})\not \cap (\overline{Guard}\cup G_{0}),~\forall t\in [0,\varDelta _{0}+\varepsilon _{0}],\end{aligned}$$

(20.17b)

$$\begin{aligned}&B_{\phi _{0}}(\xi _{0}(t,x_{0}),r_{0})\not \cap Inv(\ell _{0}),\end{aligned}$$

(20.17c)

$$\begin{aligned}&B_{\phi _{0}}(\xi _{0}(t,x_{0}),r_{0})\not \cap Guard_{0},~\forall t\in [0,\varDelta _{0}-\varepsilon _{0}^{\prime }] \end{aligned}$$

(20.17d)

Then, for any $x_{0}^{\prime }\in B_{\phi _{0}}(x_{0},r_{0})$ the following are also true:

• The execution trajectory starting from $(x_{0}^{\prime },\ell _{0})$ also exits $\ell _{0}$ through transition $e_{0}$.

• The transition occurs at time $\varDelta _{0}^{\prime }$, where $\varDelta _{0}^{\prime }\in [\varDelta _{0}-\varepsilon _{0}^{\prime },\varDelta _{0}+\varepsilon _{0}]$.

• In the first interval, for all $t\in [0,\varDelta _{0}^{\prime }]$, $\xi _{0}(t,x_{0}^{\prime })\in B_{\phi _{0}}(\xi _{0}(t,x_{0}),r_{0})$.

• After the transition $e_{0}$, the continuous state is reset into $B_{\phi _{1}}(x_{1},r_{1})$.

This theorem can be generalized to trajectories with more intervals. Essentially, it shows that the trajectory starting at $(\ell _{0},x_{0})$ is an approximation of those starting in the location $\ell _{0}$ with initial continuous state in the neighborhood of $x_{0}$ in the sense that (i) the divergence of the continuous state trajectory is bounded in the sense of Theorem 20.2, (ii) the sequence of transitions are preserved, and (iii) the divergence of the transition times is bounded. Following the same idea as in Theorem 20.2, if the set of initial states is compact, we can use Theorem 20.3 to approximate the set of trajectories of a hybrid automaton with a finite set of trajectories.

20.5 Safety/Reachability Analysis

Safety/reachability analysis is concerned with the question whether any of the system’s state trajectories enters a predefined set of unsafe states. For a dynamical system as in (20.5) with a set of initial states Init, we define a set $Unsafe\subset \mathcal {X}$ and ask whether there is an initial state $x_{0}^{\prime }\in Init$ such that $\xi (t^{\prime },x_{0})\in Unsafe$ for some $t^{\prime }\in [0,T]$. If such initial state does not exist then the system is safe.² This is illustrated in Fig. 20.4. The question described above is called bounded-time safety/reachability analysis, because of the specified upper bound T. If the dynamics (20.5) admits an autobisimulation function $\phi$, then the following result can be stated.

Fig. 20.4

Left An illustration of the safety property. Right How trajectory robustness can be used in safety/reachability analysis

Proposition 20.4

See the illustration in Fig. 20.4. If $r>0$ is such that

$$ B_{\phi }(\xi (t,x_{0}),r)\not \cap {\,}Unsafe,~\forall t\in [0,T], $$

then there exists no initial state $x_{0}^{\prime }\in B_{\phi }(x_{0},r)$ from which the state trajectory enters Unsafe in the time interval [0, T].

This proposition allows us to generalize the safety property of the trajectory initialized at $x_{0}$ to other trajectories initialized at other states in its neighborhood. Further, the safety of the entire system can be proved by analyzing the safety of finitely many trajectories, as stated below.

Theorem 20.5

Consider a family of initial states $x_{0,1},x_{0,2}, \ldots ,x_{0,M}\in \mathcal {X}$ and positive numbers $r_{1},r_{2}, \ldots ,r_{M}$ such that

$$\begin{aligned} Init\subset {\displaystyle \bigcup \limits _{k=1}^{M}} B_{\phi }(x_{0,k},r_{k}). \end{aligned}$$

(20.18)

If for each $k\in \{1, \ldots ,M\}$

$$ B_{\phi }(\xi (t,x_{0,k}),r_{k})\not \,\cap Unsafe,~\forall t\in [0,T], $$

then the system is safe.

For an autonomous hybrid automaton $\mathcal {H}$, safety/reachability analyis can be setup by defining a set of unsafe states $Unsafe\subset \mathcal {X} \times L$. Again, the system is deemed safe if for any state trajectory initialized in $Init\subset \mathcal {X} \times L$, the resulting state trajectory does not enter Unsafe. Next, we formulate the analog of Proposition 20.4 for autonomous hybrid automaton. Consider the hybrid automaton discussed in Sect. 20.4, and its execution trajectory that is discussed in Theorem 20.3. The trajectory is $(\ell _{0} ,x_{0},e_{0},\varDelta _{0}),(\ell _{1},x_{1},\varnothing ,\varDelta _{1})$.

Proposition 20.6

Suppose that $r_{0},r_{1},\varepsilon _{0},\varepsilon _{0}^{\prime }>0$ satisfy the conditions (20.17a), (20.17d) in Theorem 20.3. In addition, suppose that

$$\begin{aligned} B_{\phi _{0}}(\xi _{0}(t,x_{0}),r_{0})\not \,\cap Unsafe,~\forall t&\in [0,\varDelta _{0}+\varepsilon _{0}],\\ B_{\phi _{1}}(\xi _{1}(t,x_{1}),r_{1})\not \,\cap Unsafe,~\forall t&\in [0,\varDelta _{1}]. \end{aligned}$$

Then, for any $x_{0}^{\prime }\in B_{\phi _{0}}(x_{0},r_{0})$ the following are also true:

• The execution trajectory starting from $(x_{0}^{\prime },\ell _{0})$ is safe until transition $e_{0}$ that happens at time $\varDelta _{0}^{\prime }$, i.e.,

  $$ \xi _{0}(t,x_{0}^{\prime })\notin Unsafe,~\forall t\in [0,\varDelta _{0}^{\prime }]. $$

• Afterwards, in location $\ell _{1}$, the execution trajectory is safe for $\varDelta _{1}$ time units, i.e.,

  $$ \xi _{1}(t,R_{0}\left( \xi _{0}(\varDelta _{0}^{\prime },x_{0}^{\prime })\right) )\notin Unsafe,~\forall t\in [0,\varDelta _{1}]. $$

This proposition can be generalized to the case where the execution trajectory has more intervals. Also, if the set of initial states Init can be covered by the union of balls as in Theorem 20.5, then we can prove that the system is safe. More details on this idea is reported in [38, 42, 43].

20.6 Observability and Fault Diagnosability

Observability analysis can be intuitively explained as follows. Suppose that the set $\mathfrak {B}$ contains all trajectories of the system, and $\pi _{1}:\mathfrak {B}\rightarrow \mathfrak {P}_{1}$ and $\pi _{2}:\mathfrak {B} \rightarrow \mathfrak {P}_{2}$ are surjective maps with co-domains $\mathfrak {P}_{1}$ and $\mathfrak {P}_{2}$ respectively. The map $\pi _{1}$ can be considered as observation map that extracts information from the trajectories in $\mathfrak {B}$. If this map is bijective, then all information from the trajectories in $\mathfrak {B}$ is retained. Otherwise, multiple distinct trajectories in $\mathfrak {B}$ are mapped to the same element in $\mathfrak {P}_{1}$, representing the idea that some information (that distinguishes these trajectories) is lost in the observation. The map $\pi _{2}$ represents another aspect of the trajectories in $\mathfrak {B}$. We say that $\mathfrak {P}_{2}$ is observable from $\mathfrak {P}_{1}$ if the composite map $\pi _{1}^{-1}\circ \pi _{2}$ is injective, where $\pi _{1}^{-1}$ is the set-theoretic inverse map of $\pi _{1}$. This means the observed information from $\pi _{1}$ can uniquely determine the output of $\pi _{2}$.

In classical linear systems theory, this (behavioral) definition of observability coincides with the notion of observability for state-space systems [44]. That is, if we define the state-space system as

$$\begin{aligned} \varSigma _{\mathrm {lin}}:\left\{ \begin{array} [c]{l} \dot{x}=Ax+Bu,~x\in \mathbb {R}^{n},u\in \mathbb {R}^{m},\\ y=Cx+Du,~y\in \mathbb {R}^{p}, \end{array} \right. \end{aligned}$$

(20.19)

we define $\mathfrak {B}$ to be the set of (x, u, y) trajectories that are compatible with this system description. The map $\pi _{1}$ takes such trajectories and retains only the x components. The map $\pi _{2}$ is the identity map. The characterization of observability as discussed in the previous paragraph coincides with the well-known Kalman rank condition

$$\begin{aligned} \mathrm {rank}[C^{T}~A^{T}C^{T}~ \ldots \left( A^{T}\right) ^{n}C^{T}]=n. \end{aligned}$$

(20.20)

For hybrid automata as in Sect. 20.3.1, the notion of observation can be more general. In particular, in this chapter, we consider the observation that simply retains only the discrete aspect of the trajectories. This can be made precise using the following definition.

Definition 20.7

For a hybrid automaton $\mathcal {H}$ as defined in Sect. 20.3.1, we define the function $\varGamma :E\rightarrow A$ to map any transition $e\in E$ to its transition symbol. For an execution trajectory

$$\begin{aligned} \omega \triangleq (\ell _{0},x_{0},e_{0},\varDelta _{0}),(\ell _{1},x_{1},e_{1} ,\varDelta _{1}), \ldots ,(\ell _{N},x_{N},\varnothing ,\varDelta _{N}), \end{aligned}$$

(20.21)

we define the map

$$\begin{aligned} \pi _{\mathrm {discrete}}(\omega )\triangleq \left( \varGamma (e_{0}),\varDelta _{0}\right) ,(\varGamma (e_{1}),\varDelta _{1}), \ldots ,(\varnothing ,\varDelta _{N}). \end{aligned}$$

(20.22)

The map $\pi _{\mathrm {discrete}}$ essentially takes the execution trajectory and returns only the symbols of the transitions and the intervals between the occurrence of the symbols. Note that $\varGamma$ is not necessarily injective, which implies that the transitions are not necessarily distinguishable one from another. As an extreme case, A is a singleton. That means we can only observe when a transition has occurred, but not which transition. Observability analysis for this kind of observation map has been considered, for example by Di Benedetto et al. in [45] where the question is whether the discrete state can be uniquely determined there from.

Fault diagnosability analysis is related to observability analysis. Suppose that $\mathfrak {B}$, the set of trajectories of the system, can be divided into two disjoint partitions, $\mathfrak {B}_{\mathrm {nom}}$ and $\mathfrak {B} _{\mathrm {fault}}$. $\mathfrak {B}_{\mathrm {nom}}$ represents the normal behavior of the system, while $\mathfrak {B}_{\mathrm {fault}}$ represents the faulty behavior of the system. That is, $\mathfrak {B}_{\mathrm {fault}}$ consists of trajectories where a fault occurs. If we again define the observation map $\pi _{1}:\mathfrak {B}\rightarrow \mathfrak {P}_{1}$ as above, then the system is fault diagnosable from the observation map $\pi _{1}$ if for any $p\in \mathfrak {P}_{1}$, $\pi _{1}^{-1}(p)$ is either strictly in $\mathfrak {B}_{\mathrm {nom}}$ or strictly in $\mathfrak {B}_{\mathrm {fault}}$. In other words, based on the observation defined by $\pi _{1}$, we can always conclude whether the trajectory is normal or faulty.

Although the basic concept is easy to understand, in practice verifying fault diagnosabilty is difficult because the system typically has infinitely many trajectories. However, if we can approximate the system with another one with finitely many trajectories, as explained in Sect. 20.4, then the analysis is much simpler. This is illustrated in Fig. 20.5.

Fig. 20.5

By approximating all the system’s trajectories with a set of finitely many trajectories, we can reduce fault diagnosability analysis to a finite problem

Suppose that $\mathfrak {B}$ can be approximated with $\mathfrak {B}^{\prime }$ that only has finitely many trajectories. That is, there exists an injective map $\alpha :\mathfrak {B}\rightarrow \mathfrak {B}^{\prime }$ such that for any trajectory $\omega \in \mathfrak {B}$, $\alpha (\omega )\in \mathfrak {B}^{\prime }$ is an approximation of $\omega$. Intuitively, $\omega$ and $\alpha (\omega )$ are close to each other. To be precise, suppose that $\mathfrak {P}_{1}$ is equipped with a metric $\left\| \cdot \right\| _{p}$ and

$$\begin{aligned} \left\| \pi _{1}(\omega )-\pi _{1}(\alpha (\omega ))\right\| _{p}\le r,~\forall \omega \in \mathfrak {B}. \end{aligned}$$

(20.23)

Then, if we define

$$ \mathfrak {B}_{\mathrm {nom}}^{\prime }\triangleq \alpha (\mathfrak {B} _{\mathrm {nom}}),~\mathfrak {B}_{\mathrm {fault}}^{\prime }\triangleq \alpha (\mathfrak {B}_{\mathrm {fault}}), $$

we have the following result.

Theorem 20.8

If for any $\omega _{1}\in \mathfrak {B}_{\mathrm {nom}}^{\prime }$ and $\omega _{2}\in \mathfrak {B}_{\mathrm {fault}}^{\prime }$

$$\begin{aligned} \left\| \pi _{1}(\omega _{1})-\pi _{1}(\omega _{2})\right\| >2r \end{aligned}$$

(20.24)

then the system is fault diagnosable.

Note that checking the condition (20.24) in this theorem is practically possible because both $\mathfrak {B}_{\mathrm {nom}}^{\prime }$ and $\mathfrak {B}_{\mathrm {fault}}^{\prime }$ have finitely many trajectories.

For an autonomous hybrid automaton, suppose that $\omega$ is an execution trajectory given in (20.21) and $\alpha (\omega )$ is the approximate trajectory in the sense of Theorem 20.3. From the theorem, we know that both trajectories have the same sequence of transitions, and the timing of transitions are close. That is, if the observation map is $\pi _{\mathrm {discrete}}$ and $\pi _{\mathrm {discrete}}(\omega )$ is as given in (20.22), then

$$\begin{aligned}&\pi _{\mathrm {discrete}}(\alpha (\omega ))=\left( \varGamma (e_{0}),\varDelta _{0}^{\prime }\right) ,(\varGamma (e_{1}),\varDelta _{1}^{\prime }), \ldots ,(\varnothing ,\varDelta _{N}),\end{aligned}$$

(20.25)

$$\begin{aligned}&\varDelta _{k}^{\prime }\in [\varDelta _{k}-\varepsilon ,\varDelta _{k} +\varepsilon ],\forall k\in \{0,1, \ldots ,N-1\}, \end{aligned}$$

(20.26)

for some $\varepsilon > 0$. The distance between $\pi _{\mathrm {discrete}}(\omega )$ and $\pi _{\mathrm {discrete}}(\alpha (\omega ))$ can be defined in terms of the timing difference, and hence the distance can be bounded as in (20.23). Therefore, we can use Theorem 20.8 to verify fault diagnosability for autonomous hybrid automata based on observing the timing of the transitions and the respective transition symbols. This is the underlying idea behind some recent work on fault diagnosability of some classes of hybrid systems [46] and probabilistic hybrid systems [47].

20.7 Controller Synthesis

In this section, we discuss the controller synthesis problem related to safety/ reachability properties. For a dynamical system given by

$$\begin{aligned} \varSigma :\dot{x}=F(x,u),~x\in \mathcal {X},~u\in \mathcal {U}, \end{aligned}$$

(20.27)

where F is well-posed, the problem can be posed as follows. Given a compact set of initial condition $Init\subset \mathcal {X}$, and a set of goal states $Goal\subset \mathcal {X}$, we want to steer the state starting from any initial state $x_{0}\in Init$ such that the state trajectories enter Goal at time $t=T$ and in the time interval [0, T] the state remains safe (does not enter a set of states termed Unsafe).

The notion of trajectory robustness discussed in Sect. 20.3.2 can also be used in trajectory-based controller synthesis. The key concept in this approach is the control autobisimulation function (CAF) [48, 49]. A continuously differentiable function $\psi :\mathcal {X}\times \mathcal {X}\rightarrow \mathbb {R}$ is a control autobisimulation function of (20.5) if for any $x,x^{\prime }\in \mathcal {X},$ $\psi (x,x^{\prime })\ge \left\| x-x^{\prime }\right\|$, and there exists a function $k:\mathcal {X}\rightarrow \mathcal {U}$ such that

$$\begin{aligned} \frac{d\psi }{dt}=\frac{\mathbb {\partial }\psi }{\partial x}f(x,k(x))+\frac{\mathbb {\partial }\psi }{\partial x^{\prime }}f(x^{\prime },k(x^{\prime }))\le 0. \end{aligned}$$

(20.28)

Remark 20.9

The control autobisimulation function is an analog of the control Lyapunov function (CLF) [50], for trajectory robustness [33, 38]. While control Lyapunov function has been used to construct control laws that guarantee stability (e.g., [51]), we shall use the control autobisimulation function to construct control laws that guarantee trajectory robustness.

A consequence of the existence of a CAF is the existence of a feedback control law $u=k(x),$ such that the closed-loop system

$$\begin{aligned} \dot{x}=F(x,k(x)),x\in \mathcal {X}, \end{aligned}$$

(20.29)

has $\psi (\cdot ,\cdot )$ as a autobisimulation function (see Sect. 20.3.2). For a given dynamical system $\varSigma$ in (20.27) and a control autobisimulation function $\psi$, the class of all feedback control laws $k(\cdot )$ that satisfy (20.28) is called the class of admissible feedback laws.

Notation For a given dynamical system $\varSigma$ in (20.27) and a feedback control law $u=k(x),$ the closed-loop trajectory with initial condition $x(0)=x_{0}$ is denoted by $\xi _{k}(t,x_{0})$. For a control autobisimulation function $\psi$, $x\in \mathcal {X},$ $r>0$, we define the ball

$$\begin{aligned} B_{\psi }(x,r)\triangleq \{y\in \mathcal {X}~|~\psi (x,y)\le r\}. \end{aligned}$$

The trajectory-based controller synthesis paradigm can be stated as follows. We first construct feedback controllers from the class of feasible feedback laws. By definition, the closed-loop system will then admit a predefined autobisimulation function. This means that the trajectory robustness property discussed in Sect. 20.3.2 is guaranteed to hold. Please refer to Fig. 20.6 for an illustration.

Theorem 20.10

Suppose that for a given initial state $x_{0}\in Init$, we can design an admissible feedback law $u=k_{0}(x)$ that results in a closed-loop execution trajectory $\xi _{k_{0}}(t,x_{0})$ satisfying

$$\begin{aligned}&B_{\psi }(\xi _{k_{0}}(t,x_{0}),r_{0})\not \cap {\,} Unsafe,~\forall t\in [0,T],\end{aligned}$$

(20.30)

$$\begin{aligned}&B_{\psi }(\xi _{k_{0}}(t,x_{0}),r_{0})\subset Goal. \end{aligned}$$

(20.31)

Then, for any initial state $x_{0}^{\prime }\in B_{\psi }(\xi _{k_{0}} (t,x_{0}),r_{0}),$ the closed-loop trajectory $\xi _{k_{0}}(t,x_{0})$ is also safe for $t\in [0,T]$ and is in the Goal set at $t=T$.

Fig. 20.6

An illustration for trajectory-based controller synthesis

Therefore, the admissible feedback law $u=k_{0}(x)$ is applicable not only for the initial state $x_{0}$ but also to other initial states in its neighborhood. The controller synthesis procedure can be performed in two steps:

Step 1:

For a given initial state, synthesize an innerloop controller that endows the system with the trajectory robustness property.

Step 2:

Obtain finitely many trajectories resulting from Step 1 that have the desired qualitative properties to cover Init. Note that the controller in Step 1 can depend on the initial state.

Effectively, the trajectory robustness approach allows us to reduce the problem of finding a control law that works for infinitely many initial states in Init to a problem where this has to be done for finitely many initial states. Moreover, the control law can depend on the initial state, and the control law for each initial state can be designed independently of the others’. Steering the system from a particular initial state, is arguably an easier task than finding a control law that works for the entire Init set. Thus, we break down a hard problem into a finite number of simpler and parallelizable problems.

20.7.1 Controller Synthesis for Linear Affine Dynamics

The synthesis of the CAF and the controllers for systems with linear affine dynamics is discussed below. In this case, F(x, u) in (20.27) takes the form

$$\begin{aligned} F(x,u)=Ax+f+Bu,~x\in \mathbb {R}^{n},u\in \mathbb {R}^{m}, \end{aligned}$$

(20.32)

where $A\in \mathbb {R}^{n\times n},$ $f\in \mathbb {R}^{n},$ and $B\in \mathbb {R}^{n\times m}$. For such systems, we again construct CAF as quadratic functions [48, 49]. That is, we assume that

$$\begin{aligned} \psi (x,x^{\prime })=\sqrt{(x-x^{\prime })^{T}P(x-x^{\prime })}, \end{aligned}$$

(20.33)

where $P\in \mathbb {R}^{n\times n}$ is a positive definite matrix. In this case, the inequality (20.28) becomes

$$\begin{aligned} (x-x^{\prime })^{T}P\left( A(x-x^{\prime })+B(k(x)-k(x^{\prime }))\right) \le 0. \end{aligned}$$

(20.34)

We then construct a feedback law of the form $u(t)=k(x)=Kx+v(t),$ where $K\in \mathbb {R}^{m\times n}$, and $v(t)\in \mathbb {R}^{m}$ is a time-varying function, both to be determined later. With this controller, (20.34) becomes

$$\begin{aligned} (x-x^{\prime })^{T}P\left( A+BK\right) (x-x^{\prime })\le 0. \end{aligned}$$

(20.35)

A well-known result in control theory (see e.g., [52, 53]) states that there exist P and K such that (20.35) holds if and only if (A, B) is stabilizable. In this case, there are well-known methods to synthesize the suitable P and K. For example, we can pose (20.24) as a linear matrix inequality (LMI) [54], which can be solved efficiently using existing semidefinite programming software tools, such as SeDuMi or SDPT3. With some modification, this method can also be used to handle magnitude constraint on the input signal, $\left\| u\right\| _{L_{\infty }}\le M,$ for some $M>0$ [48, 49].

Notice that given P and K that satisfy (20.35), we are still free to design v(t). Whatever v(t) is, the control law is admissible. The remaining task in the controller design is therefore to find v(t) that steers the trajectories of the closed-loop system from Init to the Goal set, without entering the Unsafe set. This corresponds to Step 2 in the previous section. The problem of finding such v(t) for a given initial state is easier to solve than the original problem, because the control input is only required to work for that particular initial state. We can use a variety of methods for this, for example, using path planning methods from robotics [48], or by using human inputs [49].

In this chapter, we use v(t) as a feedforward control input that depends on the initial state x(0). It is actually possible to define v(t) through a feedback control law, i.e., as a function of x(t). Such feedback law can be learned from the feedforward control input, and is guaranteed to have the same safety property as the feedforward controller above. For further discussion on this topic, the reader is referred to [55].

20.7.2 Controller Synthesis for Nonlinear Dynamics

The results from the previous section can be generalized to some classes of systems with nonlinear dynamics [56]. We consider systems of the form:

$$\begin{aligned} \varSigma :\left\{ \begin{array} [c]{l} \frac{dx}{dt}=f(x)+g(x)u,~x\in \mathbb {R}^{n},u\in \mathbb {R}^{m},\\ y=h(x),~y\in \mathbb {R}^{m}, \end{array} \right. \end{aligned}$$

(20.36)

where y is the output of the system. We assume that the safety and goal reaching properties of the system can be expressed in terms of y (instead of x).

20.7.2.1 Feedback Linearizable Systems

If (20.36) is feedback linearizable (for a comprehensive discussion, the reader is referred to standard textbooks on Nonlinear Control Systems such as [57, 58]), there exists a feedback law

$$\begin{aligned} u(t)=\kappa (x)+\lambda (x)w(t),~w(\cdot )\in \mathbb {R}^{m}, \end{aligned}$$

(20.37)

such that the closed-loop system, with new input w(t) and output y(t), is a linear system. The necessary and sufficient conditions for feedback linearizability and the design procedure for $\kappa (x)$ and $\lambda (x)$ are covered in the above-mentioned books. In the context of our discussion, the linearizing feedback can be implemented as an inner feedback loop. Once the system is linear, we can apply the results from the previous section for controller synthesis. This method has been applied in designing a controller for fully actuated flexible robot arms [59], whose dynamics are feedback linearizable.

20.7.2.2 Differentially Flat Systems

Differentially flat systems are widely encountered in mechanical and robotics systems. For examples and comprehensive discussion, the reader is referred to [60–62]. The system in (20.37) is differentially flat if it has flat outputs. The outputs $y=(y_{1},\ldots ,y_{m})$ are flat outputs if x and u can be written as functions of y and its time derivatives,

$$\begin{aligned} x=\varXi (y,\dot{y},\ldots ,y^{(\ell )}),~~u=\varUpsilon (y,\dot{y},\ldots ,y^{(\ell +1)}), \end{aligned}$$

(20.38)

for some integer $\ell$, and $(y,\dot{y},\ldots ,y^{(\ell )})$ are not constrained to satisfy a differential equation by themselves. In other words, any sufficiently smooth trajectory y is admissible as an output trajectory of the system.

A differentially flat system is related to a linear system, namely an $\ell {\text {th}}$ order integrator chain, through the transformation in (20.38). In the context of our discussion, we can apply the results from the previous section for controller synthesis for the integrator chain. The controller for the nonlinear system (20.37) can then be obtained using the transformation in (20.38).

20.7.3 Controller Synthesis for Hybrid Systems

Consider the control hybrid automata defined in Sect. 20.3.1. For simplicity of the discussion, let us assume that the continuous state dynamics in each location is linear affine. That is, suppose that $L=\{\ell _{0},\ell _{1}, \ldots ,\ell _{|L|}\}$ and that for each discrete state $\ell _{i}\in L$ the continuous state dynamics is

$$ \varSigma (\ell _{i}):\dot{x}=A_{\ell _{i}}x\,+\,f_{\ell _{i}}+B_{\ell _{i}}u, $$

where $A_{\ell _{i}}$, $B_{\ell _{i}}$, and $f_{\ell _{i}}$ are matrices with appropriate dimensions, and the pair $(A_{\ell _{i}},B_{\ell _{i}})$ is stabilizable. Therefore, the continuous state dynamics in each location admits a control autobisimulation function $\psi _{i}$.

Fig. 20.7

Illustration of forcing and nonforcing guards of hybrid automata. From different initial states in location $\ell _{1}$, the trajectories can undergo different evolution and transition to different locations. The set Guard 1 represents a nonforcing transition, while Guard 2 represents a forcing transition

We assume there are two types of transitions, forcing and nonforcing. A forcing transition occurs immediately when the continuous state hits the guard, which is the case for autonomous hybrid automata in Sect. 20.4. See Fig. 20.7, where the guards of forcing transitions are illustrated as lines on the boundary of the invariant set of location $\ell _{1}$. A nonforcing transition can happen at any time while the continuous state is in its guard. In Fig. 20.7, this is illustrated by the transition from location $\ell _{1}$ to $\ell _{2}$. In this case, the guard set is “thick,” indicating that the transition can happen, but not necessarily as soon as the guard is hit. The occurrence of a nonforcing transition can be user-triggered (corresponding to a discrete control input), or externally triggered. Nonforcing transitions are useful to model events whose occurrence is not predetermined (uncertain) because it is to be triggered by the user/controller, or it is triggered externally at an a priori unknown time.

In defining the control specification, we define a set of initial state $Init\subset \mathcal {X}\times L$. We assume that there is a subset $Unsafe\subset \mathcal {X}\times L$ of unsafe states. A trajectory of the hybrid system corresponds to an unsafe execution if it enters the unsafe set. We also define the set $Goal\subset \mathcal {X}\times L$, which must be entered by the state trajectory. Again, the control problem is defined as finding the feedback control strategy that is guaranteed to bring any initial state in Init to the Goal set without entering the Unsafe set.

Without any loss of generality, we can assume that the set Init is contained in (the invariant set of) one location, called $\ell _{\mathrm {init}}\in L$. If this is not the case, we can divide the problem into several subproblems, each with an Init set contained in a specific location. Similarly, we can assume the Goal is also entirely contained in one location, called $\ell _{\mathrm {goal}}\in L.$

Controller synthesis for hybrid systems can be done using a hierarchical approach, which can be described in the following steps:

Step 1: Discrete Synthesis. We compute a discrete trajectory that starts in $\ell _{\mathrm {init}}$ and ends in $\ell _{\mathrm {goal}}$. By discrete trajectory, we mean an alternating sequence of locations and transitions

$$\begin{aligned} \ell _{\mathrm {init}}=\ell _{0}\overset{e_{0}}{\rightarrow }\ell _{1} \overset{e_{1}}{\rightarrow }\ell _{2}\overset{e_{2}}{\rightarrow }\cdots \overset{e_{N-1}}{\rightarrow }\ell _{N}=\ell _{\mathrm {goal}}. \end{aligned}$$

(20.39)

Each transition $e_{i}$, $i\in \{0,\ldots ,N-1\}$, is an element of E, originating in $\ell _{i}$, and targeting $\ell _{i+1}$. We require that each transition here is either forcing or user-triggered. Such a discrete trajectory is not necessarily unique, but at this step we only need one. The computation of such a discrete trajectory is a standard procedure in formal verification of discrete event systems [63]. For this purpose, there are many good algorithms and computational tools that can be used, such as STRIPS and PDLL [64].

Step 2: Continuous Synthesis. In this step, we synthesize the continuous controller for each of the visited locations ($\ell _{0,1,\dots ,N}$) in order to implement the computed discrete trajectory. In each location $\ell _{i},$, we define an initial set based on how $\ell _{i}$ is reached from $\ell _{i-1}$. We then formulate the control problem of bringing the continuous state from this initial set to the interim goal set, which is the guard of transition $e_{i}$ that will bring the state to location $\ell _{i+1}$ without entering the forbidden set. The forbidden set is defined as the union of Unsafe and the guards of other forcing transitions from $\ell _{i}$. This is thus an instance of the control problem discussed in Sect. 20.7.1. If we are able to construct a continuous controller that implements the discrete trajectory, then the hybrid control problem is solved. Otherwise, we go back to Step 1, and compute another discrete trajectory.

Remark 20.11

The control problem that we discuss in this chapter is only concerned with the safety/reachability property. In addition, it is possible to formulate an optimal control problem in which a performance objective needs to be optimized while maintaining the safety/reachability property. For further discussion on the trajectory-based approach to this problem, the reader is referred to [65].

20.8 Concluding Remarks

We review some results that allow us to use trajectory-level reasoning in solving some problems in safety/reachability analysis of hybrid systems, controller synthesis for safety/reachability, and fault diagnosability of hybrid systems. The main feature of this approach is the possibility to break down a problem involving infinitely many trajectories of the system into one that only involves finitely many of them.

While we focus solely on safety/reachability property in this chapter, the discussion is actually generalizable to verification of and controller synthesis for other properties, such as those that can be described with temporal logics. In addition, there have also been extension work that consider stochasticity in the dynamics.