Ahmed Bouajjani, Rachid Echached, and Joseph Sifakis, "On model checking for real-time properties with durations", Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (LICS), IEEE Press, Los Alamitos, CA, 1993, pp. 147--159.

Specifications for real-time systems include complicated temporal statements, e.g., statements of the type ``whenever a property \$P_0\$ holds, eventually, a property \$P_1\$ will hold before \$t\$ time units expire'' (e.g., ``if there is a disk failure, then the system has to switch to a backup disk in \$\le 5\$ time units''). In the paper under review, a general interval-based language is described for such statements, and it is shown that there exists an algorithm for checking whether a given real-time system satisfies the given specifications.

``Algorithm'' does not necessarily mean ``feasible'', because the problem is NP-hard. However, the authors show that their algorithm works efficiently for several realistic (and reasonably complicated) specifications.