Deeper Connections Between LTL and Alternating Automata

Abstract. It is known that Linear Temporal Logic (LTL) has the same expressive power as alternating 1-weak automata (A1W automata, also called alternating linear automata or very weak alternating automata). A translation of LTL formulae into a language equivalent A1W automata has been introduced in [1]. The inverse translation has been developed independently in [2] and [3]. In the first part of the paper we show that the latter translation wastes temporal operators and we propose some improvements of this translation. The second part of the paper draws a direct connection between fragments of the Until-Release hierarchy [4] and alternation depth of nonaccepting and accepting states in A1W automata. We also indicate some corollaries and applications of these results.