 Early studies of temporal logics for linear time are presented in Rescher and Urquhart (1971) and McArthur (1976). Proofs of completeness of variations of the axiomatic system given above can be found in Gabbay et al. (1980; 1994); Goldblatt (1992); and Finger et al. (2002). All logics mentioned in this section have the finite model property (usually, with respect to non-standard models) and therefore are decidable. For proofs of decidability, see the references on completeness.