© 20052018 Joachim Klein <j.klein@ltl2dstar.de>
Contents
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 worstcase 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 LTLtoBüchi translators for the conversion from LTL to NBA and can thus benefit from the stateoftheart algorithms, implementations and optimizations available in this well researched area.
You can download the latest version of ltl2dstar at http://www.ltl2dstar.de/.
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 ltl2dstar0.5.4.tar.gz cd ltl2dstar0.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 email.
There is also a Makefile for CMake, see the README file.
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.
To generate DRA/DSA for an LTL formula, ltl2dstar relies on external LTLtoNBA translators. There are many different translators available, each providing a different commandline 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):
Placeholder  Replacement 

%s  LTL formula in Spin syntax 
%S  Filename of a file containing the LTL formula in Spin syntax 
%l  LTL formula in LBT(T) syntax 
%L  Filename of a file containing the LTL formula in LBT(T) syntax 
%N  Filename for the automaton file (in Spin neverclaim syntax) 
%T  Filename for the automaton file (in LBT(T) syntax) 
%H  Filename for the automaton file (in HOA syntax) 
The filename placeholders can be used asis 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 LTLtoBü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 "doublequote" 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:
Program  Remarks  

ltl2ba  download  Written in C, uses a translation via alternating automata [GastinOddoux01]. Via spin:ltl2ba or ltl2ba f %s > %N 
Spot's ltl2tgba  download  Written in C++,
supports advanced simplification algorithms [DuretLutz14]. Check out the cool web interface to ltl2tgba. Via spin:ltl2tgba@B D s (Spin interface), ltl2tgba lbtinput %l B D H > %H (LBT input, HOA output), ... The B selects Büchi automaton output, the D signals a preference for deterministic automata. 
ltl3ba  download  Written in C++, extended version of ltl2ba with additional simplifications [Babiak+12]. Via spin:ltl3ba or ltl3ba H3 f %s > %H (HOA output of the NBA). 
spin  download  Fullfeatured model checker, can also be used to translate LTL formulas to NBA. Based on [GerthPeledVardiWolper95]. Via spin:spin or spin f %s > %N. 
LTL>NBA  download Offline  Written in Python, using alternating Büchi automata and simulation relations [FritzWilke03]. Via lbtt:script4lbtt.py or script4lbtt.py %L %T. 
Modella  download Offline  Written in C, tries to produce "more deterministic" NBA [SebastianiTonetta03]. Via lbtt:modella or modella %L %T. 
For a comparison of several LTLtoNBA 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.
In these examples we will use ltl2ba as the LTLtoNBA 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 dotrepresentation 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 outputformat=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 commandline option detailedstates=yes:
echo "F G a" > FGa.ltl ltl2dstar ltl2nba=spin:ltl2ba stutter=no outputformat=dot \ detailedstates=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.
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 PSPACEcomplete and is not enabled by default (use partialstutter=yes to enable). The user of ltl2dstar should determine if the additional time needed to check the stutter invariance is an acceptable tradeoff 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 outputformat=dot \ detailedstates=yes FGa.ltl FGa_stutter.dot dot Tpdf FGa_detailed.dot > FGa_stutter.pdf
Result:
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 nondeterministic 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) accname: 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 outputformat=dot detailedstates=yes nba.hoa drafromnba.dot dot Tpdf drafromnba.dot > drafromnba.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
complementinput=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 stutterinsensitiveness,
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 stutterinsensitiveness. However, if the HOA automaton has the stutterinsensitive 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 trusthoaproperties=no option. With this option, the languagerelated HOA properties are ignored.
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 as used by ltl2dstar are in prefix format using the following grammar:
formula ::= t // True  f // False  atomicproposition // 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 // NextStep  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.
atomicproposition can either be a string containing no whitespace (and not being one of the operators) and starting with a character from [azAZ] or an arbitrary string enclosed in double quotes (").
ltl2dstar notation  spin notation 

& p0 "p1"  p0 && p1 
i G F a G F b  ([] <> a) > ([] <> b) 
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 (DRA) and Deterministic Streett Automata (DSA) are subtypes of Deterministic ωAutomata.
A Deterministic Rabin Automaton is a 5tuple DRA=(Q, Σ, q_{0}, δ, Acc), with:
Deterministic StreettAutomata 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_{0},a_{1}, ... is a sequence of states in the DRA/DSA ρ=q_{0},q_{1}, ..., with q_{0} being the initial state and for all q_{i+1}=δ(q_{i}, a_{0}).
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:
A run ρ of a Deterministic Rabin Automaton with
Acc ={(L_{1},U_{1}), ..., (L_{n},U_{n})}
is called accepting if:
There exists a pair (L_{i},U_{i}) such that the intersection of L_{i} and Inf(ρ) is nonempty and the intersection of U_{i} and Inf(ρ) is empty.
A run ρ of a Deterministic Streett Automaton with
Acc ={(L_{1},U_{1}), ..., (L_{n},U_{n})}
is called accepting if:
For all n pairs (L_{i},U_{i}) the intersection of L_{i} and Inf(ρ) is empty or the intersection of U_{i} and Inf(ρ) is nonempty.
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.
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? statecount acceptancepairs startstate atomicpropositions id ::= automatontype version edgetype '\n' automatontype ::= DRA // Rabin automaton  DSA // Streett automaton version ::= v2 // Format version edgetype ::= explicit comment ::= Comment: "<string>" '\n' // A quoted string, optional comment statecount ::= States: [09]+ '\n' // Number of states acceptancepairs ::= AcceptancePairs: [09]+ '\n' // Number of acceptance pairs startstate ::= Start: [09]+ '\n' // The name of the start state atomicpropositions ::= AP: [09]+ ap* '\n' // The number and the list of atomic propositions ap ::= "<string>" // A quoted (") string states ::= (statename acceptancesignature transitions)* statename ::= State: [09]+ ("<string>")? '\n' // The name of the state // (with an optional quoted string as a comment) acceptancesignature ::= AccSig: accsig* '\n' // A list of accsig accsig ::= (+)[09]+ // + or  followed by the name of the acceptance pair transitions ::= transition* transition ::= [09]+ '\n' // The name of the 'to'state
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 AcceptancePairs: 1 Start: 0 AP: 2 "a" "b"  State: 0 AccSig: 1 // 00 = !a & !b 0 // 01 = a & !b 2 // 10 = !a & b 2 // 11 = a & b State: 1 AccSig: 0 1 // 00 = !a & !b 1 // 01 = a & !b 1 // 10 = !a & b 1 // 11 = a & b State: 2 AccSig: +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_{0} is state 0, there is one acceptance pair with L_{0}={2} and U_{0}={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'.
The Hanoi OmegaAutomata Format (HOA) was recently introduced [Babiak+15] and aims at a flexible and robust exchange format for ωautomata.
Using the outputformat=hoa option (or the H short cut), ltl2dstar will output automata in HOA format. The deterministic automata will be complete, have Rabin or Streett statebased acceptance and implicit transition labels. The nondeterministic automata will have statebased Büchi acceptance and explicit transition labels.
For further information, visit the HOA tool support page and the HOA page on automata.tools.
Invocation of ltl2dstar:
If inputfile or outputfile are '', standard input/output is used.
Option  Description 

External LTLtoBüchi translator  
ltl2nba=tool arguments ltl2nba=interface:path ltl2nba=interface:path@parameters 
Specifies the external LTLtoNBA translator to use, see above. interface can be either spin or lbtt. parameters are passed through to the LTLtoNBA translator. Default (ltl2ba in current working directory): ltl2nba=spin:ltl2ba 
Automata types  
automata=rabin,streett automata=rabin automata=streett automata=originalnba 
Which automata types should be generated? Use originalnba to get the NBA as generated for the formula by the external LTLtoNBA translator. Default: automata=rabin 
Input options  
input=ltl input=nba 
What is the format of the input?
Default: input=ltl 
complementinput=yes/no 
Should the input be complemented? In case of input=ltl, negate the formula. In case of input=nba, generate a deterministic Streett automaton recognizing the complement language of the NBA. Default: complementinput=no 
trusthoaproperties=yes/no 
Should properties headers in a parsed HOA automaton be trusted?
Currently, this concerns the stutterinsensitive property.
Default: trusthoaproperties=yes 
Output options  
output=automaton output=nba output=plugin:name 
What should be output?
Default: output=automaton 
outputformat=native outputformat=hoa outputformat=dot 
What should be the output format?

extraoutput=format:filename 
new in version 0.5.4
Optional, request additional output (may occur multiple times). This is useful, for example, if one wants to generate both a HOA and DOT output from the same run.
format can be one of the valid options for the
outputformat (see above).
Prefixing nba will output the
NBA generated from the deterministic automaton (see
output=nba).
Examples:

detailedstates=yes/no  Output detailed descriptions of the internal structure of the states of the DRA/DSA. This includes Safra trees, the internal structure of the product automaton of the union construction and the equivalence class of the automaton after the bisimulation optimization, as well as which states where used in the stuttered translation.
Default: detailedstates=no 
Optimizations  
safra=options  Enable/disable "onthefly" optimizations of Safra's construction. options is a commaseperated list of the following options (with a minus '' to disable), interpreted lefttoright:
safra=all,rename Example: Only renaming and reordering: safra=rename,reorder Default: safra=all 
bisimulation=yes/no  Enable/disable calculation of the quotient automaton.
Default: bisimulation=yes 
optacceptance=yes/no  Optimize acceptance condition.
Default: optacceptance=yes 
dbadirect=yes/no 
new in version 0.5.4
If the NBA is already deterministic, skip Safra's determinization. Stutter (if applicable) and bisimulation quotienting are applied nonetheless. Default: dbadirect=yes 
union=yes/no  Enable/disable the construction of the union DRA for formulas with the logical disjunction as toplevel operator.
Default: union=yes 
scheck=path  Enable the direct calculation of a deterministic Büchi automaton using the tool scheck for the subset of safety/cosafety LTL formulas. The executable is given by path.
Default: disabled. 
Stuttering  
stutter=yes/no  Enable/disable stuttering in the construction of the deterministic automaton. Default: stutter=yes 
partialstutter=yes/no  Enable/disable determining the exact set of symbols that are stutter insensitive, which allows using the stuttering construction even in the case that the formula contains the Nextstep operator. This option only has an effect if stutter=yes. Default: partialstutter=no 
Plugins  
plugin=name plugin=name:argument 
Activate the plugin called name, optionally configured with argument. 
Short options  
t 'X'  Expanded to ltl2nba='X'. 
D  Expanded to outputformat=dot. 
H  Expanded to outputformat=hoa. 
B  Expanded to input=nba (HOA NBA input). 
Other  
help  Print command line help and quit. 
version  Print version string to standard out and quit. 
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 thus has to be able to output LTL formulas in the proper syntax and to read the produced automata.
The LBT(T) interface is the one used by the LTLtoBü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 LTLtoNBA translator will be called as follows:
pathtotranslator parameters inputfile outputfile
The inputfile will contain a single line with the LTL to be translated. After execution, outputfile 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.
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:
pathtotranslator f "ltlformula"
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.
Since version 0.5.3, ltl2dstar can read nondeterministic Büchi automata in the HOA format. Currently, only automata with a single starting state, statebased acceptance, explicit transition labels and a nongeneralized Büchi acceptance condition are supported. The parser is implemented using the cpphoafparser library.
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 hardcoded limit of at most 32 atomic propositions.