Runtime verification revisited

In this paper, we address a typical obstacle in runtime verification of linear temporal logic (LTL) formulae: standard models of linear temporal logic are infinite traces, whereas run-time verification has to deal with only finite system behaviours. This problem is usually addressed by defining an LTL semantics for finite traces, which, however, does usually not fit well to the infinite trace semantics. We define a 3-valued semantics (true, false, inconclusive) for LTL on finite traces that resembles the infinite trace semantics in a preferable manner. Furthermore, we describe how to construct, given an LTL formula, a (deterministic) finite state machine with three output symbols. This automaton reads finite traces and yields their 3-valued LTL semantics. Thus, it can directly be deployed for runtime verification. Our concepts are first developed in the setting of LTL and then extended to the timed case for which a linear real-time logic, abbreviated as TLTL, is considered. Consequently, for a TLTL formula a monitor is constructed that operates over finite timed traces. We have implemented the untimed setting and validated our whole approach by examining a real-world case study.