 Other methods that have proven practically fruitful for deciding satisfiability as well as for model checking of temporal logics in computer science are the automata-based methods, which have been actively developing since the early 1990s. These methods transform temporal formulae into automata on infinite words (for linear time logics) or infinite trees (for branching time logics) and represent models for the logics as input objects (infinite words or trees) for their associated automata. Thus, satisfiability of a formula becomes equivalent to the language of the associated automaton being non-empty. The methods are based on classical results about decidability of the monadic second-order theories of the natural numbers (by Büchi) and of the infinite binary tree (by Rabin). For instance, in Emerson and Sistla (1984), automata on infinite trees and Rabin’s theorem were used to obtain a decision procedure for CTL*. For further details see Vardi (2006).