A generalized nexttime operator in temporal logic
作者：
Highlights：
•
摘要
This paper introduces a new binary operator atnext into temporal logic generalizing the usual nexttime operator in a straightforward way. This operator has the same expressive power as the until operator and turns out to be a useful means for naturally describing and proving safety properties of programs.
论文关键词：
论文评审过程：Received 14 March 1983, Revised 9 November 1983, Available online 2 December 2003.
论文官网地址：https://doi.org/10.1016/0022-0000(84)90015-1
