The extension of temporal logic to measuring time durations is the basis of the theory of timed and hybrid automata, leading to the verification of metric temporal properties. Alur et al. (reference [1] in the paper), and more recently Madnani et al. [2], pointed out that using “punctual” specifications (using singleton intervals) both in future and past modalities leads to undecidability, and they weakened the logic to avoid singleton intervals in one temporal direction.

Reynolds introduces new modal operators with further decorations: precision specifications e = 1/2^m, for nonnegative m. Such a metric modality is to be satisfied in the nearest non-singleton interval, which has multiples of e as its endpoints. This idea has appeared in Gupta et al.’s robust timed automata [3] (reference [19] in the paper), Agrawal and Thiagarajan’s lazy rectangular hybrid automata [4], and Pandya et al.’s sampling model checkers [5], but for the first time as a logic in the author’s work [6] (reference [40] in the paper). By a careful exponential translation of his earlier temporal logic over the real order [7] (reference [38] in the paper), an exponential space decision procedure is obtained.

This logic is incomparable to the earlier metric temporal logic, but it is open whether formulas of these logics can approximate each other to a desired precision. This holds even for formulas with a single modal operator.