The relationship between Büchi automata on infinite words and a specific logical formalism based on a normal form for temporal logic formulae, called SNF/PLTL (separated normal form for propositional linear-time temporal logic) is considered. The known representation of Büchi automata in quantified propositional temporal logic (QPTL) inspired the work of this paper. Two main theorems are proved. Theorem 1. Given a Büchi automaton \(A\), we can construct a characteristic clause set \(\text{SNF}(A)\) such that \(A\) has an accepting run if and only if \(\text{SNF}(A)\) is satisfiable. Theorem 2. Given a set \(C\) of SNF/PLTL clauses, we can construct a Büchi automaton \(A(C)\) such that \(C\) is satisfiable if and only if \(A(C)\) has an accepting run. SNF/PLTL is applied as a specification language to express the property “\(p\) occurs at every even moment of time”, i.e., the \(\text{Even}(p)\) property.