A proof system, with perhaps some small examples to illustrate the method of proof, is not on its own sufficient to make the proof system practically useful for infinite state systems. Additional guidelines and heuristics must provide insight to the design and verification procedures. Automated support tools (beyond model checking for finite state systems) are needed. Theorem provers must be provided with adequate tacticals (built in heuristics) to support verification.
RTTL has heuristics for doing proofs using proof diagrams and weakest-preconditions [104,108]. A proof diagram is an abstract view of a state reachability graph. It is not confined to finite state systems because a node in the proof diagram is a predicate that can characterize a possibly infinite set of states. The proof diagram contains the intuition of system executions without the distracting proliferation of states. Most of the reasoning takes place in the ordinary predicate calculus, with temporal or real-time reasoning introduced only where absolutely needed.
Constraint logic programming has been used to semi-automate the heuristics. The language CLP(ℜ) was used initially [106], but more recently the constraint logic language PrologIII [107] has been investigated for providing automated support. Methods of synthesizing controllers (for some infinite state systems) to satisfy given plant specifications are provided in [107] (see also the last paragraph of Section 4.2.2).
In [64], it is claimed that explicit clock logics such as RTTL do not ``hide'' time in accordance with the original philosophy of temporal logic (which was to abstract from time as much as possible). Specifications are not as succinct as hidden clock logics. However, most of the reasoning about time in RTTL involves the use of abbreviated formulas (similar to the bounded operators of hidden clock logic). Explicit time is resorted to only in those instances where needed (e.g. to refer to adjacent time contexts or other properties that hidden clock logics cannot specify).
It has also been claimed [56,62] that while the interleaving model of computation may be adequate for qualitative analysis of systems, a more realistic model such as maximal parallelism is needed for real-time systems. This claim is refuted by the interleaving model in the TTM/RTTL framework, in which system actions are interleaved with clock ticks. A careful incorporation of time allows for an adequate representation of most real-time phenomena while preserving the simplicity associated with interleaving models, namely, at any one point in time only one transition can occur and has to be analyzed.
The main disadvantage of the framework is its lack of compositional proof methods, although some of the synthesis methods allow for a modular style of controller development. The question of modular specification and verification methods is an active area of research in the field. Manna-Pnueli temporal logic has recently been provided with a compositional proof system [82]. Since RTTL is based on the untimed Manna-Pnueli system, it appears that their compositional methods should also carry over to RTTL.
The TTM/RTTL framework is a state-based, linear discrete time, interleaved, asynchronous, explicit clock logic formalism. It is state-based because states rather than actions are the primitive components of behaviours. State-based approaches may be more general than action based methods (e.g. process algebras) because state based methods can easily encode actions as well as histories of actions It is difficult to extract the state from action based formalisms.
TTM/RTTL uses a discrete time domain rather than a dense (e.g. the rationals) time domain. If simplicity of use can be preserved, the more general modelling powers of a dense time domain would be preferable. Concurrency is modelled by interleaving rather than a partial order or maximal parallelism. It is asynchronous because a finite number of events can occur between clock ticks. In a synchronous model, all concurrent activity happens in lock-step with the tick of the clock.
Many of the choices made in TTM/RTTL computational model are independent of each other. For example, RTTL can be defined over dense as well as continuous time domains. It can be given a branching time semantics or be based on time intervals. The choice of semantics is, in principle, independent of the syntax of the specification language [61,46]. The reader is referred to [118,46,47] for other explicit clock logics. In particular, [47] compares explicit clock logics with hidden clock logics.