[jason_wo]

Linear Temporal Logic looks very interesting to specify invariant of a system and monitor them at runtime. I guess this is called monitoring. So you can check if your system behaves as expected and e.g. issue an alert if it fails.

There is also Metric Temporal Logic, a special case of Temporal Logic. It allows statement like "There must be an account login (event) 5 minutes before an account deletion." There is also the Signal Temporal Logic, a special case of Temporal Logic. It allows statement like "Whenever the temperatue is over 100 degrees it will be lower than 50 degrees within 10 minutes."

Unfortunately, it seems like it allows to formulate invariants that need an unbounded amount of memory if you monitor infinitely long or a huge amount of memory because the implementation essentially computes a window minimum/maximum function over a large window and has to save all the values in this window.

Do you know if there is a restricted subset of temporal logic that can be monitored fast and with a bounded or even small amount (e.g. O(f(lenght of formula)) of memory?