Source-linked AI summary
On-Line Monitoring for Temporal Logic Robustness
Adel Dokhanchi, Bardh Hoxha, Georgios Fainekos
TL;DR
Safety-critical CPS require monitoring beyond Boolean pass/fail because verification can be undecidable and supervisors need quantitative distance from specification violation. This paper develops dynamic-programming online robustness monitoring for MTL with unbounded past and bounded future, implemented as a Matlab/Simulink toolbox. The experiments report minimal simulation overhead for practical specifications, while the method assumes sampled traces and can use finite-horizon predictions.
Problem
Safety-critical CPS need runtime information about how close behaviors are to satisfying or violating requirements, beyond Boolean pass/fail results.
Method
The paper uses dynamic programming to monitor MTL robustness with unbounded past and bounded future over sampled CPS traces, implemented in Matlab/Simulink.
Results
The Simulink toolbox adds minimal overhead to simulation time and supports runtime analysis and offline testing for practical CPS models.
Takeaways & Limitations
Online robustness values can support early warning, runtime analysis, temporal-logic testing, feedback control, and supervision of CPS behavior.
Takeaways & Limitations
The current tool assumes timed state sequences generated under a constant sampling rate and uses finite-horizon predictions when future requirements must be resolved.
Abstract
from arXiv · showhide
In this paper, we provide a Dynamic Programming algorithm for on-line monitoring of the state robustness of Metric Temporal Logic specifications with past time operators. We compute the robustness of MTL with unbounded past and bounded future temporal operators MTL over sampled traces of Cyber-Physical Systems. We implemented our tool in Matlab as a Simulink block that can be used in any Simulink model. We experimentally demonstrate that the overhead of the MTL robustness monitoring is acceptable for certain classes of practical specifications.
1 Introduction
The paper targets runtime monitoring for safety-critical CPS, where verification can be undecidable and Boolean pass/fail results may not show how close a behavior is to violation. It proposes online quantitative MTL robustness monitoring using dynamic programming for specifications with unbounded past and bounded future.
- Motivation: Runtime monitoring analyzes formal requirements during CPS execution and reports violations to a supervisor for remedial action.
- Motivation: A robustness value can distinguish less alarming and more alarming failures that Boolean semantics treat identically.For the UAV example, being 10ft below altitude with one minute remaining may be less alarming than being 100ft below at the same time.
- Motivation: Quantitative robustness indicates both whether an MTL specification is satisfied and how much state-sequence perturbation it can tolerate.Positive robustness denotes satisfaction and tolerance to perturbations up to that value; negative robustness denotes falsification under perturbations of the corresponding magnitude.
- Approach: The approach uses dynamic programming because automata-based monitors cannot synthesize robustness valuations for these specifications.The method assumes finite-horizon predictions can be appended to observed CPS behavior when future operators require them.
- Contributions: The paper provides an online robustness algorithm and Matlab/Simulink toolbox, with bounded memory and negligible runtime overhead for practical applications.The monitor is also positioned for temporal-logic testing and feedback control, extending prior robustness work focused on offline testing.
2 Problem Formulation
The problem formulation monitors MTL safety specifications over sampled CPS traces, combining current observations with a formula-dependent prediction horizon. The proposed monitor stores bounded trace and robustness information, supports feedback or supervision, and has bounded memory with worst-case quadratic time in the horizon/history range.
- Applications: Monitored robustness values can be plotted for a human supervisor, used as CPS feedback, or integrated into Simulink monitoring and code-generation workflows.
- Problem Formulation: The framework operates on timed state sequences containing timestamps and CPS state vectors, under a generalized quasi-metric space assumption.The metric structure supports distances needed for quantitative atomic-proposition valuations.
- Problem Formulation: Robust MTL semantics quantify distance from satisfaction or falsification: positive values indicate satisfaction, while negative values indicate violation.
- Problem Formulation: The monitor receives a current CPS state and finite predictions through a horizon Hrz determined by the future-time requirements of the MTL formula.The prediction horizon is defined as the number of samples needed to resolve all future requirements.
- Online Monitoring: The online algorithm computes current robustness by retaining prior robustness values and only a bounded portion of the execution trace.Its memory is bounded, while worst-case time complexity is quadratic in the magnitude of the horizon/history interval.
3 Robustness of Metric Temporal Logic Specifications
The paper defines robustness for MTL over sampled traces using signed distances and recursive quantitative semantics. Its syntax includes bounded-future Until and unbounded-past Since operators, with timing constraints expressed in sample counts.
- Robust Semantics: Signed distance assigns positive values inside an observation set and negative values outside it, quantifying the trace’s distance from predicate satisfaction.The definition uses infimum distances to the set or its complement.
- Syntax: MTL formulas are built from atomic propositions, negation, disjunction, bounded-future Until, and past-time Since operators.
- Syntax: Temporal operators use sample-index intervals, so a 0.1-second sampling period converts a [0,0.5] second interval into [0,5] samples.
- Syntax: Bounded-future Until requires its left formula to hold until the right formula becomes true within the specified future interval.
- Robust Semantics: The robust valuation is defined recursively over traces using quantitative interpretations of propositions and temporal operators.The semantics use max and min, with extended values for empty-set cases.
4 Robustness Monitoring of MTL<+∞
The monitor combines finite future-horizon and history tables with a stored Pre vector to compute MTL robustness online, including bounded future, bounded past, and unbounded past operators. At each sampling step, it updates subformula entries in direction-specific dynamic-programming order and returns the top-level robustness.
- Finite horizon and history: The robustness table has width Hst + 1 + Hrz, with Hrz equal to the specification's finite horizon and Hst conservatively extended by that horizon plus finite history.The table height is the number of subformulas, and unbounded past operators additionally require the Pre vector.
- Worked example: The worked example uses ϕ = ◇[0,+∞)p ∧ □q, for which Hst = 2 and Hrz = 2, illustrating the combined Pre vector and robustness table.The example's table entries are computed using the online algorithms and a vector containing the current state plus predictions.
- On-Line Monitor: At each step, the monitor appends current and predicted states, stores selected unbounded-past values in Pre, shifts predicate entries, and recomputes the table.The current state occupies column 0, while predicted states occupy columns 1 through Hrz.
- Robustness Computation: The monitor processes subformulas with Algorithm 2, fills entries according to operator type, and returns T1,0 as the robustness of the complete specification.The algorithm handles constants, predicates, negation, propositional disjunction, bounded temporal operators, and unbounded past operators.
- Robustness Computation: Bounded future subformulas are evaluated from right to left over columns through min{j + u, Hrz}, while bounded past subformulas are evaluated from left to right down to j − u′.These directions match the temporal dependence of future and past operators.
- Robustness Computation: Unbounded past subformulas use the previous table entry and the stored Pre value to update robustness recursively without retaining the full history table.Nested future operators still require the history to be extended sufficiently to contain the needed values.
5 Experimental Analysis and Case Studies
Experiments evaluate monitoring overhead on an Automatic Transmission model and apply the method to a high-fidelity engine model. The results show negligible overhead for practical horizon/history sizes and demonstrate that past-time monitoring avoids false falsification when no predictor is available.
- 5.1 Runtime Overhead: For horizon/history windows below 2,000 samples, monitoring overhead per simulation step is negligible in the Automatic Transmission experiments.The experiments generated 30 formulas and evaluated 100 monitoring runs of 100 simulation steps per specification.
- 5.1 Runtime Overhead: The monitoring algorithm has O(n^2) complexity in horizon/history size, while the number of nested temporal operators usually has less impact.The reported overhead becomes quadratic in the window size for some formulas, such as φ1(H).
- 5.2 Case Study: The high-fidelity engine case study uses a 56-state nonlinear model whose monitored output is the normalized air-to-fuel ratio λ.The model includes lookup tables, nonlinear components, switching guards, and a Simulink monitoring block.
- 5.2 Case Study: The engine specification permits temporary λ fluctuations while requiring the ratio to settle within bounds for one second within the preceding two seconds.The past-time and future-time formulations are trace-equivalent, but differ in real-time monitoring when future predictions are unavailable.
- 5.2 Case Study: Without predictor information, the future-time monitor falsely reports falsification around 4 seconds, whereas the past-time monitor does not.The combined past/future specification uses observed past information and may also incorporate predictor information.
- 5.2 Case Study: 0.97% is the reported difference in estimated mean simulation runtime after adding the monitor to the high-fidelity engine model.Table 4 reports runtime statistics for a 35-second simulation with 0.01-second steps.
6 Conclusions and Future Work
The paper concludes that its algorithm monitors robustness for combined past- and future-time MTL specifications and that its Simulink toolbox adds minimal simulation overhead. Future work targets arbitrary sampling, FPGA implementation, and event-based monitoring.
- Conclusions: The Simulink toolbox supports runtime analysis and off-line testing while adding minimal overhead to simulation time.The toolbox is distributed with the S-Taliro tools.
- Future Work: The current tool assumes a constant sampling rate, motivating future work on arbitrary sampling functions.The authors also propose FPGA deployment and event-based monitoring using model information.
Appendix: Proof of Section 4.2
The proof establishes by induction that the CR algorithm returns the correct robustness semantics for predicates and temporal sub-formulas at each simulation step. It covers bounded and unbounded past operators, using stored previous values and unchanged table entries to support dynamic-programming updates.
- Correctness proof: The induction proves that, for each sub-formula and valid offset j, the robustness semantics equal the value returned by CR.The proof handles simulation steps after the history threshold and notes that earlier steps follow immediately from temporal-logic semantics.
- Predicate case: For predicates, CR stores the distance-based robustness in the table, so it computes the correct robustness value at every simulation time.The predicate case identifies robustness with Dist_d(s(i+j), O(p)).
- Incremental table update: The proof also shows that entries from −Hst through −Hst+hst(ϕ_k) depend only on actual simulation values and therefore remain unchanged across later runs.These entries need not be recomputed, as illustrated by the gray cells in Table 5.
- Boolean operators: For Boolean operators, the proof propagates correctness through negation and disjunction using arithmetic negation and the robustness maximum operation.The stored child values T_m,j and T_n,j are combined according to the corresponding operator semantics.
- Bounded Since: For bounded Since, CR combines the right sub-formula over j−u through j−l with the left sub-formula over j−u+1 through j, and the induction verifies both history ranges.The two cases for hst(ϕ_k) ensure that all required table entries correspond to their semantic robustness values.
- Unbounded Since: For unbounded Since, dynamic programming reuses the previous robustness value through Pre when the current offset is the initial required position, while later offsets use the preceding table entry.This recurrence avoids recomputing the entire unbounded past history at each step.