In this paper we propose a novel technique for constructing timed automata
from properties expressed in the logic MTL, under bounded-variability
assumptions.
We handle full MTL and include all future operators.
Our construction is based on separation of the continuous time monitoring
of the input sequence and discrete predictions regarding the future.
The separation of the continuous from the discrete allows us to
determinize our automata in an exponential construction that does not
increase the number of clocks.
This leads to a doubly exponential construction from MTL to
deterministic timed automata, compared with triply exponential using
existing approaches.
We offer an alternative to the existing approach to linear real-time
model checking, which has never been implemented.
It further offers a unified framework for model checking, runtime
monitoring, and synthesis, in an approach that can reuse tools,
implementations, and insights from the discrete setting.