ltl2dstar documentation (v.0.5.1)

© 2005-2007 Joachim Klein <j.klein@ltl2dstar.de>

Contents

• Overview
• Getting started
• LTL formulas
• Deterministic Rabin/Streett Automata
• Command line options
• Interface to external LTL-to-NBA translators
• Literature

Overview

ltl2dstar ("LTL to deterministic Streett and Rabin automata") converts formulas in Linear Time Logic to deterministic ω-automata, specifically Rabin (DRA) and Streett automata (DSA).

It is an implementation of Safra's construction to translate nondeterministic Büchi automata (NBA) to deterministic Rabin automata, which has a worst-case complexity of 2^{O(n log n)}, with n being the number of states in the NBA. ltl2dstar employs optimizations and heuristics in an attempt to generate smaller automata in practice. It uses external LTL-to-Büchi translators for the conversion from LTL to NBA and can thus benefit from the state-of-the-art algorithms, implementations and optimizations available in this well researched area.

Getting started

Obtaining ltl2dstar

You can download the latest version of ltl2dstar at http://www.ltl2dstar.de/.

Compiling

Linux and other POSIX systems, Mac OS X

A Makefile for GNU Make and the GNU C++ compiler (versions 3.3 and higher) is provided in the src directory.

To compile, just type make in the src subdirectory. If everything works correctly, this will create the program file ltl2dstar, which you may copy to a convenient location. Later versions will probably be equipped to use autoconf as a build system.

# tar xzvf ltl2dstar-0.5.1.tar.gz
# cd ltl2dstar-0.5.1/src
# make      (on Linux)
# gmake     (on *BSD)
    

If you have problems compiling or have success compiling using another compiler, please drop me an e-mail.

Microsoft Windows

ltl2dstar can be compiled using a GNU C++ version for Windows (like cygwin or mingw) or using current Microsoft Visual C++ compilers. You have to make sure that the src directory is in the include path.

A compiled binary for win32 systems is included in the ZIP archive.

LTL-to-NBA translators

To generate DRA/DSA for an LTL formula, ltl2dstar needs an external LTL-to-NBA translator. There are many different translators available, the following table gives an overview of translators that have been successfully used with ltl2dstar:

The programs can be interfaced with ltl2dstar either using the spin or the lbtt interface, as described later.

For a comparison of several LTL-to-NBA translators in the context of subsequent determinization, you are referred to the diploma thesis.

On invocation of ltl2dstar, you have to provide the path to the executable with a command line parameter of the following format:

interface can be either spin or lbtt, path is the path to the executable of the translator. parameters is optional and can be used to pass additional parameters (like enabling optimizations) as command line arguments to the translator. Take care to quote the whole command line argument if whitespace or characters interpreted by the shell occur.

Examples

Spin in /usr/bin/spin:

ltl2ba in current working directory

LTL->NBA in current working directory

Modella in current working directory with parameters '-r2 -e'

Generating automata

In these examples we will use ltl2ba as the LTL-to-NBA translator and assume that the executable is located in the current working directory.

ltl2dstar can output the generated automata either as a text file as described later or in a format that can be translated using the dot tool from the graphviz package.

The following commands put the formula "F G a" (Finally Globally a) in prefix format into the file FGa.ltl, translate this to a dot-representation of the automaton in file FGa.dot and then generate a PostScript file FGa.ps containing the automaton:

# echo "F G a" > FGa.ltl
# ltl2dstar --ltl2nba=spin:ltl2ba --stutter=no --output=dot FGa.ltl FGa.dot
# dot -Tps FGa.dot > FGa.ps
    

Note: We use the command line option --stutter=no to disable the use of the stuttering construction to get the automaton as it is generated by Safra's algorithm (see Stuttering).

Result:

The start state is shaded gray. The first number in the states is the name of the state, the second row is the acceptance signature for this state (see Semantics).

To see the Safra trees that make up the states of the automaton, we can use the command-line option --detailed-states=yes:

# echo "F G a" > FGa.ltl
# ltl2dstar --ltl2nba=spin:ltl2ba --stutter=no --output=dot --detailed-states=yes FGa.ltl FGa_detailed.dot
# dot -Tps FGa_detailed.dot > FGa_detailed.ps
    

Result

The upper left number in the states is the name of the state, on the right of it is the acceptance signature for this state (see Semantics). Below this line, we can see the trees used in the construction process.

You can use '-' as the argument for the formula file to get the LTL formula directly from standard input (the console). Used as the argument for the output file, the automaton is output on the standard output.

Stuttering

Since version 0.5, ltl2dstar supports the stuttered translation from NBA to DRA. Provided that the formula is invariant under stuttering, this allows the merging of intermediate states that are redundant under stuttering, leading to potentially smaller automata.

For formulas/automata that are not completely insensitive to stuttering, we can determine the exact set of symbols for which stuttering is allowed and use the stuttered translation only on exactly these symbols. Determining the set of symbols for which stuttering is allowed is unfortunately PSPACE-complete and is not enabled by default (use --partial-stutter=yes to enable). The user of ltl2dstar should determine if the additional time needed to check the stutter invariance is an acceptable trade-off for getting potentially significantly smaller automata.

Stuttering for formulas not containing the NextStep operator (X) (which are completely insensitive to stuttering), is enabled by default (--stutter=no to disable).

# echo "F G a" > FGa.ltl
# ltl2dstar --ltl2nba=spin:ltl2ba --stutter=yes --output=dot --detailed-states=yes FGa.ltl FGa_stutter.dot
# dot -Tps FGa_detailed.dot > FGa_stutter.ps
    

Result

Plugins

Since version 0.5.1, ltl2dstar has a mechanism to call plugins at several points during the translation process such that users can perform additional analysis or output in a different format. Take a look inside the src/plugins directory for the interface and some sample plugins and uncomment the PLUGINS line in the Makefile to start experimenting. Activate a plugin using the --plugin command line option or using --output=plugin:name for an output plugin. There may be multiple --plugin specifications, the plugins are called in the order they are specified on the command line.

LTL formulas

Input format

LTL formulas as used by ltl2dstar are in prefix format using the following grammar:

      formula  ::=  
               t                   // True
            |  f                   // False
            |  atomic-proposition

      // propositional logic
            |  ! formula           // Negation
            |  & formula formula   // Conjunction (And)
            |  | formula formula   // Disjunction (Or)
            |  i formula formula   // Implication
            |  e formula formula   // Equivalence
            |  ^ formula formula   // Exclusive Or (XOR)

      // temporal logic
            |  X formula           // Next-Step
            |  F formula           // Finally (Eventually)
            |  G formula           // Globally (Always)
            |  U formula formula   // Until (strong)
            |  V formula formula   // Release (weak)
            |  W formula formula   // Weak-Release


    

There is at least one space between all tokens in an LTL formula.

atomic-proposition can either be a string containing no whitespace (and not being one of the operators) and starting with a character from [a-zA-Z] or an arbitrary string enclosed in double quotes (").

Examples

Deterministic Rabin/Streett Automata

Semantics

Deterministic Rabin (DRA) and Deterministic Streett Automata (DSA) are subtypes of Deterministic ω-Automata.

A Deterministic Rabin Automaton is a 5-tuple DRA=(Q, Σ, q₀, δ, Acc), with:

• Q : a non-empty, finite set of states,
• Σ : a non-empty, finite alphabet,
• q₀: a single initial state from Q
• δ : a deterministic transition function Q × Σ -> Q
• Acc : an acceptance condition {(L₁,U₁), ..., (L_n,U_n)}, being a set of n pairs (L_i, U_i) with L_i and U_i being subsets of the states Q.

Deterministic Streett-Automata are defined the same, they only differ in the semantic interpretation of the acceptance condition.

A run of a DRA or DSA over an infinite word σ=a₀,a₁, ... is a sequence of states in the DRA/DSA ρ=q₀,q₁, ..., with q₀ being the initial state and for all q_i+1=&delta(q_i, a₀).

The infinity set Inf(&rho) of a run ρ is the set of states that occur (are visited) infinitely often in ρ.

Rabin and Street acceptance are defined as follows:

When we consider the acceptance condition not in the context of the whole automaton but in the context of every indiviual state, we get the acceptance signature of a state: A string of the indizes of the acceptance pairs the state is a member of. If for an acceptance pair (L_i,U_i) the current state is a member of L_i, '+i' is part of the acceptance signature, if it is a member of U_i, '-1' is part of the acceptance signature. This allows reconstruction of the acceptance condition for the whole automaton.

The language of a DRA/DSA is defined as the set of infinite words (subset of Σ^ω) that have an accepting run on the automaton.

Output format

Grammar

The following grammar defines the output format (version 2) for DRA and DSA. '\n' signifies a new line, comments start with //.

      automaton        ::= header --- '\n' states
      header           ::= id comment? state-count acceptance-pairs start-state atomic-propositions

      id               ::= automaton-type version edge-type '\n'

      automaton-type   ::=  DRA       // Rabin automaton
                          | DSA       // Streett automaton
      version          ::=  v2        // Format version
      edge-type        ::=  explicit

      comment          ::=  "<string>" '\n'  // A quoted string, optional comment
      state-count      ::=  States: [0-9]+ '\n'           // Number of states
      acceptance-pairs ::=  Acceptance-Pairs: [0-9]+ '\n' // Number of acceptance pairs
      start-state      ::=  Start: [0-9]+ '\n'            // The name of the start state

      atomic-propositions ::= AP: [0-9]+ ap* '\n'  // The number and the list of atomic propositions
      ap                  ::= "<string>"           // A quoted (") string


      states           ::=  (state-name acceptance-signature transitions)*
      state-name       ::=  State: [0-9]+ ("<string>")? '\n'    // The name of the state (with an optional quoted string as a comment)
      acceptance-signature ::= Acc-Sig: acc-sig* '\n'           // A list of acc-sig
      acc-sig          ::= (+|-)[0-9]+            // + or - followed by the name of the acceptance pair

      transitions      ::= transition*
      transition       ::= [0-9]+ '\n'            // The name of the 'to'-state

    

Additional details

• There are state-count states, named from 0 to state-count - 1. They appear in-order in states.
• There are acceptance-pairs acceptance pairs, named from 0 to acceptance-pairs - 1.
• If the the set of atomic propositions AP has k members, the transition function δ is of the form Q × 2^AP -> Q, therefore there are exactly 2^k different transitions from every state. For the transitions, the member a of 2^AP is encoded implicitly in the position of the transition: If a transition t is the i^th transition of a state (starting with 0), then the member a of 2^AP can be deduced by interpreting i as a bitset. If the j^th (least-significant) bit of i is set, then the atomic proposition in that position of the list of atomic propositions atomic-propositions is a member of a, if the bit is not set then it is not a member of a.
  This means that the 2^k transitions are efficiently encoded by the 'to'-state and the order of transitions.

Example

The following example shows the DRA output for the LTL formula 'U a b' (a until b), with the bitset and corresponding propositional description for the transitions (as comments in italic after //, that are not part of the actual output file).

DRA v2 explicit
States: 3
Acceptance-Pairs: 1
Start: 0
AP: 2 "a" "b"
---
State: 0
Acc-Sig:
1             // 00 = !a & !b
0             // 01 =  a & !b 
2             // 10 = !a &  b
2             // 11 =  a &  b 
State: 1
Acc-Sig: -0
1             // 00 = !a & !b
1             // 01 =  a & !b 
1             // 10 = !a &  b
1             // 11 =  a &  b 
State: 2
Acc-Sig: +0
2             // 00 = !a & !b
2             // 01 =  a & !b 
2             // 10 = !a &  b
2             // 11 =  a &  b 
    

For this DRA, the set of states Q is {0,1,2}, the start state q₀ is state 0, there is one acceptance pair with L₀={2} and U₀={1}. States 1 and 2 loop back to themself on any input, state 1 transitions to state 2 on an input containing 'b', to state 1 on an input not containing 'a' and 'b' and back to itself on an input with 'a' but not 'b'.

Command line options

Invocation of ltl2dstar:

If input-file or output-file are '-', standard input/output is used.

Interface to external LTL-to-NBA translators

ltl2dstar is designed to use an external tool to convert LTL formulas to a nondeterministic Büchi automaton (NBA) as the first step in generating a deterministic ω-automaton. It supports two interfaces to these external tools:

LBTT interface

The preferred interface is the one used by the LTL-to-Büchi testbench lbtt. For a description of the input format of the LTL formulas and the output format of the NBA see this description.

The LTL-to-NBA translator will be called as follows:

path-to-translator parameters input-file output-file

The input-file will contain a single line with the LTL to be translated. After execution, output-file should contain the generated NBA.

Currently, only nongeneralized NBA (i.e. NBA with only a single acceptance condition) are supported. The extension of the output format that also allows acceptance on the transitions and not only on the states available with lbtt in version >1.1.0 is not supported by ltl2dstar.

SPIN interface

The model checker spin converts LTL to formulas to never claims, constructs in the programming language PROMELA that spin uses. ltl2dstar does not attempt to parse the full range of PROMELA language constructs that could be used in never claims, but instead focuses on the simpler structure used by actual translators, such as spin and ltl2ba. This subset may be insufficient in the future or for other translators, so the LBTT interface is preferred as it can be parsed easier.

A translator conforming to the SPIN interface will be called as follows:

path-to-translator -f "ltl-formula"

The LTL formula is in infix form using the SPIN syntax for the operators always ([]) and eventually (<>).

The generated automaton is output by the translator on the standard output.

Literature

• Joachim Klein, Christel Baier:
  "On-the-fly Stuttering in the Construction of Deterministic omega-Automata"
  in: Proceedings CIAA 2007, to appear
• Joachim Klein, Christel Baier:
  "Experiments with deterministic omega-automata for formulas of linear temporal logic"
  in: Theoretical Computer Science, 363/2, 2006, p182-195
  [link]
• Joachim Klein:
  "Linear Time Logic and Deterministic omega-Automata"
  Diploma thesis, January 2005, University of Bonn
  [pdf].
• Shmuel Safra:
  "On the Complexity of omega-Automata"
  FOCS, 1988