In this talk we consider the model checking problem for Metric Temporal Logic (MTL)---a version of Linear Temporal Logic with timing constraints, which is interpreted over dense time. We consider the model checking problem for a `safety' fragment of MTL, including invariance and bounded liveness. Our main result is to show EXPSPACE-completeness in case the timing constraints in the logic are encoded in binary, and PSPACE-completeness in case timing constraints are encoded in unary. Our upper and lower complexity bounds involve a connection between MTL formulas and reversal-bounded Turing machines.

Existing decision procedures for MTL or related quantitative monadic logics, due to Alur and Henzinger, and Hirshfeld and Rabinovich, involve restricting the precision of the timing constraints, or restricting the precision of the semantics (e.g., by adopting an integer-time model). The model checking problem in these settings has been shown to be EXPSPACE-complete. We found it surprising that by staying with safety properties one can accommodate dense time and infinitely precise `punctual' specifications, with no complexity penalty.

This is joint work with Patricia Bouyer, Nicolas Markey and Joel Ouaknine.