In this talk we consider a natural extension of Linear-time Temporal Logic (LTL) with constraints interpreted over a concrete domain like the integers Z, with the relations < and =. While the model-checking problem for the logic reduces easily to that of LTL, the satisfiability problem is non-trivial even for common domains like (Z,<,=). We use a new automata-theoretic technique to show PSPACE decidability of the satisfiability problem of the logic for the constraint systems (Z,<,=) and (N,<,=). This is joint work with Stephane Demri, LSV ENS-Cachan.