A Rocq Prover STL Formalization with Transformations for Mission Planning

Abstract We introduce a formally verified transformation of Signal Temporal Logic (STL) formulas into a simplified form to ease their encoding as constraints in optimal control problems. Nested temporal operators and disjunctions in STL introduce combinatorial complexity for solvers that handle constraints resulting from STL specifications translation. Our four-pass transformation process addresses this issue by lifting operators and reducing formulas to a layered disjunctive normal form, while preserving their satisfiability. The transformations are proven correct in the Rocq Prover, contributing to reliable constraints generation. Our approach simplifies the encoding of STL specifications into optimization problems and identifies a minimal set of expressive formula patterns. This is critical for mission planning in embedded systems, where complex specifications must be efficiently handled. This work also provides a formal STL library and proves the termination, correctness and completeness of the algorithm implementing the transformations. Similar content being viewed by others Data Availability No datasets were generated or analysed during the current study. Notes Note that the literature (e.g. [5]) also provides alternative names for \(\lozenge \) (also called F for “Finally”) and \(\square \) (also known as G for “Globally”). This point should not make significant differences with our formalization. References Bellanger, C., Garoche, P.-L., Martel, M., Picard, C.: Towards proved formal specification and verification of STL operators as synchronous observers. Electron. Proc. Theor. Comput. Sci. 395, 188–204 (2023). https://doi.org/10.4204/eptcs.395.14 Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development. Springer, Berlin (2004) Bourbaki, N.: Theory of Sets. Elements of Mathematics. Springer, Berlin (2004). https://doi.org/10.1007/978-3-642-59309-3 Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, Cambridge (2004). https://doi.org/10.1017/CBO9780511804441 Brim, L., Dluhos, P., Šafránek, D., Vejpustek, T.: STL*: extending signal temporal logic with signal-value freezing operator. Inf. Comput. (2014). https://doi.org/10.1016/j.ic.2014.01.012 Cardona, G.A., Kamale, D., Vasile, C.-I.: STL and wSTL control synthesis: A disjunction-centric mixed-integer linear programming approach. Nonlinear Anal. Hybrid Syst 56, 101576 (2025). https://doi.org/10.1016/j.nahs.2025.101576 Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: Lustre: a declarative language for real-time programming. In: 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 178–188. Association for Computing Machinery, New York (1987). https://doi.org/10.1145/41625.41641 Champion, A., Gurfinkel, A., Kahsai, T., Tinelli, C.: CoCoSpec: A mode-aware contract language for reactive systems. In: Software Engineering and Formal Methods, pp. 347–366. Springer, Berlin (2016). https://doi.org/10.1007/978-3-319-41591-8_24 Chattopadhyay, A., Mamouras, K.: A verified online monitor for metric temporal logic with quantitative semantics. In: Runtime Verification, pp. 383–403. Springer, Berlin (2020). https://doi.org/10.1007/978-3-030-60508-7_21 Collaborative work: NASALib PVS Library. https://github.com/nasa/pvslib Conrad, E., Titolo, L., Giannakopoulou, D., Pressburger, T., Dutle, A.: A compositional proof framework for Fretish requirements. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2022, pp. 68–81. Association for Computing Machinery, New York (2022).https://doi.org/10.1145/3497775.3503685 Coupet-Grimal, S.: An axiomatization of linear temporal logic in the calculus of inductive constructions. J. Log. Comput. 13(6), 801–813 (2003). https://doi.org/10.1093/logcom/13.6.801 Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: International Conference on Formal Modeling and Analysis of Timed Systems. Springer (2010). https://doi.org/10.1007/978-3-642-15297-9_9 Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009). https://doi.org/10.1016/j.tcs.2009.06.021 Giannakopoulou, D., Pressburger, T., Mavridou, A., Rhein, J., Schumann, J., Shi, N.: Formal requirements elicitation with fret. In: REFSQ Workshops, Co-located with the 26th International Conference on Requirements Engineering: Foundation for Software Quality (2020) Giannakopoulou, D., Pressburger, T., Mavridou, A., Schumann, J.: Generation of formal requirements from structured natural language. In: Requirements Engineering: Foundation for Software Quality, pp. 19–35. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-44429-7_2 Gilpin, Y., Kurtz, V., Lin, H.: A smooth robustness measure of signal temporal logic for symbolic control. IEEE Control Syst. Lett. 5, 241–246 (2020). https://doi.org/10.1109/LCSYS.2020.3001875 Johannsen, C., Kempa, B., Jones, P.H., Rozier, K.Y., Wongpiromsarn, T.: Impossible made possible: Encoding intractable specifications via implied domain constraints. In: Formal Methods for Industrial Critical Systems: 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20–22, 2023, Proceedings, pp. 151–169. Springer, Berlin (2023).https://doi.org/10.1007/978-3-031-43681-9_9 Kosaian, K., Wang, Z., Sloan, E., Rozier, K.Y.: Formalizing MLTL formula progression in Isabelle/HOL. In: Intelligent Computer Mathematics CICM 2025. Lecture Notes in Computer Science, vol. 16136, pp. 371–391. Springer, Cham (2026). https://doi.org/10.1007/978-3-032-07021-0_21 Krasowski, H., Palanques-Tost, E., Belta, C., Arcak, M.: Learning biomolecular models using signal temporal logic. In: Proceedings of the 7th Annual Learning for Dynamics & Control Conference. Proceedings of Machine Learning Research, vol. 283, pp. 1365–1377 (2025). https://doi.org/10.48550/arXiv.2412.15227 Kurtz, V., Lin, H.: Mixed-integer programming for signal temporal logic with fewer binary variables. IEEE Control Syst. Lett. (2022). https://doi.org/10.1109/lcsys.2022.3172857 Li, J., Vardi, M., Rozier, K.: Satisfiability checking for mission-time LTL. Inf. Comput. 289, 104923 (2022). https://doi.org/10.1016/j.ic.2022.104923 Liberzon, D.: Calculus of Variations and Optimal Control Theory: A Concise Introduction. Princeton University Press, Princeton (2011) 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, Berlin (2004). https://doi.org/10.1007/978-3-540-30206-3_12 Malyuta, D., Yu, Y., Elango, P., Açikmeşe, B.: Advances in trajectory optimization for space vehicle control. Annu. Rev. Control. 52, 282–315 (2021). https://doi.org/10.1016/j.arcontrol.2021.04.013 Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995). https://doi.org/10.1007/978-1-4612-4222-2 Nivelle, H., Bezem, M., Hendriks, D.: Automated proof construction in type theory using resolution. In: Proceedings of the 17th International Conference on Automated Deduction (CADE-17). Lecture Notes in Artificial Intelligence, vol. 1831, pp. 148–163. Springer, Berlin (2000). https://doi.org/10.1023/A:1021939521172 Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) 11th International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 607, pp. 748–752. Springer, Saratoga (1992). https://doi.org/10.1007/3-540-55602-8_217 Pant, Y.V., Abbas, H., Quaye, R.A., Mangharam, R.: Fly-by-logic: control of multi-drone fleets with temporal logic objectives. In: ACM/IEEE 9th International Conference on Cyber-Physical Systems (ICCPS), pp. 186–197 (2018). https://doi.org/10.1109/ICCPS.2018.00026 Pant, Y.V., Li, M.Z., Rodionova, A., Quaye, R.A., Abbas, H., Ryerson, M.S., Mangharam, R.: Fads: A framework for autonomous drone safety using temporal logic-based trajectory planning. Transportation Research Part C: Emerging Technologies 130, 103275 (2021). https://doi.org/10.1016/j.trc.2021.103275 Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46–57 (1977).https://doi.org/10.1109/SFCS.1977.32 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 (2014).https://doi.org/10.1109/cdc.2014.7039363 Reinbacher, T., Rozier, K., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 357–372. Springer (2014). https://doi.org/10.1007/978-3-642-54862-8_24 Sato, S., An, J., Zhang, Z., Hasuo, I.: Optimization-based model checking and trace synthesis for complex STL specifications. In: Computer Aided Verification. Lecture Notes in Computer Science, pp. 282–306. Springer, Montreal (2024). https://doi.org/10.1007/978-3-031-65633-0_13 Silano, G., Afifi, A., Saska, M., Franchi, A.: A signal temporal logic planner for ergonomic human–robot collaboration. In: International Conference on Unmanned Aircraft Systems (ICUAS), pp. 328–335 (2023).https://doi.org/10.1109/ICUAS57906.2023.10156559 Sun, D., Chen, J., Mitra, S., Fan, C.: Multi-agent motion planning from signal temporal logic specifications. IEEE Robot. Autom. Lett. (RA-L) 7(2), 3451–3458 (2022). https://doi.org/10.1109/lra.2022.3146951 Sun, D., Chen, J., Mitra, S., Fan, C.: Multi-agent motion planning from signal temporal logic specifications. IEEE Robot. Autom. Lett. 7, 1–1 (2022). https://doi.org/10.1109/LRA.2022.3146951 Szmuk, M., Malyuta, D., Reynolds, T.P., Mceowen, M.S., Açikmeşe, B.: Real-time quad-rotor path planning using convex optimization and compound state-triggered constraints. In: IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 7666–7673 (2019). https://doi.org/10.1109/iros40897.2019.8967706 Takayama, Y., Hashimoto, K., Ohtsuka, T.: STLCCP: efficient convex optimization-based framework for signal temporal logic specifications. IEEE Trans. Autom. Control 70(9), 6064–6079 (2025). https://doi.org/10.1109/TAC.2025.3555949 Team, R.: The Rocq Prover. https://rocq-prover.org Uzun, S., Elango, P., Garoche, P.-L., Açikmeşe, B.: Optimization with temporal and logical specifications via generalized mean-based smooth robustness measures. arXiv Preprint (2024). https://doi.org/10.48550/arXiv.2405.10996 Acknowledgements We want to warmly thank Catherine Dubois for the discussions we had about some proofs and some Rocq tips she taught us. This work was partially supported by Agence de l’Innovation de Défense via Centre Interdisciplinaire d’Études pour la Défense et la Sécurité in the project FARO. Funding This work was partially supported by Agence de l’Innovation de Défense via Centre Interdisciplinaire d’Études pour la Défense et la Sécurité in the project FARO. Author information Authors and Affiliations Contributions These authors contributed equally to this work. Corresponding author Ethics declarations Conflict of interest The authors have no relevant financial or non-financial interests to disclose. Additional information Publisher's Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations. Rights and permissions Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law. About this article Cite this article Berrah, D., Pessaux, F. & Chapoutot, A. A Rocq Prover STL Formalization with Transformations for Mission Planning. J Autom Reasoning 70, 16 (2026). https://doi.org/10.1007/s10817-026-09763-y Received: Accepted: Published: Version of record: DOI: https://doi.org/10.1007/s10817-026-09763-y