Control Platform — Algorytmy sterowania w praktyce

Verification & Validation — formalne gwarancje bezpieczeństwa

Stabilność (Lyapunov) mówi czy stan zbiega do zera. W aplikacjach safety-critical (autonomiczne pojazdy, medycyna, roboty współpracujące) potrzebujemy mocniejszej gwarancji: czy stan nigdy nie wejdzie w obszar niedopuszczalny. To jest safety verification.

Control Barrier Functions (CBF)

Analogia. Wyobraź sobie ogrodzenie wokół obszaru niedopuszczalnego (np. przepaść). Nominalny kontroler może chcieć tam wejść (gradient celu prowadzi przez przepaść). CBF to minimalna modyfikacja sterowania, która gwarantuje, że ogrodzenie zostanie nieprzekroczone — bez zmiany nominalnego zachowania gdziekolwiek indziej.

Idea (Ames, Coogan, Egerstedt 2017): zdefiniuj funkcję barriera $h(x)$ taką że bezpieczny obszar to $\{x : h(x) \ge 0\}$ . Wtedy gwarantujemy niezmienność obszaru przez warunek:

\dot h(x) + \alpha\,h(x) \ge 0, \quad \alpha > 0

Co prowadzi do liniowego warunku na $u$ :

\nabla h(x)^T (f(x) + g(x) u) + \alpha h(x) \ge 0

Minimum-modification sterowanie: rozwiąż QP:

u^* = \arg\min_u \|u - u_{nom}\|^2 \;\text{s.t. CBF constraint}

Gdy $u_{nom}$ jest bezpieczne, CBF nic nie robi (u* = u_nom). Gdy $u_{nom}$ łamie barrier, CBF modyfikuje minimalnie żeby barriera zostać zachowana.

x_0 (start x)-2.0

Reachability analysis

Dla danego zbioru stanów początkowych $X_0$ i ograniczonej polityki, reachable set $\mathcal R$ = wszystkie stany osiągalne. Verification: sprawdź, czy $\mathcal R \cap X_{unsafe} = \emptyset$ .

Algorytmy:

Hamilton-Jacobi reachability (Mitchell, Bayen, Tomlin 2005) — PDE na funkcji wartości najgorszego przypadku. Skalowalne do ~5 wymiarów.
Zonotopes, polytopy (Althoff, Krogh 2014) — reprezentacja reachable set jako wielokąty/zbiory wypukłe. Skalowalność do 10+ wymiarów ale tylko dla układów liniowych i sektorowych nieliniowości.
Numerical sampling — Monte Carlo dla wysoko wymiarowych. Brak formalnych gwarancji, ale praktyczne.

Sum-of-Squares (SOS) programming

Parrilo 2000 — technika konstrukcji funkcji Lapunova dla układów wielomianowych przez convex optimization. Funkcja $V(x)$ jest sum-of-squares jeśli $V = \sum_i p_i(x)^2 \ge 0$ . Warunek $-\dot V \ge 0$ dla układów wielomianowych można sprawdzić przez programming SDP.

Pozwala automatycznie generować dowody stabilności dla układów wielomianowych — bez wyboru kandydata V „z głowy". Krytyczne dla weryfikacji złożonych nieliniowych regulatorów (np. sieci neuronowe).

Aktualne kierunki badawcze

Safe RL z CBF — RL eksploruje, CBF gwarantuje że eksploracja nie naruszy ograniczeń. Krytyczne dla autonomicznych systemów uczących się online.
Neural network verification — algorytmy do dowodzenia własności sieci jako kontrolerów (Reluplex, Marabou).
Hybrid verification — łączenie SMT solvers z reachability dla systemów hybrydowych.

Lektura: Ames et al. „Control Barrier Functions: Theory and Applications" (ECC 2019) — przegląd; Tedrake „Underactuated Robotics" — Lyapunov methods w robotyce.