On the Expressiveness of MTL with Past Operators

Pavithra Prabhakar and Deepak D'Souza

We compare the expressiveness of variants of Metric Temporal Logic (MTL) obtained by adding the past operators `S' and `S_I'. We consider these variants under the ``pointwise'' and ``continuous'' interpretations over both finite and infinite models. Among other results, we show that for each of these variants the continuous version is strictly more expressive than the pointwise version. We also prove a counter-freeness result for MTL which helps to carry over some results from [BCM05] for the case of infinite models to the case of finite models.

Formal Modeling and Analysis of Timed Systems, 4th International Conference (FORMATS), 2006
Download: BIB PS PDF