{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T19:34:57Z","timestamp":1757619297587,"version":"3.44.0"},"publisher-location":"Cham","reference-count":60,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986840"},{"type":"electronic","value":"9783031986857"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Automatically constructing smooth paths that satisfy a formal specification is a challenging problem. Existing methods struggle to scale to long horizon specifications and challenging environments. We present a method that uses abstraction, model checking, and convex optimization to solve for a smooth B\u00e9zier spline that is guaranteed to satisfy a Linear Temporal Logic specification. Our approach uses a coarse abstraction to avoid the state explosion of other abstraction based methods, and successfully avoids the computational challenges of directly optimizing the non-convex temporal logic semantics. We prove our method is sound and complete and demonstrate a significant computational advantage relative to state of the art approaches. Generating such smooth paths has natural applications in path planning for autonomous robots, and we demonstrate the applicability of our method on path planning for a quadrotor.<\/jats:p>","DOI":"10.1007\/978-3-031-98685-7_12","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:32:29Z","timestamp":1753155149000},"page":"249-273","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automatic Synthesis of\u00a0Smooth Infinite Horizon Paths Satisfying Linear Temporal Logic Specifications"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-8620-1297","authenticated-orcid":false,"given":"Samuel","family":"Williams","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4683-5540","authenticated-orcid":false,"given":"Jyotirmoy","family":"Deshmukh","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Baca, T., Hert, D., Loianno, G., Saska, M., Kumar, V.: Model predictive trajectory tracking and collision avoidance for reliable outdoor deployment of unmanned aerial vehicles. In: 2018 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 6753\u20136760 (2018). https:\/\/doi.org\/10.1109\/IROS.2018.8594266","DOI":"10.1109\/IROS.2018.8594266"},{"key":"12_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Belta, C., Sadraddini, S.: Formal methods for control synthesis: an optimization perspective. Annu. Rev. Control Robot. Auton. Syst. 2, 115\u2013140 (2019). https:\/\/doi.org\/10.1146\/annurev-control-053018-023717","DOI":"10.1146\/annurev-control-053018-023717"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Bhatia, A., Kavraki, L.E., Vardi, M.Y.: Sampling-based motion planning with temporal goals. In: 2010 IEEE International Conference on Robotics and Automation, Anchorage, AK, pp. 2689\u20132696. IEEE (2010). https:\/\/doi.org\/10.1109\/ROBOT.2010.5509503","DOI":"10.1109\/ROBOT.2010.5509503"},{"issue":"3","key":"12_CR5","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012). https:\/\/doi.org\/10.1016\/j.jcss.2011.08.007","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"12_CR6","doi-asserted-by":"publisher","first-page":"1375","DOI":"10.1109\/LRA.2021.3057049","volume":"6","author":"AT Buyukkocak","year":"2021","unstructured":"Buyukkocak, A.T., Aksaray, D., Yaz\u0131c\u0131o\u011flu, Y.: Planning of heterogeneous multi-agent systems under signal temporal logic specifications with integral predicates. IEEE Robot. Autom. Lett. 6(2), 1375\u20131382 (2021). https:\/\/doi.org\/10.1109\/LRA.2021.3057049","journal-title":"IEEE Robot. Autom. Lett."},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Camacho, A., Baier, J., Muise, C., McIlraith, S.: Finite LTL synthesis as planning. In: Proceedings of the International Conference on Automated Planning and Scheduling, vol. 28, pp. 29\u201338 (2018). https:\/\/doi.org\/10.1609\/icaps.v28i1.13908","DOI":"10.1609\/icaps.v28i1.13908"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From spot 2.0 to spot 2.10: what\u2019s new? In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification, pp. 174\u2013187. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"issue":"2","key":"12_CR10","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1109\/LRA.2017.2776353","volume":"3","author":"M Faessler","year":"2018","unstructured":"Faessler, M., Franchi, A., Scaramuzza, D.: Differential flatness of quadrotor dynamics subject to rotor drag for accurate tracking of high-speed trajectories. IEEE Robot. Autom. Lett. 3(2), 620\u2013626 (2018). https:\/\/doi.org\/10.1109\/LRA.2017.2776353","journal-title":"IEEE Robot. Autom. Lett."},{"issue":"2","key":"12_CR11","doi-asserted-by":"publisher","first-page":"750","DOI":"10.1109\/LRA.2018.2789844","volume":"3","author":"J Faigl","year":"2018","unstructured":"Faigl, J., V\u00e1\u0148a, P.: Surveillance planning with B\u00e9zier curves. IEEE Robot. Autom. Lett. 3(2), 750\u2013757 (2018). https:\/\/doi.org\/10.1109\/LRA.2018.2789844","journal-title":"IEEE Robot. Autom. Lett."},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Fainekos, G.E., Loizou, S.G., Pappas, G.J.: Translating temporal logic to controller specifications. In: Proceedings of the 45th IEEE Conference on Decision and Control, pp. 899\u2013904 (2006). https:\/\/doi.org\/10.1109\/CDC.2006.377825","DOI":"10.1109\/CDC.2006.377825"},{"issue":"42","key":"12_CR13","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"GE Fainekos","year":"2009","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoret. Comput. Sci. 410(42), 4262\u20134291 (2009). https:\/\/doi.org\/10.1016\/j.tcs.2009.06.021","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"12_CR14","doi-asserted-by":"publisher","first-page":"219","DOI":"10.2514\/2.4732","volume":"24","author":"N Faiz","year":"2001","unstructured":"Faiz, N., Agrawal, S., Murray, R.: Differentially flat systems with inequality constraints: an approach to real-time feasible trajectory generation. J. Guid. Control. Dyn. 24(2), 219\u2013227 (2001)","journal-title":"J. Guid. Control. Dyn."},{"issue":"6","key":"12_CR15","doi-asserted-by":"publisher","first-page":"1327","DOI":"10.1080\/00207179508921959","volume":"61","author":"M Fliess","year":"1995","unstructured":"Fliess, M., L\u00e9vine, J., Martin, P., Rouchon, P.: Flatness and defect of non-linear systems: introductory theory and examples. Int. J. Control 61(6), 1327\u20131361 (1995). https:\/\/doi.org\/10.1080\/00207179508921959","journal-title":"Int. J. Control"},{"issue":"1","key":"12_CR16","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1109\/LCSYS.2020.3001875","volume":"5","author":"Y Gilpin","year":"2021","unstructured":"Gilpin, Y., Kurtz, V., Lin, H.: A smooth robustness measure of signal temporal logic for symbolic control. IEEE Control Syst. Lett. 5(1), 241\u2013246 (2021). https:\/\/doi.org\/10.1109\/LCSYS.2020.3001875","journal-title":"IEEE Control Syst. Lett."},{"issue":"11","key":"12_CR17","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.ifacol.2024.07.445","volume":"58","author":"N Hashemi","year":"2024","unstructured":"Hashemi, N., Williams, S., Hoxha, B., Prokhorov, D., Fainekos, G., Deshmukh, J.: LB4TL: a smooth semantics for temporal logic to train neural feedback controllers. IFAC-PapersOnLine 58(11), 183\u2013188 (2024). https:\/\/doi.org\/10.1016\/j.ifacol.2024.07.445","journal-title":"IFAC-PapersOnLine"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Jing, G., Kress-Gazit, H.: Improving the continuous execution of reactive LTL-based controllers. In: 2013 IEEE International Conference on Robotics and Automation, pp. 5439\u20135445. IEEE (2013)","DOI":"10.1109\/ICRA.2013.6631357"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Karaman, S., Frazzoli, E.: Sampling-based motion planning with deterministic $$\\mu $$-calculus specifications. In: Proceedings of the 48h IEEE Conference on Decision and Control (CDC) held jointly with 2009 28th Chinese Control Conference, pp. 2222\u20132229 (2009). https:\/\/doi.org\/10.1109\/CDC.2009.5400278","DOI":"10.1109\/CDC.2009.5400278"},{"issue":"1","key":"12_CR20","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1109\/TRO.2009.2035776","volume":"26","author":"M Kloetzer","year":"2010","unstructured":"Kloetzer, M., Belta, C.: Automatic deployment of distributed teams of robots from temporal logic motion specifications. IEEE Trans. Rob. 26(1), 48\u201361 (2010). https:\/\/doi.org\/10.1109\/TRO.2009.2035776","journal-title":"IEEE Trans. Rob."},{"issue":"6","key":"12_CR21","doi-asserted-by":"publisher","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","volume":"25","author":"H Kress-Gazit","year":"2009","unstructured":"Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-logic-based reactive mission and motion planning. IEEE Trans. Rob. 25(6), 1370\u20131381 (2009). https:\/\/doi.org\/10.1109\/TRO.2009.2030225","journal-title":"IEEE Trans. Rob."},{"issue":"4","key":"12_CR22","doi-asserted-by":"publisher","first-page":"1429","DOI":"10.1109\/LCSYS.2020.3038640","volume":"5","author":"V Kurtz","year":"2021","unstructured":"Kurtz, V., Lin, H.: Trajectory optimization for high-dimensional nonlinear systems under STL specifications. IEEE Control Syst. Lett. 5(4), 1429\u20131434 (2021). https:\/\/doi.org\/10.1109\/LCSYS.2020.3038640","journal-title":"IEEE Control Syst. Lett."},{"issue":"5","key":"12_CR23","doi-asserted-by":"publisher","first-page":"3791","DOI":"10.1109\/TRO.2023.3291463","volume":"39","author":"V Kurtz","year":"2023","unstructured":"Kurtz, V., Lin, H.: Temporal logic motion planning with convex optimization via graphs of convex sets. IEEE Trans. Rob. 39(5), 3791\u20133804 (2023). https:\/\/doi.org\/10.1109\/TRO.2023.3291463","journal-title":"IEEE Trans. Rob."},{"key":"12_CR24","unstructured":"Latombe, J.C.: Robot Motion Planning, vol.\u00a0124. Springer (2012)"},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"Lau, B., Sprunk, C., Burgard, W.: Kinodynamic motion planning for mobile robots using splines. In: 2009 IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 2427\u20132433 (2009). https:\/\/doi.org\/10.1109\/IROS.2009.5354805","DOI":"10.1109\/IROS.2009.5354805"},{"issue":"1","key":"12_CR26","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1109\/TCST.2017.2656060","volume":"26","author":"T Lee","year":"2018","unstructured":"Lee, T.: Geometric control of quadrotor UAVs transporting a cable-suspended rigid body. IEEE Trans. Control Syst. Technol. 26(1), 255\u2013264 (2018). https:\/\/doi.org\/10.1109\/TCST.2017.2656060","journal-title":"IEEE Trans. Control Syst. Technol."},{"key":"12_CR27","doi-asserted-by":"publisher","unstructured":"Lee, T., Leok, M., McClamroch, N.H.: Geometric tracking control of a quadrotor UAV on SE(3). In: 49th IEEE Conference on Decision and Control (CDC), pp. 5420\u20135425 (2010). https:\/\/doi.org\/10.1109\/CDC.2010.5717652","DOI":"10.1109\/CDC.2010.5717652"},{"issue":"6","key":"12_CR28","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1177\/02783649221082115","volume":"42","author":"K Leung","year":"2023","unstructured":"Leung, K., Ar\u00e9chiga, N., Pavone, M.: Backpropagation through signal temporal logic specifications: infusing logical structure into gradient-based methods. Int. J. Robot. Res. 42(6), 356\u2013370 (2023). https:\/\/doi.org\/10.1177\/02783649221082115","journal-title":"Int. J. Robot. Res."},{"issue":"1","key":"12_CR29","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1109\/LCSYS.2018.2853182","volume":"3","author":"L Lindemann","year":"2019","unstructured":"Lindemann, L., Dimarogonas, D.V.: Control barrier functions for signal temporal logic tasks. IEEE Control Syst. Lett. 3(1), 96\u2013101 (2019). https:\/\/doi.org\/10.1109\/LCSYS.2018.2853182","journal-title":"IEEE Control Syst. Lett."},{"key":"12_CR30","doi-asserted-by":"publisher","unstructured":"Lindemann, L., Dimarogonas, D.V.: Decentralized control barrier functions for coupled multi-agent systems under signal temporal logic tasks. In: 2019 18th European Control Conference (ECC), pp. 89\u201394 (2019). https:\/\/doi.org\/10.23919\/ECC.2019.8796109","DOI":"10.23919\/ECC.2019.8796109"},{"issue":"5","key":"12_CR31","doi-asserted-by":"publisher","first-page":"1487","DOI":"10.1109\/TRO.2021.3061983","volume":"37","author":"X Luo","year":"2021","unstructured":"Luo, X., Kantaros, Y., Zavlanos, M.M.: An abstraction-free method for multirobot temporal logic optimal control synthesis. IEEE Trans. Rob. 37(5), 1487\u20131507 (2021). https:\/\/doi.org\/10.1109\/TRO.2021.3061983","journal-title":"IEEE Trans. Rob."},{"key":"12_CR32","doi-asserted-by":"publisher","unstructured":"Majumdar, R., Ozay, N., Schmuck, A.K.: On abstraction-based controller design with output feedback. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, HSCC 2020, pp. 1\u201311. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3365365.3382219","DOI":"10.1145\/3365365.3382219"},{"key":"12_CR33","doi-asserted-by":"publisher","unstructured":"Marcucci, T., Petersen, M., von Wrangel, D., Tedrake, R.: Motion planning around obstacles with convex optimization. Sci. Robot. 8(84), eadf7843 (2023). https:\/\/doi.org\/10.1126\/scirobotics.adf7843","DOI":"10.1126\/scirobotics.adf7843"},{"issue":"1","key":"12_CR34","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1137\/22M1523790","volume":"34","author":"T Marcucci","year":"2024","unstructured":"Marcucci, T., Umenberger, J., Parrilo, P., Tedrake, R.: Shortest paths in graphs of convex sets. SIAM J. Optim. 34(1), 507\u2013532 (2024). https:\/\/doi.org\/10.1137\/22M1523790","journal-title":"SIAM J. Optim."},{"key":"12_CR35","doi-asserted-by":"publisher","unstructured":"McMahon, J., Plaku, E.: Sampling-based tree search with discrete abstractions for motion planning with dynamics and temporal logic. In: 2014 IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 3726\u20133733 (2014). https:\/\/doi.org\/10.1109\/IROS.2014.6943085","DOI":"10.1109\/IROS.2014.6943085"},{"key":"12_CR36","doi-asserted-by":"publisher","unstructured":"Mellinger, D., Kumar, V.: Minimum snap trajectory generation and control for quadrotors. In: 2011 IEEE International Conference on Robotics and Automation, pp. 2520\u20132525 (2011). https:\/\/doi.org\/10.1109\/ICRA.2011.5980409","DOI":"10.1109\/ICRA.2011.5980409"},{"key":"12_CR37","doi-asserted-by":"publisher","unstructured":"Nilsson, P., Ames, A.D.: Barrier functions: bridging the gap between planning from specifications and safety-critical control. In: 2018 IEEE Conference on Decision and Control (CDC), pp. 765\u2013772 (2018). https:\/\/doi.org\/10.1109\/CDC.2018.8619142","DOI":"10.1109\/CDC.2018.8619142"},{"key":"12_CR38","doi-asserted-by":"publisher","unstructured":"Pant, Y.V., Abbas, H., Mangharam, R.: Smooth operator: control using the smooth robustness of temporal logic. In: 2017 IEEE Conference on Control Technology and Applications (CCTA), pp. 1235\u20131240 (2017). https:\/\/doi.org\/10.1109\/CCTA.2017.8062628","DOI":"10.1109\/CCTA.2017.8062628"},{"key":"12_CR39","doi-asserted-by":"publisher","unstructured":"Pant, Y.V., Abbas, H., Quaye, R.A., Mangharam, R.: Fly-by-logic: control of multi-drone fleets with temporal logic objectives. In: 2018 ACM\/IEEE 9th International Conference on Cyber-Physical Systems (ICCPS), pp. 186\u2013197 (2018). https:\/\/doi.org\/10.1109\/ICCPS.2018.00026","DOI":"10.1109\/ICCPS.2018.00026"},{"key":"12_CR40","doi-asserted-by":"publisher","unstructured":"Piegl, L., Tiller, W.: The NURBS Book. Monographs in Visual Communication, Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/978-3-642-59223-2","DOI":"10.1007\/978-3-642-59223-2"},{"issue":"1","key":"12_CR41","doi-asserted-by":"publisher","first-page":"151","DOI":"10.3233\/AIC-150682","volume":"29","author":"E Plaku","year":"2016","unstructured":"Plaku, E., Karaman, S.: Motion planning with temporal-logic specifications: progress and challenges. AI Commun. 29(1), 151\u2013162 (2016). https:\/\/doi.org\/10.3233\/AIC-150682","journal-title":"AI Commun."},{"key":"12_CR42","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46\u201357 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"12_CR43","doi-asserted-by":"publisher","unstructured":"Preiss, J., Hausman, K., Sukhatme, G., Weiss, S.: Trajectory optimization for self-calibration and navigation. In: Robotics: Science and Systems XIII. Robotics: Science and Systems Foundation (2017). https:\/\/doi.org\/10.15607\/RSS.2017.XIII.054","DOI":"10.15607\/RSS.2017.XIII.054"},{"key":"12_CR44","doi-asserted-by":"publisher","unstructured":"Raman, V., Donz\u00e9, A., Maasoumy, M., Murray, R.M., Sangiovanni-Vincentelli, A., Seshia, S.A.: Model predictive control with signal temporal logic specifications. In: 53rd IEEE Conference on Decision and Control, pp. 81\u201387 (2014). https:\/\/doi.org\/10.1109\/CDC.2014.7039363","DOI":"10.1109\/CDC.2014.7039363"},{"key":"12_CR45","series-title":"Springer Tracts in Advanced Robotics","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1007\/978-3-319-28872-7_37","volume-title":"Robotics Research","author":"C Richter","year":"2016","unstructured":"Richter, C., Bry, A., Roy, N.: Polynomial trajectory planning for aggressive quadrotor flight in dense indoor environments. In: Inaba, M., Corke, P. (eds.) Robotics Research. STAR, vol. 114, pp. 649\u2013666. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-28872-7_37"},{"key":"12_CR46","doi-asserted-by":"crossref","unstructured":"Rungger, M., Mazo\u00a0Jr, M., Tabuada, P.: Specification-guided controller synthesis for linear systems and safe linear-time temporal logic. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, pp. 333\u2013342 (2013)","DOI":"10.1145\/2461328.2461378"},{"key":"12_CR47","doi-asserted-by":"publisher","unstructured":"Saha, S., Julius, A.A.: An MILP approach for real-time optimal controller synthesis with metric temporal logic specifications. In: 2016 American Control Conference (ACC), pp. 1105\u20131110 (2016). https:\/\/doi.org\/10.1109\/ACC.2016.7525063","DOI":"10.1109\/ACC.2016.7525063"},{"key":"12_CR48","unstructured":"Schmuck, A.K.: Building Bridges in Abstraction-Based Controller Synthesis: Advancing, Combining, and Comparing Methods From Computer and Control. Technische Universitaet Berlin (Germany) (2015)"},{"key":"12_CR49","doi-asserted-by":"publisher","unstructured":"Sreenath, K., Lee, T., Kumar, V.: Geometric control and differential flatness of a quadrotor UAV with a cable-suspended load. In: 52nd IEEE Conference on Decision and Control, pp. 2269\u20132274 (2013). https:\/\/doi.org\/10.1109\/CDC.2013.6760219","DOI":"10.1109\/CDC.2013.6760219"},{"issue":"2","key":"12_CR50","doi-asserted-by":"publisher","first-page":"3451","DOI":"10.1109\/LRA.2022.3146951","volume":"7","author":"D Sun","year":"2022","unstructured":"Sun, D., Chen, J., Mitra, S., Fan, C.: Multi-agent motion planning from signal temporal logic specifications. IEEE Robot. Autom. Lett. 7(2), 3451\u20133458 (2022). https:\/\/doi.org\/10.1109\/LRA.2022.3146951","journal-title":"IEEE Robot. Autom. Lett."},{"issue":"6","key":"12_CR51","doi-asserted-by":"publisher","first-page":"3357","DOI":"10.1109\/TRO.2022.3177279","volume":"38","author":"S Sun","year":"2022","unstructured":"Sun, S., Romero, A., Foehn, P., Kaufmann, E., Scaramuzza, D.: A comparative study of nonlinear MPC and differential-flatness-based control for quadrotor agile flight. IEEE Trans. Rob. 38(6), 3357\u20133373 (2022). https:\/\/doi.org\/10.1109\/TRO.2022.3177279","journal-title":"IEEE Trans. Rob."},{"issue":"6","key":"12_CR52","doi-asserted-by":"publisher","first-page":"1003","DOI":"10.1109\/TAC.2006.876946","volume":"51","author":"P Tabuada","year":"2006","unstructured":"Tabuada, P.: Symbolic control of linear systems based on symbolic subsystems. IEEE Trans. Autom. Control 51(6), 1003\u20131013 (2006)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"6","key":"12_CR53","doi-asserted-by":"publisher","first-page":"1406","DOI":"10.1109\/TAC.2008.925824","volume":"53","author":"P Tabuada","year":"2008","unstructured":"Tabuada, P.: An approximate simulation approach to symbolic control. IEEE Trans. Autom. Control 53(6), 1406\u20131418 (2008). https:\/\/doi.org\/10.1109\/TAC.2008.925824","journal-title":"IEEE Trans. Autom. Control"},{"key":"12_CR54","doi-asserted-by":"publisher","unstructured":"Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, Boston (2009). https:\/\/doi.org\/10.1007\/978-1-4419-0224-5","DOI":"10.1007\/978-1-4419-0224-5"},{"issue":"12","key":"12_CR55","doi-asserted-by":"publisher","first-page":"1862","DOI":"10.1109\/TAC.2006.886494","volume":"51","author":"P Tabuada","year":"2006","unstructured":"Tabuada, P., Pappas, G.J.: Linear time logic control of discrete-time linear systems. IEEE Trans. Autom. Control 51(12), 1862\u20131877 (2006). https:\/\/doi.org\/10.1109\/TAC.2006.886494","journal-title":"IEEE Trans. Autom. Control"},{"key":"12_CR56","doi-asserted-by":"publisher","unstructured":"Tordesillas, J., Lopez, B.T., How, J.P.: FASTER: fast and safe trajectory planner for flights in unknown environments. In: 2019 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 1934\u20131940 (2019). https:\/\/doi.org\/10.1109\/IROS40897.2019.8968021","DOI":"10.1109\/IROS40897.2019.8968021"},{"key":"12_CR57","doi-asserted-by":"publisher","unstructured":"Vasile, C.I., Belta, C.: Sampling-based temporal logic path planning. In: 2013 IEEE\/RSJ International Conference on Intelligent Robots and Systems, pp. 4817\u20134822 (2013). https:\/\/doi.org\/10.1109\/IROS.2013.6697051","DOI":"10.1109\/IROS.2013.6697051"},{"key":"12_CR58","doi-asserted-by":"publisher","unstructured":"Vega-Brown, W., Roy, N.: Admissible abstractions for near-optimal task and motion planning. In: Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, pp. 4852\u20134859. International Joint Conferences on Artificial Intelligence Organization, Stockholm, Sweden (2018). https:\/\/doi.org\/10.24963\/ijcai.2018\/674","DOI":"10.24963\/ijcai.2018\/674"},{"key":"12_CR59","doi-asserted-by":"publisher","unstructured":"Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon control for temporal logic specifications. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, pp. 101\u2013110. Association for Computing Machinery, New York (2010). https:\/\/doi.org\/10.1145\/1755952.1755968","DOI":"10.1145\/1755952.1755968"},{"issue":"4","key":"12_CR60","doi-asserted-by":"publisher","first-page":"3529","DOI":"10.1109\/LRA.2019.2927938","volume":"4","author":"B Zhou","year":"2019","unstructured":"Zhou, B., Gao, F., Wang, L., Liu, C., Shen, S.: Robust and efficient quadrotor trajectory generation for fast autonomous flight. IEEE Robot. Autom. Lett. 4(4), 3529\u20133536 (2019). https:\/\/doi.org\/10.1109\/LRA.2019.2927938","journal-title":"IEEE Robot. Autom. Lett."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98685-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T17:19:28Z","timestamp":1757265568000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98685-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986840","9783031986857"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98685-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}