Typesetting LTL in Unicode? Unicode has an abundance of open circles, diamonds and boxes. Using these, we can typeset linear-time temporal logic formulas such as

$$
(\mathop{⬦}ψ)\ \,\land\ \,\mathop{⬦}(θ\ \mathsf{U}\ \mathop{◻}\mathop{○}φ)\ \ .
$$

However, in my browser, the sizes of the symbols vary too much; the heights don't match, and the result looks ugly. The same happens in LaTeX (though, you could fiddle with sizes there manually in some circumstances, but it's a mess). Are there any "proper" Unicode codepoints made specifically for typesetting LTL formulas? I failed to find any, but, maybe, I have not looked everywhere. As the pre-Unicode LTL standard take a look into the papers and books by Manna/Pnueli, e.g., http://theory.stanford.edu/~zm/tvors3.html .

Crosspost: http://latex.org/forum/viewtopic.php?f=46&amp;t=32886
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)