{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:54:00Z","timestamp":1756000440610,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T00:00:00Z","timestamp":1570492800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"<jats:p>Computing the set of reachable states is a widely used technique for proving that a hybrid system satisfies its safety specification. Flow-pipe construction methods interleave phases of computing continuous successors and phases of computing discrete successors. Directly doing this leads to a combinatorial explosion problem, though, as with each discrete successor there may be an interval of time where the transition can occur, so that the number of paths becomes exponential in the number of discrete transitions. For this reason, most reachable set computation tools implement some form of set aggregation for discrete transitions, such as, performing a template-based overapproximation or convex hull aggregation. These aggregation methods, however, in theory can lead to unbounded error, and in practice are often the root cause of why a safety specification cannot be proven.<\/jats:p>\n          <jats:p>This paper proposes techniques for improving the accuracy of the aggregation operations performed for reachable set computation. First, we present two aggregation strategies over generalized stars, namely convex hull aggregation and template based aggregation. Second, we perform adaptive deaggregation using a data structure called Aggregated Directed Acyclic Graph (AGGDAG). Our deaggregation strategy is driven by counterexamples and hence has soundness and relative completeness guarantees. We demonstrate the computational benefits of our approach through two case studies involving satellite rendezvous and gearbox meshing.<\/jats:p>","DOI":"10.1145\/3358214","type":"journal-article","created":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T13:13:05Z","timestamp":1570713185000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Aggregation Strategies in Reachable Set Computation of Hybrid Systems"],"prefix":"10.1145","volume":"18","author":[{"given":"Parasara Sridhar","family":"Duggirala","sequence":"first","affiliation":[{"name":"University of North Carolina at Chapel Hill"}]},{"given":"Stanley","family":"Bak","sequence":"additional","affiliation":[{"name":"Safe Sky Analytics LLC"}]}],"member":"320","published-online":{"date-parts":[[2019,10,8]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"5th International Workshop on Applied Verification of Continuous and Hybrid Systems","volume":"54","author":"Althoff Matthias","year":"2018","unstructured":"Matthias Althoff , Stanley Bak , Xin Chen , Chuchu Fan , Marcelo Forets , Goran Frehse , Niklas Kochdumper , Yangge Li , Sayan Mitra , Rajarshi Ray , Christian Schilling , and Stefan Schupp . 2018 . ARCH-COMP18 category report: Continuous and hybrid systems with linear continuous dynamics. In ARCH18 . 5th International Workshop on Applied Verification of Continuous and Hybrid Systems , Vol. 54 . 23--52. Matthias Althoff, Stanley Bak, Xin Chen, Chuchu Fan, Marcelo Forets, Goran Frehse, Niklas Kochdumper, Yangge Li, Sayan Mitra, Rajarshi Ray, Christian Schilling, and Stefan Schupp. 2018. ARCH-COMP18 category report: Continuous and hybrid systems with linear continuous dynamics. In ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems, Vol. 54. 23--52."},{"key":"e_1_2_1_2_1","volume-title":"6th International Workshop on Applied Verification of Continuous and Hybrid Systems. 14--40","author":"Althoff Matthias","year":"2019","unstructured":"Matthias Althoff , Stanley Bak , Marcelo Forets , Goran Frehse , Niklas Kochdumper , Rajarshi Ray , Christian Schilling , and Stefan Schupp . 2019 . ARCH-COMP19 category report: Continuous and hybrid systems with linear continuous dynamics. In ARCH19 . 6th International Workshop on Applied Verification of Continuous and Hybrid Systems. 14--40 . Matthias Althoff, Stanley Bak, Marcelo Forets, Goran Frehse, Niklas Kochdumper, Rajarshi Ray, Christian Schilling, and Stefan Schupp. 2019. ARCH-COMP19 category report: Continuous and hybrid systems with linear continuous dynamics. In ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems. 14--40."},{"volume-title":"18th International Conference on Hybrid Systems: Computation and Control. ACM.","author":"Bak Stanley","key":"e_1_2_1_3_1","unstructured":"Stanley Bak , Sergiy Bogomolov , and Taylor T. Johnson . 2015. HyST: A source transformation and translation tool for hybrid automaton models . In 18th International Conference on Hybrid Systems: Computation and Control. ACM. Stanley Bak, Sergiy Bogomolov, and Taylor T. Johnson. 2015. HyST: A source transformation and translation tool for hybrid automaton models. In 18th International Conference on Hybrid Systems: Computation and Control. ACM."},{"key":"e_1_2_1_4_1","volume-title":"ARCH\u201916: Proc. of the 3rd Workshop on Applied Verification for Continuous and Hybrid Systems.","author":"Bak Stanley","year":"2016","unstructured":"Stanley Bak , Sergiy Bogomolov , and Christian Schilling . 2016 . High-level hybrid systems analysis with hypy . In ARCH\u201916: Proc. of the 3rd Workshop on Applied Verification for Continuous and Hybrid Systems. Stanley Bak, Sergiy Bogomolov, and Christian Schilling. 2016. High-level hybrid systems analysis with hypy. In ARCH\u201916: Proc. of the 3rd Workshop on Applied Verification for Continuous and Hybrid Systems."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3049797.3049808"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_32"},{"volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 589--606","author":"Bogomolov Sergiy","key":"e_1_2_1_7_1","unstructured":"Sergiy Bogomolov , Goran Frehse , Mirco Giacobbe , and Thomas A. Henzinger . 2017. Counterexample-guided refinement of template polyhedra . In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 589--606 . Sergiy Bogomolov, Goran Frehse, Mirco Giacobbe, and Thomas A. Henzinger. 2017. Counterexample-guided refinement of template polyhedra. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 589--606."},{"key":"e_1_2_1_8_1","volume-title":"4th International Workshop on Applied Verification of Continuous and Hybrid Systems. EasyChair.","author":"Chan Nicole","year":"2017","unstructured":"Nicole Chan and Sayan Mitra . 2017 . Verifying safety of an autonomous spacecraft rendezvous mission. In ARCH17 . 4th International Workshop on Applied Verification of Continuous and Hybrid Systems. EasyChair. Nicole Chan and Sayan Mitra. 2017. Verifying safety of an autonomous spacecraft rendezvous mission. In ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems. EasyChair."},{"key":"e_1_2_1_9_1","unstructured":"Hongxu Chen Sayan Mitra and Guangyu Tian. 2014. Motor-transmission drive system: A benchmark example for safety verification. In ARCH@CPSWeek. 9--18.  Hongxu Chen Sayan Mitra and Guangyu Tian. 2014. Motor-transmission drive system: A benchmark example for safety verification. In ARCH@CPSWeek. 9--18."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.2514\/8.8704"},{"key":"e_1_2_1_11_1","volume-title":"Overview of the DART mishap investigation results. NASA Report","author":"Croomes S.","year":"2006","unstructured":"S. Croomes . 2006. Overview of the DART mishap investigation results. NASA Report ( 2006 ), 1--10. S. Croomes. 2006. Overview of the DART mishap investigation results. NASA Report (2006), 1--10."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_26"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_16"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Goran Frehse. 2005. PHAVer: Algorithmic verification of hybrid systems past HyTech. In HSCC. 258--273.  Goran Frehse. 2005. PHAVer: Algorithmic verification of hybrid systems past HyTech. In HSCC. 258--273.","DOI":"10.1007\/978-3-540-31954-2_17"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461361"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_21"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_27"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_2"},{"volume-title":"Decision and Control (CDC), 2016 IEEE 55th Conference on. 3300--3305","author":"Jewison Christopher","key":"e_1_2_1_20_1","unstructured":"Christopher Jewison and R. Scott Erwin . 2016. A spacecraft benchmark problem for hybrid control and estimation . In Decision and Control (CDC), 2016 IEEE 55th Conference on. 3300--3305 . Christopher Jewison and R. Scott Erwin. 2016. A spacecraft benchmark problem for hybrid control and estimation. In Decision and Control (CDC), 2016 IEEE 55th Conference on. 3300--3305."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_22"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24743-2_30"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"C\u00e9sar Munoz Anthony Narkawicz and James Chamberlain. 2013. A TCAS-II resolution advisory detection algorithm. In AIAA Guidance Navigation and Control (GNC) Conference. 4622.  C\u00e9sar Munoz Anthony Narkawicz and James Chamberlain. 2013. A TCAS-II resolution advisory detection algorithm. In AIAA Guidance Navigation and Control (GNC) Conference. 4622.","DOI":"10.2514\/6.2013-4622"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/6979.994791"},{"volume-title":"Real-Time Systems Symposium, 2009, RTSS 2009. 30th IEEE. IEEE, 181--190","author":"Prabhakar Pavithra","key":"e_1_2_1_25_1","unstructured":"Pavithra Prabhakar , Vladimeros Vladimerou , Mahesh Viswanathan , and Geir E. Dullerud . 2009. Verifying tolerant systems using polynomial approximations . In Real-Time Systems Symposium, 2009, RTSS 2009. 30th IEEE. IEEE, 181--190 . Pavithra Prabhakar, Vladimeros Vladimerou, Mahesh Viswanathan, and Geir E. Dullerud. 2009. Verifying tolerant systems using polynomial approximations. In Real-Time Systems Symposium, 2009, RTSS 2009. 30th IEEE. IEEE, 181--190."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_17"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/9.664154"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.04.002"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358214","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358214","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:23:07Z","timestamp":1750202587000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358214"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,8]]},"references-count":28,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3358214"],"URL":"https:\/\/doi.org\/10.1145\/3358214","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2019,10,8]]},"assertion":[{"value":"2019-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-10-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}