A generalized nexttime operator in temporal logic

DOI10.1016/0022-0000(84)90015-1MaRDI QIDQ800722zbMATH OpenOpenAlexFDO

Authors N. E. Zubov

Publication date 1984

Published in Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0022-0000(84)90015-1

zbMATH Keywords

alternating bit protocolnexttime operatorsafety properties of programstemporal logicuntil operator

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Review text

The paper introduces a new binary operator atnext into temporal logic generalizing the usual nexttime operator in a straightforward way. Some dualities with the until operator are proved which also show that the new operator has the same expressive power as until. An axiomatization and several proof rules are given. An example (the alternating bit protocol) shows how the operator can profitably be used to describe and prove safety properties of programs.

Recommendations

• scientific article; zbMATH DE number 3898203
• The temporal logic of branching time
• scientific article; zbMATH DE number 4081516
• scientific article; zbMATH DE number 3889506
• scientific article; zbMATH DE number 4016870

Cites work

• scientific article; zbMATH DE number 3564294 (Why is no real title available?)
• scientific article; zbMATH DE number 3581596 (Why is no real title available?)
• scientific article; zbMATH DE number 3624762 (Why is no real title available?)
• scientific article; zbMATH DE number 3415379 (Why is no real title available?)
• Infinite proof rules for loops
• Proving Liveness Properties of Concurrent Programs
• The temporal semantics of concurrent programs
• Verifying concurrent processes using temporal logic

Cited in

(7)

• ``During cannot be expressed by ``after
• Arithmetical axiomatization of first-order temporal logic
• A complete axiomatic characterization of first-order temporal logic of linear time
• Incompleteness of first-order temporal logic with until
• Time-extraction for temporal logic -- logic programming and local process time
• scientific article; zbMATH DE number 3898203 (Why is no real title available?)
• scientific article; zbMATH DE number 3943779 (Why is no real title available?)

This page was built for publication: A generalized nexttime operator in temporal logic

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