A generalized nexttime operator in temporal logic (Q800722)

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.