On the expressiveness of MTL in the pointwise and continuous semantics
Deepak D'Souza and Pavithra Prabhakar
IISc-CSA-TR-2005-7
(May 2005) Available formats: [ps] [ps.gz]
Filed on June 2, 2005
Updated on June 20, 2005
The Metric Temporal Logic (MTL) introduced by Koymans has been
interpreted in two ways in the literature: the "pointwise" version
and the "continuous" version. We show that the pointwise version
of the logic is strictly less expressive than the continuous
version. The proof is constructive in the sense that we exhibit a
timed language which is definable in the continuous semantics but
is not definable in the pointwise semantics. This result holds
for the case where we consider finite timed models. The technique
used essentially exploits the fact that the pointwise logic is
decidable while the continuous one is undecidable.
Please bookmark this technical report as http://aditya.csa.iisc.ernet.in/TR/2005/7/.Problems ? Contact techrep@csa.iisc.ernet.in
[Updated at 2009-10-22T06:42Z]