{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/45481"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/45481","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"On simulation based verification of nonlinear nondeterministic hybrid systems","abstract":"Automatic safety verification of hybrid systems typically involves computing precise reach sets of such systems. This computation limits scalability of verification as for many model classes it scales exponentially with the number of continuous variables. First we propose a simulation-based algorithm for computing the reach set of a class of deterministic hybrid system. The algorithm first constructs a cover of the initial set of the hybrid system. Then the reach set of executions from the same cover are overapproximated by simulation traces and tubes around them. Experiments are performed on several benchmark problems including navigation benchmarks, room heating benchmarks, non-linear satellite systems and engine hybrid control systems. The results suggest the algorithm may scale to larger systems. Finally, we present a reachability algorithm that computes precise reach set of dynamical systems $A$ with non-linear differential inclusions. The algorithm constructs a sequence of shrink concretizations of $A$. Then the reach sets of the concretizations are used to construct an overapproximation of the reach set of $A$. Soundness and Completeness of both algorithms presented are formally proved.","abstract_html":"Automatic safety verification of hybrid systems typically involves computing precise reach sets of such systems. This computation limits scalability of verification as for many model classes it scales exponentially with the number of continuous variables. First we propose a simulation-based algorithm for computing the reach set of a class of deterministic hybrid system. The algorithm first constructs a cover of the initial set of the hybrid system. Then the reach set of executions from the same cover are overapproximated by simulation traces and tubes around them. Experiments are performed on several benchmark problems including navigation benchmarks, room heating benchmarks, non-linear satellite systems and engine hybrid control systems. The results suggest the algorithm may scale to larger systems. Finally, we present a reachability algorithm that computes precise reach set of dynamical systems $A$ with non-linear differential inclusions. The algorithm constructs a sequence of shrink concretizations of $A$. Then the reach sets of the concretizations are used to construct an overapproximation of the reach set of $A$. Soundness and Completeness of both algorithms presented are formally proved.","abstract_has_math":true,"creators":["Huang, Zhenqi"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Mechanical Engineering","degree_department":null,"school":null,"contributors":["Mitra, Sayan"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2013,"date_issued":"2013-08-22T16:41:31Z","date_published":"2013-08-22T16:41:31Z","updated_at":"2026-07-22T22:25:36Z","subjects":["hybrid system","verification","differential inclusion","simulation"],"languages":["en"],"rights":["Copyright 2013 Zhenqi Huang"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/45481","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Mitra, Sayan"]},{"key":"dc:creator","label":"Author","values":["Huang, Zhenqi"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2013-08-22T16:41:31Z","2013-08"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Mechanical Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["hybrid system","verification","differential inclusion","simulation"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2013 Zhenqi Huang"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/45481"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Automatic safety verification of hybrid systems typically involves computing precise reach sets of such systems. This computation limits scalability of verification as for many model classes it scales exponentially with the number of continuous variables. First we propose a simulation-based algorithm for computing the reach set of a class of deterministic hybrid system. The algorithm first constructs a cover of the initial set of the hybrid system. Then the reach set of executions from the same cover are overapproximated by simulation traces and tubes around them. Experiments are performed on several benchmark problems including navigation benchmarks, room heating benchmarks, non-linear satellite systems and engine hybrid control systems. The results suggest the algorithm may scale to larger systems. Finally, we present a reachability algorithm that computes precise reach set of dynamical systems $A$ with non-linear differential inclusions. The algorithm constructs a sequence of shrink concretizations of $A$. Then the reach sets of the concretizations are used to construct an overapproximation of the reach set of $A$. Soundness and Completeness of both algorithms presented are formally proved.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2013-07-19T19:13:19Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Huang_Zhenqi.pdf: 965090 bytes, checksum: 932ac647412c02f318bc9de6d0205960 (MD5)","Made available in DSpace on 2013-08-22T16:41:31Z (GMT). No. of bitstreams: 2 Zhenqi_Huang.pdf: 965085 bytes, checksum: 9ffbdfcf914aca3a4d2ba0a988aa5bb5 (MD5) license.txt: 4062 bytes, checksum: a3d99d38ef1c92356c544924f1797c3f (MD5)"]},{"key":"dc:title","label":"Title","values":["On simulation based verification of nonlinear nondeterministic hybrid systems"]}]}],"canonical_facts":{"dc:contributor":["Mitra, Sayan"],"dc:creator":["Huang, Zhenqi"],"dc:date":["2013-08-22T16:41:31Z","2013-08"],"dc:description":["Automatic safety verification of hybrid systems typically involves computing precise reach sets of such systems. This computation limits scalability of verification as for many model classes it scales exponentially with the number of continuous variables. First we propose a simulation-based algorithm for computing the reach set of a class of deterministic hybrid system. The algorithm first constructs a cover of the initial set of the hybrid system. Then the reach set of executions from the same cover are overapproximated by simulation traces and tubes around them. Experiments are performed on several benchmark problems including navigation benchmarks, room heating benchmarks, non-linear satellite systems and engine hybrid control systems. The results suggest the algorithm may scale to larger systems. Finally, we present a reachability algorithm that computes precise reach set of dynamical systems $A$ with non-linear differential inclusions. The algorithm constructs a sequence of shrink concretizations of $A$. Then the reach sets of the concretizations are used to construct an overapproximation of the reach set of $A$. Soundness and Completeness of both algorithms presented are formally proved.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2013-07-19T19:13:19Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Huang_Zhenqi.pdf: 965090 bytes, checksum: 932ac647412c02f318bc9de6d0205960 (MD5)","Made available in DSpace on 2013-08-22T16:41:31Z (GMT). No. of bitstreams: 2 Zhenqi_Huang.pdf: 965085 bytes, checksum: 9ffbdfcf914aca3a4d2ba0a988aa5bb5 (MD5) license.txt: 4062 bytes, checksum: a3d99d38ef1c92356c544924f1797c3f (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/45481"],"dc:language":["en"],"dc:rights":["Copyright 2013 Zhenqi Huang"],"dc:subject":["hybrid system","verification","differential inclusion","simulation"],"dc:title":["On simulation based verification of nonlinear nondeterministic hybrid systems"],"dc:type":["text"],"thesis:degree_discipline":["Mechanical Engineering"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:36Z"}