Model predictive monitoring of dynamical systems for signal temporal logic specifications. (English) Zbl 1534.93289
Summary: Online monitoring aims to evaluate or to predict, at runtime, whether or not the behaviors of a system satisfy some desired specification. It plays a key role in safety-critical cyber-physical systems. In this work, we propose a new monitoring approach, called model predictive monitoring, for specifications described by signal temporal logic (STL) formulae. Specifically, we assume that the observed state traces are generated by an underlying dynamical system whose model is known but the control law is unknown. The main idea is to use the dynamic of the system to predict future states when evaluating the satisfaction of the STL formulae. To this end, effective approaches for the computation of feasible sets of STL formulae are provided. We show that, by explicitly utilizing the model information of the dynamical system, the proposed online monitoring algorithm can falsify or certify of the specification in advance compared with existing algorithms, where no model information is used. We also demonstrate the proposed monitoring algorithm by several real world case studies.
MSC:
| 93C55 | Discrete-time control/observation systems |
| 94A12 | Signal theory (characterization, reconstruction, filtering, etc.) |
| 03B44 | Temporal logic |
References:
| [1] | Abate, M., Feron, E., & Coogan, S. (2019). Monitor-based runtime assurance for temporal logic specifications. In IEEE conference on decision and control |
| [2] | Abbas, H.; Bonakdarpour, B., Leveraging system dynamics in runtime verification of cyber-physical systems, 264-278 |
| [3] | Bae, K.; Lee, J., Bounded model checking of signal temporal logic properties using syntactic separation. Proceedings of the ACM on Programming Languages, POPL, 1-30 (2019) |
| [4] | Bartocci, E.; Deshmukh, J.; Donzé, A.; Fainekos, G.; Maler, O.; Ničković, D., Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications, 135-175 |
| [5] | Bauer, A.; Leucker, M.; Schallhart, C., Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology, 4, 1-64 (2011) |
| [6] | Benet, L.; Forets, M.; Sanders, D.; Schilling, C., TaylorModels. jl: Taylor models in julia and their application to validated solutions of ODEs |
| [7] | Bezanson, J.; Edelman, A.; Karpinski, S.; Shah, V., Julia: A fresh approach to numerical computing. SIAM Review, 1, 65-98 (2017) · Zbl 1356.68030 |
| [8] | Blanchini, F., Ultimate boundedness control for uncertain discrete-time systems via set-induced Lyapunov functions. IEEE Transactions on Automatic Control, 2, 428-433 (1994) · Zbl 0800.93754 |
| [9] | Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., & Schilling, C. (2019). JuliaReach: a toolbox for set-based reachability. In ACM international conference on hybrid systems: computation and control · Zbl 1542.93019 |
| [10] | Bonnah, E.; Hoque, K., Runtime monitoring of time window temporal logic. IEEE Robotics and Automation Letters, 3, 5888-5895 (2022) |
| [11] | Bravo, J.; Limón, D.; Alamo, T.; Camacho, E., On the computation of invariant sets for constrained nonlinear systems: An interval arithmetic approach. Automatica, 9, 1583-1589 (2005) · Zbl 1086.93035 |
| [12] | Buyukkocak, A.; Aksaray, D.; Yazıcıoğlu, Y., Control barrier functions with actuation constraints under signal temporal logic specifications, 162-168 |
| [13] | Chan, N.; Mitra, S., Verifying safety of an autonomous spacecraft rendezvous mission. EPiC Series in Computing, 20-32 (2017) |
| [14] | Deshmukh, J.; Donzé, A.; Ghosh, S.; Jin, X.; Juniwal, G.; Seshia, S., Robust online monitoring of signal temporal logic. Formal Methods in System Design, 1, 5-30 (2017) · Zbl 1370.68199 |
| [15] | Devonport, A.; Arcak, M., Data-driven reachable set computation using adaptive Gaussian process classification and Monte Carlo methods, 2629-2634 |
| [16] | Dokhanchi, A.; Hoxha, B.; Fainekos, G., On-line monitoring for temporal logic robustness, 231-246 |
| [17] | Donzé, A.; Ferrere, T.; Maler, O., Efficient robust monitoring for STL, 264-279 |
| [18] | Donzé, A.; Maler, O., Robust satisfaction of temporal logic over real-valued signals, 92-106 · Zbl 1290.68071 |
| [19] | Eisner, C.; Fisman, D.; Havlicek, J.; Lustig, Y.; McIsaac, A.; Campenhout, D., Reasoning with temporal logic on truncated paths, 27-39 · Zbl 1278.68168 |
| [20] | Evtushenko, Y.; Posypkin, M.; Rybak, L.; Turkin, A., Approximating a solution set of nonlinear inequalities. Journal of Global Optimization, 129-145 (2018) · Zbl 1402.90177 |
| [21] | Fainekos, G.; Pappas, G., Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science, 42, 4262-4291 (2009) · Zbl 1186.68287 |
| [22] | Ferrando, A.; Cardoso, R.; Farrell, M.; Luckcuck, M.; Papacchini, F.; Fisher, M., Bridging the gap between single-and multi-model predictive runtime verification. Formal Methods in System Design, 1-33 (2022) |
| [23] | Forets, M.; Schilling, C., LazySets.jl: Scalable Symbolic-Numeric Set Computations. Proceedings of the JuliaCon Conferences, 1, 11 (2021) |
| [24] | Ghosh, B.; André, É., Offline and online monitoring of scattered uncertain logs using uncertain linear dynamical systems. International Conference on Formal Techniques for Distributed Objects, Components, and Systems, 67-87 (2022), Springer · Zbl 1499.68036 |
| [25] | Gilpin, Y.; Kurtz, V.; Lin, H., A smooth robustness measure of signal temporal logic for symbolic control. IEEE Control Systems Letters, 1, 241-246 (2020) |
| [26] | Hashimoto, W.; Hashimoto, K.; Takai, S., STL2vec: Signal temporal logic embeddings for control synthesis with recurrent neural networks. IEEE Robotics and Automation Letters (2022) |
| [27] | Ho, H., Ouaknine, J., & Worrell, J. (2014). Online monitoring of metric temporal logic. In International conference on runtime verification |
| [28] | Jagtap, P.; Soudjani, S.; Zamani, M., Formal synthesis of stochastic systems via control barrier certificates. IEEE Transactions on Automatic Control, 7, 3097-3110 (2020) · Zbl 1467.93293 |
| [29] | Jakšić, S.; Bartocci, E.; Grosu, R.; Nguyen, T.; Ničković, D., Quantitative monitoring of STL with edit distance. Formal Methods in System Design, 1, 83-112 (2018) · Zbl 1394.68230 |
| [30] | Kerrigan, E., Robust constraint satisfaction: Invariant sets and predictive control (2001), University of Cambridge, (Ph.D. thesis) |
| [31] | Lee, J.; Yu, G.; Bae, K., Efficient SMT-based model checking for signal temporal logic, 343-354 |
| [32] | Leucker, M., Sliding between model checking and runtime verification, 82-87 |
| [33] | Lindemann, L.; Dimarogonas, D., Robust motion planning employing signal temporal logic, 2950-2955 |
| [34] | Lindemann, L.; Dimarogonas, D., Control barrier functions for signal temporal logic tasks. IEEE Control Systems Letters, 1, 96-101 (2018) |
| [35] | Lindemann, L.; Dimarogonas, D., Robust control for signal temporal logic specifications using discrete average space robustness. Automatica, 377-387 (2019) · Zbl 1415.93092 |
| [36] | Lindemann, L., Qin, X., Deshmukh, J., & Pappas, G. (2023). Conformal prediction for STL runtime verification. In ACM/IEEE International Conference on Cyber-Physical Systems |
| [37] | Ma, M.; Bartocci, E.; Lifland, E.; Stankovic, J.; Feng, L., A novel spatial-temporal specification-based monitoring system for smart cities. IEEE Internet of Things Journal, 15, 11793-11806 (2021) |
| [38] | Ma, M.; Stankovic, J.; Bartocci, E.; Feng, L., Predictive monitoring with logic-calibrated uncertainty for cyber-physical systems. ACM Transactions on Embedded Computing Systems, 5s, 1-25 (2021) |
| [39] | Maler, O.; Nickovic, D., Monitoring temporal properties of continuous signals, 152-166 · Zbl 1109.68518 |
| [40] | Mascle, C., Neider, D., Schwenger, M., Tabuada, P., Weinert, A., & Zimmermann, M. (2020). From LTL to rLTL monitoring: Improved monitorability through robust semantics. In International conference on hybrid systems: computation and control · Zbl 07300848 |
| [41] | Mayne, D., Control of constrained dynamic systems. European Journal of Control, 2-3, 87-99 (2001) · Zbl 1293.93299 |
| [42] | Mitchell, I.; Tomlin, C., Overapproximating reachable sets by Hamilton-Jacobi projections. Journal of Scientific Computing, 323-346 (2003) · Zbl 1045.93008 |
| [43] | Momtaz, A.; Basnet, N.; Abbas, H.; Bonakdarpour, B., Predicate monitoring in distributed cyber-physical systems, 3-22 |
| [44] | Pinisetty, S.; Jéron, T.; Tripakis, S.; Falcone, Y.; Marchand, H.; Preoteasa, V., Predictive runtime verification of timed properties. Journal of Systems and Software, 353-365 (2017) |
| [45] | Qin, X.; Deshmukh, J., Clairvoyant monitoring for signal temporal logic, 178-195 · Zbl 07317097 |
| [46] | Raman, V., Donzé, A., Maasoumy, M., Murray, R., Sangiovanni-Vincentelli, A., & Seshia, S. (2014). Model predictive control with signal temporal logic specifications. In IEEE conference on decision and control |
| [47] | Roehm, H.; Oehlerking, J.; Heinz, T.; Althoff, M., STL model checking of continuous and hybrid systems, 412-427 · Zbl 1398.68347 |
| [48] | Sahin, Y.; Quirynen, R.; Di Cairano, S., Autonomous vehicle decision-making and monitoring based on signal temporal logic and mixed-integer programming, 454-459 |
| [49] | Salamati, A.; Soudjani, S.; Zamani, M., Data-driven verification of stochastic linear systems with signal temporal logic constraints. Automatica (2021) · Zbl 1478.93672 |
| [50] | Stipanović, D.; Hwang, I.; Tomlin, C., Computation of an over-approximation of the backward reachable set using subsystem level set functions, 300-305 |
| [51] | Thati, P.; Roşu, G., Monitoring algorithms for metric temporal logic specifications. Electronic Notes in Theoretical Computer Science, 145-162 (2005) |
| [52] | Waga, M.; André, É.; Hasuo, I., Model-bounded monitoring of hybrid systems, 21-32 |
| [53] | Yoon, H.; Sankaranarayanan, S., Predictive runtime monitoring for mobile robots using logic-based Bayesian intent inference, 8565-8571 |
| [54] | Yu, X.; Dong, W.; Yin, X.; Li, S., Online monitoring of dynamic systems for signal temporal logic specifications with model information, 1553-1559 |
| [55] | Yu, G.; Lee, J.; Bae, K., STLmc: Robust STL model checking of hybrid systems using SMT, 524-537 |
| [56] | Yu, X.; Su, R., Decentralized circular formation control of nonholonomic mobile robots under a directed sensor graph. IEEE Transactions on Automatic Control, 6, 3656-3663 (2023) · Zbl 07744851 |
| [57] | Zhang, X.; Leucker, M.; Dong, W., Runtime verification with predictive semantics, 418-432 |
| [58] | Zhao, D.; Zhou, Z.; Cai, Z.; Yangui, S.; Xue, X., ASTL: Accumulative STL with a novel robustness metric for IoT service monitoring. IEEE Transactions on Mobile Computing (2022) |
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.
