diff --git a/NEWS b/NEWS
index 261418295..c540aec68 100644
--- a/NEWS
+++ b/NEWS
@@ -104,6 +104,13 @@ New in spot 2.9.4.dev  (not yet released)
     automaton, but we should not waste too much space and time trying
     that.
 
+    spot::translator additionally honor the following new variable:
+
+     tls-max-states  Maximum number of states of automata involved in
+                     automata-based implication checks for formula
+                     simplifications.  Defaults to 64.
+
+
   Python:
 
   - Bindings for functions related to parity games.
diff --git a/bin/spot-x.cc b/bin/spot-x.cc
index ce15fed27..2f74bf167 100644
--- a/bin/spot-x.cc
+++ b/bin/spot-x.cc
@@ -44,6 +44,9 @@ static const argp_option options[] =
 (2) additionally allows automata-based implication checks, (3) enables \
 more rules based on automata-based implication checks.  The default value \
 depends on the --low, --medium, or --high settings.") },
+    { DOC("tls-max-states",
+          "Maximum number of states of automata involved in automata-based \
+implication checks for formula simplifications.  Defaults to 64.") },
     { nullptr, 0, nullptr, 0, "Translation options:", 0 },
     { DOC("ltl-split", "Set to 0 to disable the translation of automata \
 as product or sum of subformulas.") },
diff --git a/spot/tl/contain.cc b/spot/tl/contain.cc
index a6cb12806..858afc52d 100644
--- a/spot/tl/contain.cc
+++ b/spot/tl/contain.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009-2012, 2014-2016, 2018, 2019 Laboratoire de Recherche
+// Copyright (C) 2009-2012, 2014-2016, 2018-2020 Laboratoire de Recherche
 // et Développement de l'Epita (LRDE).
 // Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -52,12 +52,15 @@ namespace spot
 
   language_containment_checker::language_containment_checker
   (bdd_dict_ptr dict, bool exprop, bool symb_merge,
-   bool branching_postponement, bool fair_loop_approx)
+   bool branching_postponement, bool fair_loop_approx,
+   unsigned max_states)
     : dict_(dict), exprop_(exprop), symb_merge_(symb_merge),
       branching_postponement_(branching_postponement),
       fair_loop_approx_(fair_loop_approx),
       translated_(new trans_map_)
   {
+    if (max_states)
+      aborter_ = std::make_unique<output_aborter>(max_states);
   }
 
   language_containment_checker::~language_containment_checker()
@@ -104,7 +107,11 @@ namespace spot
       return false;
     trim_common_Xs(l, g);
     record_* rl = register_formula_(l);
+    if (!rl->translation)
+      return false;
     record_* rg = register_formula_(g);
+    if (!rg->translation)
+      return false;
     return incompatible_(rl, rg);
   }
 
@@ -139,7 +146,11 @@ namespace spot
     if (l == g)
       return true;
     record_* rl = register_formula_(l);
+    if (!rl->translation)
+      return false;
     record_* rg = register_formula_(g);
+    if (!rg->translation)
+      return false;
     if (isomorphism_checker::are_isomorphic(rl->translation, rg->translation))
       return true;
     return contained(l, g) && contained(g, l);
@@ -153,7 +164,8 @@ namespace spot
       return &i->second;
 
     auto e = ltl_to_tgba_fm(f, dict_, exprop_, symb_merge_,
-                            branching_postponement_, fair_loop_approx_);
+                            branching_postponement_, fair_loop_approx_,
+                            nullptr, nullptr, false, aborter_.get());
     return &translated_->emplace(f, std::move(e)).first->second;
   }
 }
diff --git a/spot/tl/contain.hh b/spot/tl/contain.hh
index 20fa714fd..28d83172f 100644
--- a/spot/tl/contain.hh
+++ b/spot/tl/contain.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011-2016, 2019 Laboratoire de Recherche
+// Copyright (C) 2011-2016, 2019, 2020 Laboratoire de Recherche
 // et Développement de l'Epita (LRDE).
 // Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -24,6 +24,7 @@
 
 #include <spot/tl/formula.hh>
 #include <spot/twa/bdddict.hh>
+#include <spot/twaalgos/powerset.hh>
 
 namespace spot
 {
@@ -41,7 +42,8 @@ namespace spot
                                  bool exprop = false,
                                  bool symb_merge = true,
                                  bool branching_postponement = false,
-                                 bool fair_loop_approx = false);
+                                 bool fair_loop_approx = false,
+                                 unsigned max_states = 0U);
 
     ~language_containment_checker();
 
@@ -72,5 +74,6 @@ namespace spot
     /* Translation Maps */
     trans_map_* translated_;
     tl_simplifier_cache* c_;
+    std::unique_ptr<const output_aborter> aborter_ = nullptr;
   };
 }
diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc
index 2848c3e9e..1a7f179b3 100644
--- a/spot/tl/simplify.cc
+++ b/spot/tl/simplify.cc
@@ -70,7 +70,8 @@ namespace spot
 
     tl_simplifier_cache(const bdd_dict_ptr& d,
                          const tl_simplifier_options& opt)
-      : dict(d), options(opt), lcc(d, true, true, false, false)
+      : dict(d), options(opt),
+        lcc(d, true, true, false, false, opt.containment_max_states)
     {
       options.containment_checks |= options.containment_checks_stronger;
       options.event_univ |= options.favor_event_univ;
diff --git a/spot/tl/simplify.hh b/spot/tl/simplify.hh
index 7ecde7498..e5838544d 100644
--- a/spot/tl/simplify.hh
+++ b/spot/tl/simplify.hh
@@ -93,6 +93,9 @@ namespace spot
     // &,|, and X operators.  Only rewrite Xor and Equiv under
     // temporal operators.
     bool keep_top_xor;
+    // If greater than 0, bound the number of states used by automata
+    // in containment checks.
+    unsigned containment_max_states = 0;
   };
 
   // fwd declaration to hide technical details.
diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc
index 33019fe22..c560bc2e3 100644
--- a/spot/twaalgos/ltl2tgba_fm.cc
+++ b/spot/twaalgos/ltl2tgba_fm.cc
@@ -1947,7 +1947,8 @@ namespace spot
   ltl_to_tgba_fm(formula f2, const bdd_dict_ptr& dict,
                  bool exprop, bool symb_merge, bool branching_postponement,
                  bool fair_loop_approx, const atomic_prop_set* unobs,
-                 tl_simplifier* simplifier, bool unambiguous)
+                 tl_simplifier* simplifier, bool unambiguous,
+                 const output_aborter* aborter)
   {
     tl_simplifier* s = simplifier;
 
@@ -2051,6 +2052,13 @@ namespace spot
     dest_map dests;
     while (!formulae_to_translate.empty())
       {
+        if (aborter && aborter->too_large(a))
+          {
+            if (!simplifier)
+              delete s;
+            return nullptr;
+          }
+
         // Pick one formula.
         formula now = *formulae_to_translate.begin();
         formulae_to_translate.erase(formulae_to_translate.begin());
diff --git a/spot/twaalgos/ltl2tgba_fm.hh b/spot/twaalgos/ltl2tgba_fm.hh
index 76a5a15b9..8c1827490 100644
--- a/spot/twaalgos/ltl2tgba_fm.hh
+++ b/spot/twaalgos/ltl2tgba_fm.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2017, 2019 Laboratoire de
+// Copyright (C) 2010-2015, 2017, 2019-2020 Laboratoire de
 // Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -26,6 +26,7 @@
 #include <spot/twa/twagraph.hh>
 #include <spot/tl/apcollect.hh>
 #include <spot/tl/simplify.hh>
+#include <spot/twaalgos/powerset.hh>
 
 namespace spot
 {
@@ -73,6 +74,10 @@ namespace spot
   /// \param unambiguous When true, unambigous TGBA will be produced
   /// using the trick described in \cite benedikt.13.tacas .
   ///
+  /// \param aborter When given, aborts the construction whenever the
+  /// constructed automaton would become larger than specified by the
+  /// output_aborter.
+  ///
   /// \return A spot::twa_graph that recognizes the language of \a f.
   SPOT_API twa_graph_ptr
   ltl_to_tgba_fm(formula f, const bdd_dict_ptr& dict,
@@ -81,5 +86,6 @@ namespace spot
                  bool fair_loop_approx = false,
                  const atomic_prop_set* unobs = nullptr,
                  tl_simplifier* simplifier = nullptr,
-                 bool unambiguous = false);
+                 bool unambiguous = false,
+                 const output_aborter* aborter = nullptr);
 }
diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc
index 4415a6439..dcdcb8175 100644
--- a/spot/twaalgos/translate.cc
+++ b/spot/twaalgos/translate.cc
@@ -60,11 +60,14 @@ namespace spot
         gf_guarantee_set_ = true;
       }
     ltl_split_ = opt->get("ltl-split", 1);
+    int tls_max_states = opt->get("tls-max-states", 64);
+    tls_max_states_ = std::max(0, tls_max_states);
   }
 
   void translator::build_simplifier(const bdd_dict_ptr& dict)
   {
     tl_simplifier_options options(false, false, false);
+    options.containment_max_states = tls_max_states_;
     switch (level_)
       {
       case High:
diff --git a/spot/twaalgos/translate.hh b/spot/twaalgos/translate.hh
index db65348dd..344cae3ba 100644
--- a/spot/twaalgos/translate.hh
+++ b/spot/twaalgos/translate.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2013-2018, 2020 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -154,6 +154,7 @@ namespace spot
     bool gf_guarantee_ = true;
     bool gf_guarantee_set_ = false;
     bool ltl_split_;
+    unsigned tls_max_states_ = 0;
     const option_map* opt_;
   };
   /// @}
diff --git a/tests/core/bdd.test b/tests/core/bdd.test
index e70216a11..ba2e11232 100755
--- a/tests/core/bdd.test
+++ b/tests/core/bdd.test
@@ -23,7 +23,8 @@ set -e
 
 # Make sure that setting the SPOT_BDD_TRACE envvar actually does
 # something.
-genltl --kr-nlogn=2 | SPOT_BDD_TRACE=1 ltl2tgba -D >out 2>err
+genltl --kr-nlogn=2 |
+    SPOT_BDD_TRACE=1 ltl2tgba -x tls-max-states=0 -D >out 2>err
 cat err
 grep spot: out && exit 1
 grep 'spot: BDD package initialized' err
@@ -34,3 +35,10 @@ test 11 = `grep -c 'spot: BDD GC' err`
 # Minimal size for this automaton.
 # See also https://www.lrde.epita.fr/dload/spot/mochart10-fixes.pdf
 test "147,207" = `autfilt --stats=%s,%e out`
+
+# With the default value of tls-max-states, no GC is needed
+genltl --kr-nlogn=2 | SPOT_BDD_TRACE=1 ltl2tgba -D --stats=%s,%e >out 2>err
+cat err
+grep 'spot: BDD package initialized' err
+test 0 = `grep -c 'spot: BDD GC' err`
+test "147,207" = `cat out`