scientific article; zbMATH DE number 17797

DOI10.1007/3-540-51486-4_61MaRDI QIDQ3975138zbMATH OpenFDO

Authors István Németi, Ildikó Sain, Hajnal Andréka

Publication date 26 June 1992

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-51486-4_61

zbMATH Keywords

program verificationreasoning powerstemporal logicstime-oriented nonstandard logics of programs

Mathematics Subject Classification ID

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

Review text

[For the entire collection see Zbl 0726.00018.] In the framework of time-oriented nonstandard logics of programs, the authors characterize the reasoning powers of various established temporal logics used in computer science such as the Floyd-Hoare method, Intermittent Assertions method, Pnueli's temporal method and the inference system of dynamic logic. Then, based on an axiomatization of temporal logic with the five modalities First, Next, Always, ``Always-in- the-future, and ``Always-in-the-past, they are compared in connection with several properties on both deterministic and nondeterministic programs. The provability of temporal formulas in general is also discussed, that is, several completeness and incompleteness results on the logics axiomatized in that way are given.

Recommendations

• On the strength of temporal proofs
• scientific article; zbMATH DE number 1786650
• scientific article; zbMATH DE number 4153903
• scientific article; zbMATH DE number 830431
• scientific article; zbMATH DE number 19762

Cited in

(14)

• ``During cannot be expressed by ``after
• A Hoare-like proof system for analysing the computation time of programs
• The logic of ``initially and ``next: complete axiomatization and complexity
• scientific article; zbMATH DE number 3846835 (Why is no real title available?)
• VARIABLE TRUTH
• scientific article; zbMATH DE number 3858393 (Why is no real title available?)
• scientific article; zbMATH DE number 4139719 (Why is no real title available?)
• scientific article; zbMATH DE number 4153903 (Why is no real title available?)
• scientific article; zbMATH DE number 18642 (Why is no real title available?)
• scientific article; zbMATH DE number 19762 (Why is no real title available?)
• scientific article; zbMATH DE number 1786650 (Why is no real title available?)
• Similarity saturation for first order linear temporal logic with UNLESS
• Does “N+1 times” prove more programs correct than “N times”?
• On the strength of temporal proofs

This page was built for publication:

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