Contributions to LTL and $\omega$-automata for model checking

Abstract