Abstract
This paper introduces a partial satisfaction (PS) notion for Signal Temporal Logic (STL), finding solutions for specifications that might contain unfeasible or conflicting subformulae. We formulate the planning problem for teams of agents with robust PS of STL missions as a bi-level optimization problem. The goal is to maximize the number of subformulae satisfied with preference to larger ones that have lower depth in the syntax tree of the overall specification. The second objective is to maximize the smallest STL robustness of the feasible subformulae. First, we propose three Mixed Integer Linear Programming (MILP) methods to solve the inner level of the optimization problem, two exact and a relaxation. Then, the MILP solutions are used to find approximate solutions to the outer level optimization using a linear program. Finally, we show the performance of our methods in two multi-robot case studies: motion planning in continuous spaces, and routing for heterogeneous teams over finite graph abstractions.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Lower-depth node satisfaction implies a higher percentage of specification satisfaction since every all node underneath are guaranteed to be satisfied when their parent nodes are satisfied.
- 2.
A formula can have many equivalent ASTs [15] determined by the parsing methods used.
References
Cai, M., Peng, H., Li, Z., Gao, H., Kan, Z.: Receding horizon control-based motion planning with partially infeasible ltl constraints. IEEE Control Syst. Lett. 5(4), 1279–1284 (2020)
Cai, M., Peng, H., Li, Z., Kan, Z.: Learning-based probabilistic ltl motion planning with environment and motion uncertainties. IEEE Trans. Autom. Control 66(5), 2386–2392 (2020)
Cardona, G.A., Calderon, J.M.: Robot swarm navigation and victim detection using rendezvous consensus in search and rescue operations. Appl. Sci. 9(8), 1702 (2019)
Choudhury, S., Gupta, J.K., Kochenderfer, M.J., Sadigh, D., Bohg, J.: Dynamic multi-robot task allocation under uncertainty and temporal constraints. Robot.: Sci. Syst. 46(1), 231–247 (2020)
Cortés, J., Egerstedt, M.: Coordinated control of multi-robot systems: a survey. SICE J. Control Meas. Syst. Integr. 10(6), 495–503 (2017)
Cortes, J., Martinez, S., Karatas, T., Bullo, F.: Coverage control for mobile sensing networks. IEEE Trans. Robot. Autom. 20(2), 243–255 (2004)
Davey, B.A., Priestley, H.A.: Introduction to lattices and order. Cambridge University Press, Cambridge (2002)
Dokhanchi, A., Hoxha, B., Fainekos, G.: On-line monitoring for temporal logic robustness. In: 5th International Conference on Runtime Verification, Toronto, ON, Canada, pp. 231–246. Springer (2014)
Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: International Conference on Formal Modeling and Analysis of Timed Systems, pp. 92–106. Springer (2010)
Emam, Y., Mayya, S., Notomista, G., Bohannon, A., Egerstedt, M.: Adaptive task allocation for heterogeneous multi-robot teams with evolving and unknown robot capabilities (2020). arXiv:2003.03344
Emam, Y., Wilson, S., Hakenberg, M., Munz, U., Egerstedt, M.: A receding horizon scheduling approach for search & rescue scenarios. arXiv pp. arXiv-2004 (2020)
Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009)
Gurobi Optimization, LLC: Gurobi optimizer reference manual. https://www.gurobi.com (2021)
Heemels, W., De Schutter, B., Bemporad, A.: Equivalence of hybrid dynamical models. Automatica 37(7), 1085–1091 (2001)
Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation. Acm Sigact. News 32(1), 60–65 (2001)
Jones, A.M., Leahy, K., Vasile, C., Sadraddini, S., Serlin, Z., Tron, R., Belta, C.: Scratchs: Scalable and robust algorithms for task-based coordination from high-level specifications. In: International Symposium of Robotics Research, International Federation of Robotics Research (2019)
Kamale, D., Karyofylli, E., Vasile, C.I.: Automata-based optimal planning with relaxed specifications. In: 2021 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). IEEE (2021)
Khalil, H.K.: Nonlinear Systems, 3rd edn. Patience Hall, Hoboken (2002)
Lacerda, B., Parker, D., Hawes, N.: Optimal policy generation for partially satisfiable co-safe ltl specifications. In: Twenty-Fourth International Joint Conference on Artificial Intelligence (2015)
Lahijanian, M., Almagor, S., Fried, D., Kavraki, L.E., Vardi, M.Y.: This time the robot settles for a cost: a quantitative approach to temporal logic planning with partial satisfaction. In: Twenty-Ninth AAAI Conference on Artificial Intelligence (2015)
Leahy, K., Jones, A., Vasile, C.I.: Fast decomposition of temporal logic specifications for heterogeneous teams. IEEE Robot. Autom. Lett. 7(2), 2297–2304 (2022)
Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, pp. 152–166. Springer (2004)
Notomista, G., Mayya, S., Hutchinson, S., Egerstedt, M.: An optimal task allocation strategy for heterogeneous multi-robot systems. In: 2019 18th European Control Conference (ECC), pp. 2071–2076. IEEE (2019)
Raman, V., Donzé, 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–87. IEEE (2014)
Sadraddini, S., Belta, C.: Robust temporal logic model predictive control. In: 2015 53rd Annual Allerton Conference on Communication, Control, and Computing (Allerton), pp. 772–779. IEEE (2015)
Schillinger, P., Bürger, M., Dimarogonas, D.V.: Simultaneous task allocation and planning for temporal logic goals in heterogeneous multi-robot systems. Inter. J. Robot. Res. 37(7), 818–838 (2018)
Ulusoy, A., Smith, S.L., Ding, X.C., Belta, C., Rus, D.: Optimality and robustness in multi-robot path planning with temporal logic constraints. Int. J. Robot. Res. 32(8), 889–911 (2013)
Voos, H.: Nonlinear control of a quadrotor micro-uav using feedback-linearization. In: 2009 IEEE International Conference on Mechatronics, pp. 1–6. IEEE (2009)
Wilamowsky, Y., Epstein, S., Dickman, B.: Optimization in multiple-objective linear programming problems with pre-emptive priorities. J. Oper. Res. Soc. 41(4), 351–356 (1990)
Zhou, D., Schwager, M.: Vector field following for quadrotors using differential flatness. In: IEEE International Conference on Robotics and Automation (ICRA), pp. 6567–6572 (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Cardona, G.A., Vasile, CI. (2023). Partial Satisfaction of Signal Temporal Logic Specifications for Coordination of Multi-robot Systems. In: LaValle, S.M., O’Kane, J.M., Otte, M., Sadigh, D., Tokekar, P. (eds) Algorithmic Foundations of Robotics XV. WAFR 2022. Springer Proceedings in Advanced Robotics, vol 25. Springer, Cham. https://doi.org/10.1007/978-3-031-21090-7_14
Download citation
DOI: https://doi.org/10.1007/978-3-031-21090-7_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-21089-1
Online ISBN: 978-3-031-21090-7
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)