Temporal logic TPTL for the specification of real-time systems is introduced. TPTL extends PTL 
to discrete time with *freeze quantifiers* that bind a variable to the local temporal context.
For example, 
	Gx.(p -> Fy.(q and y <= x + 10)
means at any time x, if p is true then there exists an instant y >= x such that q is true and y <= x+ 10.
In TPTL terms are ::= x + c | c      (i.e. no sum of variables, no multiplication. Constants are integers)
Formulae contain <=, >=, =_d (modulo), boolean combinations, next and until operators. 

The model assumes that time is measured with a discrete clock, that is a clock that only outputs the
discrete part of the current time. Dense time (Q) is also considered only with negative results.

Results
-----------------------
1) In discrete time, they give a tableau based procedure to decide satisfiability of a given TPTL formula in EXPSPACE.
2) They show that the validity problem for TPTL is EXPSPACE-complete.
3) Since MC TPTL is harder (considering a structure accepting any run), MC is also EXSPACE-complete.
4) See Undecidability

Technics
-----------------------
Satisfiability here means the existence of a timed run (called timed state sequence) that is both "monotonous" and that
"progresses" verifying the formula. For a formula \phi, the tableau based procedure creates an automaton whose states 
are the maximal consistent subsets of subformulas of \phi (similar to LTL MC algorithm). This automaton is finite since
they show that there exists an accepting run iff there exists a bounded run, and they give an upper bound (k = the
product of all constants appearing in \phi). The construction is singly exponential in the size of \phi, and doubly
exponential in k.

Undecidability
----------------------
Relaxing monotonicity, allowing multiplication by 2, interpreting formulas over Q (instead of N) renders the
satisfiability \Sigma_1^1-complete.