Before revision: In modal logic, the window operator is a modal operator with the following semantic definition: for a model and .
After revision: KripkeIn modal logic, the window operator is a modal operator with the following semantic definition: for a model and .