A generalized nexttime operator in temporal logic
type: Item
instance of: scholarly article
title: A generalized nexttime operator in temporal logic
zbMATH Open document ID: 0551.68032
DOI: 10.1016/0022-0000(84)90015-1
author: N. E. Zubov
published in: Journal of Computer and System Sciences
publication date: 1984-01-01T00:00:00Z
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.
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B45
zbMATH DE Number: 3878350
zbMATH Keywords: temporal logic
zbMATH Keywords: nexttime operator
zbMATH Keywords: until operator
zbMATH Keywords: alternating bit protocol
zbMATH Keywords: safety properties of programs
MaRDI profile type: Publication
full work available at URL: 0022-0000(84)90015-1
OpenAlex ID: W2005856245
cites work: Verifying concurrent processes using temporal logic
cites work: Q4136521
cites work: Q4151145
cites work: Infinite proof rules for loops
cites work: Q5679697
cites work: Proving Liveness Properties of Concurrent Programs
cites work: Q4187287
cites work: The temporal semantics of concurrent programs
description: scientific article; zbMATH DE number 3878350