  A Metric Interval Temporal Logic (MITL) verification algorithm is presented.
It verifies continuous-time signals without relying on high frequency sampling.
Instead, it is assumed that collections of over- and under-approximating
intervals are available for the times at which the individual atomic
propositions hold true for a given signal. These are combined inductively to
generate corresponding over- and under-approximations for the specified MITL
formula. The gap between the over- and under-approximations reflects timing
uncertainty with respect to the signal being verified, thereby providing a
quantitative measure of the conservativeness of the algorithm. The verification
is exact when the over-approximations for the atomic propositions coincide with
the under-approximations. Numerical examples are provided to illustrate.
