Extended Temporal Logic Revisited
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 w-regular
properties. Also,
familiar with finite-state machines, designers
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 ETL2a, 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 ETL2a a very powerful and convenient logic.
We show that ETL2a formulas can be translated to nondeterministic
B\"uchi automata with an exponential blow up. It follows that the
satisfiability and model-checking problems for ETL2a 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 ETL2a are obtained essentially for
free. 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 ETL2a.
PDF