Technical Reports

The report FIMU-RS-2004-08

Deeper Connections between LTL and Alternating Automata

by Radek Pelánek, Jan Strejèek, September 2004, 26 pages.

FIMU-RS-2004-08. Available as Postscript, PDF.

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 [MSS88]. The inverse translation has been developed independently in [Roh97] and [LT00]. We improve the latter translation and present deeper connections between LTL and A1W automata. Using these translations we identify the classes of A1W automata equivalent to LTL fragments given by bounds on nesting depths of temporal operators (see, e.g., [Wil99,KS02]) and the fragments of Until-Release hierarchy [CP03].