{"id":612267,"date":"2019-09-06T13:00:39","date_gmt":"2019-09-06T20:00:39","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?post_type=msr-research-item&#038;p=612267"},"modified":"2019-10-02T12:11:09","modified_gmt":"2019-10-02T19:11:09","slug":"non-linear-invariants-for-control-command-systems","status":"publish","type":"msr-video","link":"https:\/\/www.microsoft.com\/en-us\/research\/video\/non-linear-invariants-for-control-command-systems\/","title":{"rendered":"Non-linear Invariants for Control-Command Systems"},"content":{"rendered":"<p>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.<\/p>\n<p>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.<\/p>\n<p>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.<\/p>\n<p>[<a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2019\/10\/44120_Non-linear-Invariants-for-Control-Command-Systems.pdf\" target=\"_blank\" rel=\"noopener noreferrer\">Slides<\/a>]<\/p>\n","protected":false},"excerpt":{"rendered":"<p>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 [&hellip;]<\/p>\n","protected":false},"featured_media":612273,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"footnotes":""},"research-area":[13560],"msr-video-type":[206954],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-612267","msr-video","type-msr-video","status-publish","has-post-thumbnail","hentry","msr-research-area-programming-languages-software-engineering","msr-video-type-microsoft-research-talks","msr-locale-en_us"],"msr_download_urls":"","msr_external_url":"https:\/\/youtu.be\/xb70OdDHhTo","msr_secondary_video_url":"","msr_video_file":"","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/612267"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-video"}],"version-history":[{"count":3,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/612267\/revisions"}],"predecessor-version":[{"id":612282,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/612267\/revisions\/612282"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/612273"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=612267"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=612267"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=612267"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=612267"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=612267"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=612267"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}