In this chapter we present the automata-based approach for a variety of temporal logics and classes of automata and compare the advantages and the drawbacks of the different constructions. We do not always aim at optimal complexity upper bounds but also take other criteria into account. This is not a chapter on automata theory but rather a chapter on automata for temporal logics. We focus our attention on reductions of decision problems for temporal logics into decision problems on automata instead of in-depth treatment of automata. References are provided, as usual, as bibliographical notes.

As already discussed in Section 1.1.3, the automata-based approach consists of reducing logical problems to automata-based decision problems in order to take advantage of known results and decision procedures from automata theory. The notion of models for logical formulae is substituted by the notion of words or trees accepted by automata (or any other type of structures accepted by automata). The correspondence between formulae and automata, which underlines the difference between a declarative statement (a formula) and an operational device (an automaton), allows to reduce many logical problems, viz.:

1. • satisfiability of a formula φ (i.e. existence of a model for φ) reduces to checking nonemptiness of an automaton Aφ (i.e. existence of a word/tree accepted by Aφ) by using a map between models and, respectively, words or trees;

2. • validity of a formula φ (i.e. truth of φ is all models) reduces to checking universality of an automaton Aφ (i.e. checking whether Aφ accepts all words/trees);

3. • entailment of one formula φ by another formula ψ reduces to checking whether all what is accepted by the automaton Aφ is also accepted by the automaton Aψ (the inclusion problem).

The idea in a nutshell: the automata considered here are not Turing-complete and have restricted computational power and decidable decision problems, so logical decision problems can be reduced to respective automata-based decision problems for which algorithms exist. This is all the magic around this approach to solve logical decision problems: design a reduction and then rely on automata-based decision procedures.Alternatively, this approach can be viewed as a means to solving logical decision problems by using a class of devices with limited computational power, i.e. automata. This is why it helps to better understand their computational power.