Runtime Verification for LTL and TLTL

2 min read

This paper sets out what a runtime monitor for a temporal logic formula should say about a finite, still growing trace. LTL is defined over infinite executions, so the authors give it a three-valued semantics, LTL3: a prefix is true (every continuation satisfies the formula), false (every continuation violates it) or inconclusive. They build a minimal deterministic finite-state monitor for any LTL formula that reports a verdict as early as possible, then repeat the construction for a timed logic, TLTL, using event-recording and event-predicting clocks.

Findings

  • Runtime verification is a word problem (does this one trace belong to the language?), while model checking is an inclusion problem over all traces. The word problem is far cheaper, and the monitor needs no model of the system.
  • Monitor construction goes through Büchi automata for the formula and its negation and is doubly exponential in the worst case. On 97 usable LTL formulae from Dwyer et al.’s specification patterns, the monitors stayed small (mostly under 100 states and transitions) and were always smaller than the two Büchi automata.
  • Only 54 of those 97 formulae were monitorable. For the rest the monitor is a single inconclusive state: no finite prefix can ever settle them.
  • The monitorable properties strictly contain the safety and co-safety properties, so “monitoring only works for safety” is wrong as a slogan.
  • The timed construction works in principle, but the TLTL monitor had not been implemented when the paper was written.

Limits

  • Assumes the monitor sees a correct trace of events. Sensor noise, dropped messages and a lying component are outside the model.
  • A pure liveness property such as “the robot eventually reaches the dock” without a deadline stays inconclusive forever. A practical monitor has to add a bound, which changes the property.
  • The authors admit the timed case is technically involved and left the implementation to future work.

Relevance

Most LTL monitors used on robots, including ROSMonitoring, rest on this semantics. It builds on Pnueli’s temporal logic and is summarised for a wider audience in A brief account of runtime verification. The “inconclusive forever” verdict is the formal reason a monitor cannot catch a robot that is stuck but safe without a deadline; see runtime monitoring and robust robotics.