# 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 .

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) => \Box
◇ (U+25C7) => \Diamond
○ (U+25CB) => \medcirc (from txfonts/pxfonts)

• Which math fonts (or fonts combinations) have you used while compiling with {xe|lua}latex? Or have you compiled with [pdf]latex and hoped that CM+txfonts/pxfonts would lead to Unicode in the text layer of the PDF? Note that \medcirc is a binary operator, so you might have said something like \mathop{\medcirc} or similar. – MdAyq7 Oct 2 at 8:16
• We used the standard CM fonts with pdflatex, remapping Unicode characters using the ucs package. And you are right about the binary operator, though we had \mathord\medcirc to be in line with the other symbols. – siracusa Oct 2 at 14:21
• First, thank you. Second, it turned out that I cannot use your answer directly, since I'm using TeX Ryge Termes Math, but the \Diamond ◇ (U+25C7) is unavailable there. In STIX, this symbol is much larger. – MdAyq7 Oct 2 at 17:01
• I use xelatex only rarely, so I'm not familiar with the various font options. But it should also provide a way to remap single math characters to a different font. Perhaps this thread is of any help? As a last resort, one could create a set of visually compatible operators by hand using the tikz package. – siracusa Oct 3 at 0:35
• Yes, of course. – MdAyq7 Oct 3 at 13:23

(This may be slightly off-topic here.) Manna & Pnueli typeset their books in (La)TeX using the font ZMSY10. Here's the head of the metafont file zmsy10.mf that I'm hesitant to publish in full because I'm unsure about its copyright situation:

% Font parameters

% This is the font ZMSY10, containing special symbols used by Zohar Manna.
% It has been worked on by several people, notably:
%
%   Frank Yellin, who converted it from old MF to new MF;
%   Eric Muller, who added various symbols;
%   Joe Weening, who added more symbols, modified some existing ones,
%   and cleaned up various things.
%   Eric Muller, who added some more symbol and tried to convert the thing
%       to use Metafont 2.0. Added Min{C,B,D}.

% Last modified on Wed Nov  6 14:36:40 PST 1991 by muller


Perhaps you can find it somewhere else on the net.