Alternating automata and temporal logic normal forms

Annals of Pure and Applied Logic 135 (1-3):263-285 (2005)
  Copy   BIBTEX


We provide a translation from SNFPLTL, a normal form for propositional linear time temporal logic, into alternating automata on infinite words, and vice versa. We show this translation has the property that the set of SNFPLTL clauses is satisfiable if and only if the alternating automaton has an accepting run. As there is no direct method known for checking the non-emptiness of alternating automata, the translation to SNFPLTL, together with a temporal proof on the resulting SNFPLTL clauses, provides an indirect non-emptiness check for alternating automata



    Upload a copy of this work     Papers currently archived: 92,923

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Branching-time logics repeatedly referring to states.Volker Weber - 2009 - Journal of Logic, Language and Information 18 (4):593-624.
Automata for Epistemic Temporal Logic with Synchronous Communication.Swarup Mohalik & R. Ramanujam - 2010 - Journal of Logic, Language and Information 19 (4):451-484.
Normal subgroups of nonstandard symmetric and alternating groups.John Allsup & Richard Kaye - 2007 - Archive for Mathematical Logic 46 (2):107-121.
Formulas in modal logic s4.Katsumi Sasaki - 2010 - Review of Symbolic Logic 3 (4):600-627.
On the non-confluence of cut-elimination.Matthias Baaz & Stefan Hetzl - 2011 - Journal of Symbolic Logic 76 (1):313 - 340.


Added to PP

9 (#1,278,126)

6 months
4 (#859,620)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references