WestminsterResearch

Alternating automata and temporal logic normal forms

Dixon, Clare and Bolotov, Alexander and Fisher, Michael (2005) Alternating automata and temporal logic normal forms. Annals of Pure and Applied Logic, 135 (1-3). pp. 263-285. ISSN 0168-0072

Full text not available from this repository.

Official URL: http://dx.doi.org/10.1016/j.apal.2005.03.002

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.

Item Type:Article
Uncontrolled Keywords:Temporal logic, Alternating automata, specification and verification
Research Community:University of Westminster > Electronics and Computer Science, School of
ID Code:2129
Deposited On:19 Jun 2006
Last Modified:14 Oct 2009 10:20

Repository Staff Only: item control page