{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T20:14:47Z","timestamp":1773778487982,"version":"3.50.1"},"reference-count":62,"publisher":"SAGE Publications","issue":"6","license":[{"start":{"date-parts":[[2023,12,19]],"date-time":"2023-12-19T00:00:00Z","timestamp":1702944000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["CoG LEAFHOUND"],"award-info":[{"award-number":["CoG LEAFHOUND"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004063","name":"Knut and Alice Wallenberg Foundation (Wallenberg Scholar Grant and Wallenberg Academy Fellow), the ERC COG LEAFHOUND","doi-asserted-by":"publisher","award":["864720"],"award-info":[{"award-number":["864720"]}],"id":[{"id":"10.13039\/501100004063","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004359","name":"Vetenskapsr\u00e5det","doi-asserted-by":"publisher","award":["2017-01078"],"award-info":[{"award-number":["2017-01078"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"publisher"}]},{"name":"International Postdoc","award":["2021-06727"],"award-info":[{"award-number":["2021-06727"]}]},{"name":"ERC ADG FUN2MODEL","award":["834115"],"award-info":[{"award-number":["834115"]}]}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["The International Journal of Robotics Research"],"published-print":{"date-parts":[[2024,5]]},"abstract":"<jats:p> Signal temporal logic (STL) formulas have been widely used as a formal language to express complex robotic specifications, thanks to their rich expressiveness and explicit time semantics. Existing approaches for STL control synthesis suffer from limited scalability with respect to the task complexity and lack of robustness against the uncertainty, for example, external disturbances. In this paper, we study the online control synthesis problem for uncertain discrete-time systems subject to STL specifications. Different from existing techniques, we propose an approach based on STL, reachability analysis, and temporal logic trees. First, based on a real-time version of STL semantics, we develop the notion of tube-based temporal logic tree (tTLT) and its recursive (offline) construction algorithm. We show that the tTLT is an under-approximation of the STL formula, in the sense that a trajectory satisfying a tTLT also satisfies the corresponding STL formula. Then, an online control synthesis algorithm is designed using the constructed tTLT. It is shown that when the STL formula is robustly satisfiable and the initial state of the system belongs to the initial root node of the tTLT, it is guaranteed that the trajectory generated by the control synthesis algorithm satisfies the STL formula. We validate the effectiveness of the proposed approach by several simulation examples and further demonstrate its practical usability on a hardware experiment. These results show that our approach is able to handle complex STL formulas with long horizons and ensure the robustness against the disturbances, which is beyond the scope of the state-of-the-art STL control synthesis approaches. <\/jats:p>","DOI":"10.1177\/02783649231212572","type":"journal-article","created":{"date-parts":[[2023,12,19]],"date-time":"2023-12-19T09:31:20Z","timestamp":1702978280000},"page":"765-790","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":6,"title":["Online control synthesis for uncertain systems under signal temporal logic specifications"],"prefix":"10.1177","volume":"43","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6046-7129","authenticated-orcid":false,"given":"Pian","family":"Yu","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Oxford, Oxford, UK"}]},{"given":"Yulong","family":"Gao","sequence":"additional","affiliation":[{"name":"Department of Electrical and Electronic Engineering, Imperial College London, London, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6653-5508","authenticated-orcid":false,"given":"Frank J.","family":"Jiang","sequence":"additional","affiliation":[{"name":"Division of Decision and Control Systems, KTH Royal Institute of Technology, Stockholm, Sweden"},{"name":"Digital Futures, Stockholm, Sweden"}]},{"given":"Karl H.","family":"Johansson","sequence":"additional","affiliation":[{"name":"Division of Decision and Control Systems, KTH Royal Institute of Technology, Stockholm, Sweden"},{"name":"Digital Futures, Stockholm, Sweden"}]},{"given":"Dimos V.","family":"Dimarogonas","sequence":"additional","affiliation":[{"name":"Division of Decision and Control Systems, KTH Royal Institute of Technology, Stockholm, Sweden"},{"name":"Digital Futures, Stockholm, Sweden"}]}],"member":"179","published-online":{"date-parts":[[2023,12,19]]},"reference":[{"key":"bibr1-02783649231212572","doi-asserted-by":"crossref","unstructured":"Allen RE, Clark AA, Starek JA, et al. (2014) A machine learning approach for real-time reachability analysis In: Proceedings of IEEE\/RSJ international conference on intelligent robots and systems, Chicago, IL, 14-18 September 2014, pp. 2202\u20132208.","DOI":"10.1109\/IROS.2014.6942859"},{"key":"bibr2-02783649231212572","unstructured":"Althoff M (2015) An introduction to CORA 2015. In: Proceedings of the workshop on applied verification for continuous and hybrid systems. pp. 120\u2013151."},{"key":"bibr3-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227602"},{"key":"bibr4-02783649231212572","volume-title":"Principles of Model Checking","author":"Baier C","year":"2008"},{"key":"bibr5-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44184-5"},{"key":"bibr6-02783649231212572","doi-asserted-by":"crossref","unstructured":"Bansal S, Tomlin CJ (2021) Deepreach: a deep learning approach to high-dimensional reachability. In: Proceedings of IEEE international conference on robotics and automation, pp. 1817\u20131824.","DOI":"10.1109\/ICRA48506.2021.9561949"},{"key":"bibr7-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/LRA.2019.2926669"},{"key":"bibr8-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2007.339624"},{"key":"bibr9-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-50763-7"},{"key":"bibr10-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.1972.1100085"},{"key":"bibr11-02783649231212572","volume-title":"OptimizedDP: an Eeficient, user-friendly library for optimal control and dynamic programming","author":"Bui M","year":"2022"},{"key":"bibr12-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/LRA.2021.3057049"},{"key":"bibr13-02783649231212572","doi-asserted-by":"crossref","unstructured":"Buyukkocak AT, Aksaray D, Yaz\u0131c\u0131o\u011flu Y (2022) Control barrier functions with actuation constraints under signal temporal logic specifications. In: Proceedings of European control conference, London, 12-15 July 2022.","DOI":"10.23919\/ECC55457.2022.9838028"},{"key":"bibr14-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2018.2797194"},{"key":"bibr15-02783649231212572","doi-asserted-by":"crossref","unstructured":"Chen M, Tam Q, Livingston SC, et al. (2018b) Signal temporal logic meets Hamilton-Jacobi reachability: connections and applications. In: Proceedings of workshop on algorithmic foundations of robotics, pp. 581\u2013601.","DOI":"10.1007\/978-3-030-44051-0_34"},{"key":"bibr16-02783649231212572","doi-asserted-by":"crossref","unstructured":"Dokhanchi A, Hoxha B, Fainekos G (2014) On-line monitoring for temporal logic robustness. In: Proceedings of international conference on runtime verification, pp. 231\u2013246.","DOI":"10.1007\/978-3-319-11164-3_19"},{"key":"bibr17-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"bibr18-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2018.2880651"},{"key":"bibr19-02783649231212572","doi-asserted-by":"crossref","unstructured":"Fu J, Topcu U (2015) Computational methods for stochastic control with metric interval temporal logic specifications. In: Proceedings of 54th IEEE conference on decision and control, Osaka, 15-18 December 2015, pp. 7440\u20137447.","DOI":"10.1109\/CDC.2015.7403395"},{"key":"bibr20-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2021.3118335"},{"key":"bibr21-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_6"},{"key":"bibr22-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2020.3001875"},{"key":"bibr23-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17108-6_12"},{"key":"bibr24-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/LRA.2022.3155197"},{"key":"bibr25-02783649231212572","doi-asserted-by":"crossref","unstructured":"Herceg M, Kvasnica M, Jones CN, et al. (2013) Multi-parametric toolbox 3.0. In: Proceedings of European control conference, Zurich, 17-19 July 2013, pp. 502\u2013510.","DOI":"10.23919\/ECC.2013.6669862"},{"key":"bibr26-02783649231212572","doi-asserted-by":"crossref","unstructured":"Ho QH, Ilyes RB, Sunberg ZN, et al. (2022) Automaton-guided control synthesis for signal temporal logic specifications. In: 2022 IEEE 61st conference on decision and control (CDC), pp. 3243\u20133249.","DOI":"10.1109\/CDC51059.2022.9993090"},{"key":"bibr27-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/CDC42340.2020.9304186"},{"key":"bibr28-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/ITSC55140.2022.9922544"},{"key":"bibr29-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2018.2853558"},{"key":"bibr30-02783649231212572","volume-title":"Model-based Reinforcement Learning from Signal Temporal Logic Specifications","author":"Kapoor P","year":"2020"},{"key":"bibr31-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2020.12.2397"},{"key":"bibr32-02783649231212572","volume-title":"Fully Automated Verification of Linear Time-Invariant Systems against Signal Temporal Logic Specifications via Reachability Analysis","author":"Kochdumper N","year":"2023"},{"key":"bibr33-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"bibr34-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1146\/annurev-control-060117-104838"},{"key":"bibr35-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2022.3172857"},{"key":"bibr36-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10277-1"},{"key":"bibr37-02783649231212572","doi-asserted-by":"crossref","unstructured":"Leung K, Pavone M (2022) Semi-supervised trajectory-feedback controller synthesis for signal temporal logic specifications. In: 2022 American Control Conference (ACC). pp. 178\u2013185.","DOI":"10.23919\/ACC53348.2022.9867345"},{"key":"bibr38-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1177\/02783649221082115"},{"key":"bibr39-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2018.2853182"},{"key":"bibr40-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2019.05.013"},{"key":"bibr41-02783649231212572","doi-asserted-by":"crossref","unstructured":"Lindemann L, Matni N, Pappas GJ (2021a) Stl robustness risk over discrete-time stochastic processes. In: 2021 60th IEEE conference on decision and control (CDC), Austin, TX, 14-17 December 2021, pp. 1329\u20131335.","DOI":"10.1109\/CDC45484.2021.9683305"},{"key":"bibr42-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2021.3120681"},{"key":"bibr43-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2021.3049917"},{"key":"bibr44-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"bibr45-02783649231212572","doi-asserted-by":"crossref","unstructured":"Mitchell IM, Templeton JA (2005) A toolbox of Hamilton-Jacobi solvers for analysis of nondeterministic continuous and hybrid systems. In: Proceedings of international workshop on hybrid systems: computation and control, pp. 480\u2013494.","DOI":"10.1007\/978-3-540-31954-2_31"},{"key":"bibr46-02783649231212572","doi-asserted-by":"crossref","unstructured":"Murgovski N, Sj\u00f6berg J (2015) Predictive cruise control with autonomous overtaking. In Proceedings of 54th IEEE conference on decision and control, pp. 644\u2013649.","DOI":"10.1109\/CDC.2015.7402302"},{"key":"bibr47-02783649231212572","doi-asserted-by":"crossref","unstructured":"Raman V, Donz\u00e9 A, Maasoumy M, et al. (2014) Model predictive control with signal temporal logic specifications. In: Proceedings of 53rd IEEE conference on decision and control, Los Angeles, CA, 15-17 December 2014, pp. 81\u201387.","DOI":"10.1109\/CDC.2014.7039363"},{"key":"bibr48-02783649231212572","doi-asserted-by":"crossref","unstructured":"Raman V, Donz\u00e9 A, Sadigh D, et al. (2015) Reactive synthesis from signal temporal logic specifications. In: Proceedings of the 18th international conference on hybrid systems: computation and control, pp. 239\u2013248.","DOI":"10.1145\/2728606.2728628"},{"key":"bibr49-02783649231212572","doi-asserted-by":"crossref","unstructured":"Roehm H, Oehlerking J, Heinz T, et al. (2016) Stl model checking of continuous and hybrid systems. In: Automated technology for verification and analysis: 14th international symposium, ATVA 2016, Chiba, October 17-20, 2016, Proceedings vol. 14. pp. 412\u2013427.","DOI":"10.1007\/978-3-319-46520-3_26"},{"key":"bibr50-02783649231212572","doi-asserted-by":"crossref","unstructured":"Sadraddini S, Belta C (2015) Robust temporal logic model predictive control. In: Proceedings of 53rd annual Allerton conference on communication, control, and computing (Allerton), Monticello, IL, 29 September 2015 - 02 October 2015, pp. 772\u2013779.","DOI":"10.1109\/ALLERTON.2015.7447084"},{"key":"bibr51-02783649231212572","doi-asserted-by":"crossref","unstructured":"Scher G, Sadraddini S, Kress-Gazit H (2022) Robustness-based synthesis for stochastic systems under signal temporal logic tasks. In: 2022 IEEE\/RSJ international conference on intelligent robots and systems (IROS), Koyoto, 23-27 October 2022, pp. 1269\u20131275.","DOI":"10.1109\/IROS47612.2022.9982233"},{"key":"bibr52-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v37i12.26764"},{"key":"bibr53-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1109\/LRA.2022.3146951"},{"key":"bibr54-02783649231212572","volume-title":"Signal Temporal Logic Meets Convex-Concave Programming: A Structure-Exploiting Sqp Algorithm for Stl Specifications","author":"Takayama Y","year":"2023"},{"key":"bibr55-02783649231212572","volume-title":"Direct Data-Driven Signal Temporal Logic Control of Linear Systems","author":"van Huijgevoort BC","year":"2023"},{"key":"bibr56-02783649231212572","doi-asserted-by":"crossref","unstructured":"Vasile CI, Belta C (2013) Sampling-based temporal logic path planning. In: Proceedings of IEEE\/RSJ international conference on intelligent robots and systems, pp. 4817\u20134822.","DOI":"10.1109\/IROS.2013.6697051"},{"key":"bibr57-02783649231212572","doi-asserted-by":"crossref","unstructured":"Vasile CI, Raman V, Karaman S (2017a) Sampling-based synthesis of maximally-satisfying controllers for temporal logic specifications. In: Proceedings of IEEE\/RSJ international conference on intelligent robots and systems, pp. 3840\u20133847.","DOI":"10.1109\/IROS.2017.8206235"},{"key":"bibr58-02783649231212572","doi-asserted-by":"crossref","unstructured":"Vasile CI, Raman V, Karaman S (2017b) Sampling-based synthesis of maximally-satisfying controllers for temporal logic specifications. In: 2017 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS). pp. 3840\u20133847.","DOI":"10.1109\/IROS.2017.8206235"},{"key":"bibr59-02783649231212572","unstructured":"Venkataraman H, Aksaray D, Seiler P (2020) Tractable reinforcement learning of signal temporal logic objectives. In: Learning for Dynamics and Control. PMLR, pp. 308\u2013317."},{"key":"bibr60-02783649231212572","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-28872-7_2"},{"key":"bibr61-02783649231212572","doi-asserted-by":"crossref","unstructured":"Yang G, Belta C, Tron R (2020) Continuous-time signal temporal logic planning with control barrier functions. In: Proceedings of American Control Conference, pp. 4612\u20134618.","DOI":"10.23919\/ACC45564.2020.9147387"},{"key":"bibr62-02783649231212572","doi-asserted-by":"crossref","unstructured":"Zhou Y, Maity D, Baras JS (2016) Timed automata approach for motion planning using metric interval temporal logic. In: Proceedings of European Control Conference, pp. 690\u2013695.","DOI":"10.1109\/ECC.2016.7810369"}],"container-title":["The International Journal of Robotics Research"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/02783649231212572","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.1177\/02783649231212572","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/02783649231212572","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,2]],"date-time":"2025-03-02T20:14:36Z","timestamp":1740946476000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.1177\/02783649231212572"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,19]]},"references-count":62,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2024,5]]}},"alternative-id":["10.1177\/02783649231212572"],"URL":"https:\/\/doi.org\/10.1177\/02783649231212572","relation":{},"ISSN":["0278-3649","1741-3176"],"issn-type":[{"value":"0278-3649","type":"print"},{"value":"1741-3176","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,12,19]]}}}