Typesetting LTL in Unicode?
I don't know if there is a correct or recommended usage of Unicode codepoints for the LTL operators, but the mapping we used in LaTeX was the following:

□ (U+25A1) =&gt; \Box
◇ (U+25C7) =&gt; \Diamond
○ (U+25CB) =&gt; \medcirc (from txfonts/pxfonts)