Flattening Metric Temporal Logic
Deepak D'Souza, Raj Mohan M. and Pavithra Prabhakar
IISc-CSA-TR-2006-11
(September 2006) Available formats: [ps] [ps.gz]
Filed on September 26, 2006
Updated on October 9, 2006
Title: Flattening Metric Temporal Logic
Authors: Deepak D'Souza, Raj Mohan M., and Pavithra Prabhakar
Abstract:
We show that Metric Temporal Logic (MTL) can be "flattened" in the
sense that for any formula in the logic we can construct a
satisfiability-equivalent formula which has no nested distance
subformulas. This holds for both the pointwise and continuous
semantics and for past operators and modalities. We also show
that the S (``since'') modality can be eliminated using U and some
new propositions. Finally, we show that in the continuous
semantics we can eliminate S_I subformulas using the <>_I ("future
in the interval I") operator, the U modality, and some new
propositions.
Keywords: Metric Temporal Logic, temporal logics, timed systems.
Please bookmark this technical report as http://aditya.csa.iisc.ernet.in/TR/2006/11/.Problems ? Contact techrep@csa.iisc.ernet.in
[Updated at 2009-10-22T06:42Z]