{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T05:37:08Z","timestamp":1769751428014,"version":"3.49.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2023,9,9]],"date-time":"2023-09-09T00:00:00Z","timestamp":1694217600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"DFG","award":["389792660 TRR 248\u2013CPEC"],"award-info":[{"award-number":["389792660 TRR 248\u2013CPEC"]}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/V043676\/1, EIC 101070802, ERC 101089047"],"award-info":[{"award-number":["EP\/V043676\/1, EIC 101070802, ERC 101089047"]}],"id":[{"id":"10.13039\/501100000266","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":[[2023,10,31]]},"abstract":"<jats:p>Abstraction-based techniques are an attractive approach for synthesizing correct-by-construction controllers to satisfy high-level temporal requirements. A main bottleneck for successful application of these techniques is the memory requirement, both during controller synthesis (to store the abstract transition relation) and in controller deployment (to store the control map).<\/jats:p>\n          <jats:p>\n            We propose memory-efficient methods for mitigating the high memory demands of the abstraction-based techniques using\n            <jats:italic>neural network representations<\/jats:italic>\n            . To perform synthesis for reach-avoid specifications, we propose an on-the-fly algorithm that relies on compressed neural network representations of the forward and backward dynamics of the system. In contrast to usual applications of neural representations, our technique maintains soundness of the end-to-end process. To ensure this, we correct the output of the trained neural network such that the corrected output representations are sound with respect to the finite abstraction. For deployment, we provide a novel training algorithm to find a neural network representation of the synthesized controller and experimentally show that the controller can be correctly represented as a combination of a neural network and a look-up table that requires a substantially smaller memory.\n          <\/jats:p>\n          <jats:p>\n            We demonstrate experimentally that our approach significantly reduces the memory requirements of abstraction-based methods. We compare the performance of our approach with the standard abstraction-based synthesis on several models. For the selected benchmarks, our approach reduces the memory requirements respectively for the synthesis and deployment by a factor of 1.31\u00d7 10\n            <jats:sup>5<\/jats:sup>\n            and 7.13\u00d7 10\n            <jats:sup>3<\/jats:sup>\n            on average, and up to 7.54\u00d7 10\n            <jats:sup>5<\/jats:sup>\n            and 3.18\u00d7 10\n            <jats:sup>4<\/jats:sup>\n            . Although this reduction is at the cost of increased off-line computations to train the neural networks, all the steps of our approach are parallelizable and can be implemented on machines with higher number of processing units to reduce the required computational time.\n          <\/jats:p>","DOI":"10.1145\/3608104","type":"journal-article","created":{"date-parts":[[2023,9,9]],"date-time":"2023-09-09T13:33:18Z","timestamp":1694266398000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Neural Abstraction-Based Controller Synthesis and Deployment"],"prefix":"10.1145","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2136-0542","authenticated-orcid":false,"given":"Rupak","family":"Majumdar","sequence":"first","affiliation":[{"name":"Max Planck Institute for Software Systems, Kaiserslautern, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3790-3935","authenticated-orcid":false,"given":"Mahmoud","family":"Salamati","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems, Kaiserslautern, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1922-6678","authenticated-orcid":false,"given":"Sadegh","family":"Soudjani","sequence":"additional","affiliation":[{"name":"Newcastle University, Newcastle, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2023,9,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/2774947"},{"key":"e_1_3_2_3_2","volume-title":"Principles of Model Checking","author":"Baier C.","year":"2008","unstructured":"C. Baier and J.-P. Katoen. 2008. Principles of Model Checking. MIT press."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-50763-7"},{"key":"e_1_3_2_5_2","volume-title":"Nonlinear Programming","author":"Bertsekas D. P.","year":"1999","unstructured":"D. P. Bertsekas. 1999. Nonlinear Programming. Athena Scientific."},{"key":"e_1_3_2_6_2","volume-title":"Advances in Neural Information Processing Systems","author":"Boyan Justin","year":"1994","unstructured":"Justin Boyan and Andrew Moore. 1994. Generalization in reinforcement learning: Safely approximating the value function. In Advances in Neural Information Processing Systems, Vol. 7. MIT Press."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_8_2","first-page":"568","volume-title":"Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2018, Stockholm, Sweden, July 10\u201315, 2018","author":"Chen Ji","year":"2018","unstructured":"Ji Chen, Salar Moarref, and Hadas Kress-Gazit. 2018. Verifiable control of robotic swarm from high-level specifications. In Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2018, Stockholm, Sweden, July 10\u201315, 2018. International Foundation for Autonomous Agents and Multiagent Systems Richland, SC, USA \/ ACM, 568\u2013576."},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC45484.2021.9683316"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311807"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.3182\/20120606-3-NL-3011.00022"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2018.2843682"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3178126.3178143"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-19992-9_27"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3358228"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311806"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2021.109993"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/87.491203"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.2514\/1.G003724"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/DASC.2016.7778091"},{"key":"e_1_3_2_21_2","unstructured":"Milad Kazemi Rupak Majumdar Mahmoud Salamati Sadegh Soudjani and Ben Wooding. 2022. Data-Driven Abstraction-Based Control Synthesis. (2022)."},{"key":"e_1_3_2_22_2","first-page":"265","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6\u201311, 2019, Proceedings, Part II (Lecture Notes in Computer Science)","volume":"11428","author":"Khaled Mahmoud","year":"2019","unstructured":"Mahmoud Khaled, Eric S. Kim, Murat Arcak, and Majid Zamani. 2019. Synthesis of symbolic controllers: A parallelized and sparsity-aware approach. In Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6\u201311, 2019, Proceedings, Part II (Lecture Notes in Computer Science), Vol. 11428. Springer, 265\u2013281."},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311798"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/DCC.2013.81"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/1059816.1059820"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_24"},{"key":"e_1_3_2_27_2","volume-title":"Introduction to Embedded Systems: A Cyber-physical Systems Approach","author":"Lee Edward Ashford","year":"2016","unstructured":"Edward Ashford Lee and Sanjit Arunkumar Seshia. 2016. Introduction to Embedded Systems: A Cyber-physical Systems Approach. MIT Press."},{"key":"e_1_3_2_28_2","first-page":"142","volume-title":"Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22\u201922) (EPiC Series in Computing)","volume":"90","author":"Lopez Diego Manzanas","year":"2022","unstructured":"Diego Manzanas Lopez, Matthias Althoff, Luis Benet, Xin Chen, Jiameng Fan, Marcelo Forets, Chao Huang, Taylor T. Johnson, Tobias Ladner, Wenchao Li, Christian Schilling, and Qi Zhu. 2022. ARCH-COMP22 category report: Artificial intelligence and neural network control systems (AINNCS) for continuous and hybrid systems plants. In Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22\u201922) (EPiC Series in Computing), Vol. 90. EasyChair, 142\u2013184."},{"issue":"4","key":"e_1_3_2_29_2","first-page":"1","article-title":"On-the-fly symbolic synthesis with memory reduction guarantees","volume":"68","author":"Macoveiciuc E.","year":"2022","unstructured":"E. Macoveiciuc and G. Reissig. 2022. On-the-fly symbolic synthesis with memory reduction guarantees. IEEE Trans. Automat. Control 68, 4 (2022), 1\u20138.","journal-title":"IEEE Trans. Automat. Control"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3365365.3382219"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2021.08.473"},{"issue":"4","key":"e_1_3_2_32_2","first-page":"1781","article-title":"Feedback refinement relations for the synthesis of symbolic controllers","volume":"62","author":"Reissig G.","year":"2016","unstructured":"G. Reissig, A. Weber, and M. Rungger. 2016. Feedback refinement relations for the synthesis of symbolic controllers. IEEE TAC 62, 4 (2016), 1781\u20131796.","journal-title":"IEEE TAC"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/1967701.1967748"},{"key":"e_1_3_2_34_2","article-title":"An overview of gradient descent optimization algorithms","volume":"1609","author":"Ruder Sebastian","year":"2016","unstructured":"Sebastian Ruder. 2016. An overview of gradient descent optimization algorithms. ArXiv abs\/1609.04747 (2016).","journal-title":"ArXiv"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2012.6314891"},{"key":"e_1_3_2_36_2","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1145\/2883817.2883834","volume-title":"HSCC","author":"Rungger M.","year":"2016","unstructured":"M. Rungger and M. Zamani. 2016. SCOTS: A tool for the synthesis of symbolic controllers. In HSCC. ACM, Vienna, Austria, 99\u2013104."},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3358223"},{"key":"e_1_3_2_38_2","first-page":"33:1\u201333:2","volume-title":"HSCC\u201920: 23rd ACM International Conference on Hybrid Systems: Computation and Control, Sydney, New South Wales, Australia, April 21\u201324, 2020","author":"Samuel Stanly","year":"2020","unstructured":"Stanly Samuel, Kaushik Mallik, Anne-Kathrin Schmuck, and Daniel Neider. 2020. Resilient abstraction-based controller design. In HSCC\u201920: 23rd ACM International Conference on Hybrid Systems: Computation and Control, Sydney, New South Wales, Australia, April 21\u201324, 2020. ACM, Jeju, South Korea, 33:1\u201333:2."},{"key":"e_1_3_2_39_2","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1007\/978-3-030-44051-0_32","volume-title":"Algorithmic Foundations of Robotics XIII","author":"Singh Sumeet","year":"2020","unstructured":"Sumeet Singh, Mo Chen, Sylvia L. Herbert, Claire J. Tomlin, and Marco Pavone. 2020. Robust tracking with model mismatch for fast and safe planning: An SOS optimization approach. In Algorithmic Foundations of Robotics XIII. Springer International Publishing, Cham, 545\u2013564."},{"key":"e_1_3_2_40_2","volume-title":"Reinforcement Learning: An Introduction (2nd ed.)","author":"Sutton Richard S.","year":"2018","unstructured":"Richard S. Sutton and Andrew G. Barto. 2018. Reinforcement Learning: An Introduction (2nd ed.)."},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0224-5"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3358230"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_1"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/9.580874"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2018.08.001"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3608104","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3608104","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:32Z","timestamp":1750178792000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3608104"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,9]]},"references-count":44,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2023,10,31]]}},"alternative-id":["10.1145\/3608104"],"URL":"https:\/\/doi.org\/10.1145\/3608104","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,9,9]]},"assertion":[{"value":"2023-03-23","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-06-30","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-09-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}