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

temporal logicalternating bit protocolnexttime operatorsafety properties of programsuntil 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)

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
• Publication:3028984

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)

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