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

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. 
<P>
``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. 
<P>