LTL v.s. Buchi Automata
- Buchi automata are more expressive than LTL
- For every LTL formula, an NBA can be constructed
LTL v.s. Omega-regular Language
- LTL formulae describe omega-regular LT properties, but do not have the same expressiveness as omega-regular languages
- LTL is less expressive than omega-regular expressions
Buchi Automata v.s. Omega-regular Language
- Every omega-regular language is recognized by a nondeterministic Buchi automaton
- NBA is not equivalent to DBA as NBA > DBA
Rabin Automata v.s. Omega-regular Language
- The class of languages accepted by DRAs agrees with the class of omega-regular languages
- DRAs and NBAs are equally expressive
Summary for expressive power
- omega-regular language == NBA == DRA > LTL