Math & Science ⇒ Typesetting LTL using Unicode?

[user49915]

Unicode has an abundance of open circles, diamonds and boxes. An example of a linear-time temporal logic formula is

(◇ψ) ∧ ◇(θ U ◻◯φ)

In my browser, the sizes of the symbols vary too much; they don't match, and the result looks ugly. The same happens in LaTeX, though, you could fiddle with sizes there in some circumstances. Are there any "proper" Unicode symbols made specifically for typesetting LTL formulas? I failed to find any, but, maybe, I have not looked everywhere. The LaTeX packages known to me are all pre-{xe|lua}latex. As the pre-Unicode LTL typesetting standard take a look into the books on Manna/Pnueli, e.g., http://theory.stanford.edu/~zm/tvors3.html .

Crosspost: http://cs.stackexchange.com/questions/1 ... in-unicode