2012/08/24 by Paul Hunter, Joël Ouaknine, Hunter, Paul +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1208.4993
openalex publication_date 2012/08/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Metric Temporal Logic (MTL) is a generalisation of Linear Temporal Logic in which the Until and Since modalities are annotated with intervals that express metric constraints. A seminal result of Hirshfeld and Rabinovich shows that over the reals, first-order logic with binary order relation < and unary function +1 is strictly more expressive than MTL with integer constants. Indeed they prove that no temporal logic whose modalities are definable by formulas of bounded quantifier depth can be expressively complete for FO(