{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/120171"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/120171","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Parallelization and incremental algorithms in the verse hybrid system verification library","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-09-01 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-09-01 without embargo terms","abstract_has_math":false,"creators":["Zhu, Haoqing"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Mitra, Sayan"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2023,"date_issued":"2023-05","date_published":"2023-05","updated_at":"2026-07-22T22:24:56Z","subjects":["Scenario Verification","Reachability Analysis","Hybrid Systems","Parallel Programming"],"languages":["en","eng"],"rights":["Copyright 2023 Haoqing Zhu"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/120171","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":["Zhu, Haoqing"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2023-05","2023-05-04"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"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":["Scenario Verification","Reachability Analysis","Hybrid Systems","Parallel Programming"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en","eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2023 Haoqing Zhu"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/120171"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-09-01 without embargo terms","The student, Haoqing Zhu, accepted the attached license on 2023-05-03 at 16:21.","The student, Haoqing Zhu, submitted this Thesis for approval on 2023-05-03 at 16:25.","This Thesis was approved for publication on 2023-05-04 at 13:36.","DSpace SAF Submission Ingestion Package generated from Vireo submission #19318 on 2023-09-01 at 16:56:15","Hybrid systems is a popular model for modeling and verifying cyber physical systems, combining the discrete transition logic and physical dynamics of agents. However, it is difficult for most users to adopt this technology without formal methods training. Verse is a verification library which tries to address this issue and make the hybrid system technology more usable. Verse has shown some promise and in a short amount of time is currently used by several research groups. But Verse has scalability issues yet to be solved. In this thesis, we present parallelization and incremental verification algorithms in Verse. Verse computes reachsets of a system as a reachability tree, and the parallelization algorithm can compute different parts of the tree concurrently in different processors. Using the popular Ray parallelization framework, we are able to efficiently parallelize the computations without the use of locks. The incremental verification algorithm can reuse computation from previous experiments and reduce computation time for similar scenarios. We evaluate the implementation of our algorithms on a variety of scenarios, and observed that we can achieve 2 to 4 times speedup on moderately large scenarios. In one experiment with 12 agents and 133 transitions, we are able to compute the reachsets in 8 minutes 30 seconds, a 3.5x speedup over the previous 30 minutes."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Parallelization and incremental algorithms in the verse hybrid system verification library"]}]}],"canonical_facts":{"dc:contributor":["Mitra, Sayan"],"dc:creator":["Zhu, Haoqing"],"dc:date":["2023-05","2023-05-04"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2023-09-01 without embargo terms","The student, Haoqing Zhu, accepted the attached license on 2023-05-03 at 16:21.","The student, Haoqing Zhu, submitted this Thesis for approval on 2023-05-03 at 16:25.","This Thesis was approved for publication on 2023-05-04 at 13:36.","DSpace SAF Submission Ingestion Package generated from Vireo submission #19318 on 2023-09-01 at 16:56:15","Hybrid systems is a popular model for modeling and verifying cyber physical systems, combining the discrete transition logic and physical dynamics of agents. However, it is difficult for most users to adopt this technology without formal methods training. Verse is a verification library which tries to address this issue and make the hybrid system technology more usable. Verse has shown some promise and in a short amount of time is currently used by several research groups. But Verse has scalability issues yet to be solved. In this thesis, we present parallelization and incremental verification algorithms in Verse. Verse computes reachsets of a system as a reachability tree, and the parallelization algorithm can compute different parts of the tree concurrently in different processors. Using the popular Ray parallelization framework, we are able to efficiently parallelize the computations without the use of locks. The incremental verification algorithm can reuse computation from previous experiments and reduce computation time for similar scenarios. We evaluate the implementation of our algorithms on a variety of scenarios, and observed that we can achieve 2 to 4 times speedup on moderately large scenarios. In one experiment with 12 agents and 133 transitions, we are able to compute the reachsets in 8 minutes 30 seconds, a 3.5x speedup over the previous 30 minutes."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/120171"],"dc:language":["en","eng"],"dc:rights":["Copyright 2023 Haoqing Zhu"],"dc:subject":["Scenario Verification","Reachability Analysis","Hybrid Systems","Parallel Programming"],"dc:title":["Parallelization and incremental algorithms in the verse hybrid system verification library"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:56Z"}