LTL3 Tools

SourceForge.net Logo

General information:

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.

Latest news:

(2009-04-30) There seems to be an issue with newer versions of AT&T's fsm-library when used in combination with LTL3 tools. Until this issue is fixed, please download version 3.7 of the fsm-library as indicated below in the section Required software, and not the latest available version 4.0. It won't work with LTL3 tools.

Thanks to Rico Backasch for figuring this one out.

Usage:

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:

  • extractalphabet: takes as input a formula, and returns the alphabet of the corresponding Büchi automaton as a comma-separated string.
  • formulatosymbols: takes as input a formula and prints the corresponding symbol table (alphabet) in AT&T's fsmlibrary format.
  • fsmcrossprod: takes as input two files representing deterministic finite-state machines in AT&T's fsmlibrary format, and one string representing an input alphabet, and prints the product of the state machines.
  • nevertofsm: takes as input a SPIN never-claim representing a nondeterministic Büchi automaton (generated by LTL2BA), and one string representing an input alphabet, and prints the corresponding state-machine in AT&T's fsmlibrary format.
  • ltl2mon: a wrapper shell script around the above programs which takes as input an LTL formula, and prints a corresponding 3-valued/coloured monitor for it.

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.

Download

Downloadable archive:

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:

  svn co https://ltl3tools.svn.sourceforge.net/svnroot/ltl3tools ltl3tools

Alternatively, you can only browse the SVN-repository via a web-interface. To see what's new, consult the NEWS file, or read the detailed ChangeLog.

Papers

The LTL3 tools are based on the following research papers that also describe the semantics of the generated state machine in more detail.

  • Andreas Bauer, Martin Leucker, and Christian Schallhart.
    Runtime Verification for LTL and TLTL.
    Technical report TUM-I0724, Institut für Informatik, Technische Universität München, December 2007.
    [pdf] [postscript] [bibtex-entry]

  • Andreas Bauer, Martin Leucker, and Christian Schallhart.
    Monitoring of real-time properties.
    In S. Arun-Kumar and N. Garg, editors, Proceedings of the 26th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 4337 of Lecture Notes in Computer Science, pages 261-273. Springer-Verlag, Berlin, Heidelberg, December 2006.
    [pdf] [postscript] [bibtex-entry]

Copyright

The source code of the LTL3 tools is released under the terms of the GNU General Public License.

Copyright © 2008-2009 by Andreas Bauer. All rights reserved.


Andreas Bauer, <baueran@gmail.com>
Last modified: Thu Apr 30 11:04:14 EST 2009
Valid HTML 4.0