Deeper Connections between LTL and Alternating Automata
| Authors | |
|---|---|
| Year of publication | 2005 |
| Type | Article in Proceedings |
| Conference | Implementation and Application of Automata |
| MU Faculty or unit | |
| Citation | |
| Field | Informatics |
| Keywords | LTL; alternating automata; model checking |
| Description | 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]. 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 [CP03] and alternation depth of nonaccepting and accepting states in A1W automata. We also indicate some corollaries and applications of these results. |
| Related projects: |