Emerson, E. Allen; Sadler, Tom; Srinivasan, Jai Efficient temporal satisfiability. (English) Zbl 0767.03013 J. Log. Comput. 2, No. 2, 173-210 (1992). The complexity of testing satisfiability of almost all extant propositional logics of programs is \(NP\)-hard, because these logics subsume ordinary propositional logic. If the conjecture \(P\neq NP\) is true, it seems likely that the best deterministic decision procedure we could hope for is of exponential time complexity. This interesting paper gives a temporal logic of polynomial time complexity, whose formulae are allowed to be built up essentially from Horn propositional logic, interacting with each other so as to limit the depth of nesting of the basic temporal operators \(F\) (sometime), \(G\) (always), \(X\) (next time), and \(U\) (until). The success of this approach hinges on the ability to separate the propositional reasoning from that of temporal reasoning. The authors apply their brand-new logic to program synthesis, arguing that even a compositional fragment of the logic is rich enough in practice. Reviewer: Hirokazu Nishimura (Ibaraki) Cited in 2 Documents MSC: 03B70 Logic in computer science 03B45 Modal logic (including the logic of norms) 68Q25 Analysis of algorithms and problem complexity 03B25 Decidability of theories and sets of sentences Keywords:\(P=NP\); complexity of testing satisfiability; exponential time complexity; temporal logic; polynomial time complexity; Horn propositional logic; program synthesis PDFBibTeX XMLCite \textit{E. A. Emerson} et al., J. Log. Comput. 2, No. 2, 173--210 (1992; Zbl 0767.03013) Full Text: DOI