On the Expressiveness of MTL Variants over Dense Time

The basic modal operator bounded until of Metric Temporal Logic (MTL) comes in several variants. In particular it can be strict (when it does not constrain the current instant) or not, and matching (when it requires its two arguments to eventually hold together) or not. This paper compares the relative expressiveness of the resulting MTL variants over dense time. We prove that the expressiveness is not affected by the variations when considering non-Zeno interpretations and arbitrary nesting of temporal operators. On the contrary, the expressiveness changes for flat (i.e., without nesting) formulas, or when Zeno interpretations are allowed.