Real-Time Monitoring, Verification, and Control of Cyber-Physical Systems
summary
Introduces satisfiability modulo convex programming — a concrete solver that loops a SAT engine with a convex optimizer that returns infeasibility certificates, turning hybrid-system feasibility into a finite disjunction of convex programs. Uses application structure (reverse‑BFS ordering) to extract a shortest infeasible prefix so the loop needs only a constant or linear number of convex solves, yielding orders‑of‑magnitude speedups. Demonstrates near‑real‑timesecure state estimation on a drone that isolates attacked sensors and recovers, plus stream monitors that do constant work per sample.
AI-written summary · about
chapters (21)
- 0:00Intro
- 1:26Safety-Critical CPS
- 4:52Robot Control and Motion Planning
- 6:55Run-Time Verification and Monitoring
- 9:16Secure State Estimation and Localization
- 11:27Talk Outline Hybrid Systems
- 12:03Abstraction Based Techniques
- 12:52Optimization Based Techniques
- 13:32Two Extremes
- 16:28Example: Obstacle Avoidance
- 17:53Generalizing: Monotone SMC Formulas
- 18:21Applications: Controller Synthesis
- 18:32Applications: CPS Security
- 19:23Boolean Expansion
- 20:01Lazy Solver Approach
- 21:42Complexity of Solving SMC
- 22:23Minimal UNSAT Certificate
- 22:36Summary of UNSAT certificates
- 23:16Minimum Prefix Certificates
- 25:41Scalability Results
- 26:10Applications (2): Secure CPS