You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
733 lines
33 KiB
733 lines
33 KiB
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">
|
|
<html>
|
|
<head>
|
|
<meta http-equiv="content-type" content="text/html; charset=ISO-8859-1">
|
|
<style type="text/css">
|
|
<!--
|
|
body {font-family:sans-serif; padding-left:2em}
|
|
|
|
.prog
|
|
{font-weight:bold;
|
|
font-family:monospace;
|
|
font-size:larger;}
|
|
|
|
.cmdline
|
|
{font-weight:normal;
|
|
font-family:monospace;
|
|
font-size:larger;}
|
|
|
|
.ltl
|
|
{font-family:monospace;
|
|
font-size:larger;}
|
|
|
|
h1 {border-bottom: 3px solid darkgreen}
|
|
|
|
h2
|
|
{background-color: #A0FFA0;
|
|
padding: 0.3em;
|
|
margin-left: -1em;
|
|
margin-top: 3em;
|
|
border: 1px solid black;
|
|
}
|
|
|
|
|
|
h3
|
|
{background-color: #80FF80;
|
|
padding: 0.3em;
|
|
margin-left: -0.5em;
|
|
margin-top: 2em;
|
|
border: 1px solid black;
|
|
}
|
|
|
|
div.block
|
|
{margin-left:2em;
|
|
margin-right:2em;
|
|
padding:0.5em;
|
|
border: 1px solid darkgreen;
|
|
margin-bottom:1em;}
|
|
|
|
table.ltl-example {border:1px solid black; border-collapse:collapse; text-align:center;}
|
|
|
|
table.ltl-example td {border:1px solid black;}
|
|
table.ltl-example th {border:1px solid black; background-color:#d0d0d0}
|
|
|
|
table.cmdline-options {border:1px solid black; border-collapse:collapse;}
|
|
|
|
table.cmdline-options td {border:1px solid black; vertical-align:top;}
|
|
table.cmdline-options th {border:1px solid black; background-color:#d0d0d0; vertical-align:top; text-align:left;padding-left:1em;}
|
|
|
|
table.cmdline-options th.sections {border:1px solid black; background-color:#a0a0ff; vertical-align:top; text-align:left;padding-left:1em;}
|
|
|
|
|
|
|
|
table.ltl-nba-progs {border:1px solid black; border-collapse:collapse;margin:1em;}
|
|
table.ltl-nba-progs td {border:1px solid black; vertical-align:top; padding:0.25em;}
|
|
table.ltl-nba-progs th {border:1px solid black; background-color:#d0d0d0; padding: 0.5em;}
|
|
|
|
-->
|
|
</style>
|
|
<title>ltl2dstar documentation</title>
|
|
</head>
|
|
|
|
<body>
|
|
<h1>ltl2dstar documentation (v.0.5.1)</h1>
|
|
|
|
<p>© 2005-2007 Joachim Klein <j.klein@ltl2dstar.de></p>
|
|
|
|
<p><b>Contents</b></p>
|
|
<ul>
|
|
<li><a href="#overview">Overview</a></li>
|
|
<li><a href="#getting-started">Getting started</a></li>
|
|
<li><a href="#ltl-formulas">LTL formulas</a></li>
|
|
<li><a href="#dra_dsa">Deterministic Rabin/Streett Automata</a></li>
|
|
<li><a href="#cmdline">Command line options</a></li>
|
|
<li><a href="#ltl-to-nba-interface">Interface to external LTL-to-NBA translators</a></li>
|
|
<li><a href="#literature">Literature</a></li>
|
|
</ul>
|
|
|
|
<h2><a name="overview">Overview</a></h2>
|
|
|
|
<p>
|
|
<span class="prog">ltl2dstar</span> ("<b>LTL</b> to <b>d</b>eterministic <b>St</b>reett <b>a</b>nd <b>R</b>abin automata") converts formulas in Linear Time Logic to deterministic ω-automata, specifically Rabin (DRA) and Streett automata (DSA).
|
|
</p>
|
|
<p>It is an implementation of <a href="#lit-safra">Safra's construction</a> to translate nondeterministic Büchi automata (NBA) to deterministic Rabin automata, which has a worst-case
|
|
complexity of 2<sup>O(n log n)</sup>, with n being the number of states in the NBA. <span class="prog">ltl2dstar</span> 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.
|
|
</p>
|
|
|
|
<h2><a name="getting-started">Getting started</a></h2>
|
|
|
|
<h3>Obtaining <span class="prog">ltl2dstar</span></h3>
|
|
|
|
<p>
|
|
You can download the latest version of <span class="prog">ltl2dstar</span> at <a href="http://www.ltl2dstar.de/">http://www.ltl2dstar.de/</a>.</p>
|
|
|
|
<h3>Compiling</h3>
|
|
|
|
<h4>Linux and other POSIX systems, Mac OS X</h4>
|
|
|
|
<p>
|
|
A Makefile for GNU Make and the GNU C++ compiler (versions 3.3 and higher) is provided in the <span class="cmdline">src</span> directory.
|
|
</p>
|
|
|
|
<p>To compile, just type <span class="cmdline">make</span> in the <span class="cmdline">src</span> subdirectory. If everything works correctly, this will create the program file <span class="cmdline">ltl2dstar</span>, which you may copy to a convenient location. Later versions will probably be equipped to use autoconf as a build system.
|
|
|
|
<pre>
|
|
# tar xzvf ltl2dstar-0.5.1.tar.gz
|
|
# cd ltl2dstar-0.5.1/src
|
|
# make (on Linux)
|
|
# gmake (on *BSD)
|
|
</pre>
|
|
|
|
<p>
|
|
If you have problems compiling or have success compiling using another compiler, please drop me an e-mail.
|
|
</p>
|
|
|
|
<h4>Microsoft Windows</h4>
|
|
|
|
<p>
|
|
<span class="prog">ltl2dstar</span> 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 <span class="cmdline">src</span> directory is in the include path.
|
|
</p>
|
|
|
|
<p>
|
|
A compiled binary for win32 systems is included in the ZIP archive.
|
|
</p>
|
|
|
|
<h3>LTL-to-NBA translators</h3>
|
|
|
|
<p>
|
|
To generate DRA/DSA for an LTL formula, <span class="prog">ltl2dstar</span> 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 <span class="prog">ltl2dstar</span>:</p>
|
|
|
|
<table class="ltl-nba-progs" border="1">
|
|
<tr>
|
|
<th colspan="2">Program</th><th>Interface</th><th>Remarks</th>
|
|
</tr>
|
|
<tr><td><a href="http://www.liafa.jussieu.fr/~oddoux/">ltl2ba</a></td><td><a href="http://www.liafa.jussieu.fr/~oddoux/ltl2ba/download.html">download</a></td><td>spin</td><td>Written in C, uses alternating Büchi automata (<b>recommended</b>)</td></tr>
|
|
<tr><td><a href="http://www.ti.informatik.uni-kiel.de/~fritz/">LTL->NBA</a></td><td><a href="http://www.ti.informatik.uni-kiel.de/~fritz/LTL-NBA.zip">download</a></td><td>lbtt</td><td>Written in Python, using alternating Büchi automata and simulation relations.<br>Use file <span class="cmdline">script4lbtt.py</span> as executable.</td></tr>
|
|
<tr><td><a href="http://www.spinroot.com/">spin</a></td><td><a href="http://spinroot.com/spin/Src/index.html">download</a></td><td>spin</td><td>Full-featured model checker, can also be used to translate LTL formulas to NBA.<br>
|
|
Uses tableaux-based approach.</td></tr>
|
|
<tr><td><a href="http://www.science.unitn.it/~stonetta/modella.html">Modella</a></td><td><a href="http://www.science.unitn.it/~stonetta/modella.html">download</a></td><td>lbtt</td><td>Written in C, tries to produce "more deterministic" NBA.</td></tr>
|
|
</table>
|
|
|
|
<p>The programs can be interfaced with <span class="prog">ltl2dstar</span> either using the spin or the lbtt interface, as described <a href="#ltl-to-nba-interface">later</a>.</p>
|
|
|
|
<p>For a comparison of several LTL-to-NBA translators in the context of subsequent determinization, you are referred to the <a href="#diploma-thesis">diploma thesis</a>.</p>
|
|
|
|
<p>
|
|
On invocation of <span class="prog">ltl2dstar</span>, you have to provide the path to the executable with a command line parameter of the following format:
|
|
</p>
|
|
|
|
<div class="cmdline">
|
|
--ltl2nba=<i>interface</i>:<i>path</i>
|
|
</div>
|
|
|
|
<div class="cmdline">
|
|
'--ltl2nba=<i>interface</i>:<i>path</i>@<i>parameters</i>'
|
|
</div>
|
|
|
|
<p>
|
|
<i>interface</i> can be either <span class="cmdline">spin</span> or <span class="cmdline">lbtt</span>, <i>path</i> is the path to the executable of the translator. <i>parameters</i> 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.
|
|
</p>
|
|
|
|
<h4>Examples</h4>
|
|
|
|
|
|
<p>Spin in /usr/bin/spin: </p>
|
|
<div class="cmdline">--ltl2nba=spin:/usr/bin/spin</div>
|
|
|
|
|
|
<p>
|
|
ltl2ba in current working directory </p>
|
|
<div class="cmdline">--ltl2nba=spin:ltl2ba</div>
|
|
|
|
|
|
<p>
|
|
LTL->NBA in current working directory </p>
|
|
<div class="cmdline">--ltl2nba=lbtt:script4lbtt.py</div>
|
|
|
|
|
|
<p>
|
|
Modella in current working directory with parameters '-r2 -e'</p>
|
|
<div class="cmdline">'--ltl2nba=lbtt:script4lbtt.py@-r2 -e'</div>
|
|
|
|
|
|
|
|
<h3>Generating automata</h3>
|
|
|
|
<p>
|
|
In these examples we will use <span class="prog">ltl2ba</span> as the LTL-to-NBA translator and assume that the executable is located in the current working directory.
|
|
</p>
|
|
|
|
<p>
|
|
<span class="prog">ltl2dstar</span> can output the generated automata either as a text file as described later or in a format that can be translated using the <span class="prog">dot</span> tool from the <span class="prog"><a href="http://www.graphviz.org/">graphviz</a></span> package.
|
|
</p>
|
|
|
|
<p>
|
|
The following commands put the formula "F G a" (Finally Globally a) in prefix format into the file <span class="cmdline">FGa.ltl</span>, translate this to a <span class="prog">dot</span>-representation of the automaton in file <span class="cmdline">FGa.dot</span> and then generate a PostScript file <span class="cmdline">FGa.ps</span> containing the automaton:
|
|
</p>
|
|
|
|
<pre>
|
|
# echo "F G a" > FGa.ltl
|
|
# ltl2dstar --ltl2nba=spin:ltl2ba --stutter=no --output=dot FGa.ltl FGa.dot
|
|
# dot -Tps FGa.dot > FGa.ps
|
|
</pre>
|
|
|
|
<p><i>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 <a href="#stuttering">Stuttering</a>).</i></p>
|
|
|
|
<h4>Result:</h4>
|
|
<p><img style="border:1px solid black;" src="FGa.png" alt="Automaton for FGa"></p>
|
|
|
|
<p>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 <a href="#semantics">Semantics</a>).</p>
|
|
|
|
<p>
|
|
To see the Safra trees that make up the states of the automaton, we can use the command-line option <span class="cmdline">--detailed-states=yes</span>:
|
|
|
|
<pre>
|
|
# 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
|
|
</pre>
|
|
|
|
<h4>Result</h4>
|
|
<p><img style="border:1px solid black;" src="FGa_detailed.png" alt="Automaton for FGa"></p>
|
|
|
|
<p>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 <a href="#semantics">Semantics</a>). Below this line, we can see the trees used in the construction process.</p>
|
|
|
|
|
|
<p>
|
|
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.
|
|
</p>
|
|
|
|
|
|
|
|
<h3><a name="stuttering">Stuttering</a></h3>
|
|
|
|
<p> Since version 0.5, <span class="prog">ltl2dstar</span> supports the <i>stuttered translation</i> 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.</p>
|
|
<p> 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 <span class="cmdline">--partial-stutter=yes</span> to enable). The user of <span class="prog">ltl2dstar</span> should determine if the additional time needed to check the stutter invariance is an acceptable trade-off for getting potentially significantly smaller automata.</p>
|
|
<p> Stuttering for formulas not containing the NextStep operator (X) (which are completely insensitive to stuttering), is enabled by default (<span class="cmdline">--stutter=no</span> to disable).</p>
|
|
|
|
<pre>
|
|
# 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
|
|
</pre>
|
|
|
|
<h4>Result</h4>
|
|
<p><img style="border:1px solid black;" src="FGa_stutter.png" alt="Automaton for FGa"></p>
|
|
|
|
|
|
|
|
<h3><a name="Plugins">Plugins</a></h3>
|
|
|
|
<p>Since version 0.5.1, <span class="prog">ltl2dstar</span> 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 <span class="cmdline">--plugin</span> command
|
|
line option or using
|
|
<span class="cmdline">--output=plugin:<i>name</i></span> for an output
|
|
plugin. There may be multiple
|
|
<span class="cmdline">--plugin</span> specifications, the plugins are
|
|
called in the order they are specified on the command line.</p>
|
|
|
|
|
|
|
|
<h2><a name="ltl-formulas">LTL formulas</a></h2>
|
|
|
|
<h3>Input format</h3>
|
|
|
|
<p>
|
|
LTL formulas as used by <span class="prog">ltl2dstar</span> are in prefix format using the following grammar:
|
|
</p>
|
|
|
|
<pre>
|
|
<i>formula</i> ::=
|
|
t // True
|
|
| f // False
|
|
| <i>atomic-proposition</i>
|
|
|
|
// propositional logic
|
|
| ! <i>formula</i> // Negation
|
|
| & <i>formula</i> <i>formula</i> // Conjunction (And)
|
|
| | <i>formula</i> <i>formula</i> // Disjunction (Or)
|
|
| i <i>formula</i> <i>formula</i> // Implication
|
|
| e <i>formula</i> <i>formula</i> // Equivalence
|
|
| ^ <i>formula</i> <i>formula</i> // Exclusive Or (XOR)
|
|
|
|
// temporal logic
|
|
| X <i>formula</i> // Next-Step
|
|
| F <i>formula</i> // Finally (Eventually)
|
|
| G <i>formula</i> // Globally (Always)
|
|
| U <i>formula</i> <i>formula</i> // Until (strong)
|
|
| V <i>formula</i> <i>formula</i> // Release (weak)
|
|
| W <i>formula</i> <i>formula</i> // Weak-Release
|
|
|
|
<!-- perhaps in the future
|
|
<span style="background-color:red;">TODO</span>
|
|
| 'M' <i>formula</i> <i>formula</i>
|
|
| 'B' <i>formula</i> <i>formula</i>
|
|
-->
|
|
</pre>
|
|
|
|
<p>
|
|
There is at least one space between all tokens in an LTL formula.
|
|
</p>
|
|
|
|
<p><i>atomic-proposition</i> 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 (").</p>
|
|
|
|
<h4>Examples</h4>
|
|
|
|
<table class="ltl-example">
|
|
<tr>
|
|
<th><span class="prog">ltl2dstar</span> notation</th>
|
|
<th><span class="prog">spin</span> notation</th>
|
|
</tr>
|
|
<tr>
|
|
<td><span class="ltl">& p0 "p1"</span></td><td><span class="ltl">p0 && p1</span></td>
|
|
</tr><tr>
|
|
<td><span class="ltl">i G F a G F b</span></td><td><span class="ltl">([] <> a) -> ([] <> b)</span></td>
|
|
</tr>
|
|
</table>
|
|
|
|
|
|
<h2><a name="dra_dsa">Deterministic Rabin/Streett Automata</a></h2>
|
|
|
|
<h3><a name="semantics">Semantics</a></h3>
|
|
|
|
<p>
|
|
Deterministic Rabin (DRA) and Deterministic Streett Automata (DSA) are subtypes of Deterministic <span title="omega">ω</span>-Automata.
|
|
</p>
|
|
|
|
<p>
|
|
A Deterministic Rabin Automaton is a 5-tuple DRA=(Q, <span title="Sigma">Σ</span>, q<sub>0</sub>, <span title="delta">δ</span>, Acc), with: </p>
|
|
<ul>
|
|
<li>Q : a non-empty, finite set of <b>states</b>,</li>
|
|
<li><span title="Sigma">Σ</span> : a non-empty, finite <b>alphabet</b>,</li>
|
|
<li>q<sub>0</sub>: a single <b>initial state</b> from Q</li>
|
|
<li><span title="delta">δ</span> : a deterministic <b>transition function</b> Q × <span title="Sigma">Σ</span> -> Q</li>
|
|
<li>Acc : an <b>acceptance condition</b> {(L<sub>1</sub>,U<sub>1</sub>), ..., (L<sub>n</sub>,U<sub>n</sub>)},
|
|
being a set of <i>n</i> pairs (L<sub>i</sub>, U<sub>i</sub>) with L<sub>i</sub> and U<sub>i</sub> being subsets of the states Q.
|
|
</ul>
|
|
|
|
|
|
<p>
|
|
Deterministic Streett-Automata are defined the same, they only differ in the semantic interpretation of the acceptance condition.
|
|
</p>
|
|
|
|
<p> A <b>run</b> of a DRA or DSA over an infinite word σ=a<sub>0</sub>,a<sub>1</sub>, ... is a sequence of states in the DRA/DSA ρ=q<sub>0</sub>,q<sub>1</sub>, ..., with q<sub>0</sub> being the initial state and for all q<sub>i+1</sub>=&delta(q<sub>i</sub>, a<sub>0</sub>).</p>
|
|
<p>
|
|
The <b>infinity set</b> <i>Inf</i>(&rho) of a run ρ is the set of states that occur (are visited) infinitely often in ρ.
|
|
</p>
|
|
|
|
<p>Rabin and Street acceptance are defined as follows:</p>
|
|
|
|
<div class="block">
|
|
<h4>Rabin acceptance</h4>
|
|
|
|
<p>
|
|
A run ρ of a Deterministic Rabin Automaton with
|
|
Acc ={(L<sub>1</sub>,U<sub>1</sub>), ..., (L<sub>n</sub>,U<sub>n</sub>)}
|
|
is called accepting if:<br>
|
|
There exists a pair (L<sub>i</sub>,U<sub>i</sub>) such that the intersection of L<sub>i</sub> and <i>Inf</i>(ρ) is <b>non-empty</b> and the intersection of U<sub>i</sub> and <i>Inf</i>(ρ) is <b>empty</b>.
|
|
</p>
|
|
</div>
|
|
|
|
<div class="block">
|
|
<h4>Streett acceptance</h4>
|
|
|
|
<p>
|
|
A run ρ of a Deterministic Streett Automaton with
|
|
Acc ={(L<sub>1</sub>,U<sub>1</sub>), ..., (L<sub>n</sub>,U<sub>n</sub>)}
|
|
is called accepting if:<br>
|
|
For all <i>n</i> pairs (L<sub>i</sub>,U<sub>i</sub>) the intersection of L<sub>i</sub> and <i>Inf</i>(ρ) is <b>empty</b> or the intersection of U<sub>i</sub> and <i>Inf</i>(ρ) is <b>non-empty</b>.
|
|
</p>
|
|
</div>
|
|
|
|
<p>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 <b>acceptance signature</b> of a state: A string of the indizes of the acceptance pairs the state is a member of. If for an acceptance pair (L<sub>i</sub>,U<sub>i</sub>) the current state is a member of L<sub>i</sub>, '+i' is part of the acceptance signature, if it is a member of U<sub>i</sub>, '-1' is part of the acceptance signature. This allows reconstruction of the acceptance condition for the whole automaton.
|
|
</p>
|
|
|
|
|
|
|
|
<p>
|
|
The <b>language of a DRA/DSA</b> is defined as the set of infinite words (subset of Σ<sup>ω</sup>) that have an accepting run on the automaton.
|
|
</p>
|
|
|
|
|
|
<h3><a name="output-format">Output format</a></h3>
|
|
|
|
<h4>Grammar</h4>
|
|
|
|
<p>The following grammar defines the output format (version 2) for DRA and DSA. '\n' signifies a new line, comments start with //.</p>
|
|
<pre>
|
|
<i>automaton</i> ::= <i>header</i> --- '\n' <i>states</i>
|
|
<i>header</i> ::= <i>id</i> <i>comment</i>? <i>state-count</i> <i>acceptance-pairs</i> <i>start-state</i> <i>atomic-propositions</i>
|
|
|
|
<i>id</i> ::= <i>automaton-type</i> <i>version</i> <i>edge-type</i> '\n'
|
|
|
|
<i>automaton-type</i> ::= DRA // Rabin automaton
|
|
| DSA // Streett automaton
|
|
<i>version</i> ::= v2 // Format version
|
|
<i>edge-type</i> ::= explicit
|
|
|
|
<i>comment</i> ::= "<i><string></i>" '\n' // A quoted string, optional comment
|
|
<i>state-count</i> ::= States: [0-9]+ '\n' // Number of states
|
|
<i>acceptance-pairs</i> ::= Acceptance-Pairs: [0-9]+ '\n' // Number of acceptance pairs
|
|
<i>start-state</i> ::= Start: [0-9]+ '\n' // The name of the start state
|
|
|
|
<i>atomic-propositions</i> ::= AP: [0-9]+ <i>ap</i>* '\n' // The number and the list of atomic propositions
|
|
<i>ap</i> ::= "<i><string></i>" // A quoted (") string
|
|
|
|
|
|
<i>states</i> ::= (<i>state-name</i> <i>acceptance-signature</i> <i>transitions</i>)*
|
|
<i>state-name</i> ::= State: [0-9]+ ("<i><string></i>")? '\n' // The name of the state (with an optional quoted string as a comment)
|
|
<i>acceptance-signature</i> ::= Acc-Sig: <i>acc-sig</i>* '\n' // A list of <i>acc-sig</i>
|
|
<i>acc-sig</i> ::= (+|-)[0-9]+ // + or - followed by the name of the acceptance pair
|
|
|
|
<i>transitions</i> ::= transition*
|
|
<i>transition</i> ::= [0-9]+ '\n' // The name of the 'to'-state
|
|
|
|
</pre>
|
|
|
|
<h4>Additional details</h4>
|
|
<ul>
|
|
<li>There are <i>state-count</i> states,
|
|
named from 0 to <i>state-count</i> - 1.
|
|
They appear in-order in <i>states</i>.</li>
|
|
<li>There are <i>acceptance-pairs</i> acceptance pairs, named from 0 to <i>acceptance-pairs</i> - 1.</li>
|
|
<li>If the the set of atomic propositions AP has <i>k</i> members, the transition function δ is of the form Q × 2<sup>AP</sup> -> Q, therefore there are exactly 2<sup>k</sup> different transitions from every state. For the transitions, the member <i>a</i> of 2<sup>AP</sup> is encoded implicitly in the position of the transition: If a transition <i>t</i> is the <i>i</i><sup>th</sup> transition of a state (starting with 0), then the member <i>a</i> of 2<sup>AP</sup> can be deduced by interpreting <i>i</i> as a bitset. If the <i>j</i><sup>th</sup> (least-significant) bit of <i>i</i> is set, then the atomic proposition in that position of the list of atomic propositions <i>atomic-propositions</i> is a member of <i>a</i>, if the bit is not set then it is not a member of <i>a</i>.<br>
|
|
This means that the 2<sup>k</sup> transitions are efficiently encoded by the 'to'-state and the order of transitions.</li>
|
|
</ul>
|
|
|
|
<h4>Example</h4>
|
|
<p>
|
|
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 <i>comments in italic</i> after //, that are not part of the actual output file).
|
|
</p>
|
|
|
|
<pre>
|
|
DRA v2 explicit
|
|
States: 3
|
|
Acceptance-Pairs: 1
|
|
Start: 0
|
|
AP: 2 "a" "b"
|
|
---
|
|
State: 0
|
|
Acc-Sig:
|
|
1 <i>// 00 = !a & !b</i>
|
|
0 <i>// 01 = a & !b</i>
|
|
2 <i>// 10 = !a & b</i>
|
|
2 <i>// 11 = a & b</i>
|
|
State: 1
|
|
Acc-Sig: -0
|
|
1 <i>// 00 = !a & !b</i>
|
|
1 <i>// 01 = a & !b</i>
|
|
1 <i>// 10 = !a & b</i>
|
|
1 <i>// 11 = a & b</i>
|
|
State: 2
|
|
Acc-Sig: +0
|
|
2 <i>// 00 = !a & !b</i>
|
|
2 <i>// 01 = a & !b</i>
|
|
2 <i>// 10 = !a & b</i>
|
|
2 <i>// 11 = a & b</i>
|
|
</pre>
|
|
|
|
|
|
<p>For this DRA, the set of states Q is {0,1,2}, the start state q<sub>0</sub> is state 0, there is one acceptance pair with L<sub>0</sub>={2} and U<sub>0</sub>={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'.</p>
|
|
|
|
|
|
|
|
|
|
<!-- <h3>Graphical representation</h3> -->
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
<h2><a name="cmdline">Command line options</a></h2>
|
|
|
|
<p>
|
|
Invocation of <span class="prog">ltl2dstar</span>:
|
|
</p>
|
|
<div class="cmdline">ltl2dstar <i>options</i> <i>input-file</i> <i>output-file</i>
|
|
</div>
|
|
|
|
<p>
|
|
If <i>input-file</i> or <i>output-file</i> are '-', standard input/output is used.
|
|
</p>
|
|
|
|
<table class="cmdline-options" border="1">
|
|
<tr><th>Option</th><th>Description</th></tr>
|
|
|
|
<tr><th class="sections" colspan="2">External LTL-to-Büchi translator</th></tr>
|
|
<tr><td class="cmdline">
|
|
--ltl2nba=<i>interface</i>:<i>path</i><br>
|
|
--ltl2nba=<i>interface</i>:<i>path</i>@<i>parameters</i></td>
|
|
<td>Specifies the external LTL-to-NBA translator to use.<br>
|
|
<i>interface</i> can be either <span class="cmdline">spin</span> or <span class="cmdline">lbtt</span>.<br>
|
|
<i>parameters</i> are passed through to the LTL-to-NBA translator.<br><br>
|
|
<b>Default</b> (<span class="cmdline">ltl2ba</span> in current working directory):<br>
|
|
<div class="cmdline">--ltl2nba=spin:ltl2ba</div>
|
|
</td>
|
|
</tr>
|
|
|
|
|
|
<tr><th class="sections" colspan="2">Automata types</th></tr>
|
|
|
|
<tr>
|
|
<td class="cmdline">
|
|
--automata=rabin,streett<br>
|
|
--automata=rabin<br>
|
|
--automata=streett<br>
|
|
--automata=original-nba
|
|
</td>
|
|
<td>
|
|
Which automata types should be generated?<br>
|
|
Use <span class="cmdline">original-nba</span> to get
|
|
the NBA as generated for the formula by the
|
|
external LTL-to-NBA translator.
|
|
<br><br>
|
|
<b>Default:</b> <span class="cmdline">--automata=rabin</span>
|
|
</td>
|
|
</tr>
|
|
|
|
<tr><th class="sections" colspan="2">Output format</th></tr>
|
|
|
|
<tr>
|
|
<td class="cmdline">
|
|
--output=automaton<br>
|
|
--output=dot<br>
|
|
--output=nba<br>
|
|
--output=plugin:<i>name</i>
|
|
</td>
|
|
<td>
|
|
Which output format should be used?
|
|
<ul>
|
|
<li><span class="cmdline">automaton</span> : output a <a href="#output-format">textual representation</a> of the automaton.</li>
|
|
<li><span class="cmdline">dot</span> : output a graph description, that can be used as input to <span class="prog">dot</span> from the <span class="prog"><a href="http://www.graphviz.org/">graphviz</a></span> package, which generates a graphical representation of the automaton.</li>
|
|
|
|
<li><span class="cmdline">nba</span> : transform the DRA/DSA to a nondeterministic Büchi automaton (NBA) and output the NBA in LBTT-format. This basically transforms <span class="prog">ltl2dstar</span> into a LTL-to-NBA translator (LTL -> NBA -(Safra)-> DRA/DSA -> NBA), which allows testing the correctness of the implementation using the LTL-to-Büchi testbench <a href="http://www.tcs.hut.fi/Software/lbtt/"><span class="prog">lbtt</span></a>. </li>
|
|
|
|
<li><span class="cmdline">plugin</span> : Delegate output of the DRA/DSA to the plugin called <i>name</i></li>
|
|
</ul>
|
|
|
|
<b>Default:</b> <span class="cmdline">--output=automaton</span>
|
|
</td>
|
|
</tr>
|
|
|
|
|
|
<tr>
|
|
<td class="cmdline">--detailed-states=<i>yes/no</i></td>
|
|
<td>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.
|
|
<br><br>
|
|
<b>Default:</b><span class="cmdline">--detailed-states=no</span>
|
|
</td>
|
|
</tr>
|
|
|
|
|
|
<tr><th class="sections" colspan="2">Optimizations</th></tr>
|
|
|
|
<tr>
|
|
<td class="cmdline">--safra=<i>options</i></td>
|
|
<td>Enable/disable "on-the-fly" optimizations of Safra's construction.<br>
|
|
<i>options</i> is a comma-seperated list of the following options (with a minus '-' to disable), interpreted left-to-right:<br>
|
|
|
|
<ul>
|
|
<li><span class="cmdline">all</span> : enable all optimizations</li>
|
|
|
|
<li><span class="cmdline">none</span> : disable all optimizations</li>
|
|
|
|
<li><span class="cmdline">accloop</span> : detect accepting self-loops</li>
|
|
|
|
<li><span class="cmdline">accsucc</span> : detect "all successors in NBA are accepting"</li>
|
|
|
|
<li><span class="cmdline">rename</span> : try to name new nodes in Safra trees intelligently</li>
|
|
|
|
<li><span class="cmdline">reorder</span> : try to reorder nodes in Safra trees intelligently</li>
|
|
</ul>
|
|
|
|
|
|
<b>Example:</b> All optimizations but renaming:<br>
|
|
<span class="cmdline">--safra=all,-rename</span>
|
|
<br><br>
|
|
<b>Example:</b> Only renaming and reordering:<br>
|
|
<span class="cmdline">--safra=rename,reorder</span>
|
|
|
|
<br><br>
|
|
<b>Default:</b><span class="cmdline">--safra=all</span>
|
|
</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td class="cmdline">--bisimulation=<i>yes/no</i></td>
|
|
<td>Enable/disable calculation of the quotient automaton.
|
|
<br><br>
|
|
<b>Default:</b><span class="cmdline">--bisimulation=yes</span>
|
|
</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td class="cmdline">--opt-acceptance=<i>yes/no</i></td>
|
|
<td>Optimize acceptance condition.
|
|
<br><br>
|
|
<b>Default:</b><span class="cmdline">--opt-acceptance=yes</span>
|
|
</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td class="cmdline">--union=<i>yes/no</i></td>
|
|
<td>Enable/disable the construction of the union DRA for formulas with the logical disjunction as top-level operator.
|
|
<br><br>
|
|
<b>Default:</b><span class="cmdline">--union=yes</span>
|
|
</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td class="cmdline">--scheck=<i>path</i></td>
|
|
<td>Enable the direct calculation of a deterministic Büchi automaton using the tool <a href="http://www.tcs.hut.fi/~timo/scheck/"><span class="prog">scheck</span></a> for the subset of safety/co-safety LTL formulas. The executable is given by <i>path</i>.
|
|
<br><br>
|
|
<b>Default:</b> disabled.
|
|
</td>
|
|
</tr>
|
|
|
|
<tr><th class="sections" colspan="2">Stuttering</th></tr>
|
|
|
|
<tr>
|
|
<td class="cmdline">--stutter=<i>yes/no</i></td>
|
|
<td>Enable/disable stuttering in the construction of the deterministic automaton.<br>
|
|
<br>
|
|
<b>Default:</b><span class="cmdline">--stutter=yes</span>
|
|
</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td class="cmdline">--partial-stutter=<i>yes/no</i></td>
|
|
<td>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 <span class="cmdline">--stutter=yes</span>.<br>
|
|
<br>
|
|
<b>Default:</b><span class="cmdline">--partial-stutter=no</span>
|
|
</td>
|
|
</tr>
|
|
|
|
|
|
<tr><th class="sections" colspan="2">Plugins</th></tr>
|
|
<td class="cmdline">
|
|
--plugin=<i>name</i><br>
|
|
--plugin=<i>name</i>:<i>argument</i></td>
|
|
<td>Activate the plugin called <i>name</i>, optionally configured with <i>argument</i>.
|
|
</td>
|
|
</tr>
|
|
|
|
<tr><th class="sections" colspan="2">Other</th></tr>
|
|
|
|
<tr>
|
|
<td class="cmdline">--help</td>
|
|
<td>Print command line help and quit.</td>
|
|
</tr>
|
|
|
|
<tr>
|
|
<td class="cmdline">--version</td>
|
|
<td>Print version string to standard out and quit.</td>
|
|
</tr>
|
|
|
|
|
|
</table>
|
|
|
|
|
|
|
|
|
|
|
|
<h2><a name="ltl-to-nba-interface">Interface to external LTL-to-NBA translators </a></h2>
|
|
|
|
<p>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: </p>
|
|
|
|
<h3>LBTT interface</h3>
|
|
|
|
<p>The preferred interface is the one used by the LTL-to-Büchi testbench <a href="http://www.tcs.hut.fi/Software/lbtt/">lbtt</a>. For a description of the input format of the LTL formulas and the output format of the NBA see <a href="http://www.tcs.hut.fi/Software/maria/tools/lbt/">this description</a>.</p>
|
|
|
|
<p>The LTL-to-NBA translator will be called as follows:</p>
|
|
|
|
<blockquote><p><i>path-to-translator</i> <i>parameters</i> <i>input-file</i> <i>output-file</i></p></blockquote>
|
|
|
|
<p> The <i>input-file</i> will contain a single line with the LTL to be translated. After execution, <i>output-file</i> should contain the generated NBA.</p>
|
|
|
|
<p> 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 <span class="prog">lbtt</span> in version >1.1.0 is not supported by <span class="prog">ltl2dstar</span>.</p>
|
|
|
|
|
|
<h3>SPIN interface</h3>
|
|
|
|
<p> The model checker <a href="http://www.spinroot.com/"><span class="prog">spin</span></a> converts LTL to formulas to <i>never claims</i>, constructs in the programming language PROMELA that <span class="prog">spin</span> uses. <span class="prog">ltl2dstar</span> 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 <span class="prog">spin</span> and <span class="prog">ltl2ba</span>. This subset may be insufficient in the future or for other translators, so the LBTT interface is preferred as it can be parsed easier.</p>
|
|
|
|
<p> A translator conforming to the SPIN interface will be called as follows:</p>
|
|
<blockquote><p><i>path-to-translator</i> -f "<i>ltl-formula</i>"</p></blockquote>
|
|
|
|
<p>The LTL formula is in infix form using the SPIN syntax for the operators always (<span class="ltl">[]</span>) and eventually (<span class="ltl"><></span>).</p>
|
|
|
|
<p> The generated automaton is output by the translator on the standard output.</p>
|
|
|
|
<h2><a name="literature">Literature</a></h2>
|
|
|
|
<ul>
|
|
<li><a name="lit-stutter">Joachim Klein, Christel Baier</a>:<br>
|
|
"On-the-fly Stuttering in the Construction of Deterministic omega-Automata"<br>
|
|
in: Proceedings CIAA 2007, <i>to appear</i>
|
|
</li>
|
|
<li><a name="lit-tcs2006">Joachim Klein, Christel Baier</a>:<br>
|
|
"Experiments with deterministic omega-automata for formulas of linear temporal logic"<br>
|
|
in: Theoretical Computer Science, 363/2, 2006, p182-195<br>
|
|
[<a href="http://dx.doi.org/10.1016/j.tcs.2006.07.022">link</a>]</li>
|
|
<li><a name="diploma-thesis">Joachim Klein</a>:<br>
|
|
"Linear Time Logic and Deterministic omega-Automata"<br>
|
|
Diploma thesis, January 2005, University of Bonn<br>
|
|
[<a href="http://www.ltl2dstar.de/literature/ltl2dstar-diploma-thesis.pdf">pdf</a>].
|
|
<li><a name="lit-safra">Shmuel Safra</a>:<br>
|
|
"On the Complexity of omega-Automata"<br>
|
|
FOCS, 1988</li>
|
|
</ul>
|
|
|
|
|
|
|
|
</body>
|
|
</html>
|