# Writing Linear Temporal Logic in LaTeX

I am writing some LTL (Linear Temporal Logic) statements in LaTeX and am having issues finding any packages online or information as to this can be done. Any help would be appreciated.

-
Can you give examples how it should look like? –  Uwe Ziegenhagen Nov 30 '12 at 19:20
this might be a start svn.kwarc.info/repos/arXMLiv/trunk/sty/temporal.sty –  David Carlisle Nov 30 '12 at 19:31
sure something like this ¬[](critical_section1 ^ critical_section2) –  mitchnufc Nov 30 '12 at 19:55
Are you sure you don't mean Linear Temporal Logic? Logical temporal logic seems somewhat redundant. –  Scott H. Nov 30 '12 at 22:29

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}


-
Any difference between \vee/\wedge and \lor/\land? –  Peter Grill Mar 26 '13 at 19:44
@PeterGrill I think they're aliases of each other. –  A.Ellett Mar 26 '13 at 20:08

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.

-

There is also the turnstile package which offers more powerful and flexible options for typesetting turnstiles. (They also have more intuitive command names - more intuitive if you are typesetting logic, that is.)

-