On the strength of temporal proofs
type: Item
instance of: scholarly article
title: On the strength of temporal proofs
zbMATH Open document ID: 0732.03020
DOI: 10.1016/0304-3975(91)90386-G
author: Hajnal Andréka
author: István Németi
author: Ildikó Sain
published in: Theoretical Computer Science
publication date: 1991-01-01T00:00:00Z
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.
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B45
zbMATH DE Number: 4210114
zbMATH Keywords: temporal logics
zbMATH Keywords: correctness assertions
reviewed by: Robert S. Lubarsky
MaRDI profile type: Publication
cites work: The power of temporal proofs
cites work: Q4193440
cites work: Q3208642
cites work: A complete logic for reasoning about programs via nonstandard model theory. II
cites work: Q3975138
cites work: Programs and program verifications in a general setting
cites work: A completeness theorem for dynamic logic
cites work: A PROPERTY OF 2‐SORTED PEANO MODELS AND PROGRAM VERIFICATION
cites work: Handbook of philosophical logic. Vol. 9
cites work: Q3898023
cites work: Q3773852
cites work: Q4726228
cites work: First-order dynamic logic
cites work: Cylindric algebras. Part II
cites work: To the memory of Arthur Prior Formal properties of ‘now’
cites work: On the termination of program schemas
cites work: Q3711745
cites work: Weak second order characterizations of various program verification systems
cites work: Q4190096
cites work: Q4745241
cites work: Q4733399
cites work: Q3956390
cites work: Non-standard algorithmic and dynamic logic
cites work: Recursive programs and denotational semantics in absolute logics of programs
cites work: Q4268476
cites work: Q3744163
cites work: Q3896482
cites work: Q3325017
cites work: STRUCTURED NONSTANDARD DYNAMIC LOGIC
cites work: A simple proof for the completeness of Floyd's method
cites work: Q3698302
cites work: Total correctness in nonstandard logics of programs
cites work: An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic
cites work: Temporal logics need their clocks
cites work: Q3472083
cites work: Q4198727
cites work: Determinateness of program equivalence over peano axioms
cites work: Q3979260
full work available at URL: 0304-3975(91)90386-g
OpenAlex ID: W1571059814
description: scientific article; zbMATH DE number 4210114