ON THE EXPRESSIVENESS AND MONITORING OF METRIC TEMPORAL LOGIC
LOGICAL METHODS IN COMPUTER SCIENCE(2019)
摘要
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 is an element of 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.
更多查看译文
关键词
Computer Science,Logic in Computer Science
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络