We consider the relationship between ω-automata and a specific logical formulation based on a normal form for temporal logic formulae. While this normal form was developed for use with execution and clausal resolution in temporal logics, we here show how it can represent , syntactically, ω-automata in a high-level way. Technical proofs of the correctness of this representation are given.
展开▼
