\RequirePackage{amssymb}

\let\eventually\lozenge
\let\always\square
\def\until{\mathop{\mathsf U}}
\let\next\bigcirc

\let\then\Rightarrow
