On the expressiveness of MTL with past operators
Pavithra Prabhakar and Deepak D'Souza

IISc-CSA-TR-2006-5
(May 2006)

Available formats: [pdf]

Filed on May 8, 2006
Updated on May 12, 2006


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.


Please bookmark this technical report as http://aditya.csa.iisc.ernet.in/TR/2006/5/.

Problems ? Contact techrep@csa.iisc.ernet.in
[Updated at 2009-10-22T06:42Z]