一句话：扩展 MTL 使其在有界及允许有理常数的无界 timed words 上与 FO[<,+1] 等表达力，并给出迹长无关监控。
已知在 timed words 上，度量时序逻辑（MTL）的表达力严格弱于带序与度量的单子一阶逻辑 FO[<,+1]，即使时间域先验有界亦如此。本文提出 MTL 的一个扩展，使其在有界 timed words（以及时间有界信号）上与 FO[<,+1] 表达力相同；并证明在一般无界情形下，若允许公式使用有理常数 q∈Q，表达完备性仍成立。该扩展因此给出 Kamp 定理的实时对应版本。作为应用，作者给出该扩展的迹长无关（trace-length independent）监控过程，这是稠密实时设置下的首个此类过程。
It is known that Metric Temporal Logic (MTL) is strictly less expressive than the Monadic First-Order Logic of Order and Metric (FO[<, +1]) when interpreted over timed words; this remains true even when the time domain is bounded a priori. In this work, we present an extension of MTL with the same expressive power as FO[<, +1] over bounded timed words (and also, trivially, over time-bounded signals). We then show that expressive completeness also holds in the general (time-unbounded) case if we allow the use of rational constants $q \in \mathbb{Q}$ in formulas. This extended version of MTL therefore yields a definitive real-time analogue of Kamp's theorem. As an application, we propose a trace-length independent monitoring procedure for our extension of MTL, the first such procedure in a dense real-time setting.
@article{paperbot793,
title = {On the Expressiveness and Monitoring of Metric Temporal Logic},
author = {Hsi-Ming Ho and Joël Ouaknine and James Worrell},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 2},
year = {2019},
doi = {10.23638/lmcs-15(2:13)2019}
}