We consider variants of Metric Temporal Logic (MTL) with the past operators S and S_I . We show that these operators can be "eliminated" in the sense that for any formula in these logics containing the S and S_I modalities, we can give a formula over an extended set of propositions which does not contain these past operators, and which is equivalent to the original formula modulo a projection onto the original set of propositions. These results have implications with regard to decidability and closure under projection for some well-known real-time logics in the literature.

Perspectives in Concurrency Theory, 2008

Back