The expressive completeness of Metric Temporal Logic

LTL has emerged as the primary logic for specifying temporal properties. This is largely due to the low complexity of its associated model checking problem and its high expressibility - with the celebrated result of Kamp showing that LTL has the same expressive power as first-order logic. In the quantitative setting, Metric Temporal Logic is quickly becoming the standard to which all other temporal logics are compared. It turns out that the expressive power of MTL is dependent on the set of constants available, and I will give a precise characterization of when MTL has the same expressive power as first-order logic.

Authors

• Paul Hunter

Keywords

No keywords are indexed for this paper.