Deeper Connections between LTL and Alternating Automata

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

PELÁNEK Radek STREJČEK Jan

Year of publication 2005
Type Article in Proceedings
Conference Implementation and Application of Automata
MU Faculty or unit

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.