The LTL3 tools are a collection of programs that convert a given LTL formula into a Moore-type finite-state machine (FSM), which can be used as a monitor for that formula. It uses techniques known from the area of runtime verification. The semantics of the FSM is explained in greater detail in the papers linked to below.
This software is released under the terms of the GNU General Public License. For more information, see the README and COPYING documents provided with the LTL3 tools.
To allow maximum flexibility, the LTL3 tools consist of a number of independent programs for manipulating LTL formulae and automata, which can be combined in different ways. Note that although the LTL3 tools process SPIN/Promela never claims, the tools have really been optimised to only work with the ones generated by LTL2BA. This may change in future versions of the tools.
Currently, the LTL3 tools consist of:
Formulas can be built according to the following grammar. (Note the somewhat peculiar use of "!" as negation with a space between.)
φ ::= s | ( φ ) | (! φ) | φ && φ | φ || φ | φ -> φ | φ <-> φ |  φ | <> φ | X φ | φ U φ | φ V φ
where s is an alphanumeric string. For example, you can use ltl2mon like this:
You can easily make up your own functionality by combining the LTL3 tools with others. For example, LTL2BA produces by default only a never-claim. To get a corresponding dot-output, you could use these straightforward commands:
For further use cases and examples, consult the ltl2mon file and the --help options of the corresponding programs.
The LTL3 tools are available as Ocaml source code and as statically linked binaries (Linux-i686 only) both in one package:
For installation instructions, read the accompanying README and take a look inside ltl2mon.
Latest source code:
You can check out the latest version of the source code via the following instruction set:
git clone https://github.com/nondeterministic/ltl3tools
The LTL3 tools are based on the following research papers that also describe the semantics of the generated state machine in more detail.
The source code of the LTL3 tools is released under the terms of the GNU General Public License.
Copyright © 2008-2018 by Andreas Bauer. All rights reserved.