Source-linked AI summary
Robust Online Monitoring of Signal Temporal Logic
Jyotirmoy V. Deshmukh, Alexandre Donzé, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, Sanjit A. Seshia
TL;DR
Offline monitoring is poorly suited to resource-constrained deployment and long simulations, while robust online monitoring over partial traces has limited prior support. The paper formalizes robust interval semantics, develops efficient algorithms, and finds 10%-20% simulation-time savings in most experiments with overhead below 1%.
Problem
Offline monitoring can require storing entire traces, and limited prior work computes quantitative robust satisfaction online from partial signals.
Method
The paper defines robust interval semantics over partial traces and develops efficient algorithms for bounded- and selected unbounded-horizon STL formulas.
Results
10%-20% simulation-time savings occur in a majority of experiments, with negligible online-monitoring overhead below 1%.
Takeaways & Limitations
Online monitoring benefits outweigh its overhead in the reported automotive and CPS-education case studies.
Takeaways & Limitations
The paper omits the untimed-until case from its presentation, although it notes that the rewriting approach can also handle it.
Abstract
from arXiv · showhide
Signal Temporal Logic (STL) is a formalism used to rigorously specify requirements of cyberphysical systems (CPS), i.e., systems mixing digital or discrete components in interaction with a continuous environment or analog com- ponents. STL is naturally equipped with a quantitative semantics which can be used for various purposes: from assessing the robustness of a specification to guiding searches over the input and parameter space with the goal of falsifying the given property over system behaviors. Algorithms have been proposed and implemented for offline computation of such quantitative semantics, but only few methods exist for an online setting, where one would want to monitor the satisfaction of a formula during simulation. In this paper, we formalize a semantics for robust online monitoring of partial traces, i.e., traces for which there might not be enough data to decide the Boolean satisfaction (and to compute its quantitative counterpart). We propose an efficient algorithm to compute it and demonstrate its usage on two large scale real-world case studies coming from the automotive domain and from CPS education in a Massively Open Online Course (MOOC) setting. We show that savings in computationally expensive simulations far outweigh any overheads incurred by an online approach.
1 Introduction
Online monitoring is needed when storing complete traces or running simulations to completion is impractical. The paper defines robust interval semantics, develops efficient bounded- and unbounded-horizon algorithms, and reports substantial simulation-time savings with negligible overhead.
- Offline monitoring can be impractical because deployed monitors may lack storage for entire traces and simulations may run for hours.
- Online monitoring must estimate satisfaction from partial signals, minimize data storage, and execute fast enough for real-time use.
- Robust satisfaction assigns real values indicating whether a trace satisfies a property, approaches violation, or violates it.
- The paper introduces robust interval semantics that unify weak, strong, and neutral views for STL properties on partial traces.
- The authors provide efficient algorithms for bounded-horizon formulas and bounded-memory methods for commonly used unbounded-horizon formulas.
- 10%-20% simulation-time savings occur in a majority of experiments, while online-monitoring overhead remains below 1%.The evaluation covers industrial-scale automotive Simulink models and a CPS MOOC grading system.
2 Background
The paper models sampled CPS behavior as piecewise-constant signals and uses STL syntax with quantitative robust semantics. Boolean satisfaction is obtained by thresholding robustness at zero.
- A partial signal is a signal defined on a subset of the full time domain.
- Signals are reconstructed from sampled time-value pairs using constant interpolation between consecutive time instants.
- STL formulas combine predicates, negation, conjunction, and bounded temporal operators including always, eventually, and until.
- Quantitative STL semantics recursively evaluate predicates, negation, conjunction, and temporal operators through real-valued operations such as min, infimum, and supremum.
- Boolean satisfaction holds exactly when the robust satisfaction value ρ(ϕ, x, τ) is at least zero.
3 Robust Interval Semantics
The paper defines robust satisfaction intervals for partial signals as bounds over all compatible completions. A recursive construction is proved correct for arbitrary STL formulas.
- The paper monitors finite-horizon signals obtained by piecewise-constant interpolation from incrementally revealed samples.
- A partial signal is treated as a prefix, and its completions are full signals sharing that prefix.
- The robust satisfaction interval contains the infimum and supremum of quantitative satisfaction values across all completions.
- The recursive interval function maps an STL formula, partial signal, and time to an interval-valued robust semantics.
- Lemma 1 proves that the recursive interval function equals the robust satisfaction interval for any STL formula.
4 Online Algorithm
The online algorithm extends offline STL monitoring to compute robust satisfaction intervals on partial traces while avoiding repeated computations and full-trace storage. It maintains worklists over the formula syntax tree, updates them incrementally, and supports bounded-horizon operators, with an example showing early satisfaction determination.
- Algorithm motivation: The algorithm targets online monitoring of STL formulas by avoiding repeated computations and storing the entire signal over the time horizon.It is designed to be memory-efficient while computing robust satisfaction intervals on partial traces.
- Bounded-horizon monitoring: The procedure focuses first on STL formulas whose temporal operators have intervals with finite upper bounds.The syntax tree is maintained in memory with bookkeeping information for online computation.
- Incremental worklists: Each syntax-tree node has a worklist storing RoSIs for relevant times, and new data points trigger incremental updates to affected entries.The algorithm tracks only times within each node’s horizon and propagates changes upward through the syntax tree.
- Incremental execution: The algorithm’s worklists evolve as signal fragments arrive, with newly available values producing updates that propagate to ancestor nodes.The example illustrates this propagation after receiving data at time t3.
- Example outcome: At time t4, the example yields RoSI [−2, −2] for ϕ, establishing non-satisfaction before all data required by the formula’s horizon is available.The negative upper bound shows that no possible suffix can make the formula satisfied.
- Node updates: Boolean nodes combine child worklists using pointwise minima or sign changes, while temporal nodes use sliding maximum or minimum operations over their intervals.The implementation relies on running-window filtering for temporal operators such as ✸I.
5 Monitoring untimed formulas
Untimed temporal operators can require unbounded history, but several formula classes admit online RoSI monitoring with bounded memory. The section derives constant- or O(kϕ)-memory summaries and states the assumptions enabling these reductions.
- 5 Monitoring untimed formulas: Untimed operators normally require tracking values over arbitrarily long intervals, but certain operators and combinations can be monitored with bounded information.A direct application of the bounded-horizon algorithm gives unbounded horizons below untimed operators.
- 5 Monitoring untimed formulas: Theorem 1 establishes constant-memory online RoSI monitoring for five classes, including untimed always, eventually, until, nested operators, and selected combinations.The result assumes ϕ and ψ are atomic predicates of the form f(x) > 0.
- 5 Monitoring untimed formulas: For ✷ϕ, a single interval summary of the minimum prior predicate robustness is updated when the next sample arrives; ✸ϕ has a dual result.The stored summary represents the minimum of the previously available f(x) values.
- 5 Monitoring untimed formulas: For ✷(ϕ∨✸ψ) and its dual, two interval values suffice: one tracks the accumulated minimum and the other updates the outer maximum.The recurrences update Mn and Un using only their previous values and the new sample.
- 5 Monitoring untimed formulas: For ✷✸ϕ and its dual, the interval robustness reduces to the newest predicate robustness, so no historical information must be stored.The reduction follows from the stated interval equivalence and yields the value at time tn+1.
- 5 Monitoring untimed formulas: The generalization permits bounded-horizon subformulae and requires consecutive signal samples to be at least a known finite ∆ apart.These conditions bound the number of relevant discrete time-points in a finite horizon.
- 5.1 Generalizing Theorem 1: Theorem 2 extends the result to specified untimed formula classes using O(kϕ) memory when the largest subformula horizon wϕ is finite.Here kϕ is the largest number of discrete points in any wϕ interval.
- 5.1 Generalizing Theorem 1: The generalized procedure combines a summary for sufficiently old exact values with worklists holding at most kϕ recent RoSI values.This split applies once t0 < ti − wϕ; the recent interval contains at most kϕ time-points.
6 Experimental Results
The experiments evaluate online monitoring in an industrial diesel-engine model and CPSGrader. Online monitoring saves simulation time through early termination while adding negligible monitoring overhead.
- Experimental setup: The evaluation measures simulation-time savings and monitoring overhead, including comparison with naïve recomputation at every step.
- Diesel Engine Model (DEM): The diesel-engine study uses an industrial Simulink airpath model exceeding 3000 blocks, with simulation running about five times slower than real time.Two parameterized safety requirements address overshoot and transient settling behavior.
- Diesel Engine Model (DEM): The DEM requirements cover bounded overshoot and settling-time behavior under multiple parameter valuations.The overshoot requirement uses three valuations, while the transient requirement uses two.
- Diesel Engine Model (DEM): When the online algorithm processes the entire trace for ϕovershoot(ν3), its bookkeeping overhead is about 0.1%.This case prevents early termination and therefore isolates monitoring overhead from simulation savings.
- CPSGrader: In CPSGrader, online monitoring saves up to 24% of simulation time, exceeds 10% in most cases, and has less than 1% overhead.Algorithm 2 consistently incurs 40x to 80x less overhead than naïve online recomputation.