Signal Temporal Logic (STL) is a timed temporal logic formalism that has found widespread adoption for rigorous specification of properties in Cyber-Physical Systems. However, STL is unable to specify oscillatory properties commonly required in engineering design. This limitation can be overcome by the addition of additional operators, for example, signal-value freeze operators, or with first order quantification. Previous work on augmenting STL with such operators has resulted in intractable monitoring algorithms. We present the first efficient and scalable offline monitoring algorithms for STL augmented with independent freeze quantifiers. Our final optimized algorithm has a |ρ|log (|ρ|) dependence on the trace length |ρ| for most traces ρ arising in practice, and a |ρ|2 dependence in the worst case. We also provide experimental validation of our algorithms – we show the algorithms scale to traces having 100k time samples.

Researchers have previously proposed augmenting Signal Temporal Logic (STL) with the value freezing operator in order to express engineering properties that cannot be expressed in STL. This augmented logic is known as STL*. The previous algorithms for STL*monitoring were intractable, and did not scale formulae with nested freeze variables. We present offline discrete-time monitoring algorithms with an acceleration heuristic, both for Boolean monitoring as well as for quantitative robustness monitoring. The acceleration heuristic operates over time intervals where subformulae hold true, rather than over the original trace sample-points. We present experimental validation of our algorithms, the results show that our algorithms can monitor over long traces for formulae with two or three nested freeze variables. Our work is the first work with monitoring algorithm implementations for STL*formulae with nested freeze variables.

Signal temporal logic (STL) is a variant of metric temporal logic (MTL) which can express intricate temporal requirements over signals and has found wide adoption for expressing requirements over complex control systems models. A key factor in the success of STL has been that of quantitative robustness, and the development of efficient algorithms for computing the robustness values over traces. The real-valued quantitative robustness of a signal with respect to an STL property quantifies the degree of satisfaction or violation of the property by the signal. In this work, we introduce a notion of robustness for a more expressive logic, timed STL (TSTL), which can be seen as timed propositional temporal logic (TPTL) with predicates defined over real-valued signals. This logic can express many natural engineering requirements that STL cannot. We also develop algorithms for computing this robustness value over traces in the pointwise semantics. While the robustness computation for general TSTL formulas is PSPACE-hard due to the PSPACE-hardness of the monitoring problem for TPTL, for the special case of one variable TSTL, a fragment of TSTL which is still more expressive than STL, we develop an optimized algorithm which computes robustness in time linear in the length of the trace. Finally, we experimentally validate the tractability of our algorithms with our prototype tool in MATLAB.

The temporal logic Timed Propositional Temporal Logic () extends with freeze quantifiers in order to express timing constraints, and is strictly more expressive than Metric Temporal Logic () over future modalities. The monitoring problem is to check whether a particular timed trace satisfies a given temporal logic specification, and monitoring procedures form core subroutines of testing and falsification approaches for Cyber-Physical Systems. In this work, we develop an efficient linear time monitoring algorithm, linear in the length of the trace (for traces that have at most a constant number of sample points in any unit interval), for one variable in the pointwise semantics. This one variable fragment is known to be already more expressive than and thus allows specifications of richer timed properties. Our algorithm carefully combines a divide and conquer approach with dynamic programming in order to achieve a linear time algorithm. As a plus, our algorithm uses only a simple two-dimensional table, and a syntax tree of the formula, as the data structures, and hence can be easily implemented on various platforms. We demonstrate the tractability of our approach with our prototype tool implementation on Matlab; our experiments show the tool scales easily to long trace lengths.