{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,15]],"date-time":"2025-10-15T10:38:57Z","timestamp":1760524737449,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T00:00:00Z","timestamp":1747785600000},"content-version":"vor","delay-in-days":15,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"U.S. Army Contracting Command, Army Research Lab","award":["W911NF-23-2-0040"],"award-info":[{"award-number":["W911NF-23-2-0040"]}]},{"DOI":"10.13039\/501100006374","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N000141712622"],"award-info":[{"award-number":["N000141712622"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"name":"AFOSR","award":["FA9550-23-1-0529"],"award-info":[{"award-number":["FA9550-23-1-0529"]}]},{"DOI":"10.13039\/501100006374","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["2422282,2219101"],"award-info":[{"award-number":["2422282,2219101"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,5,6]]},"DOI":"10.1145\/3716863.3718042","type":"proceedings-article","created":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T06:20:33Z","timestamp":1747808433000},"page":"1-11","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["BT2Automata: Expressing Behavior Trees as Automata for Formal Control Synthesis"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-0669-7661","authenticated-orcid":false,"given":"Ryan","family":"Matheu","sequence":"first","affiliation":[{"name":"University of Maryland, College Park, Maryland, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0010-9789","authenticated-orcid":false,"given":"Aniruddh G.","family":"Puranic","sequence":"additional","affiliation":[{"name":"University of Maryland, College Park, Maryland, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4955-8561","authenticated-orcid":false,"given":"John S.","family":"Baras","sequence":"additional","affiliation":[{"name":"University of Maryland, College Park, Maryland, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7141-2657","authenticated-orcid":false,"given":"Calin","family":"Belta","sequence":"additional","affiliation":[{"name":"University of Maryland, College Park, Maryland, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,5,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/3545946.3599102"},{"volume-title":"Q-Learning for Robust Satisfaction of Signal Temporal Logic Specifications. In 2016 IEEE 55th Conference on Decision and Control (CDC). 6565--6570","author":"Aksaray D.","key":"e_1_3_2_1_2_1","unstructured":"D. Aksaray, A. Jones, Z. Kong, M. Schwager, and C. Belta. 2016. Q-Learning for Robust Satisfaction of Signal Temporal Logic Specifications. In 2016 IEEE 55th Conference on Decision and Control (CDC). 6565--6570."},{"key":"e_1_3_2_1_3_1","volume-title":"MITL model checking via generalized timed automata and a new liveness algorithm. arXiv preprint arXiv:2407.08452","author":"Akshay S","year":"2024","unstructured":"S Akshay, Paul Gastin, R Govind, and B Srivathsan. 2024. MITL model checking via generalized timed automata and a new liveness algorithm. arXiv preprint arXiv:2407.08452 (2024)."},{"key":"e_1_3_2_1_4_1","volume-title":"A theory of timed automata. Theoretical computer science 126, 2","author":"Alur Rajeev","year":"1994","unstructured":"Rajeev Alur and David L Dill. 1994. A theory of timed automata. Theoretical computer science 126, 2 (1994), 183--235."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227602"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Aaron D. Ames Samuel Coogan Magnus Egerstedt Gennaro Notomista Koushil Sreenath and Paulo Tabuada. 2019. Control Barrier Functions: Theory and Applications. arXiv:1903.11199 [cs.SY] https:\/\/arxiv.org\/abs\/1903.11199","DOI":"10.23919\/ECC.2019.8796030"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2021\/298"},{"key":"e_1_3_2_1_8_1","volume-title":"2019 IEEE\/RSJ International Conference on Intelligent Robots and Systems, IROS 2019","author":"Balakrishnan Anand","year":"2019","unstructured":"Anand Balakrishnan and Jyotirmoy V. Deshmukh. 2019. Structured Reward Shaping using Signal Temporal Logic specifications. In 2019 IEEE\/RSJ International Conference on Intelligent Robots and Systems, IROS 2019, Macau, SAR, China, November 3-8, 2019. IEEE, 3481--3486."},{"key":"e_1_3_2_1_9_1","volume-title":"A tutorial on uppaal. Formal methods for the design of real-time systems","author":"Behrmann Gerd","year":"2004","unstructured":"Gerd Behrmann, Alexandre David, and Kim G Larsen. 2004. A tutorial on uppaal. Formal methods for the design of real-time systems (2004), 200--236."},{"key":"e_1_3_2_1_10_1","volume-title":"Efficient and Modular Implicit Differentiation. arXiv preprint arXiv:2105.15183","author":"Blondel Mathieu","year":"2021","unstructured":"Mathieu Blondel, Quentin Berthet, Marco Cuturi, Roy Frostig, Stephan Hoyer, Felipe Llinares-L\u00f3pez, Fabian Pedregosa, and Jean-Philippe Vert. 2021. Efficient and Modular Implicit Differentiation. arXiv preprint arXiv:2105.15183 (2021)."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_21"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_15"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2017.8206502"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2014.6942752"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","unstructured":"Michele Colledanchise and Petter \u00d6gren. 2018. Behavior Trees in Robotics and AI. https:\/\/doi.org\/10.1201\/9780429489105","DOI":"10.1201\/9780429489105"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2008.04.035"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LRA.2023.3313052"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Alexandre Donz\u00e9 and Oded Maler. 2010. Robust Satisfaction of Temporal Logic over Real-Valued Signals. In FORMATS.","DOI":"10.1007\/978-3-642-15297-9_9"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2003.1236202"},{"key":"e_1_3_2_1_20_1","unstructured":"Davide Faconti Michele Colledanchise et al. 2024. BehaviorTree.CPP. https:\/\/github.com\/BehaviorTree\/BehaviorTree.CPP"},{"key":"e_1_3_2_1_21_1","volume-title":"Pappas","author":"Fainekos Georgios E.","year":"2009","unstructured":"Georgios E. Fainekos and George J. Pappas. 2009. Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science (2009)."},{"key":"e_1_3_2_1_22_1","volume-title":"4th Robot Learning Workshop: Self-Supervised and Lifelong Learning at NeurIPS","author":"Gallou\u00e9dec Quentin","year":"2021","unstructured":"Quentin Gallou\u00e9dec, Nicolas Cazin, Emmanuel Dellandr\u00e9a, and Liming Chen. 2021. panda-gym: Open-Source Goal-Conditioned Environments for Robotic Learning. 4th Robot Learning Workshop: Self-Supervised and Lifelong Learning at NeurIPS (2021)."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASWEC.2007.49"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.59"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2020.XVI.004"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v35i9.16975"},{"key":"e_1_3_2_1_27_1","volume-title":"Proceedings of the 37th International Conference on Machine Learning (Proceedings of Machine Learning Research","author":"Kuznetsov Arsenii","year":"2020","unstructured":"Arsenii Kuznetsov, Pavel Shvechikov, Alexander Grishin, and Dmitry Vetrov. 2020. Controlling Overestimation Bias with Truncated Mixture of Continuous Distributional Quantile Critics. In Proceedings of the 37th International Conference on Machine Learning (Proceedings of Machine Learning Research, Vol. 119), Hal Daum\u00e9 III and Aarti Singh (Eds.). PMLR, 5556--5566. https:\/\/proceedings.mlr.press\/v119\/kuznetsov20a.html"},{"key":"e_1_3_2_1_28_1","volume-title":"Automata Guided Reinforcement Learning With Demonstrations. CoRR abs\/1809.06305","author":"Li Xiao","year":"2018","unstructured":"Xiao Li, Yao Ma, and Calin Belta. 2018. Automata Guided Reinforcement Learning With Demonstrations. CoRR abs\/1809.06305 (2018). arXiv:1809.06305 http:\/\/arxiv.org\/abs\/1809.06305"},{"volume-title":"Reinforcement Learning with Temporal Logic Rewards. In 2017 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS). 3834--3839","author":"Li X.","key":"e_1_3_2_1_29_1","unstructured":"X. Li, C. Vasile, and C. Belta. 2017. Reinforcement Learning with Temporal Logic Rewards. In 2017 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS). 3834--3839."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.23919\/ACC45564.2020.9147506"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/IROS45743.2020.9341207"},{"volume-title":"Monitoring Temporal Properties of Continuous Signals","author":"Maler Oded","key":"e_1_3_2_1_32_1","unstructured":"Oded Maler and Dejan Nickovic. 2004. Monitoring Temporal Properties of Continuous Signals. In FORMATS. Springer."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/11867340_20"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2014.6907656"},{"volume-title":"Communication and concurrency","author":"Milner R.","key":"e_1_3_2_1_35_1","unstructured":"R. Milner. 1989. Communication and concurrency. Prentice-Hall, Inc., USA."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59152-6_34"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2018.08.023"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Aniruddh G. Puranic Jyotirmoy V. Deshmukh and Stefanos Nikolaidis. 2023. Signal Temporal Logic-Guided Apprenticeship Learning. arXiv:2311.05084 [cs.RO]","DOI":"10.1109\/IROS58592.2024.10801924"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1146\/annurev-control-100819-063206"},{"key":"e_1_3_2_1_41_1","volume-title":"Artificial Life Conference Proceedings. MIT Press One Rogers Street","author":"Saberi Arash","year":"2013","unstructured":"Arash Saberi, Jan Groote, and Sarmen Keshishzadeh. 2013. Analysis of path planning algorithms: a formal verification-based approach. In Artificial Life Conference Proceedings. MIT Press One Rogers Street, Cambridge, MA 02142-1209, USA journals-info ..., 232--239."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3641513.3650180"},{"key":"e_1_3_2_1_43_1","volume-title":"Johnson","author":"Serbinowska Serena Serafina","year":"2022","unstructured":"Serena Serafina Serbinowska and Taylor T. Johnson. 2022. BehaVerify: Verifying Temporal Logic Specifications for Behavior Trees. In Software Engineering and Formal Methods, Bernd-Holger Schlingloff and Ming Chai (Eds.). Springer International Publishing, Cham, 307--323."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/92.766749"},{"key":"e_1_3_2_1_45_1","unstructured":"Daniel Stonier et al. 2023. Py Trees. https:\/\/github.com\/splintered-reality\/py_trees"},{"key":"e_1_3_2_1_46_1","volume-title":"Barto","author":"Sutton Richard S.","year":"2018","unstructured":"Richard S. Sutton and Andrew G. Barto. 2018. Reinforcement Learning: An Introduction (second ed.). The MIT Press, Cambridge, MA."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA57147.2024.10610183"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECC.2016.7810369"}],"event":{"name":"HSCC '25: Computation and Control","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems"],"location":"Irvine CA USA","acronym":"HSCC '25"},"container-title":["Proceedings of the 28th ACM International Conference on Hybrid Systems: Computation and Control"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3716863.3718042","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3716863.3718042","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3716863.3718042","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,4]],"date-time":"2025-09-04T13:47:25Z","timestamp":1756993645000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3716863.3718042"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,6]]},"references-count":48,"alternative-id":["10.1145\/3716863.3718042","10.1145\/3716863"],"URL":"https:\/\/doi.org\/10.1145\/3716863.3718042","relation":{},"subject":[],"published":{"date-parts":[[2025,5,6]]},"assertion":[{"value":"2025-05-21","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}