Sampling polynomial trajectories for LTL verification. (English) Zbl 1478.68174
Summary: This paper concerns the verification of continuous-time polynomial spline trajectories against linear temporal logic specifications (LTL without ‘next’). Each atomic proposition is assumed to represent a state space region described by a multivariate polynomial inequality. The proposed approach samples a trajectory strategically, to capture every one of its region transitions. This yields a discrete word called a trace, which is amenable to established formal methods for path checking. The original continuous-time trajectory is shown to satisfy the specification if and only if its trace does. General topological conditions on the sample points are derived that ensure a trace is recorded for arbitrary continuous paths, given arbitrary region descriptions. Using techniques from computer algebra, a trace generation algorithm is developed to satisfy these conditions when the path and region boundaries are defined by polynomials. The proposed PolyTrace algorithm has polynomial complexity in the number of atomic propositions, and is guaranteed to produce a trace of any polynomial path. Its performance is demonstrated via numerical examples and a case study from robotics.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
| 68T40 | Artificial intelligence for robotics |
| 68W30 | Symbolic computation and algebraic computation |
References:
| [1] | Basin, D.; Bhatt, B. N.; Traytel, D., Optimal proofs for linear temporal logic on lasso words, (Lahiri, S. K.; Wang, C., Automated Technology for Verification and Analysis. Automated Technology for Verification and Analysis, Lecture Notes in Computer Science (2018), Springer International Publishing: Springer International Publishing Cham), 37-55 · Zbl 1517.68222 |
| [2] | Baier, C.; Katoen, J.-P., Principles of Model Checking (2008), MIT Press · Zbl 1179.68076 |
| [3] | Markey, N.; Schnoebelen, P., Model checking a path, (Amadio, R.; Lugiez, D., CONCUR 2003 - Concurrency Theory. CONCUR 2003 - Concurrency Theory, Lecture Notes in Computer Science (2003), Springer: Springer Berlin, Heidelberg), 251-265 · Zbl 1274.68197 |
| [4] | Havelund, K.; Roşu, G., Runtime verification - 17 years later, (Colombo, C.; Leucker, M., Runtime Verification. Runtime Verification, Lecture Notes in Computer Science (2018), Springer International Publishing: Springer International Publishing Cham), 3-17 |
| [5] | Bauer, A.; Leucker, M.; Schallhart, C., Runtime verification for LTL and TLTL, ACM Trans. Softw. Eng. Methodol., 20, 14:1-14:64 (Sept. 2011) |
| [6] | Maler, O.; Nickovic, D., Monitoring temporal properties of continuous signals, (Lakhnech, Y.; Yovine, S., Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Lecture Notes in Computer Science (2004), Springer: Springer Berlin, Heidelberg), 152-166 · Zbl 1109.68518 |
| [7] | Koymans, R., Specifying real-time properties with metric temporal logic, Real-Time Syst., 2, 255-299 (Nov. 1990) |
| [8] | Eisner, C.; Fisman, D.; Havlicek, J.; Lustig, Y.; McIsaac, A.; Van Campenhout, D., Reasoning with temporal logic on truncated paths, (Hunt, W. A.; Somenzi, F., Computer Aided Verification. Computer Aided Verification, Lecture Notes in Computer Science (2003), Springer: Springer Berlin, Heidelberg), 27-39 · Zbl 1278.68168 |
| [9] | Fainekos, G. E.; Pappas, G. J., Robustness of temporal logic specifications for continuous-time signals, Theor. Comput. Sci., 410, 4262-4291 (Sept. 2009) · Zbl 1186.68287 |
| [10] | Donzé, A.; Maler, O., Robust satisfaction of temporal logic over real-valued signals, (Chatterjee, K.; Henzinger, T. A., Formal Modeling and Analysis of Timed Systems. Formal Modeling and Analysis of Timed Systems, Lecture Notes in Computer Science (2010), Springer: Springer Berlin, Heidelberg), 92-106 · Zbl 1290.68071 |
| [11] | Kloetzer, M.; Belta, C., A fully automated framework for control of linear systems from temporal logic specifications, IEEE Trans. Autom. Control, 53, 287-297 (Feb. 2008) · Zbl 1367.93202 |
| [12] | Liu, J.; Ozay, N.; Topcu, U.; Murray, R. M., Synthesis of reactive switching protocols from temporal logic specifications, IEEE Trans. Autom. Control, 58, 1771-1785 (July 2013) · Zbl 1369.93307 |
| [13] | Wongpiromsarn, T.; Topcu, U.; Lamperski, A., Automata theory meets barrier certificates: temporal logic verification of nonlinear systems, IEEE Trans. Autom. Control, 61, 3344-3355 (Nov. 2016) · Zbl 1359.68200 |
| [14] | Alur, R.; Feder, T.; Henzinger, T. A., The benefits of relaxing punctuality, J. ACM, 43, 116-146 (Jan. 1996) · Zbl 0882.68021 |
| [15] | Babin, G.; Aït-Ameur, Y.; Nakajima, S.; Pantel, M., Refinement and proof based development of systems characterized by continuous functions, (Li, X.; Liu, Z.; Yi, W., Dependable Software Engineering: Theories, Tools, and Applications. Dependable Software Engineering: Theories, Tools, and Applications, Lecture Notes in Computer Science (2015), Springer International Publishing: Springer International Publishing Cham), 55-70 |
| [16] | Donzé, A.; Ferrère, T.; Maler, O., Efficient robust monitoring for STL, (Sharygina, N.; Veith, H., Computer Aided Verification. Computer Aided Verification, Lecture Notes in Computer Science (2013), Springer: Springer Berlin, Heidelberg), 264-279 |
| [17] | Abbas, H.; Pant, Y. V.; Mangharam, R., Temporal logic robustness for general signal classes, (Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, Montreal, Quebec, Canada (Apr. 2019), ACM), 45-56 · Zbl 1542.93010 |
| [18] | von zur Gathen, J.; Gerhard, J., Modern Computer Algebra (2013), Cambridge University Press: Cambridge University Press New York, United States · Zbl 1277.68002 |
| [19] | Burke, D.; Chapman, A.; Shames, I., Fast spline trajectory planning: minimum snap and beyond (May 2021) |
| [20] | Mercy, T.; Parys, R. V.; Pipeleers, G., Spline-based motion planning for autonomous guided vehicles in a dynamic environment, IEEE Trans. Control Syst. Technol., 26, 2182-2189 (Nov. 2018) |
| [21] | Lau, B.; Sprunk, C.; Burgard, W., Kinodynamic motion planning for mobile robots using splines, (2009 IEEE/RSJ International Conference on Intelligent Robots and Systems (Oct. 2009), IEEE: IEEE St. Louis, MO, USA), 2427-2433 |
| [22] | Shiller, Z.; Gwo, Y., Dynamic motion planning of autonomous vehicles, IEEE Trans. Robot. Autom., 7, 241-249 (Apr. 1991) |
| [23] | Yoon, S.; Lee, D.; Jung, J.; Shim, D. H., Spline-based RRT_⁎ using piecewise continuous collision-checking algorithm for car-like vehicles, J. Intell. Robot. Syst., 90, 537-549 (June 2018) |
| [24] | Wein, R.; Ilushin, O.; Elber, G.; Halperin, D., Continuous path verification in multi-axis NC-machining, (Proceedings of the Twentieth Annual Symposium on Computational Geometry. Proceedings of the Twentieth Annual Symposium on Computational Geometry, SCG ’04 (June 2004), Association for Computing Machinery: Association for Computing Machinery New York, NY, USA), 86-95 · Zbl 1375.68172 |
| [25] | Munkres, J. R., Topology (2000), Prentice Hall, Inc. · Zbl 0951.54001 |
| [26] | Engelking, R., General Topology (1989), Heldermann · Zbl 0684.54001 |
| [27] | Dummit, D. S.; Foote, R. M., Abstract Algebra (2004), Wiley · Zbl 1037.00003 |
| [28] | Mignotte, M., Mathematics for Computer Algebra (1992), Springer: Springer New York · Zbl 0741.11002 |
| [29] | Gianni, P.; Trager, B., Square-free algorithms in positive characteristic, Appl. Algebra Eng. Commun. Comput., 7, 1-14 (Jan. 1996) · Zbl 0874.12009 |
| [30] | Gerhard, J., Modular Algorithms in Symbolic Summation and Symbolic Integration, Lecture Notes in Computer Science (2005), Springer-Verlag: Springer-Verlag Berlin, Heidelberg · Zbl 1131.68121 |
| [31] | Furia, C. A.; Rossi, M., On the expressiveness of MTL variants over dense time, (Raskin, J.-F.; Thiagarajan, P. S., Formal Modeling and Analysis of Timed Systems. Formal Modeling and Analysis of Timed Systems, Lecture Notes in Computer Science (2007), Springer: Springer Berlin, Heidelberg), 163-178 · Zbl 1142.68048 |
| [32] | Wolper, P., Constructing automata from temporal logic formulas: a tutorial⋆, (Brinksma, E.; Hermanns, H.; Katoen, J.-P., Lectures on Formal Methods and Performance Analysis: First EEF/Euro Summer School on Trends in Computer Science. Lectures on Formal Methods and Performance Analysis: First EEF/Euro Summer School on Trends in Computer Science, Bergen Dal, The Netherlands, July 3-7, 2000 Revised Lectures. Lectures on Formal Methods and Performance Analysis: First EEF/Euro Summer School on Trends in Computer Science. Lectures on Formal Methods and Performance Analysis: First EEF/Euro Summer School on Trends in Computer Science, Bergen Dal, The Netherlands, July 3-7, 2000 Revised Lectures, Lecture Notes in Computer Science (2001), Springer: Springer Berlin, Heidelberg), 261-277 · Zbl 0990.68088 |
| [33] | Verscheure, D.; Demeulenaere, B.; Swevers, J.; De Schutter, J.; Diehl, M., Time-optimal path tracking for robots: a convex optimization approach, IEEE Trans. Autom. Control, 54, 2318-2327 (Oct. 2009) · Zbl 1367.90088 |
| [34] | Vardi, M. Y., An automata-theoretic approach to linear temporal logic, (Moller, F.; Birtwistle, G., Logics for Concurrency: Structure Versus Automata. Logics for Concurrency: Structure Versus Automata, Lecture Notes in Computer Science (1996), Springer: Springer Berlin, Heidelberg), 238-266 · Zbl 1543.68236 |
| [35] | Khoussainov, B.; Nerode, A., Automata Theory and Its Applications (2001), Birkhäuser: Birkhäuser Boston, MA · Zbl 1083.68058 |
| [36] | Mehlhorn, K.; Sagraloff, M., A deterministic algorithm for isolating real roots of a real polynomial, J. Symb. Comput., 46, 70-90 (Jan. 2011) · Zbl 1207.65048 |
| [37] | Collins, G. E.; Loos, R., Real zeros of polynomials, (Buchberger, B.; Collins, G. E.; Loos, R., Computer Algebra: Symbolic and Algebraic Computation. Computer Algebra: Symbolic and Algebraic Computation, Computing Supplementum (1982), Springer: Springer Vienna), 83-94 · Zbl 0533.68038 |
| [38] | Krandick, W.; Mehlhorn, K., New bounds for the Descartes method, J. Symb. Comput., 41, 49-66 (Jan. 2006) · Zbl 1158.12001 |
| [39] | Collins, G. E.; Akritas, A. G., Polynomial real root isolation using Descarte’s rule of signs, (Proceedings of the Third ACM Symposium on Symbolic and Algebraic Computation. Proceedings of the Third ACM Symposium on Symbolic and Algebraic Computation, SYMSAC ’76 (Aug. 1976), Association for Computing Machinery: Association for Computing Machinery New York, NY, USA), 272-275 |
| [40] | Eigenwillig, A.; Sharma, V.; Yap, C. K., Almost tight recursion tree bounds for the Descartes method, (Proceedings of the 2006 International Symposium on Symbolic and Algebraic Computation. Proceedings of the 2006 International Symposium on Symbolic and Algebraic Computation, ISSAC ’06 (July 2006), Association for Computing Machinery: Association for Computing Machinery New York, NY, USA), 71-78 · Zbl 1356.65120 |
| [41] | Collins, G. E., Polynomial minimum root separation, J. Symb. Comput., 32, 467-473 (Nov. 2001) · Zbl 1008.12001 |
| [42] | Basu, S.; Pollack, R.; Roy, M.-F., Algorithms in Real Algebraic Geometry. Algorithms and Computation in Mathematics (2006), Springer-Verlag: Springer-Verlag Berlin, Heidelberg · Zbl 1102.14041 |
| [43] | Sendra, J., Brief atlas of offset curves, (Lambán, L.; Romero, A.; Rubio, J., Contribuciones Científicas en Honor de Mirian Andrés Gómez (2010), Universidad de la Rioja), 483-505 · Zbl 1206.14085 |
| [44] | Deshmukh, J. V.; Donzé, A.; Ghosh, S.; Jin, X.; Juniwal, G.; Seshia, S. A., Robust online monitoring of signal temporal logic, Form. Methods Syst. Des., 51, 5-30 (Aug. 2017) · Zbl 1370.68199 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
