  Runtime monitoring is commonly used to detect the violation of desired
properties in safety critical cyber-physical systems by observing its
executions. Bauer et al. introduced an influential framework for monitoring
Linear Temporal Logic (LTL) properties based on a three-valued semantics: the
formula is already satisfied by the given prefix, it is already violated, or it
is still undetermined, i.e., it can still be satisfied and violated by
appropriate extensions. However, a wide range of formulas are not monitorable
under this approach, meaning that they have a prefix for which satisfaction and
violation will always remain undetermined no matter how it is extended. In
particular, Bauer et al. report that 44% of the formulas they consider in their
experiments fall into this category.
  Recently, a robust semantics for LTL was introduced to capture different
degrees by which a property can be violated. In this paper we introduce a
robust semantics for finite strings and show its potential in monitoring: every
formula considered by Bauer et al. is monitorable under our approach.
Furthermore, we discuss which properties that come naturally in LTL monitoring
- such as the realizability of all truth values - can be transferred to the
robust setting. Lastly, we show that LTL formulas with robust semantics can be
monitored by deterministic automata and report on a prototype implementation.

Formal Languages and Automata Theory;Logic in Computer Science