×

The decision problem for linear temporal logic. (English) Zbl 0573.03004

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.

MSC:

03B25 Decidability of theories and sets of sentences
03B45 Modal logic (including the logic of norms)
03E15 Descriptive set theory
03C85 Second- and higher-order model theory
PDFBibTeX XMLCite
Full Text: DOI