Non-linear Invariants for Control-Command Systems
- Pierre Roux | ONERA
Control theorists know for long that quadratic invariants, that is ellipsoids, are a good solution to bound the behavior of linear controllers, which constitute the heart of most control-command systems. They designed methods to synthesize such invariants using some convex optimization techniques, namely semidefinite programming solvers. The first part of this talk will briefly introduce those methods.
In practice, these techniques heavily rely on numerical computations performed using floating-point arithmetic, raising stringent soundness questions about their results. We will thus investigate solutions to formally validate such results and see that this is feasible with only a small overhead.
Finally, we present a simple implementation in the Alt-Ergo SMT solver and comparison with other state-of-the-art SMT solvers on non-linear real arithmetic benchmarks. We also introduce an implementation in the Coq proof assistant with a reflexive tactic enabling to automatically discharge polynomial inequalities proofs. Benchmarks indicate that we are able to formally address problems that would otherwise be untractable with other state-of-the-art methods.
[Slides]
-
-
Tahina Ramananandro
Principal Research Software Development Engineer
-
-
Series: Microsoft Research Talks
-
Decoding the Human Brain – A Neurosurgeon’s Experience
- Dr. Pascal O. Zinn
-
-
-
-
-
-
Challenges in Evolving a Successful Database Product (SQL Server) to a Cloud Service (SQL Azure)
- Hanuma Kodavalla,
- Phil Bernstein
-
Improving text prediction accuracy using neurophysiology
- Sophia Mehdizadeh
-
Tongue-Gesture Recognition in Head-Mounted Displays
- Tan Gemicioglu
-
DIABLo: a Deep Individual-Agnostic Binaural Localizer
- Shoken Kaneko
-
-
-
-
Audio-based Toxic Language Detection
- Midia Yousefi
-
-
From SqueezeNet to SqueezeBERT: Developing Efficient Deep Neural Networks
- Forrest Iandola,
- Sujeeth Bharadwaj
-
Hope Speech and Help Speech: Surfacing Positivity Amidst Hate
- Ashique Khudabukhsh
-
-
-
Towards Mainstream Brain-Computer Interfaces (BCIs)
- Brendan Allison
-
-
-
-
Learning Structured Models for Safe Robot Control
- Subramanian Ramamoorthy
-