A modal operator representing possibility or future necessity in mathematical logic and temporal reasoning.
