The decision problem for linear temporal logic (Q1062669)

The main result of this paper is the decidability of the set of universal monadic second-order sentences true in the structure consisting of the real numbers equipped with the usual order relation. Two proofs are given, the first exploiting a theorem of Rabin, and the second a method of Läuchli and Leonard. There are two corollaries to the proofs: First, for every false univesal monadic second-order sentence about the real order, there exist Borel sets of reals constituting a counterexample. Second, exactly the same universal monadic second-order sentences that are true for the real order are true for any other order that is dense, complete, without endpoints, and satisfies one further universal monadic second-order condition. (Examples are such orders as the ''long-line'' and ''Suslin lines''.) Results about universal monadic second-order logic are closely connected with results about ''temporal logic'': This connection is exploited in one of the proofs.