  We present a hierarchical framework for analysing propositional linear-time
temporal logic (PTL) to obtain standard results such as a small model property,
decision procedures and axiomatic completeness. Both finite time and infinite
time are considered and one consequent benefit of the framework is the ability
to systematically reduce infinite-time reasoning to finite-time reasoning. The
treatment of PTL with both the operator Until and past time naturally reduces
to that for PTL without either one. Our method utilises a low-level normal form
for PTL called a "transition configuration". In addition, we employ reasoning
about intervals of time. Besides being hierarchical and interval-based, the
approach differs from other analyses of PTL typically based on sets of formulas
and sequences of such sets. Instead we describe models using time intervals
represented as finite and infinite sequences of states. The analysis relates
larger intervals with smaller ones. Steps involved are expressed in
Propositional Interval Temporal Logic (PITL) which is better suited than PTL
for sequentially combining and decomposing formulas. Consequently, we can
articulate issues in PTL model construction of equal relevance in more
conventional analyses but normally only considered at the metalevel. We also
describe a decision procedure based on Binary Decision Diagrams.
