{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,4]],"date-time":"2025-10-04T00:39:06Z","timestamp":1759538346392,"version":"build-2065373602"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","funder":[{"name":"National Key Research and Development Program of China","award":["2024YFB2505604"],"award-info":[{"award-number":["2024YFB2505604"]}]},{"name":"Leading-Edge Technology Program of Jiangsu Natural Science Foundation","award":["BK20202001"],"award-info":[{"award-number":["BK20202001"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["62232008, 62172200"],"award-info":[{"award-number":["62232008, 62172200"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2025,11,30]]},"abstract":"<jats:p>\n            For compositional linear hybrid automata (CLHA), whose dynamics can be characterized by linear constraints, bounded model checking (BMC) is challenging due to the complexity caused by interactions among member automata. Classical BMC approaches encode CLHA behavior using interleaving semantics, where compositions are handled with Cartesian product; as a result, the encoding is often large and complex, significantly limiting the scalability and efficiency of BMC. To address this problem, we propose three interaction relations to categorize and describe CLHA interactions through shared-label synchronization, discrete-variable read-write, and time-duration read-write. Based on the interaction relations, we devise interaction-oriented synchronization (IOS) semantics for CLHA behavior, which provides for a concise BMC encoding. In BMC, we employ a path-oriented method to check bounded reachability of CLHA, by enumerating candidate paths and checking each path\u2019s feasibility. To prune the search space of candidate paths, we introduce a temporal relation graph (TRG) to quickly rule out infeasible paths via graph-based checking. Our method is implemented into a CLHA bounded reachability checker,\n            <jats:sc>BACH<\/jats:sc>\n            . Experiments indicate that it enables significant efficiency improvement over state-of-the-art tools, and performs scalable bounded reachability analysis on practical CLHA cases within seconds.\n          <\/jats:p>","DOI":"10.1145\/3762645","type":"journal-article","created":{"date-parts":[[2025,8,25]],"date-time":"2025-08-25T11:25:51Z","timestamp":1756121151000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Checking Bounded Reachability of Compositional Linear Hybrid Automata Using Interaction Relations"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-1835-3170","authenticated-orcid":false,"given":"Yuhui","family":"Shi","sequence":"first","affiliation":[{"name":"State Key Laboratory of Novel Software Technology, Nanjing University","place":["Nanjing, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-0951-4882","authenticated-orcid":false,"given":"Yuming","family":"Wu","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Novel Software Technology, Nanjing University","place":["Nanjing, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0517-7801","authenticated-orcid":false,"given":"Lei","family":"Bu","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Novel Software Technology, Nanjing University","place":["Nanjing, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3090-9568","authenticated-orcid":false,"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Novel Software Technology, Nanjing University","place":["Nanjing, China"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,9,26]]},"reference":[{"key":"e_1_3_5_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_3_5_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.12.022"},{"key":"e_1_3_5_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"e_1_3_5_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_10"},{"key":"e_1_3_5_6_2","doi-asserted-by":"crossref","unstructured":"Armin Biere Alessandro Cimatti Edmund M. Clarke Ofer Strichman and Yunshan Zhu. 2003. Bounded model checking. Advances in Computers Vol. 58. Elsevier 117\u2013148.","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"e_1_3_5_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_34"},{"key":"e_1_3_5_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13464-7_13"},{"key":"e_1_3_5_9_2","doi-asserted-by":"publisher","DOI":"10.29007\/nv67"},{"key":"e_1_3_5_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0163-9"},{"key":"e_1_3_5_11_2","first-page":"1512","volume-title":"Proceedings of the Conference on Design, Automation and Test in Europe, DATE 2010","author":"Bu Lei","year":"2010","unstructured":"Lei Bu, You Li, Linzhang Wang, Xin Chen, and Xuandong Li. 2010. BACH 2 : Bounded reachability checker for compositional linear hybrid systems. In Proceedings of the Conference on Design, Automation and Test in Europe, DATE 2010. 1512\u20131517."},{"key":"e_1_3_5_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.13"},{"key":"e_1_3_5_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"e_1_3_5_14_2","doi-asserted-by":"publisher","DOI":"10.1287\/ijoc.3.2.157"},{"key":"e_1_3_5_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679406"},{"key":"e_1_3_5_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"e_1_3_5_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_4"},{"key":"e_1_3_5_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/185595.1017037"},{"key":"e_1_3_5_19_2","doi-asserted-by":"publisher","DOI":"10.5555\/256095.256126"},{"key":"e_1_3_5_20_2","first-page":"208","volume-title":"Hybrid Systems III: Verification and Control, Proceedings of the DIMACS\/SYCON Workshop on Verification and Control of Hybrid Systems","author":"Daws Conrado","year":"1995","unstructured":"Conrado Daws, Alfredo Olivero, Stavros Tripakis, and Sergio Yovine. 1995. The tool KRONOS. In Hybrid Systems III: Verification and Control, Proceedings of the DIMACS\/SYCON Workshop on Verification and Control of Hybrid Systems. 208\u2013219."},{"key":"e_1_3_5_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_5_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0062-x"},{"key":"e_1_3_5_23_2","unstructured":"Goran Frehse and Matthias Althoff. 2025. International Competition on Verifying Continuous and Hybrid Systems. (2025). Retrieved March 17 2025 from https:\/\/cps-vo.org\/group\/ARCH\/FriendlyCompetition"},{"key":"e_1_3_5_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"e_1_3_5_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454108"},{"key":"e_1_3_5_26_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068403001790"},{"key":"e_1_3_5_27_2","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788803"},{"key":"e_1_3_5_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050008"},{"key":"e_1_3_5_29_2","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"e_1_3_5_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75454-1_18"},{"key":"e_1_3_5_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71493-4_24"},{"key":"e_1_3_5_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/7351.7352"},{"key":"e_1_3_5_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.023"},{"key":"e_1_3_5_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90059-6"},{"key":"e_1_3_5_35_2","volume-title":"Proceedings of the 25th PhD Mini-Symposium","author":"Rebeka Farkas","year":"2018","unstructured":"Farkas Rebeka and G\u00e1bor Bergmann. 2018. Towards reliable benchmarks of timed automata. In Proceedings of the 25th PhD Mini-Symposium. Budapest University of Technology and Economics, Department of Measurement and Information Systems."},{"key":"e_1_3_5_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02777-2_24"},{"key":"e_1_3_5_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563321"},{"key":"e_1_3_5_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2005.13"},{"key":"e_1_3_5_39_2","doi-asserted-by":"crossref","unstructured":"Yuming Wu Lei Bu Jiawan Wang Xinyue Ren Wen Xiong and Xuandong Li. 2022. Mixed semantics guided layered bounded reachability analysis of compositional linear hybrid automata. In Verification Model Checking and Abstract Interpretation Bernd Finkbeiner and Thomas Wies (Eds.). Springer International Publishing Cham 473\u2013495.","DOI":"10.1007\/978-3-030-94583-1_23"},{"key":"e_1_3_5_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-014-0210-3"},{"key":"e_1_3_5_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2018.2864122"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3762645","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,3]],"date-time":"2025-10-03T14:05:50Z","timestamp":1759500350000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3762645"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,26]]},"references-count":40,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2025,11,30]]}},"alternative-id":["10.1145\/3762645"],"URL":"https:\/\/doi.org\/10.1145\/3762645","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2025,9,26]]},"assertion":[{"value":"2025-08-09","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-11","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-09-26","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}