On the relation of programs and computations to models of temporal logic

In recent years there has been a proliferation of program verification methods that use temporal logic. These methods differ by the version of temporal logic they are based upon and by the way they use this logic. In this chapter we attempt to give a simple, unified and coherent view of the field. For this, we first characterize the models and model generators of different versions of temporal logic using automata theory. From this characterization, we build a classification of verification and synthesis methods that use temporal logic.