A key issue in the design of a model-checking tool is the choice of
the formal language with which properties are specified. It is now
recognized that a good language should extend linear temporal logic
with the ability to specify all \omega-regular properties. Also,
designers, who are familiar with finite-state machines, prefer
extensions based on automata than these based on fixed points or
propositional quantification. Early extensions of linear temporal
logic with automata use nondeterministic B\"uchi automata. Their
drawback has been inability to refer to the past and the asymmetrical
structure of nondeterministic automata.
In this work we study an extension of linear temporal logic, called
ETL_{2a}, that uses two-way alternating automata as temporal
connectives. Two-way automata can traverse the input word back and
forth and they are exponentially more succinct than one-way
automata. Alternating automata combine existential and universal
branching and they are exponentially more succinct than
nondeterministic automata. The rich structure of two-way alternating
automata makes ETL_{2a} a very powerful and convenient logic. We
show that ETL_{2a} formulas can be translated to nondeterministic
B\"uchi automata with an exponential blow up. It follows that the
satisfiability and model-checking problems for ETL_{2a} are
PSPACE-complete, as are the ones for LTL and its earlier extensions
with automata. So, in spite of the succinctness of two-way and
alternating automata, the advantages of ETL_{2a} are obtained
without a major increase in space complexity. The recent acceptance
of alternating automata by the industry and the development of
symbolic procedures for handling them make us optimistic about the
practicality of ETL_{2a}.