A generalized nexttime operator in temporal logic

DOI10.1016/0022-0000(84)90015-1zbMath0551.68032OpenAlexW2005856245MaRDI QIDQ800722

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)

Related Items (5)

Time-extraction for temporal logic -- logic programming and local process time ⋮ 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 ⋮ Unnamed Item

Cites Work

• Infinite proof rules for loops
• The temporal semantics of concurrent programs
• Verifying concurrent processes using temporal logic
• Proving Liveness Properties of Concurrent Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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