ltl2dstar documentation (v.0.5.4)

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

Contents

• Overview
• Getting started
  
  • Compiling
  • LTL-to-NBA translators
  • Generating automata
  • Translating from NBA new in version 0.5.3
• LTL formulas
• Deterministic Rabin/Streett Automata
• Command line options
• Interface to external LTL-to-NBA translators
• Known limitations
• 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 non-deterministic 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 is provided in the src directory. Note that ltl2dstar uses C++11 features and thus needs a compiler that supports these features.

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.

tar xzvf ltl2dstar-0.5.4.tar.gz
cd ltl2dstar-0.5.4/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.

There is also a Makefile for CMake, see the README file.

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 relies on external LTL-to-NBA translators. There are many different translators available, each providing a different command-line interface.

Tool specifications:
You can specify how the translator is called by providing the command and arguments, using the following placeholders (inspired by the notation of Spot's ltlcross):

The filename placeholders can be used as-is or as the source or target of a redirection of the standard input/output of the tool. As an example, in the specification

the %s will be expanded to the formula in Spin syntax and the automaton in neverclaim format is read from the standard output. For

the formula is written, as a single line, to a file, which is piped to the standard input of the tool, while the output automaton (in HOA format) is read from the filename of %H.

To provide the LTL-to-Büchi translator, ltl2dstar provides the --ltl2nba command line option, which can take a tool specification as described above (with suitable quoting of the white space or special shell characters in the argument):

On Windows, you generally have to "double-quote" the whole argument.

Shortcuts spin/lbtt:
Furthermore, for historical reasons and for convenience, two shortcuts are available for the Spin and LBT(T) calling convention. For the Spin calling convention, use

which are, respectively, equivalent to

For the LBT(T) calling convention, use

which are, respectively, equivalent to

Path:
In general, the tool part may be an absolute or relative path to the tool executable. If it does not contain a path separator, first the current directory is considered as the location of the tool executable and then the PATH is searched.

Tools:
The following table gives an overview of translators that have been successfully used with ltl2dstar and their tool specifications:

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

Examples:

ltl2ba in current working directory or on the PATH

ltl2ba at specific location

Spot's ltl2tgba in current working directory or on the PATH (-s enables Spin input/output)

ltl3ba in current working directory or on the PATH, with HOA output

Spin in /usr/bin/spin:

Recommendations:
For the generated automata and where available, we suggest the use of the LBT(T) automata format (stable code) as well as the %H placeholder for the HOA format. For the LTL syntax, we prefer the LBT(T) syntax due to the ease of parsing provided by the prefix format, without parentheses and operator precedence rules.

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 or on the PATH.

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 PDF file FGa.pdf containing the automaton:

echo "F G a" > FGa.ltl
ltl2dstar --ltl2nba=spin:ltl2ba --stutter=no --output-format=dot FGa.ltl FGa.dot
dot -Tpdf FGa.dot > FGa.pdf

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-format=dot \
          --detailed-states=yes FGa.ltl FGa_detailed.dot
dot -Tpdf FGa_detailed.dot > FGa_detailed.pdf

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):

echo "F G a" | ltl2dstar ...

Using '-' 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-format=dot \
          --detailed-states=yes FGa.ltl FGa_stutter.dot
dot -Tpdf FGa_detailed.dot > FGa_stutter.pdf

Result:

Translating from an NBA

Since version 0.5.3, ltl2dstar supports the direct determinization of NBA using the --input=nba option. With this option, the input file is expected to be a non-deterministic Büchi automaton in HOA format. As an example, consider the following HOA automaton:

HOA: v1
name: "eventually always alternating a and !a"
AP: 1 "a"
Start: 0
States: 3
Acceptance: 1 Inf(0)
acc-name: Buchi
--BODY--
State: 0
[ t] 0         /* true -> 0 */
[!0] 1         /* !a -> 1 */
State: 1 {0}   /* accepting state */
[ 0] 2         /* a -> 2 */
State: 2 {0}   /* accepting state */
[!0] 1         /* !a -> 1 */
--END--

This automaton recognizes the language of the ω-regular expression true^* ; (a ; !a)^ω, i.e., eventually there will be always alternation between atomic proposition a being true and a being false.

Assuming this automaton is stored in file nba.hoa, we can generate a deterministic automaton via

ltl2dstar --input=nba --output-format=dot --detailed-states=yes nba.hoa dra-from-nba.dot
dot -Tpdf dra-from-nba.dot > dra-from-nba.pdf

Result:

Complementing the language:
If the input is an LTL formula, we can easily complement the recognized language just by negating the formula. For an NBA input, negation is more complicated. However, we can exploit the duality between Rabin and Streett acceptance to complement the recognized language. Using the --complement-input=yes option, ltl2dstar first determinizes the NBA to a deterministic Rabin automaton (DRA), as usual. But before outputting the deterministic automaton, it switches the acceptance to Streett, effectively complementing the language. The output in this constellation is therefore a deterministic Streett automaton.

Trusting HOA properties, Stuttering:
To determine whether a language is stutter insensitive, ltl2dstar usually inspects the LTL formula for absence of the next step operator. Optionally, it can analyze the NBA for partial stutter-insensitiveness, relying on the easy access to the complement NBA constructed for the negated formula.

In case that only an NBA is given as input, ltl2dstar can not efficiently determine stutter-insensitiveness. However, if the HOA automaton has the stutter-insensitive property, ltl2dstar will use this information during the determinization construction. For this to yield a correct deterministic automaton, it trusts that the property has been added by the automaton's producer only if the language is indeed stutter insensitive. You can change the default behavior of trusting properties with the --trust-hoa-properties=no option. With this option, the language-related HOA properties are ignored.

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   // Until (weak)


    

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

To convert LTL formulas in other formats to the ltl2dstar syntax, you can use the ltlfilt tool from Spot and select the --lbt option.

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=δ(q_i, a₀).

The infinity set Inf(ρ) 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 individual 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 (dstar)

Grammar

The following grammar defines the output format (version 2) for DRA and DSA introduced by ltl2dstar. '\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          ::=  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.
• In the quoted strings, \\ stands for \ and \" for " (this is produced correctly since ltl2dstar version 0.5.2)

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 themselves 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'.

Output Format (HOA)

The Hanoi Omega-Automata Format (HOA) was recently introduced [Babiak+15] and aims at a flexible and robust exchange format for ω-automata.

Using the --output-format=hoa option (or the -H short cut), ltl2dstar will output automata in HOA format. The deterministic automata will be complete, have Rabin or Streett state-based acceptance and implicit transition labels. The non-deterministic automata will have state-based Büchi acceptance and explicit transition labels.

For further information, visit the HOA tool support page and the HOA page on automata.tools.

Command line options

Invocation of ltl2dstar:

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

Interfacing external LTL-to-NBA translators

ltl2dstar is designed to use an external tool to convert LTL formulas to a non-deterministic Büchi automaton (NBA) as the first step in generating a deterministic ω-automaton. It thus has to be able to output LTL formulas in the proper syntax and to read the produced automata.

LBT(T) interface

The LBT(T) interface is the one used by the LTL-to-Büchi testbench lbtt, extending lbt. For a description of the input format of the LTL formulas (placeholders %L and %l) and the output format of the NBA (placeholder %T) see this description.

With the lbtt: shortcut, 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 non-generalized 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 (placeholder %N), 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

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

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

The LTL formula (placeholders %L and %l) is in infix form using the SPIN syntax for the operators always ([]) and eventually (<>), see the documentation.

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

HOA input

Since version 0.5.3, ltl2dstar can read non-deterministic Büchi automata in the HOA format. Currently, only automata with a single starting state, state-based acceptance, explicit transition labels and a non-generalized Büchi acceptance condition are supported. The parser is implemented using the cpphoafparser library.

Known limitations

As ltl2dstar produces a deterministic, complete automaton, with an explicit transition for every combination of atomic propositions, translating formulas or NBA with a large number of atomic propositions becomes infeasible. For efficient storage of the automaton, there is therefore a hard-coded limit of at most 32 atomic propositions.

Literature

• Joachim Klein, Christel Baier:
  "On-the-fly Stuttering in the Construction of Deterministic omega-Automata"
  in: CIAA 2007, Lecture Notes in Computer Science volume 4783, 2007, p51-61
  [link]
• 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
  [link]