2026-09-21T14:46:46Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/120171 2023-09-04 col_2142_5131 col_2142_10761 com_2142_5130 com_2142_10755 com_2142_234

Mitra, Sayan 2023-05 application/pdf en text 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 Parallelization and incremental algorithms in the verse hybrid system verification library Zhu, Haoqing 2023-05-04 Scenario Verification Reachability Analysis Hybrid Systems Parallel Programming 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. Text eng https://hdl.handle.net/2142/120171 Copyright 2023 Haoqing Zhu M.S. Thesis Computer Science University of Illinois at Urbana-Champaign Computer Science