L. Aceto and F. Laroussinie, “Is your Model Checker on Time? On the Complexity of Model Checking for Timed Modal Logics”, BRICS, vol. 6, no. 32, Dec. 1999.