LTLFonts

LTLFonts is a free font containing mathematical symbols for typesetting formulas of linear temporal logic (LTL) in the Manna/Pnueli notation. I designed it to be used with the LaTeX typesetting system, but it should work with other software as well.

Status

The most recent version is 0.1.2. It is available to a small group of collaborators and should be consider a beta stage. The goal is to get feedback so I can improve the font.

Design

There isn't much really, it's a circle and a square, but a few points to keep in mind are:

Requirements

The font is distributed in outline Type 1 format, with associated TeX (TFM), Adobe (AFM), and Microsoft (PFM) font metrics. It should be usable with any modern LaTeX distribution and many other typesetting or word processing software. I also provide the FontForge SFD source, so you can convert it to any other format supported by FontForge.

The TeX metric file, LaTeX companion package, and dvips map file should work on any modern LaTeX distribution. I tested it on teTeX on Fedora Core 4 GNU/Linux.

If you use LTLFonts successfully on other platforms, please let me know. Once I get enough positive reports, I will be able to update this section with confidence.

License

LTLFonts is released under the SIL Open Font License – please read it carefully and do not download the fonts unless you agree to the terms of the license:

This Font Software is Copyright (c) 2006–2007, Matteo Slanina (http://theory.stanford.edu/~matteo/ltlfonts/). All Rights Reserved.

“LTLFonts” is a Reserved Font Name for this Font Software.

This Font Software is licensed under the SIL Open Font License, Version 1.0. No modification of the license is permitted, only verbatim copy is allowed. This license is copied below, and is also available with a FAQ at: http://scripts.sil.org/OFL

SIL OPEN FONT LICENSE

Version 1.0 – 22 November 2005

PREAMBLE

The goals of the Open Font License (OFL) are to stimulate worldwide development of cooperative font projects, to support the font creation efforts of academic and linguistic communities, and to provide an open framework in which fonts may be shared and improved in partnership with others.

The OFL allows the licensed fonts to be used, studied, modified and redistributed freely as long as they are not sold by themselves. The fonts, including any derivative works, can be bundled, embedded, redistributed and sold with any software provided that the font names of derivative works are changed. The fonts and derivatives, however, cannot be released under any other type of license.

DEFINITIONS

“Font Software” refers to any and all of the following:

“Reserved Font Name” refers to the Font Software name as seen by users and any other names as specified after the copyright statement.

“Standard Version” refers to the collection of Font Software components as distributed by the Copyright Holder.

“Modified Version” refers to any derivative font software made by adding to, deleting, or substituting – in part or in whole – any of the components of the Standard Version, by changing formats or by porting the Font Software to a new environment.

“Author” refers to any designer, engineer, programmer, technical writer or other person who contributed to the Font Software.

PERMISSION & CONDITIONS

Permission is hereby granted, free of charge, to any person obtaining a copy of the Font Software, to use, study, copy, merge, embed, modify, redistribute, and sell modified and unmodified copies of the Font Software, subject to the following conditions:

1) Neither the Font Software nor any of its individual components, in Standard or Modified Versions, may be sold by itself.

2) Standard or Modified Versions of the Font Software may be bundled, redistributed and sold with any software, provided that each copy contains the above copyright notice and this license. These can be included either as stand-alone text files, human-readable headers or in the appropriate machine-readable metadata fields within text or binary files as long as those fields can be easily viewed by the user.

3) No Modified Version of the Font Software may use the Reserved Font Name(s), in part or in whole, unless explicit written permission is granted by the Copyright Holder. This restriction applies to all references stored in the Font Software, such as the font menu name and other font description fields, which are used to differentiate the font from others.

4) The name(s) of the Copyright Holder or the Author(s) of the Font Software shall not be used to promote, endorse or advertise any Modified Version, except to acknowledge the contribution(s) of the Copyright Holder and the Author(s) or with their explicit written permission.

5) The Font Software, modified or unmodified, in part or in whole, must be distributed using this license, and may not be distributed under any other license.

TERMINATION

This license becomes null and void if any of the above conditions are not met.

DISCLAIMER

THE FONT SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM OTHER DEALINGS IN THE FONT SOFTWARE.

Download

Please make sure that you read and agree with the license before you proceed.

LTLFonts is available as a compressed archive in several formats. Choose your favorite; the content is the same for all.

Installation

If you don't care and just want it to work, drop all the files from all subdirectories of the distribution in the same directory as your LaTeX document. That should do it. See the documentation section on how to use the fonts in your document.

Most likely you will want to install the fonts in a common directory in TeX's search path, so you can use it in multiple documents. This is not the place to explain how to do that, so please don't ask. Here are a few websites and book chapters to start from if you want to learn:

If you know the stuff, there should be no surprise in the LTLFonts distribution: you'll find the usual fd, tfm, pfm, pfb, and map files; just put them in the proper places.

Documentation

Quick Start

Try this document:

% File ltlfonts-quickstart.ltx
\documentclass{article}

\usepackage{ltlfonts}

\begin{document}
LTLFonts provides some nice boxes and circles. For example:

$\LTLsquare \LTLdiamond \LTLcircle a$, $\LTLcircleminus
\LTLdiamondminus \LTLsquareminus \LTLcircletilde b$, $\LTLsquarehat
\LTLdiamondminushat c$
\end{document}

If everything is installed correctly, you should be able to just run

latex ltlfonts-quickstart.ltx
dvips -u +ltlfonts.map ltlfonts-quickstart.dvi

and get this PDF.

If you want to avoid the -u option, you can add the line

p +ltlfonts.map

to your .dvipsrc.

Other Documentation

The complete documentation is available in a PDF document, also included in the distribution.

The proof sheet, also contained in the distribution, shows more use of the font. Its LaTeX source is a good example of how to use LTLFonts to get all the LTL symbols.

Feedback

If you have any comments on LTLFonts, or suggestions for improvement, please email me at matteo@cs.stanford.edu.

Currently, I would especially like to hear about:

Frequently Asked Questions

Q: I get random garbage instead of the font.

A: You are using Windows and a version of LTLFonts prior to 0.1.2, and so you are missing the PFM metric file. Upgrade to the latest version.