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&t=32886


2 Answers 2


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)
  • $\begingroup$ 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. $\endgroup$
    – siracusa
    Oct 2, 2019 at 14:21
  • $\begingroup$ 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. $\endgroup$
    – siracusa
    Oct 3, 2019 at 0:35

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

  • $\begingroup$ Definitely. I gave those files to "oliveking" because I wanted LTL to look right in his undergrad thesis. $\endgroup$
    – Kai
    May 4, 2020 at 0:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy