Writing Linear Temporal Logic in LaTeX
Here are some useful symbols
\documentclass{article}
\usepackage{amsmath,amssymb}
\pagestyle{empty}
\begin{document}
\renewcommand{\arraystretch}{2}
\begin{tabular}[t]{rl|rl}%
\verb=\lnot= & $ \lnot $ & \\
\verb=\square= & $\square$ & \verb=\lozenge= & $\lozenge$ \\
\verb=\vee= & $\vee $ & \verb=\wedge= & $\wedge$ \\
\verb=\vdash= & $\vdash$ & \verb=\models= & $\models$ \\
\end{tabular}
\end{document}
Applying DRY to A.Ellet's answer.
\documentclass[preview]{standalone}
\usepackage{amsmath,amssymb}
\renewcommand{\arraystretch}{2}
\def\x#1{\texttt{\expandafter\string\csname#1\endcsname}&\expandafter$\csname#1\endcsname$}
\begin{document}
\begin{tabular}[t]{rl|rl}%
\x{lnot} & \multicolumn{2}{c}{none}\\
\x{square} & \x{lozenge}\\
\x{vee} & \x{wedge}\\
\x{vdash} & \x{models}\\
\end{tabular}
\end{document}
There is the LTLfonts LaTeX package from Stanford, which provides commands and fonts for Linear Temporal Logic.
There is a more recent ltl LaTeX package (work in progress of this post) supporting both the letter operators F,G,etc. and the symbol operators <>,[], etc. Note that this package includes the previous as an option.
There is the circle package on CTAN, providing an improved symbol for the next operator.