From f431fc1a9615fc278de2a78cd2aa75aca28519b7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Zden=C4=9Bk=20Hur=C3=A1k?= Date: Wed, 18 Dec 2024 11:02:20 +0100 Subject: [PATCH] Built site for gh-pages --- .nojekyll | 2 +- classes_PWA 14.html | 1190 ++ classes_PWA.html | 6 + classes_references.html | 6 + classes_reset 16.html | 1499 ++ classes_reset.html | 142 +- classes_software.html | 6 + classes_switched.html | 64 +- complementarity_constraints 20.html | 1267 ++ complementarity_constraints.html | 6 + complementarity_references.html | 6 + complementarity_simulations.html | 1686 +- complementarity_software.html | 6 + complementarity_systems.html | 6 + des.html | 6 + des_automata.html | 22 +- des_references 13.html | 1108 ++ des_references.html | 6 + des_software.html | 6 + hybrid_automata 27.html | 1624 ++ hybrid_automata.html | 6 + hybrid_automata_references 13.html | 1058 ++ hybrid_automata_references.html | 6 + hybrid_automata_software.html | 6 + hybrid_equations 16.html | 1808 +++ hybrid_equations.html | 160 +- hybrid_equations_references.html | 6 + hybrid_equations_software 15.html | 1064 ++ hybrid_equations_software.html | 6 + index 18.html | 1048 ++ index.html | 6 + intro 14.html | 1175 ++ intro.html | 6 + intro_outline.html | 6 + intro_references.html | 6 + max_plus_algebra.html | 13014 ++++++++-------- max_plus_references.html | 6 + max_plus_software.html | 6 + max_plus_systems.html | 6 + mld_DHA 26.html | 1187 ++ mld_DHA.html | 6 + mld_intro.html | 6 + mld_references.html | 6 + mld_software.html | 6 + mld_why.html | 6 + mpc_mld_explicit 23.html | 1348 ++ mpc_mld_explicit.html | 146 +- mpc_mld_online 17.html | 1145 ++ mpc_mld_online.html | 6 + mpc_mld_references 25.html | 1085 ++ mpc_mld_references.html | 6 + mpc_mld_software 26.html | 1059 ++ mpc_mld_software.html | 6 + petri_nets.html | 6 + petri_nets_references.html | 6 + petri_nets_software 19.html | 1093 ++ petri_nets_software.html | 6 + petri_nets_timed.html | 6 + search.json | 1155 +- sitemap.xml | 66 +- solution_concepts 15.html | 1213 ++ solution_concepts.html | 6 + solution_references.html | 6 + solution_types.html | 6 + stability_concepts.html | 6 + stability_recap 25.html | 1263 ++ stability_recap.html | 6 + stability_references.html | 6 + stability_software.html | 6 + stability_via_common_lyapunov_function.html | 6 + stability_via_multiple_lyapunov_function.html | 8 +- verification_barrier.html | 2778 ++-- verification_intro 22.html | 1299 ++ verification_intro.html | 6 + verification_reachability.html | 6 + verification_references 26.html | 1126 ++ verification_references.html | 32 +- verification_software.html | 1115 ++ verification_temporal_logics.html | 30 +- 79 files changed, 35753 insertions(+), 9590 deletions(-) create mode 100644 classes_PWA 14.html create mode 100644 classes_reset 16.html create mode 100644 complementarity_constraints 20.html create mode 100644 des_references 13.html create mode 100644 hybrid_automata 27.html create mode 100644 hybrid_automata_references 13.html create mode 100644 hybrid_equations 16.html create mode 100644 hybrid_equations_software 15.html create mode 100644 index 18.html create mode 100644 intro 14.html create mode 100644 mld_DHA 26.html create mode 100644 mpc_mld_explicit 23.html create mode 100644 mpc_mld_online 17.html create mode 100644 mpc_mld_references 25.html create mode 100644 mpc_mld_software 26.html create mode 100644 petri_nets_software 19.html create mode 100644 solution_concepts 15.html create mode 100644 stability_recap 25.html create mode 100644 verification_intro 22.html create mode 100644 verification_references 26.html create mode 100644 verification_software.html diff --git a/.nojekyll b/.nojekyll index d918255..51436c3 100644 --- a/.nojekyll +++ b/.nojekyll @@ -1 +1 @@ -3b03cec5 \ No newline at end of file +8efd858f \ No newline at end of file diff --git a/classes_PWA 14.html b/classes_PWA 14.html new file mode 100644 index 0000000..c796f02 --- /dev/null +++ b/classes_PWA 14.html @@ -0,0 +1,1190 @@ + + + + + + + + + +Piecewise affine (PWA) systems – B(E)3M35HYS – Hybrid systems + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+
+ +
+ +
+ + +
+ + + +
+ +
+
+

Piecewise affine (PWA) systems

+
+ + + +
+ + + + +
+ + + +
+ + +

This is a subclass of switched systems where the functions on the right-hand side of the differential equations are affine functions of the state. For some (historical) reason these systems are also called piecewise linear (PWL).

+

We are going to reformulate such systems as switched systems with state-driven switching.

+

First, we consider the autonomous case, that is, systems without inputs: +\dot{\bm x} += +\begin{cases} +\bm A_1 \bm x + \bm b_1, & \mathrm{if}\, \bm H_1 \bm x + \bm g_1 \leq 0,\\ +\vdots\\ +\bm A_m \bm x + \bm b_m, & \mathrm{if}\, \bm H_m \bm x + \bm g_m \leq 0. +\end{cases} +

+

The nonautonomous case of systems with inputs is then: +\dot{\bm x} += +\begin{cases} +\bm A_1 \bm x + \bm B_1 u + \bm c_1, & \mathrm{if}\, \bm H_1 \bm x + \bm g_1 \leq 0,\\ +\vdots\\ +\bm A_m \bm x + \bm B_m + \bm c_m, & \mathrm{if}\, \bm H_m \bm x + \bm g_m \leq 0. +\end{cases} +

+
+

Example 1 (Linear system with saturated linear state feedback) In this example we consider a linear system with a saturated linear state feedback as in Fig 1.

+
+
+
+ +
+
+Figure 1: Linear system with a saturated linear state feedback +
+
+
+

The state equations for the close-loop system are +\dot{\bm x} = \bm A\bm x + \bm b \,\mathrm{sat}(v), \quad v = \bm k^T \bm x, + which can be reformulated as a piecewise affine system +\dot{\bm x} = +\begin{cases} +\bm A \bm x - \bm b, & \mathrm{if}\, \bm x \in \mathcal{X}_1,\\ +(\bm A + \bm b \bm k^\top )\bm x, & \mathrm{if}\, \bm x \in \mathcal{X}_2,\\ +\bm A \bm x + \bm b, & \mathrm{if}\, \bm x \in \mathcal{X}_3,\\ +\end{cases} + where the partitioning of the space of control inputs is shown in Fig 2.

+
+
+
+ +
+
+Figure 2: Partitioning the control input space +
+
+
+

Expressed in the state space, the partitioning is +\begin{aligned} +\mathcal{X}_1 &= \{\bm x \mid \bm H_1\bm x + g_1 \leq 0\},\\ +\mathcal{X}_2 &= \{\bm x \mid \bm H_2\bm x + \bm g_2 \leq 0\},\\ +\mathcal{X}_3 &= \{\bm x \mid \bm H_3\bm x + g_3 \leq 0\}, +\end{aligned} + where +\begin{aligned} +\bm H_1 &= \bm k^\top, \quad g_1 = 1,\\ +\bm H_2 &= \begin{bmatrix}-\bm k^\top\\\bm k^\top\end{bmatrix}, \quad \bm g_2 = \begin{bmatrix}-1\\-1\end{bmatrix},\\ +\bm H_3 &= -\bm k^\top, \quad g_3 = 1. +\end{aligned} +

+
+
+

Approximation of nonlinear systems

+

While the example with the saturated linear state feedback can be modelled as a PWA system exactly, there are many practical cases, in which the system is not exactly PWA affine but we want to approximate it as such.

+
+

Example 2 (Nonlinear system approximated by a PWA system) Consider the following nonlinear system +\begin{bmatrix} +\dot x_1\\\dot x_2 +\end{bmatrix} += +\begin{bmatrix} +x_2\\ +-x_2 |x_2| - x_1 (1+x_1^2) +\end{bmatrix} +

+

Our task is to approximate this system by a PWA system. Equivalently, we need to find a PWA approximation for the right-hand side function.

+
+ + +
+ + Back to top
+ + +
+ + + + + + \ No newline at end of file diff --git a/classes_PWA.html b/classes_PWA.html index 29e05fc..c98ebd5 100644 --- a/classes_PWA.html +++ b/classes_PWA.html @@ -608,6 +608,12 @@ Temporal logics + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
  • CTL*
  • Timed computation tree logic (TCTL)
  • Metric temporal logic (MTL)
  • +
  • Metric interval temporal logic (MITL)
  • Signal temporal logic (STL)
  • @@ -810,7 +817,7 @@

    Linear temporal

    Computation tree logic (CTL)

    -

    Supports branching. Path quantifiers needed

    +

    Also branching termporal logic as it supports branching. Path quantifiers needed

    @@ -857,13 +864,24 @@

    Metric temporal

    +
    +

    Metric interval temporal logic (MITL)

    +

    An extension of MTL, which does not allow singleton time intervals allowed by MTL. The motivation for this extension is that the verification of MTL requirements has been shown to be undecidable.

    +

    Signal temporal logic (STL)

    -

    STL je then an extension of MTL with real-valued constraints.

    +

    STL is then an extension of MTL with real-valued constraints. Available for both continuous- and discrete-time systems.

    +

    It allows combinations of surveillance (“visit regions A, B, and C every 10–60 s”), safety (“always between 5–25 s stay at least 1 m away from D”), and many others. I

    -

    Example 4 +

    Example 4 (Examples of STL formulas) \square (x(t) \leq 5.5 \Rightarrow \Diamond_{(1,10)} \mathrm{greenLight})

    +

    +\Diamond_{(0,60)}\square_{(0,20)} (x(t)\leq 5.5) +

    +

    +\square\Diamond_{[0,10]} (\bm x(t) \in \mathcal A) \land \square\Diamond_{[0,10]} (\bm x(t) \in \mathcal B) +

    @@ -1294,8 +1312,8 @@

    Signal temporal

    Path quantifiers