On the strength of temporal proofs

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

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.

Recommendations

Cites work

Cited in

(9)

This page was built for publication: On the strength of temporal proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q809066)