On the Relationship between -automata and Temporal Logic Normal Forms
Alexander Bolotov · Journal of Logic and Computation · 2002
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.