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.

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:

Example 1: Creating a monitor for the requirement "don't spawn threads until initialisation has finished!"

The most straightforward use of the LTL3 tools would be as follows, via the ltl2mon shell script. 

  $ ./ltl2mon "(! spawn) U init" | dot -Tps > graph.ps

which results in

finite state machine

This is the transition table of the FSM, where red states are "bad states" (i.e., the formula was violated), green "good states" (i.e., the formula was satisfied), and yellow "inconclusive states" (i.e., the formula was neither satisfied nor violated).

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:

Example 2: Visualising LTL2BA's output / a SPIN never-claim. 

  $ ./third-party/ltl2ba -f "a U b" | ./bin/nevertofsm -a `exec ./bin/extractalphabet "a U b"` > nba.txt
  $ ./bin/formulatosymbols "a U b" > nba-symbols.syms
  $ ./third-party/fsmcompile -i nba-symbols.syms nba.txt > nba.fsm
  $ ./third-party/fsmdraw -i nba-symbols.syms nba.fsm | dotty -

This results in:

finite state machine

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: 

  git clone https://github.com/nondeterministic/ltl3tools

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

Required software:

Although the LTL3 tools do not directly depend on third-party software, they are intended to be used in combination with the following programs:

You are strongly encouraged to download and install these (i.e., copy the binaries to a location where you and/or ltl2mon can find them, by default this is inside the third-party directory) if you want to use the LTL3 tools in the way intended. Perhaps like me, you may also find the following programs useful in connection with the LTL3 tools:

  • Graphviz, AT&T's graph library (includes the programs dot, dotty, etc.) [see example above]
  • dot2tex to convert ltl2mon's output straight into LaTeX.

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.
    ACM Transactions on Software Engineering and Methodology, 20(4):14, 2011.
    [pdf] [postscript] [doi] [bibtex]

  • 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-2018 by Andreas Bauer. All rights reserved.

Andreas Bauer <a@pspace.org>
Last modified: Sun Aug 12 11:16:53 CEST 2018 		Valid HTML 4.0