diff --git a/wrap/python/ajax/Makefile.am b/wrap/python/ajax/Makefile.am
index 8b6aaa8b8..48aad3e39 100644
--- a/wrap/python/ajax/Makefile.am
+++ b/wrap/python/ajax/Makefile.am
@@ -50,6 +50,7 @@ spot.py: $(srcdir)/spot.in Makefile
 	    -e 's|[@]top_builddir[@]|@top_builddir@|g' \
 	    -e 's|[@]PACKAGE_VERSION[@]|@PACKAGE_VERSION@|g' \
 	    -e 's|[@]DOT[@]|@DOT@|g' \
+	    -e 's|[@]LTL3BA[@]|@LTL3BA@|g' \
 	    <$(srcdir)/spot.in >spot.tmp
 	chmod +x spot.tmp
 	mv -f spot.tmp $@
diff --git a/wrap/python/ajax/css/ltl2tgba.css b/wrap/python/ajax/css/ltl2tgba.css
index a985369d3..471053d56 100644
--- a/wrap/python/ajax/css/ltl2tgba.css
+++ b/wrap/python/ajax/css/ltl2tgba.css
@@ -88,6 +88,11 @@ table.ltltable
     float: right;
 }
 
+.colleft {
+    float: left;
+    width: 49%;
+}
+
 .ltl2tgba .head .ui-icon {
     float: right;
     margin: 1px 0px;
diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index f6b5f49af..b667ad31c 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -54,6 +54,17 @@
             }
         })
 
+	$("#ltl3ba-T").change(function() {
+	    if ($(this).is(':checked')) {
+              $("#ltl3ba-S").removeAttr('checked');
+            }
+        })
+	$("#ltl3ba-S").change(function() {
+	    if ($(this).is(':checked')) {
+              $("#ltl3ba-U").attr('checked', true);
+            }
+        })
+
 	function hideOrShowPanels(output, duration) {
 	    switch (output)
 	    {
@@ -469,6 +480,7 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 	      <li><a href="#tabs-tfm" class="btip" title="A tableau construction that uses BDDs to symbolically represent each state of the automaton.  This is the best algorithm of the three, and the only one that has been extended to support PSL operators.">Couvreur/FM</a></li>
 	      <li><a href="#tabs-tla" class="btip" title="Builds a purely symbolic automaton, using BDDs to encode the transition relation.  The translation itself is fast (it uses a number of BDD operations that is linear in the size of the formula), but the resulting symbolic encoding is better used symbolically.  If you develop it explicitly (e.g. to draw it, as on this page) the result can easily have an exponential number of states.">Couvreur/LaCIM</a></li>
 	      <li><a href="#tabs-tta" class="btip" title="An implementation of Heikki Tauriainen's Ph.D. thesis algorithm to translate LTL formulas via very weak alternating automata with transition-based generalized acceptance conditions.">Tauriainen/TAA</a></li>
+	      <li><a href="#tabs-tl3" class="btip" title="An improved version of LTL2BA, overhauled by Tomáš Babiak during his Ph.D., and described at TACAS'12.<br>LTL3BA is not part of Spot.  Options in this tab correspond to options offered by LTL3BA, and have some overlap with the options offered by Spot upstream and downstream.">LTL3BA</a></li>
 	      <li class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>
 	    </ul>
 	    <input type="hidden" name="t" value="fm">
@@ -503,6 +515,42 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 		  language containment
 		</label><br>
 	      </div>
+	      <div id="tabs-tl3">
+		Use <a href="http://sourceforge.net/projects/ltl3ba/">LTL3BA</a> to build:
+		<label class="rtip" title="Stop LTL3BA once it has built a Transition-based Generalized Büchi Automaton.  Spot will take it from here and optionally apply more optimizations.">
+		  <INPUT id="ltl3ba-T" type="radio" name="lo" value="T" checked>
+		  a TGBA
+		</label> or <label class="rtip" title="Run LTL3BA until it produces its final Büchi Automaton.  Spot will consider this BA has a TGBA if further optimizations have been requested below.">
+		  <INPUT id="ltl3ba-U" type="radio" name="lo" value="U">
+		  a BA
+		</label></br>
+		<div class="colleft">
+		<label class="rtip" title="LTL simplifications performed in LTL3BA are independent of those Spot may have performed upstream.">
+		  <INPUT type="checkbox" name="l3" value="l" checked>
+		  LTL simplifications
+		</label><br>
+		<label class="rtip" title="Suspension is a technique to postpone the verification some subformulae.  Any easy way to picture it is to look at the formula <span class='formula'>F(a)&GF(b)</span>: the <span class='formula'>GF(b)</span> part need not be checked before some <span class='formula'>a</span> has been seen.  On this example, suspension amounts to translating <span class='formula'>F(a&GF(b))</span> but the technique is more general than such LTL rewritings.">
+		  <INPUT type="checkbox" name="l3" value="P" checked>
+		  suspension in TGBA
+		</label><br>
+		<label class="rtip" title="See previous tooltip for an explanation of suspension.  This version disables suspension in the intermediate alternating automaton, where it is only used for one step.">
+		  <INPUT type="checkbox" name="l3" value="A" checked>
+		  suspension in alternating automaton
+		</label><br>
+		</div>
+		<label class="rtip" title="Compute Strongly Connected Components to simplify the automaton">
+		  <INPUT type="checkbox" name="l3" value="C" checked>
+		  SCC simplifications
+		</label><br>
+		<label class="rtip" title="Try to improve the automaton's determinism when building it.  This may produce larger automata.">
+		  <INPUT type="checkbox" name="l3" value="M">
+		  more deterministic output
+		</label><br>
+		<label class="rtip" title="Compute a direct (a.k.a strong fair) simulation relation to reduce the size of the Büchi automaton.">
+		  <INPUT id="ltl3ba-S" type="checkbox" name="l3" value="S">
+		  direct simulation on BA
+		</label><br>
+	      </div>
 	    </div>
 	  </div>
 	  <div id="autsimp-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
@@ -516,7 +564,7 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 		<INPUT type="checkbox" name="as" value="wd">
 		minimize obligation properties
               </label><br>
-	      <label class="rtip" title="Attempt to reduce the automaton by using <b>direct simulation</b>.  This might also improve the determinism as a side effect.">
+	      <label class="rtip" title="Attempt to reduce the automaton by using <b>direct simulation</b> on the TGBA.  This might also improve the determinism as a side effect.">
 		<INPUT type="checkbox" name="as" value="ds">
 		direct simulation
               </label><br>
diff --git a/wrap/python/ajax/protocol.txt b/wrap/python/ajax/protocol.txt
index 0b4e649e9..54d9f484e 100644
--- a/wrap/python/ajax/protocol.txt
+++ b/wrap/python/ajax/protocol.txt
@@ -53,22 +53,37 @@ Translator algorithm (pick one)
   t=fm    Couvreur/FM
   t=la    Couvreur/LaCIM
   t=ta    Tauriainen/TAA
+  t=l3    LTL3BA
 
-Couvreur/FM options if f=fm (pick many)
+Couvreur/FM options if t=fm (pick many)
 
   fm=od   Optimize Determinism
   fm=sm   Symbolic Merge
   fm=bp   Branching Postponement
   fm=fl   Fair-Loop approximations
 
-Couvreur/LA options if f=la
+Couvreur/LA options if t=la
 
   la=sp   Symbolic Pruning
 
-Tauriainen/TAA options if f=ta
+Tauriainen/TAA options if t=ta
 
   ta=lc   refined rules based on Language Containment
 
+LTL3BA output options if t=l3 (pick one)
+
+  lo=T    output a TGBA
+  lo=U    output a BA
+
+LTL3BA processing options if t=l3 (pick many)
+
+  l3=l    LTL formula simplification
+  l3=P    suspension in TGBA construction
+  l3=A    suspension in alternating automaton construction
+  l3=C    SCC simplifications
+  l3=M    more deterministic output
+  l3=S    direct simulation
+
 Automaton simplifications (pick many)
 
   as=ps   Prune SCC
diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index e2732788f..536dfa074 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -452,13 +452,16 @@ if output_type == 'f':
 translator = form.getfirst('t', 'fm')
 
 if f.is_psl_formula() and not f.is_ltl_formula() and translator != 'fm':
-    print ('''<div class="error">The PSL formula %s
+    unbufprint('''<div class="error">The PSL formula %s
 cannot be translated using this algorithm.  Please use Couveur/FM.'''
-           % format_formula(f, 'span'));
+               % format_formula(f, 'span'))
     finish()
 
 dict = spot.bdd_dict()
 
+# Should the automaton be displayed as a SBA?
+issba = False
+
 if translator == 'fm':
     exprop = False
     symb_merge = False
@@ -485,12 +488,53 @@ elif translator == 'ta':
     if form.getfirst('ta', '') == 'lc':
         refined_rules = True
     automaton = spot.ltl_to_taa(f, dict, refined_rules)
-
-# Should it be displayed as a SBA?
-issba = False
+elif translator == 'l3':
+    l3out = '-T'
+    l3opt = { '-l', '-P', '-A', '-c', '-C' }
+    for lo in form.getfirst('lo', 'T'):
+        if lo == 'U':
+            l3out = '-U'
+            issba = True
+    for l3 in form.getlist('l3'):
+        if l3 == 'l':
+            l3opt.remove('-l')
+        elif l3 == 'P':
+            l3opt.remove('-P')
+        elif l3 == 'A':
+            l3opt.remove('-A')
+        elif l3 == 'C':
+            l3opt.remove('-C')
+            l3opt.remove('-c')
+        elif l3 == 'M':
+            l3opt.add('-M')
+        elif l3 == 'S':
+            l3opt.add('-S')
+    args = ["@LTL3BA@", l3out]
+    args.extend(l3opt)
+    args.extend(['-f', spot.to_spin_string(f)])
+    import subprocess
+    l3file = tmpdir + "/aut"
+    l3aut = open(l3file, "w+")
+    l3proc = subprocess.Popen(args, stdout=l3aut)
+    l3aut.close()
+    ret = l3proc.wait()
+    if ret != 0:
+        unbufprint('''<div class="error">ltl3ba exited with error %s</div>'''
+                   % ret)
+        finish()
+    tpel = spot.empty_tgba_parse_error_list()
+    automaton = spot.tgba_parse(l3file, tpel, dict, env)
+    if tpel:
+        unbufprint('''<div class="error">failed to read ltl3ba's output</div>''')
+        unbufprint('<div class="parse-error">')
+        err = spot.format_tgba_parse_errors(spot.get_cout(), "output", tpel)
+        unbufprint('</div>')
+        automaton = 0
+        finish()
 
 # Monitor output
 if output_type == 'm':
+    issba = False
     automaton = spot.scc_filter(automaton)
     automaton = spot.minimize_monitor(automaton)
     unbufprint('<div class="automata-stats">')
@@ -534,6 +578,7 @@ if prune_scc:
     # degeneralization or simulation is requested: keeping those that
     # lead to accepting states usually helps.
     automaton = spot.scc_filter(automaton, not (degen or direct_simul))
+    issba = False
 
 if wdba_minimize:
     minimized = spot.minimize_obligation_new(automaton, f)
@@ -546,6 +591,7 @@ if wdba_minimize:
 
 if direct_simul:
     automaton = spot.simulation(automaton)
+    issba = False
 
 if degen or neverclaim:
     degen = spot.tgba_sba_proxy(automaton)