  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.
