Monitoring Dense-Time, Continuous-Semantics, Metric Temporal Logic

The continuous semantics and dense time model most closely model the intuitive meaning of properties specified in metric temporal logic (mtl). To date, monitoring algorithms for mtl with dense time and continuous semantics lacked the simplicity the standard algorithms for discrete time and pointwise semantics. In this paper, we present a novel, transition-based, representation of dense-time boolean signals that lends itself to the construction of efficient monitors for safety properties defined in metric temporal logic with continuous semantics. Using this representation, we present a simple lookup-table-based algorithm for monitoring formulas consisting of arbitrarily nested mtl operators. We examine computational and space complexity of this monitoring algorithm for the past-only, restricted-future, and unrestricted-future temporal operators.