A generalized nexttime operator in temporal logic (Q800722): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
| Property / full work available at URL | |||
| Property / full work available at URL: https://doi.org/10.1016/0022-0000(84)90015-1 / rank | |||
Normal rank | |||
| Property / OpenAlex ID | |||
| Property / OpenAlex ID: W2005856245 / rank | |||
Normal rank | |||
Revision as of 20:05, 19 March 2024
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A generalized nexttime operator in temporal logic |
scientific article |
Statements
A generalized nexttime operator in temporal logic (English)
0 references
1984
0 references
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.
0 references
temporal logic
0 references
nexttime operator
0 references
until operator
0 references
alternating bit protocol
0 references
safety properties of programs
0 references
