On the strength of temporal proofs (Q809066): Difference between revisions

The theme in this work is the strengths of various temporal logics. The results are in the style of Abadi, Manna, and Pnueli, often drawing on their work. The system used includes the modalities ``first'', ``next'', ``always'', ``always in the future'', and ``always in the past''. A typical theorem is that the partial correctness assertions provable in some previously proposed systems (e.g. Floyd-Hoare's or Harel's) are exactly those implied (either syntactically with a proof or semantically by being true in all models) by a system currently under consideration. There is also some attention paid to total correctness assertions and arbitrary assertions in the temporal languages. Even though most of the paper is a survey, it is best suited for those with some prior experience with this subject: many notions drawn on from elsewhere are not defined, and the exposition is wanting.