{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/93069"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/93069","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Automatic simulation-driven reachability using matrix measures","abstract":"Simulation-driven verification is a promising approach that provides formal safety guarantees for otherwise intractable nonlinear and hybrid system models. A key step in simulation-driven algorithms is to compute the reach set over-approximations from a set of initial states through numerical simulations. This thesis introduces algorithms for this key step, which relies on computing piece-wise exponential bounds on the rate at which trajectories starting from neighboring states converge or diverge. We call this discrepancy function. The algorithms rely on computing local bounds on the matrix measure of the Jacobian matrices. We discuss different techniques to compute the matrix measures under different norms: regular Euclidean norm or Euclidean norm under coordinate transformation, such that the exponential rate of the discrepancy function is locally minimized. The proposed methods enable automatic reach set computations of general nonlinear systems and have been successfully used on several challenging benchmark models. All proposed algorithms for computing discrepancy function give soundness and relative completeness of the overall simulation-driven safety verification algorithm. We present a series of experiments to illustrate the accuracy and performance of the approach.","abstract_html":"Simulation-driven verification is a promising approach that provides formal safety guarantees for otherwise intractable nonlinear and hybrid system models. A key step in simulation-driven algorithms is to compute the reach set over-approximations from a set of initial states through numerical simulations. This thesis introduces algorithms for this key step, which relies on computing piece-wise exponential bounds on the rate at which trajectories starting from neighboring states converge or diverge. We call this discrepancy function. The algorithms rely on computing local bounds on the matrix measure of the Jacobian matrices. We discuss different techniques to compute the matrix measures under different norms: regular Euclidean norm or Euclidean norm under coordinate transformation, such that the exponential rate of the discrepancy function is locally minimized. The proposed methods enable automatic reach set computations of general nonlinear systems and have been successfully used on several challenging benchmark models. All proposed algorithms for computing discrepancy function give soundness and relative completeness of the overall simulation-driven safety verification algorithm. We present a series of experiments to illustrate the accuracy and performance of the approach.","abstract_has_math":false,"creators":["Fan, Chuchu"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Electrical & Computer Engr","degree_department":null,"school":null,"contributors":["Mitra, Sayan"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2016,"date_issued":"2016-11-10T18:43:03Z","date_published":"2016-11-10T18:43:03Z","updated_at":"2026-07-22T22:26:35Z","subjects":["Reachability","Nonlinear systems","Matrix measures"],"languages":["en"],"rights":["Copyright 2016 Chuchu Fan"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/93069","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":["Fan, Chuchu"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2016-11-10T18:43:03Z","2018-11-11T10:15:36Z","2016-07-18","2016-08"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical & Computer Engr"]},{"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":["Reachability","Nonlinear systems","Matrix measures"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2016 Chuchu Fan"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/93069"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Simulation-driven verification is a promising approach that provides formal safety guarantees for otherwise intractable nonlinear and hybrid system models. A key step in simulation-driven algorithms is to compute the reach set over-approximations from a set of initial states through numerical simulations. This thesis introduces algorithms for this key step, which relies on computing piece-wise exponential bounds on the rate at which trajectories starting from neighboring states converge or diverge. We call this discrepancy function. The algorithms rely on computing local bounds on the matrix measure of the Jacobian matrices. We discuss different techniques to compute the matrix measures under different norms: regular Euclidean norm or Euclidean norm under coordinate transformation, such that the exponential rate of the discrepancy function is locally minimized. The proposed methods enable automatic reach set computations of general nonlinear systems and have been successfully used on several challenging benchmark models. All proposed algorithms for computing discrepancy function give soundness and relative completeness of the overall simulation-driven safety verification algorithm. We present a series of experiments to illustrate the accuracy and performance of the approach.","Submission published under a 24 month embargo labeled 'U of I Access', the embargo will last until 2018-08-01","The student, Chuchu Fan, accepted the attached license on 2016-07-15 at 15:42.","The student, Chuchu Fan, submitted this Thesis for approval on 2016-07-15 at 15:50.","This Thesis was approved for publication on 2016-07-18 at 10:29.","DSpace SAF Submission Ingestion Package generated from Vireo submission #9968 on 2016-11-10 at 12:25:29","Made available in DSpace on 2016-11-10T18:43:03Z (GMT). No. of bitstreams: 2 FAN-THESIS-2016.pdf: 716203 bytes, checksum: 77e377890b4498a11edb70e480df23d8 (MD5) LICENSE.txt: 4207 bytes, checksum: 102da73cd46f53afa5c17cc69676127b (MD5) Previous issue date: 2016-07-18","Embargo set by: Seth Robbins for item 95492 Lift date: 2018-11-10T18:43:22Z Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD system","U of I Only Restriction Lifted for Item 95492 on 2018-11-11T10:15:36Z."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Automatic simulation-driven reachability using matrix measures"]}]}],"canonical_facts":{"dc:contributor":["Mitra, Sayan"],"dc:creator":["Fan, Chuchu"],"dc:date":["2016-11-10T18:43:03Z","2018-11-11T10:15:36Z","2016-07-18","2016-08"],"dc:description":["Simulation-driven verification is a promising approach that provides formal safety guarantees for otherwise intractable nonlinear and hybrid system models. A key step in simulation-driven algorithms is to compute the reach set over-approximations from a set of initial states through numerical simulations. This thesis introduces algorithms for this key step, which relies on computing piece-wise exponential bounds on the rate at which trajectories starting from neighboring states converge or diverge. We call this discrepancy function. The algorithms rely on computing local bounds on the matrix measure of the Jacobian matrices. We discuss different techniques to compute the matrix measures under different norms: regular Euclidean norm or Euclidean norm under coordinate transformation, such that the exponential rate of the discrepancy function is locally minimized. The proposed methods enable automatic reach set computations of general nonlinear systems and have been successfully used on several challenging benchmark models. All proposed algorithms for computing discrepancy function give soundness and relative completeness of the overall simulation-driven safety verification algorithm. We present a series of experiments to illustrate the accuracy and performance of the approach.","Submission published under a 24 month embargo labeled 'U of I Access', the embargo will last until 2018-08-01","The student, Chuchu Fan, accepted the attached license on 2016-07-15 at 15:42.","The student, Chuchu Fan, submitted this Thesis for approval on 2016-07-15 at 15:50.","This Thesis was approved for publication on 2016-07-18 at 10:29.","DSpace SAF Submission Ingestion Package generated from Vireo submission #9968 on 2016-11-10 at 12:25:29","Made available in DSpace on 2016-11-10T18:43:03Z (GMT). No. of bitstreams: 2 FAN-THESIS-2016.pdf: 716203 bytes, checksum: 77e377890b4498a11edb70e480df23d8 (MD5) LICENSE.txt: 4207 bytes, checksum: 102da73cd46f53afa5c17cc69676127b (MD5) Previous issue date: 2016-07-18","Embargo set by: Seth Robbins for item 95492 Lift date: 2018-11-10T18:43:22Z Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD system","U of I Only Restriction Lifted for Item 95492 on 2018-11-11T10:15:36Z."],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/93069"],"dc:language":["en"],"dc:rights":["Copyright 2016 Chuchu Fan"],"dc:subject":["Reachability","Nonlinear systems","Matrix measures"],"dc:title":["Automatic simulation-driven reachability using matrix measures"],"dc:type":["text"],"thesis:degree_discipline":["Electrical & Computer Engr"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:26:35Z"}