A new approach based on constraint solving techniques was recently proposed for verification of hybrid systems. This approach works by searching for inductive invariants of a given form. In this paper, we extend that work to automatic synthesis of safe hybrid systems. Starting with a multi-modal dynamical system and a safety property, we present a sound technique for synthesizing a switching logic for changing modes so as to preserve the safety property. By construction, the synthesized hybrid system is well-formed and is guaranteed safe. Our approach is based on synthesizing a controlled invariant that is sufficient to prove safety. The generation of the controlled invariant is cast as a constraint solving problem, which is solved using SMT solvers. The generated controlled invariant is then used to arrive at the maximally liberal switching logic.<\/p>\n","protected":false},"excerpt":{"rendered":"
A new approach based on constraint solving techniques was recently proposed for verification of hybrid systems. This approach works by searching for inductive invariants of a given form. In this paper, we extend that work to automatic synthesis of safe hybrid systems. Starting with a multi-modal dynamical system and a safety property, we present a […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"msr-content-type":[3],"msr-research-highlight":[],"research-area":[13561],"msr-publication-type":[193716],"msr-product-type":[],"msr-focus-area":[],"msr-platform":[],"msr-download-source":[],"msr-locale":[268875],"msr-post-option":[],"msr-field-of-study":[],"msr-conference":[],"msr-journal":[],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-336518","msr-research-item","type-msr-research-item","status-publish","hentry","msr-research-area-algorithms","msr-locale-en_us"],"msr_publishername":"Springer-Verlag","msr_edition":"VMCAI '09 Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation","msr_affiliation":"","msr_published_date":"2008-12-18","msr_host":"","msr_duration":"","msr_version":"","msr_speaker":"","msr_other_contributors":"","msr_booktitle":"","msr_pages_string":"305 - 319","msr_chapter":"","msr_isbn":"","msr_journal":"","msr_volume":"","msr_number":"","msr_editors":"","msr_series":"","msr_issue":"","msr_organization":"","msr_how_published":"","msr_notes":"","msr_highlight_text":"","msr_release_tracker_id":"","msr_original_fields_of_study":"","msr_download_urls":"","msr_external_url":"","msr_secondary_video_url":"","msr_longbiography":"","msr_microsoftintellectualproperty":1,"msr_main_download":"336536","msr_publicationurl":"http:\/\/www.springerlink.com\/openurl.asp?genre=article&id=doi:10.1007\/s10009-010-0172-8","msr_doi":"10.1007\/978-3-540-93900-9_25","msr_publication_uploader":[{"type":"file","title":"Synthesizing Switching Logic using Constraint Solving","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/12\/vmcai09_hybrid.pdf","id":336536,"label_id":0},{"type":"file","title":"Synthesizing Switching Logic using Constraint Solving (Slides)","viewUrl":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/12\/vmcai09_hybrid_slides.pdf","id":336539,"label_id":0},{"type":"url","title":"http:\/\/www.springerlink.com\/openurl.asp?genre=article&id=doi:10.1007\/s10009-010-0172-8","viewUrl":false,"id":false,"label_id":0},{"type":"doi","title":"10.1007\/978-3-540-93900-9_25","viewUrl":false,"id":false,"label_id":0}],"msr_related_uploader":"","msr_attachments":[{"id":0,"url":"http:\/\/www.springerlink.com\/openurl.asp?genre=article&id=doi:10.1007\/s10009-010-0172-8"},{"id":336539,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/12\/vmcai09_hybrid_slides.pdf"},{"id":336536,"url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/12\/vmcai09_hybrid.pdf"}],"msr-author-ordering":[{"type":"text","value":"Ankur Taly","user_id":0,"rest_url":false},{"type":"user_nicename","value":"sumitg","user_id":33755,"rest_url":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/microsoft-research\/v1\/researchers?person=sumitg"},{"type":"text","value":"Ashish Tiwari","user_id":0,"rest_url":false}],"msr_impact_theme":[],"msr_research_lab":[],"msr_event":[],"msr_group":[],"msr_project":[361034,170033],"publication":[],"video":[],"download":[],"msr_publication_type":"inproceedings","related_content":{"projects":[{"ID":361034,"post_title":"Program Synthesis","post_name":"program-synthesis","post_type":"msr-project","post_date":"2017-02-02 13:37:27","post_modified":"2020-01-24 08:27:25","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/program-synthesis\/","post_excerpt":"Introduction Program synthesis is the task of automatically discovering an executable piece of code given user intent expressed using various forms of constraints such as input-output examples, demonstrations, natural language, etc. Program synthesis has direct applications for various classes of users in the technology pyramid: (100s of millions of) End Users (people who have access to a computational device but are not expert programmers): Helping them to create small snippets of code for performing repetitive…","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/361034"}]}},{"ID":170033,"post_title":"VS3 (Verification and Specification using SMT Solvers)","post_name":"vs3-verification-and-specification-using-smt-solvers","post_type":"msr-project","post_date":"2008-12-01 20:42:05","post_modified":"2019-08-19 15:39:48","post_status":"publish","permalink":"https:\/\/www.microsoft.com\/en-us\/research\/project\/vs3-verification-and-specification-using-smt-solvers\/","post_excerpt":"SMT Solvers have traditionally been used for verifying correctness of systems that have been annotated with relevant inductive invariants. Such an annotation usually is an undesirable burden on the user. This project explores techniques for using SMT solvers to automatically discover inductive invariants for proving given safety properties of systems. Additionally, this project also explores techniques for using SMT solvers to synthesize systems in the first place given enough specifications. Saurabh Srivastava, who is leading…","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170033"}]}}]},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/336518","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-research-item"}],"version-history":[{"count":1,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/336518\/revisions"}],"predecessor-version":[{"id":524504,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-item\/336518\/revisions\/524504"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=336518"}],"wp:term":[{"taxonomy":"msr-content-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-content-type?post=336518"},{"taxonomy":"msr-research-highlight","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-research-highlight?post=336518"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=336518"},{"taxonomy":"msr-publication-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-publication-type?post=336518"},{"taxonomy":"msr-product-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-product-type?post=336518"},{"taxonomy":"msr-focus-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-focus-area?post=336518"},{"taxonomy":"msr-platform","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-platform?post=336518"},{"taxonomy":"msr-download-source","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-download-source?post=336518"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=336518"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=336518"},{"taxonomy":"msr-field-of-study","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-field-of-study?post=336518"},{"taxonomy":"msr-conference","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-conference?post=336518"},{"taxonomy":"msr-journal","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-journal?post=336518"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=336518"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=336518"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}