A generalized nexttime operator in temporal logic (Q800722)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: A generalized nexttime operator in temporal logic |
scientific article; zbMATH DE number 3878350
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A generalized nexttime operator in temporal logic |
scientific article; zbMATH DE number 3878350 |
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
