No label defined (Q3976046)

[For the entire collection see Zbl 0731.00026.] The provability power of (first-order) temporal logic is a difficult problem in general, but much more tractable when restricted to partial correctness assertions of deterministic programs. Pursuing the suggestion that it would be useful to augment this language with the modality \(\langle P\rangle\) (``sometime-in-the-past''), or, equivalently, its dual \([P]\) (``always-in-the-past''), the author had shown earlier that such an addition does not help with proving deterministic pca's. In contrast, the current theorem shows that it does prove more deterministic invariance properties, a slight generalization of pca's. The author actually shows that adding \(P\) to the system that already has \(F\) (Future) proves more statements in the language with neither. The proof is only sketched, and is not convincing without more detail or the background suggested in the references.