{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/125597"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/125597","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"On multi-agent hybrid system verification: Modeling in verse, star sets, and user studies","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-02-04 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-02-04 without embargo terms","abstract_has_math":false,"creators":["Braught, Katherine"],"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":2024,"date_issued":"2024-07-15","date_published":"2024-07-15","updated_at":"2026-07-22T22:25:02Z","subjects":["Verification","Reachability","Hybrid Systems"],"languages":["en","eng"],"rights":["Copyright 2024 Katherine Braught"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/2142/125597","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":["Braught, Katherine"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2024-07-15","2024-08"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"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":["Verification","Reachability","Hybrid Systems"]}]},{"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 2024 Katherine Braught"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/2142/125597"]}]},{"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 2025-02-04 without embargo terms","The student, Katherine Braught, accepted the attached license on 2024-07-09 at 16:42.","The student, Katherine Braught, submitted this Thesis for approval on 2024-07-09 at 16:52.","This Thesis was approved for publication on 2024-07-15 at 11:22.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21024 on 2025-02-04 at 21:04:47","Hybrid systems have become the standard mathematical framework for modeling and verifying the safety of cyber-physical systems. Many effective tools for verifying hybrid systems exist; however, using these tools requires the user to write a model according to the tool’s specifications, which has a steep learning curve in the form of training in formal logics. The Verse library was developed to address this problem, allowing users to write their specifications in Python instead of using specialized logics. While over 200 engineering students have used Verse, its usability has not yet been formally evaluated. In this thesis, we present a preliminary user study of Verse and use its findings to improve the tool further. We designed an assignment and surveyed the experience of undergraduate engineering students who used the tool for design validation in a course on safe autonomy. We found that the students gave the verification aspect of Verse an average score of 54 on the Software Usability Scale, and the simulation aspect an average score of 61. These scores indicate the tool is usable but needs improvement. The most common complaints about Verse were related to its speed and documentation. Throughout the rest of this thesis, we provide updated documentation of the Verse tool. We also explore using new data structures in the reachability algorithms to increase speed. We present the star set data structure, which is an efficient and precise generalization of zonotopes, and demonstrate its potential to speed up Verse through experimental evaluations."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["On multi-agent hybrid system verification: Modeling in verse, star sets, and user studies"]}]}],"canonical_facts":{"dc:contributor":["Mitra, Sayan"],"dc:creator":["Braught, Katherine"],"dc:date":["2024-07-15","2024-08"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2025-02-04 without embargo terms","The student, Katherine Braught, accepted the attached license on 2024-07-09 at 16:42.","The student, Katherine Braught, submitted this Thesis for approval on 2024-07-09 at 16:52.","This Thesis was approved for publication on 2024-07-15 at 11:22.","DSpace SAF Submission Ingestion Package generated from Vireo submission #21024 on 2025-02-04 at 21:04:47","Hybrid systems have become the standard mathematical framework for modeling and verifying the safety of cyber-physical systems. Many effective tools for verifying hybrid systems exist; however, using these tools requires the user to write a model according to the tool’s specifications, which has a steep learning curve in the form of training in formal logics. The Verse library was developed to address this problem, allowing users to write their specifications in Python instead of using specialized logics. While over 200 engineering students have used Verse, its usability has not yet been formally evaluated. In this thesis, we present a preliminary user study of Verse and use its findings to improve the tool further. We designed an assignment and surveyed the experience of undergraduate engineering students who used the tool for design validation in a course on safe autonomy. We found that the students gave the verification aspect of Verse an average score of 54 on the Software Usability Scale, and the simulation aspect an average score of 61. These scores indicate the tool is usable but needs improvement. The most common complaints about Verse were related to its speed and documentation. Throughout the rest of this thesis, we provide updated documentation of the Verse tool. We also explore using new data structures in the reachability algorithms to increase speed. We present the star set data structure, which is an efficient and precise generalization of zonotopes, and demonstrate its potential to speed up Verse through experimental evaluations."],"dc:format":["application/pdf"],"dc:identifier":["https://hdl.handle.net/2142/125597"],"dc:language":["en","eng"],"dc:rights":["Copyright 2024 Katherine Braught"],"dc:subject":["Verification","Reachability","Hybrid Systems"],"dc:title":["On multi-agent hybrid system verification: Modeling in verse, star sets, and user studies"],"dc:type":["text","Thesis"],"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:25:02Z"}