Publisher Summary This chapter discusses the links between finite automata and logic. Büchi was the first to set up a logical language equivalent to finite automata. This logical formalism is rather unusual because it makes use of second-order variables. It is remarkable that all the logical theories occurring in this framework are decidable theories. Such behavior is typical of the theory of finite automata in which most of the usual problems are not only decidable but also of low complexity. The only switch occurs in the interpretation of formulas, in contrast to the formalism of automata or rational expressions, in which the finite and the infinite case have to be distinguished. In particular, the chapter introduces monadic second order logic, which is the logical language equivalent to automata. The chapter presents the first-order theory of the linear order, as in contrast to the monadic case, the logic of the linear order and that of the successor are no longer equivalent.