Metric temporal logic revisited (Q266865)

This paper introduces a new kind of metric temporal logic on the real line, called 1CMTL. In this logic, one assumes to have a clock which is used for every time measurement. The logic is an expansion of the metric temporal logic MTL; unfortunately, the latter logic is undecidable on dense orders. Another problem with MTL is that it requires clocks with infinite precision for model checking of formulas. The new logic is a one-clock variant of MTL. While in MTL the temporal Until and Since operators depend only on a time interval, in 1CMTL they depend also on a number which specifies the precision of the clock. An EXPSPACE decision procedure is provided for 1CMTL. The procedure consists of a reduction to the standard since-until temporal logic RTL.