×

Efficient temporal satisfiability. (English) Zbl 0767.03013

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.

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
PDFBibTeX XMLCite
Full Text: DOI