{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/34351"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/34351","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Compositional bounded reachability using time partitioning and abstraction","abstract":"Automatic verification of cyber-physical systems (CPS) typically involves computing the reachable set of states of such systems. This computation is known to be exponential in the number of continuous variables. For systems that can be decomposed into separate components with lower dimensionality, we present an algorithm that verifies global safety properties of the complete system using the reach sets of the components. Here, the components are only coupled through a shared time variable. Using a satellite system case study, we are able to show significant savings in memory and runtime computation costs for this approach. For systems whose components are coupled through additional continuous variables, we present an abstraction to overapproximate the interaction between the components such that the aforementioned algorithm can be used. The feasibility of this abstraction is demonstrated experimentally, which also shows additional work is necessary to develop a more efficient abstraction.","abstract_html":"Automatic verification of cyber-physical systems (CPS) typically involves computing the reachable set of states of such systems. This computation is known to be exponential in the number of continuous variables. For systems that can be decomposed into separate components with lower dimensionality, we present an algorithm that verifies global safety properties of the complete system using the reach sets of the components. Here, the components are only coupled through a shared time variable. Using a satellite system case study, we are able to show significant savings in memory and runtime computation costs for this approach. For systems whose components are coupled through additional continuous variables, we present an abstraction to overapproximate the interaction between the components such that the aforementioned algorithm can be used. The feasibility of this abstraction is demonstrated experimentally, which also shows additional work is necessary to develop a more efficient abstraction.","abstract_has_math":false,"creators":["Green, Jeremy"],"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":2012,"date_issued":"2012-09-18T21:12:45Z","date_published":"2012-09-18T21:12:45Z","updated_at":"2026-07-22T22:25:31Z","subjects":["bounded reachability","decomposition","composition","hybrid system","abstraction","safety verification"],"languages":["en"],"rights":["Copyright 2012 Jeremy Green"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/34351","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":["Green, Jeremy"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2012-09-18T21:12:45Z","2012-08"]},{"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":["bounded reachability","decomposition","composition","hybrid system","abstraction","safety verification"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2012 Jeremy Green"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/34351"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Automatic verification of cyber-physical systems (CPS) typically involves computing the reachable set of states of such systems. This computation is known to be exponential in the number of continuous variables. For systems that can be decomposed into separate components with lower dimensionality, we present an algorithm that verifies global safety properties of the complete system using the reach sets of the components. Here, the components are only coupled through a shared time variable. Using a satellite system case study, we are able to show significant savings in memory and runtime computation costs for this approach. For systems whose components are coupled through additional continuous variables, we present an abstraction to overapproximate the interaction between the components such that the aforementioned algorithm can be used. The feasibility of this abstraction is demonstrated experimentally, which also shows additional work is necessary to develop a more efficient abstraction.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2012-07-18T14:59:19Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Green_Jeremy.pdf: 558271 bytes, checksum: 247b7fbaf074fee20019eb7cd44c4cb0 (MD5)","Made available in DSpace on 2012-09-18T21:12:45Z (GMT). No. of bitstreams: 2 Green_Jeremy.pdf: 558271 bytes, checksum: 247b7fbaf074fee20019eb7cd44c4cb0 (MD5) license.txt: 4062 bytes, checksum: b9f13395f27fb350a4e492038fb4c05f (MD5)"]},{"key":"dc:title","label":"Title","values":["Compositional bounded reachability using time partitioning and abstraction"]}]}],"canonical_facts":{"dc:contributor":["Mitra, Sayan"],"dc:creator":["Green, Jeremy"],"dc:date":["2012-09-18T21:12:45Z","2012-08"],"dc:description":["Automatic verification of cyber-physical systems (CPS) typically involves computing the reachable set of states of such systems. This computation is known to be exponential in the number of continuous variables. For systems that can be decomposed into separate components with lower dimensionality, we present an algorithm that verifies global safety properties of the complete system using the reach sets of the components. Here, the components are only coupled through a shared time variable. Using a satellite system case study, we are able to show significant savings in memory and runtime computation costs for this approach. For systems whose components are coupled through additional continuous variables, we present an abstraction to overapproximate the interaction between the components such that the aforementioned algorithm can be used. The feasibility of this abstraction is demonstrated experimentally, which also shows additional work is necessary to develop a more efficient abstraction.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2012-07-18T14:59:19Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Green_Jeremy.pdf: 558271 bytes, checksum: 247b7fbaf074fee20019eb7cd44c4cb0 (MD5)","Made available in DSpace on 2012-09-18T21:12:45Z (GMT). No. of bitstreams: 2 Green_Jeremy.pdf: 558271 bytes, checksum: 247b7fbaf074fee20019eb7cd44c4cb0 (MD5) license.txt: 4062 bytes, checksum: b9f13395f27fb350a4e492038fb4c05f (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/34351"],"dc:language":["en"],"dc:rights":["Copyright 2012 Jeremy Green"],"dc:subject":["bounded reachability","decomposition","composition","hybrid system","abstraction","safety verification"],"dc:title":["Compositional bounded reachability using time partitioning and abstraction"],"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:25:31Z"}