Korean, Edit

Chapter 10. Hybrid Systems

Recommended reading: 【Control Theory】 Control Theory Table of Contents

1. Overview

2. Regular Expressions

3. Hybrid System Modeling

4. Hybrid System Stability

5. Advanced Topics

1. Overview

⑴ Type 1. Discrete system

① 1-1. Combinational Logic

② 1-2. Sequential Logic

⑵ Type 2. Continuous system

① 2-1. Flow Algorithm

⑶ Type 3. Hybrid system = discrete + continuous system

2. Regular Expressions (regex, RE)

⑴ Definition

① $\Sigma$: alphabet (e.g., $\Sigma = {A, B}$)

② letter: an element of $\Sigma$. Denoted by $E$, $A$, $B$, etc.

③ $\mathcal{L}$: conversion into a regular expression (RE)

○ $\mathcal{L}(A) = A,\; \forall \text{ letter } A \in \Sigma$

④ $\epsilon$: empty string (0-length string)

○ $\mathcal{L}(\epsilon) = {\epsilon}$

⑤ $\emptyset$: empty set

○ $\mathcal{L}(\emptyset) = \emptyset$

⑥ $\mathcal{L}(E^*) = {w_1w_2\cdots w_n \mid n \ge 0,\; w_i \in \mathcal{L}(E),\; \forall i \le n}$

○ Here, $E$ is not the unknown $E$ currently being defined, but an expression that has already been recognized as a regular expression in a previous step.

⑦ $E := A \mid \epsilon \mid \emptyset \mid (E_1 + E_2) \mid E_1E_2 \mid E^*$

○ This is not circular reasoning, but a recursive/inductive definition.

○ In other words, it does not assume that an arbitrary $E$ already exists; rather, regular expressions are constructed sequentially according to the following rules.

○ $\mathcal{L}(E_1+E_2) = \mathcal{L}(E_1) \cup \mathcal{L}(E_2)$

○ $\mathcal{L}(E_1E_2) = {w_1w_2 \mid w_1 \in \mathcal{L}(E_1),\; w_2 \in \mathcal{L}(E_2)}$

○ $\mathcal{L}(\epsilon E) = \mathcal{L}(E\epsilon) = E,\; \mathcal{L}(\emptyset E) = \mathcal{L}(E\emptyset) = \emptyset$

○ If $n=0$, $E,\epsilon \in \mathcal{L}(E^*)$

○ $\mathcal{L}(\emptyset^*) = {\epsilon}$

○ If $\Sigma = {A,B}$, then $\Sigma^* = {\epsilon,A,B,AA,AB,BA,BB,\cdots}$

○ If $E_1=A$ and $E_2=E_1^$, then $\mathcal{L}(E_1)={A}\subseteq\Sigma^$, $\mathcal{L}(E_2)={\epsilon,A,AA,AAA,\cdots}\subseteq\Sigma^*$

○ If $E_1=A$ and $E_3=B$, then $\mathcal{L}(E_1^E_2)={B,AB,AAB,AAAB,\cdots}\subseteq\Sigma^$

⑧ $^\omega$: infinitely many repetitions

○ $\omega$-regular expression $G = E_1F_2^\omega + \cdots + E_nF_n^\omega$

○ $(A+B)^*B^\omega$: finitely many repetitions of $A$ or $B$ + infinitely many repetitions of $B$

⑨ A regular expression always has a corresponding graph representation.

○ Among strings in ${A,B}^$, all strings ending in $B$ are represented by $(A+B)^B$

Figure 1. Graph representation corresponding to $(A+B)^*B$

○ Example 2. A string that repeats $A$ or $B$ several times, then contains $B$, and ends with $A$ or $B$ is represented by $(A+B)^*B(A+B)$

Figure 2. Graph representation corresponding to $(A+B)^*B(A+B)$

⑵ LTL (Linear Temporal Logic): $\text{LTL-definable} \subsetneq \omega\text{-regular}$

① $\varphi ::= \mathrm{true} \mid a \mid \varphi₁ \land \varphi₂ \mid \neg\varphi \mid \bigcirc\varphi \mid \varphi₁ \mathcal{U} \varphi₂$

○ Unary operator binds strongly than binary operator.

○ $\mathcal{U}$ takes precedence over $\land,\ \lor,\ \to$.

② $a$: atomic proposition

③ $\bigcirc a$: next step $a$

○ Also called $X$.

④ $a \mathcal{U} b$: $a$ until $b$. $a$ does not have to occur once, but $b$ must occur at least once.

Figure 3. The meaning of $a,\ \bigcirc,\ \mathcal{U}$

⑤ $W$: weak until. It is acceptable even if the until condition is never satisfied.

⑥ $\Diamond\varphi := \mathrm{true}\ \mathcal{U}\ \varphi$ (eventually) = \neg\Box\neg\varphi$

○ Also called $F$ (finally).

⑦ $\Box\varphi := \neg\Diamond\neg\varphi$ (always)

○ Also called $G$ (globally).

Figure 4. The meaning of $\Diamond,\ \Box$

Figure 5. The definition of $a,\ \land,\ \neg,\ \bigcirc,\ \mathcal{U},\ \Diamond,\ \Box$

⑧ $\varphi \mathcal{R} \psi := \neg(\neg\varphi \mathcal{U} \neg\psi)$, where $\mathcal{R}$ is the release operator.

○ $\varphi \mathcal{R} \psi \equiv \psi \land \left(\varphi \lor \bigcirc(\varphi \mathcal{R} \psi)\right)$: $\psi$ must hold now, and either $\varphi$ holds now or the release condition must continue to hold from the next state onward.

○ $\mathrm{False} \mathcal{R} \psi \equiv \Box \psi$: $\psi$ must always hold.

○ $\mathrm{True} \mathcal{R} \psi \equiv \psi$: $\psi$ only needs to hold at the current state.

⑨ $p \to q$: $p$ leads to $q$

○ If the premise $p$ is false, the proposition is always true.

○ The proposition is false only when the premise $p$ is true and the conclusion $q$ is false.

⑩ $p \to \Diamond q$: $p$ implies eventually $q$ (response)

⑪ $p \to (q \mathcal{U} r)$: $p$ implies $q$ until $r$ (precedence)

⑫ $\Box\Diamond p = \Box(\Diamond p)$: always eventually $p$ (progress) = $p$ is on infinitely often

⑬ $\Diamond\Box p$: eventually always $p$ (stability)

⑭ $\Diamond p \to \Diamond q$: eventually $p$ implies eventually $q$ (correlation)

⑮ $p \mathcal{U} q \mathcal{U} r = p \mathcal{U} (q \mathcal{U} r)$

⑯ $\neg\Diamond(a \land b \land c) = \Box\neg(a \land b \land c)$

⑰ Example 1. $P = {A_0 A_1 A_2 \cdots \in (2^{AP})^\omega \mid \forall j \ge 0,\ a \in A_{2j}}$

○ $P$ is not expressed as LTL with $AP = {a, b, c}$, but still regular/$\omega$-regular.

○ With $AP’ = {a, b, c, t}$, $\psi = t \land \Box(t \to \bigcirc\neg t) \land \Box(\neg t \to \bigcirc t) \land \Box(t \to a)$

⑱ Example 2. $P = {A_0 A_1 A_2 \cdots \in (2^{AP})^\omega \mid \exists j \ge 0,\ b \in A_j,\ \exists i > j,\ c \in A_i,\ \exists k \ge i \text{ s.t. } A_\ell = {a,c}\ \forall \ell \ge k}$

○ $\Diamond(b \land \bigcirc\Diamond(c \land \Diamond\Box(\neg b \land a \land c)))$

⑲ Example 3. $P=\lbrace A_0A_1A_2\cdots\in(2^{AP})^\omega\mid \exists j\geq 0\ \text{s.t.}\ a\in A_k\ \forall k\geq j,\ \exists i>j\ \text{s.t.}\ A_i=\lbrace c,a \rbrace,\ \exists l>i\ \text{s.t.}\ c\notin A_m\ \forall m\geq l\rbrace$

○ $\Diamond(\Box a\land\bigcirc\Diamond(a\land\neg b\land c\land\bigcirc\Diamond\Box(\neg c)))$

○ True^∗𝑎𝑎^∗(𝑎∧¬𝑏∧𝑐)𝑎^∗(𝑎∧¬𝑐)^ω

⑶ Signal Temporal Logic (STL)

Figure 6. STL with an example

① Equivalent to LTL in discrete time.

② Define robust semantics using worst-case semantics.

3. Hybrid System Modeling

⑴ Overview

① Definition: interconnected continuous system + discrete system

② General automaton and hybrid automaton

○ A guard is a condition under which a transition is allowed; it does not mean that the transition must occur immediately when the condition is satisfied.

Table 1. General automaton and hybrid automaton

③ Example 1. bouncing of a ball, diauxic microbial colony growth, switching, thermostat

Figure 7. Bouncing of a ball

○ $Q = {q_0}$

○ $X = \mathbb{R}^2$

○ $f$: $f(q_0,x) = [x_2,g]$

○ $\mathrm{Init} = {q_0} \times {x \in \mathbb{R}^2 \mid x_1 \ge 0}$

○ $\mathrm{Inv}(q_0) = {x \in \mathbb{R}^2 \mid x_1 \ge 0}$

○ $E = {(q_0,q_0)}$

○ $G$: $G(q_0,q_0) = {x \in \mathbb{R}^2 \mid x_1=0,\;x_2\le0}$

○ $R$: $R((q_0,q_0),x)={x’ \in \mathbb{R}^2 \mid x_1’=x_1,\;x_2’=-cx_2}$

④ Example 2. NFA (nondeterministic finite automaton): hybrid system represented by a regular expression

○ $\mathcal{A}=(Q,\Sigma,\delta,Q_0,F)$

○ $Q$: finite set of states

○ $\Sigma$: finite set called alphabet

○ $\delta$: $\delta:Q\times\Sigma\rightarrow2^Q$ is a transition function

○ $Q_0\subseteq Q$: set of initial states

○ $F\subseteq Q$: set of accepting states = bad prefix detected

⑤ Example 3. Product of transition system and NFA

○ $S’=S\times Q$; $S$ concerns the transition system, whereas $Q$ concerns the NFA

○ $\mathrm{Act}’=\mathrm{Act}$

○ $\to’$: if $s\xrightarrow{\alpha}t$, $s,t\in S$, and $q\xrightarrow{L(t)}p$, $q,p\in Q$, then $\langle s,q\rangle\xrightarrow{\alpha}’\langle t,p\rangle$

○ $I’={\langle s_0,q\rangle \mid s_0\in I \text{ and } \exists q_0\in Q_0\text{ s.t. }q_0\xrightarrow{L(s_0)}q}$

○ $AP’=Q$

○ $L’$: $L’:S\times Q\rightarrow2^Q,\;L’(\langle s,q\rangle)={q}$

⑥ Example 4. NBA (nondeterministic Büchi automaton)

○ NFA and NBA differ only in the definition of the accepting set $F$; everything else is identical.

○ $\mathrm{Inf}(\rho)$: the set of states among the elements of $\rho$ that are visited infinitely often

⑵ Solution

① hybrid time-set

② hybrid trajectory (execution, discrete transition): one complete path representing how the system actually evolves over time

○ $\tau$: hybrid time-set indicating when the system flows and when it jumps

○ $a$: functions indicating how the actual state evolves during each time interval

○ flow → jump/reset → flow → jump/reset → $\cdots$

○ behavior: the set of all executions

○ Conditions

○ Condition 1. Starts from a valid initial state

○ Condition 2. Within each mode, the system evolves according to the corresponding differential equation (Lipschitz continuous)

○ Condition 3. When the transition condition (guard) is satisfied, the mode changes through an allowed edge

○ Condition 4. The state after a jump is determined by the reset map

○ Property 1. existence

○ Property 2. Zenoness

○ finite: when $N$ is finite and $I_N$ is closed and bounded

○ finite-open: when $N$ is finite and $I_N=[z_n,z_n’)$, $z_n’\neq\infty$

○ infinite: when $N$ is infinite or $\sum(z_i’-z_i)=\infty$

○ zeno: when $N$ is infinite and $\sum(z_i’-z_i)<\infty$. A subset of infinite executions

○ maximal execution: an execution developed to the maximum extent such that it cannot be extended any further in time. That is, it is not a subset

○ Property 3. determinism (uniqueness): the hybrid system has only one maximal execution

○ If $\mathrm{Init}$ is not a singleton, there is non-determinism

○ Property 4. blockingness (terminal): means that upon reaching a certain state, the system can no longer continue the hybrid execution

○ non-blocking = $\forall(q_0,x)\in\mathrm{Init}$, there exists at least one infinite execution

○ More precisely, the system is non-blocking if the execution can continue to be extended from every reachable state; otherwise, it is blocking

○ By introducing a dummy node, every hybrid system can be assumed to be non-blocking

③ path

○ transition system $TS=(S,\mathrm{Act},\to,I,AP,L)$

○ $\alpha$-successors of $s$: $\mathrm{Post}(s,\alpha)={s’\in S\mid s\xrightarrow{\alpha}s’}$ (where $s\in S$, $\alpha\in\mathrm{Act}$)

○ $\alpha$-predecessors of $s$: $\mathrm{Pre}(s,\alpha)={s’\in S\mid s’\xrightarrow{\alpha}s}$ (where $s\in S$, $\alpha\in\mathrm{Act}$)

○ set of successors of $s$: $\mathrm{Post}(s)=\bigcup_{\alpha\in\mathrm{Act}}\mathrm{Post}(s,\alpha)$ (where $s\in S$, $\alpha\in\mathrm{Act}$)

○ set of predecessors of $s$: $\mathrm{Pre}(s)=\bigcup_{\alpha\in\mathrm{Act}}\mathrm{Pre}(s,\alpha)$ (where $s\in S$, $\alpha\in\mathrm{Act}$)

○ $\pi=s_0s_1\cdots=\text{path fragment}\iff s_{i+1}\in\mathrm{Post}(s_i),\;\forall i\ge0$

○ $\pi=s_0s_1\cdots=\text{initial path fragment}\iff\pi=\text{path fragment AND }s_0\in\mathrm{Init}$

○ $\pi=s_0s_1\cdots s_n=\text{maximal path fragment}\iff\pi=\text{path fragment AND }(n\neq\infty\text{ AND }\mathrm{Post}(s_n)=\emptyset\text{ OR }n=\infty)$

○ $\mathrm{Paths}(TS)$ = paths in $TS$

○ $\mathrm{Paths}_{\mathrm{fin}}(TS)\iff\pi=\text{initial AND maximal path fragment}$

○ $s\in S$ is reachable $\iff\exists$ initial finite path fragment $\pi=s_0s_1\cdots s_n$ s.t. $s_n=s$

○ $\mathrm{Reach}(TS)$ = all reachable states of $TS$

④ trace

○ $\mathrm{Trace}(TS)={\mathrm{trace}(\pi)\mid\pi\in\mathrm{Paths}(TS)}$

○ $\mathrm{trace}(\pi)\in(2^{AP})^\omega$

⑤ run

○ NFA $\mathcal{A}=(Q,\Sigma,\delta,Q_0,F)$

○ $w=A_1\cdots A_n\in\Sigma^*$: finite word

○ run for $w$ in $\mathcal{A}=q_0q_1\cdots q_n$, $q_0\in Q_0$, $q_i\xrightarrow{A_{i+1}}q_{i+1}$, $\forall\,0\le i<n<\infty$

○ run is accepting: $\forall n,\;q_n\in F$

○ finite word $w\in\Sigma^$ is accepted by $$: there is an accepting run for $w$

○ accepted language of $\mathcal{A}$ = $\mathcal{L}(\mathcal{A})={w\in\Sigma^*\mid\text{there is an accepting run of }w\text{ in }\mathcal{A}}$

⑥ LT (linear time) property: a concept contrasted with a branching-time property

○ invariance: a state property represented in propositional form

○ $P_{\mathrm{inv}}:={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid j\ge0,\;A_j\models\Phi}$

○ Here, $P_{\mathrm{inv}}$ is an invariance property, $\Phi$ is propositional logic, and $A_j$ concerns only $j$

○ Verification method: if $\forall s\in\mathrm{Reach}(TS),\;L(s)\models P$, then $TS\models P$

○ Example 1. $P_1={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid\forall j\ge0,\;A_j\notin{{r,g},{r,y,g}}}$ is an invariance property Yes

○ Example 2. $P_2={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid\exists^\infty j\ge0,\;A_j={g}}$ is not an invariance property: $\exists^\infty$ means that infinitely many exist

○ Example 3. $P_3={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid(\forall j\ge0\text{ s.t. }A_j={g}),\;A_{j+1}={r}}$ is not an invariance property

○ Example 4. $P_4={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid A_0\neq{r}}$ is not an invariance property

○ Example 5. $P_5={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid\forall j\ge0,\;A_j\neq\emptyset}$ is an invariance property Yes

○ Example 6. $P_6={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid\exists n\ge0,\;A_j=\emptyset,\;\forall j\ge n}$

○ safety: a property that, once violated, remains violated forever (= it can never be repaired by appending any string)

○ $(2^{AP})^\omega\setminus P_{\mathrm{safe}}$: all infinite traces that violate $P_{\mathrm{safe}}$

○ $(2^{AP})^*$: set of finite traces (= words)

○ $\mathcal{L}\cdot(2^{AP})^\omega$: all infinite traces that begin with a finite prefix contained in $\mathcal{L}$

○ $(2^{AP})^\omega\setminus P_{\mathrm{safe}}=\mathcal{L}\cdot(2^{AP})^\omega$: means that every violating infinite trace has some finite bad prefix

○ The set of all bad prefixes (= the largest $\mathcal{L}$; the formal maximum) is called $\mathrm{BadPref}(P_{\mathrm{safe}})$

○ Verification method: use automata on finite words

○ Example 1. Every invariance property is a safe property: once it is violated, it can no longer be said to be true

○ Example 2. $P_1={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid\forall j\ge0,\;A_j\notin{{r,g},{r,y,g}}}$ is a safety property Yes

○ Example 3. $P_2={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid\exists^\infty j\ge0,\;A_j={g}}$ is not a safety property

○ Example 4. $P_3={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid\forall(j\ge0\text{ s.t. }A_j={g}),\;A_{j+1}={r}}$ is a safety property Yes

○ Example 5. $P_4={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid A_0\neq{r}}$ is a safety property Yes

○ Example 6. $P_5={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid\forall j\ge0,\;A_j\neq\emptyset}$ is a safety property Yes

○ Example 7. $P_6={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid\exists n\ge0,\;A_j=\emptyset,\;\forall j\ge n}$ is not a safety property

○ Example 8. $\mathrm{BadPref}(P_1)={w_0Aw_1\mid w_0\in(2^{AP})^,\;A\in{{r,g},{r,y,g}},\;w_1\in(2^{AP})^}$

○ Example 9. $p \mathcal{W} q$ is a safety property, whereas $p \mathcal{U} q$ is not.

○ Related to the recursively enumerablity of Turing machines.

○ liveness: a property that, regardless of any problems that occurred earlier, can remain satisfied forever after some point

○ $w\in(2^{AP})^*$: for each finite word $w$

○ $\sigma\in(2^{AP})^\omega$: infinite word

○ Verification method: use automata on infinite words

○ Example 1. $P_1={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid\forall j\ge0,\;A_j\notin{{r,g},{r,y,g}}}$ is not a liveness property

○ Example 2. $P_2={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid\exists^\infty j\ge0,\;A_j={g}}$ is a liveness property Yes

○ Example 3. $P_3={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid\forall(j\ge0\text{ s.t. }A_j={g}),\;A_{j+1}={r}}$ is not a liveness property

○ Example 4. $P_4={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid A_0\neq{r}}$ is not a liveness property

○ Example 5. $P_5={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid\forall j\ge0,\;A_j\neq\emptyset}$ is not a liveness property

○ Example 6. $P_6={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid\exists n\ge0,\;A_j=\emptyset,\;\forall j\ge n}$ is a liveness property Yes

○ Example 7. $P_8=P_2\cap P_4$ is neither a safety property nor a liveness property

○ Example 8. Safety properties and liveness properties are almost disjoint

○ regular safe property: a case in which $\mathrm{BadPref}(P_{\mathrm{safe}})$ is represented by a regular language

○ A property requiring some condition involving prime numbers in a language is not a regular language

○ Verification method

○ $\omega$-regular property

○ All invariance properties, regular safety properties, and various liveness properties are $\omega$-regular

○ persistence property

○ $P_{\mathrm{pers}}={A_0A_1A_2\cdots\in(2^{AP})^\omega\mid\exists k\ge0\text{ s.t. }\forall j\ge k,\;A_j\models\Phi}$

○ Verification method: verify whether every cycle in the traversal graph satisfies the invariance property $\Phi$

○ safety vs liveness

Table 2. safety vs liveness

○ Alpern-Schneider theorem

○ The only LP property that is both safety ($S$) and liveness ($L$) is a property satisfied by an infinite word

○ A theorem stating that every property $P$ can be decomposed into $S\cap L$

○ Example 1. $p \mathbin{U} q = (p \mathbin{W} q) \land Fq$

4. Hybrid System Stability

⑴ Overview

Figure 8. Types of stability

⑵ Stability of General Control Systems

① Type 1. continuous-time linear system

○ $\dot{x}=Ax\iff x(t)=e^{At}x(0)$ (where $A$ is a Hurwitz matrix)

○ Hurwitz stability: for $x(t)$ to be asymptotically stable, its equilibrium point must be $x=0$, and a necessary condition is $\operatorname{Re}(\lambda_i(A))<0,\;\forall i$

○ Lyapunov stability: stable if there exists $P\succ0$ satisfying $A^TP+PA\prec0$

○ Example

② Type 2. discrete-time linear system

○ $x_{k+1}=Ax_k\iff x_k=A^kx_0$

○ Schur stability: for $x_k$ to be stable, $

\lambda_i(A)

<1,\;\forall i$

○ Lyapunov stability: stable if there exists $P\succ0$ satisfying $A^TPA-P\prec0$

○ Example

③ Type 3. nonlinear system

○ $\dot{x}=f(x)$

○ linearization) Stability

○ Lyapunov stability

○ Let the equilibrium point be $x^*=0$, $f(0)=0$, and let the Lyapunov candidate be $V(x)$. Then $V(x)>0$ $(x\neq0)$, $V(0)=0$, $\dot{V}(x)=\nabla V(x)^Tf(x)$

○ If $V(x)>0$ and $\dot{V}(x)\le0$, the system is stable; if $V(x)>0$ and $\dot{V}(x)<0$, the system is asymptotically stable

○ Interpretation: $V$ represents energy, and as time passes, the energy continuously decreases → the state moves toward the equilibrium

○ LaSalle’s theorem

④ Type 4. disturbance system

○ $x_{k+1}=Ax_k+w_k$

○ If ‖w_k‖_∞ ≤ ε, to ensure ‖x_k‖_∞ ≤ α, the following inequality must hold:

○ ‖x_k+1‖_∞ ≤ ‖A‖_∞‖x_k‖_∞ + ‖w_k‖_∞ ≤ ‖A‖_∞α + ε ≤ α

○ cf. ‖A‖_∞ ≤ 1 − ε/α

⑶ Stability of Hybrid Systems

① Type 1. Deductive verification

○ Lyapunov-tye verification (barrier verification)

② Type 2. Algorithmic verification

○ Finite-state approximation

○ Construction of reachable states (e.g., Zonotope): similar to the verification of discrete systems.

5. Advanced Topics

⑴ Stability (ref1, ref2, ref3, ref4, ref5, ref6, ref7, ref8)

⑵ Verification, Reachability, and Abstraction (ref1, ref2, ref3, ref4, ref5)

⑶ Verification of Learning-enabled Systems and Safe AI (ref1, ref2, ref3, ref4, ref5, ref6, ref7, ref8, ref9, ref10, ref11)

⑷ Hybrid Model Predictive Control (ref1, ref2, ref3, ref4)

⑸ Synthesis (ref1, ref2, ref3, ref4, ref5, ref6, ref7)

⑹ Abstraction, Model Reduction, and System Identification (ref1, ref2, ref3, ref4, ref5)

⑺ Applications (ref1, ref2, ref3, ref4, ref5, ref6, ref7)

⑻ Computational Geometry (ref1, ref2, ref3, ref4, ref5)

⑼ Modeling (ref1, ref2, ref3, ref4, ref5)

Input: 2026.09.01 16:29