The model-checking6 problem is as follows: check whether all legal trajectories of a finite state timed transition model SUD satisfy a specification S. The challenge is to construct a finite reachability graph, even though the time domain is unbounded.
In [105,109], algorithms (and an implemented verifier) are provided for checking a subset of RTTL specifications. The verifier represents processes in a fashion close to the mathematical definition of TTMs. All kinds of data variables are treated including booleans, enumerated or numerical types, lists, sets and sequences. If an RTTL property fails to hold, then the failing trajectories are provided, making it possible to debug the system.
Model-checking suffers from exponential explosion in the size of the state space, when dealing with the parallel composition of processes. Model-checking is suitable for checking small core parts of real-time systems. Reduced models, such as the synchronization skeleton of a mutual exclusion protocol, can also be treated. Large systems will often require different techniques.
For large systems (or infinite data domains) a deductive proof system must be used. A sound first order proof system for RTTL is presented in [104]. The proof system reduces to standard Manna-Pnueli temporal logic if all the upper and lower bounds are zero and infinity respectively.
An advantage of RTTL is that no new temporal operators are introduced. As a result, all the proof rules of Manna-Pnueli temporal logic can be used. In addition, certain rules are added for the real-time part of the reasoning [104,108]. Systems in which there are mixed fairness and time constraints can also be handled.