A generalized nexttime operator in temporal logic (Q800722): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Set profile property. |
||
| Property / MaRDI profile type | |||
| Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Revision as of 01:14, 5 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
