  In this paper, we propose a novel one-pass and tree-shaped tableau method for
Timed Propositional Temporal Logic and for a bounded variant of its extension
with past operators. Timed Propositional Temporal Logic (TPTL) is a real-time
temporal logic, with an EXPSPACE-complete satisfiability problem, which has
been successfully applied to the verification of real-time systems. In contrast
to LTL, adding past operators to TPTL makes the satisfiability problem for the
resulting logic (TPTL+P) non-elementary. In this paper, we devise a one-pass
and tree-shaped tableau for both TPTL and bounded TPTL+P (TPTLb+P), a syntactic
restriction introduced to encode timeline-based planning problems, which
recovers the EXPSPACE-complete complexity. The tableau systems for TPTL and
TPTLb+P are presented in a unified way, being very similar to each other,
providing a common skeleton that is then specialised to each logic. In doing
that, we characterise the semantics of TPTLb+P in terms of a purely syntactic
fragment of TPTL+P, giving a translation that embeds the former into the
latter. Soundness and completeness of the system are proved fully. In
particular, we give a greatly simplified model-theoretic completeness proof,
which sidesteps the complex combinatorial argument used by known proofs for the
one-pass and tree-shaped tableau systems for LTL and LTL+P.
