The main goal of this paper is to characterize and compare the proof-theoretic powers of different temporal logics. It continues previous research that has been published during the last decade by the same authors. They reconsider some known results, together with some new ones, in order to obtain a unified treatment of the topic. The authors compare their results with related work by Pnueli, Manna, Abadi, Floyd, and Hoare.
The paper has eight sections. First, an axiomatization of temporal logic is given, followed by some characterizations of program verifying powers. The authors introduce some new program verification methods and show that they are strictly stronger than Pnueli’s temporal logics of programs (Theorems 4.1 and 4.2). The problem of the provability of eventualities is treated in the fifth section. Theorem 6.3 gives a generalization of a characterization of program verifying power to nondeterministic and concurrent programs under the hypothesis of the existence of a weak clock. Section 7 presents results about the completeness types of different semantics, but contains no proofs. In the last section of the paper are solutions to several open problems previously raised in the literature, concerning the characterizations of the proof-theoretic powers of the inference systems T0, R,T1, and T2.
The paper is an interesting and important contribution to the development of nonstandard logics to allow a formal treatment of the provability of various program properties.
