Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10118860 | Annals of Pure and Applied Logic | 2005 | 23 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Clare Dixon, Alexander Bolotov, Michael Fisher,