diff --git a/ChangeLog b/ChangeLog
index 2fca4c107..3f583ef4a 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,16 @@
 2006-07-19  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/ltlvisit/contain.hh, src/ltlvisit/contain.cc (reduce_tau03):
+	New function, performing LTL reduction a la tauriainen.03.a83.
+	* src/ltltest/equals.cc, src/ltltest/reduc.cc: Add support for
+	the new reduction.
+	* src/ltltest/reduc.test: Cut the test in half, and additionally
+	test the new reduction.
+	* src/ltltest/reduccmp.test: Run on the new reduction.
+	* src/ltltest/Makefile.am: Adjust.
+	* src/tgbatest/ltl2tgba.cc: Add new options to apply the reduction.
+	* src/tgbatest/spotlbtt.test: Use them.
+
 	* src/tgba/tgbaproduct.cc: Fix computation of common acceptance
 	conditions.
 
diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am
index 99d8fb66d..642001944 100644
--- a/src/ltltest/Makefile.am
+++ b/src/ltltest/Makefile.am
@@ -1,6 +1,6 @@
-## Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
-## département Systèmes Répartis Coopératifs (SRC), Université Pierre
-## et Marie Curie.
+## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
+## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
+## Université Pierre et Marie Curie.
 ##
 ## This file is part of Spot, a model checking library.
 ##
@@ -19,7 +19,7 @@
 ## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
 ## 02111-1307, USA.
 
-AM_CPPFLAGS = -I$(srcdir)/..
+AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS)
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 LDADD = ../libspot.la
 
@@ -33,6 +33,8 @@ check_PROGRAMS = \
   nenoform \
   reduc \
   reduccmp \
+  reductau \
+  reductaustr \
   syntimpl \
   tostring \
   tunabbrev \
@@ -53,6 +55,10 @@ randltl_SOURCES = randltl.cc
 reduc_SOURCES = reduc.cc
 reduccmp_SOURCES = equals.cc
 reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC
+reductau_SOURCES = equals.cc
+reductau_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAU
+reductaustr_SOURCES = equals.cc
+reductaustr_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAUSTR
 syntimpl_SOURCES = syntimpl.cc
 tostring_SOURCES = tostring.cc
 tunabbrev_SOURCES = equals.cc
diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc
index b426f349e..287c5b0cb 100644
--- a/src/ltltest/equals.cc
+++ b/src/ltltest/equals.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -27,6 +27,7 @@
 #include "ltlvisit/dump.hh"
 #include "ltlvisit/nenoform.hh"
 #include "ltlvisit/destroy.hh"
+#include "ltlvisit/contain.hh"
 #include "ltlast/allnodes.hh"
 #include "ltlvisit/reduce.hh"
 #include "ltlvisit/tostring.hh"
@@ -96,6 +97,20 @@ main(int argc, char** argv)
   spot::ltl::destroy(tmp);
   spot::ltl::dump(std::cout, f1);
 #endif
+#ifdef REDUC_TAU
+  spot::ltl::formula* tmp;
+  tmp = f1;
+  f1 = spot::ltl::reduce_tau03(f1, false);
+  spot::ltl::destroy(tmp);
+  spot::ltl::dump(std::cout, f1);
+#endif
+#ifdef REDUC_TAUSTR
+  spot::ltl::formula* tmp;
+  tmp = f1;
+  f1 = spot::ltl::reduce_tau03(f1, true);
+  spot::ltl::destroy(tmp);
+  spot::ltl::dump(std::cout, f1);
+#endif
 
   int exit_code = f1 != f2;
 
diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc
index 5ca105cbe..63e9d774b 100644
--- a/src/ltltest/reduc.cc
+++ b/src/ltltest/reduc.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -30,6 +30,7 @@
 #include "ltlvisit/tostring.hh"
 #include "ltlvisit/reduce.hh"
 #include "ltlvisit/length.hh"
+#include "ltlvisit/contain.hh"
 #include "ltlast/allnodes.hh"
 
 void
@@ -42,6 +43,9 @@ syntax(char* prog)
 int
 main(int argc, char** argv)
 {
+  bool tau03 = false;
+  bool stronger = false;
+
   if (argc < 3)
     syntax(argv[0]);
 
@@ -57,6 +61,9 @@ main(int argc, char** argv)
     case 2:
       o = spot::ltl::Reduce_Eventuality_And_Universality;
       break;
+    case 9:
+      tau03 = stronger = true;
+      /* fall through */
     case 3:
       o = spot::ltl::Reduce_All;
       break;
@@ -71,6 +78,12 @@ main(int argc, char** argv)
       o = (spot::ltl::Reduce_Syntactic_Implications
 	   | spot::ltl::Reduce_Eventuality_And_Universality);
       break;
+    case 8:
+      stronger = true;
+      /* fall through */
+    case 7:
+      tau03 = true;
+      break;
     default:
       return 2;
   }
@@ -114,6 +127,13 @@ main(int argc, char** argv)
   spot::ltl::destroy(ftmp1);
   spot::ltl::destroy(ftmp2);
 
+  if (tau03)
+    {
+      ftmp1 = f1;
+      f1 = spot::ltl::reduce_tau03(f1, stronger);
+      spot::ltl::destroy(ftmp1);
+    }
+
   int length_f1_after = spot::ltl::length(f1);
   std::string f1s_after = spot::ltl::to_string(f1);
 
diff --git a/src/ltltest/reduc.test b/src/ltltest/reduc.test
index f50a7fcaf..3b94c0e6c 100755
--- a/src/ltltest/reduc.test
+++ b/src/ltltest/reduc.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2004, 2005, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -28,12 +28,13 @@ set -e
 
 FILE=formulae
 : > $FILE
-for i in 10 11 12 13 14 15 16 17 18 19 20; do
+# for i in 10 11 12 13 14 15 16 17 18 19 20; do
+for i in 10 12 14 16 18 20; do
   run 0 ./randltl -u -s 0   -f $i a b c -F 100 >> $FILE
   run 0 ./randltl -u -s 100 -f $i a b c d e f -F 100 >> $FILE
 done
 
-for opt in 0 1 2 3; do
+for opt in 0 1 2 3 7 8 9; do
   rm -f result.data
 
   cat $FILE |
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index 0c68125da..a8684d108 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+# Copyright (C) 2004, 2006  Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
 #
@@ -21,81 +21,87 @@
 # 02111-1307, USA.
 
 
-# Check for the equals visitor
+# Check LTL reductions
 
 . ./defs || exit 1
 
-# No reduction
-run 0 ./reduccmp 'a U b' 'a U b'
-run 0 ./reduccmp 'a R b' 'a R b'
-run 0 ./reduccmp 'a & b' 'a & b'
-run 0 ./reduccmp 'a | b' 'a | b'
-run 0 ./reduccmp 'a & (a U b)' 'a & (a U b)'
-run 0 ./reduccmp 'a | (a U b)' 'a | (a U b)'
+for x in ./reduccmp ./reductaustr; do
 
-# Syntactic reduction
-run 0 ./reduccmp 'a & (!b R !a)' 'false'
-run 0 ./reduccmp '(!b R !a) & a' 'false'
-#run 0 ./reduccmp '(!b R !a) | a' 'true'
-#run 0 ./reduccmp 'a | (!b R !a)' 'true'
+  # No reduction
+  run 0 $x 'a U b' 'a U b'
+  run 0 $x 'a R b' 'a R b'
+  run 0 $x 'a & b' 'a & b'
+  run 0 $x 'a | b' 'a | b'
+  run 0 $x 'a & (a U b)' 'a & (a U b)'
+  run 0 $x 'a | (a U b)' 'a | (a U b)'
 
-run 0 ./reduccmp 'a & (!b R !a) & c' 'false'
-run 0 ./reduccmp 'c & (!b R !a) & a' 'false'
-#run 0 ./reduccmp 'a | (!b R !a) | c' 'true'
-#run 0 ./reduccmp 'c | (!b R !a) | a' 'true'
+  # Syntactic reduction
+  run 0 $x 'a & (!b R !a)' 'false'
+  run 0 $x '(!b R !a) & a' 'false'
 
-run 0 ./reduccmp 'a & (b U a)' 'a'
-run 0 ./reduccmp '(b U a) & a' 'a'
-run 0 ./reduccmp 'a | (b U a)' '(b U a)'
-run 0 ./reduccmp '(b U a) | a' '(b U a)'
-run 0 ./reduccmp 'a U (b U a)' '(b U a)'
+  run 0 $x 'a & (!b R !a) & c' 'false'
+  run 0 $x 'c & (!b R !a) & a' 'false'
 
-run 0 ./reduccmp 'a & (b U a) & a' 'a'
-run 0 ./reduccmp 'a & (b U a) & a' 'a'
-run 0 ./reduccmp 'a | (b U a) | a' '(b U a)'
-run 0 ./reduccmp 'a | (b U a) | a' '(b U a)'
-run 0 ./reduccmp 'a U (b U a)' '(b U a)'
+  run 0 $x 'a & (b U a)' 'a'
+  run 0 $x '(b U a) & a' 'a'
+  run 0 $x 'a | (b U a)' '(b U a)'
+  run 0 $x '(b U a) | a' '(b U a)'
+  run 0 $x 'a U (b U a)' '(b U a)'
+
+  run 0 $x 'a & (b U a) & a' 'a'
+  run 0 $x 'a & (b U a) & a' 'a'
+  run 0 $x 'a | (b U a) | a' '(b U a)'
+  run 0 $x 'a | (b U a) | a' '(b U a)'
+  run 0 $x 'a U (b U a)' '(b U a)'
 
 
-# Basics reduction
-run 0 ./reduccmp 'X(true)' 'true'
-run 0 ./reduccmp 'X(false)' 'false'
-run 0 ./reduccmp 'F(true)' 'true'
-run 0 ./reduccmp 'F(false)' 'false'
-run 0 ./reduccmp 'G(true)' 'true'
-run 0 ./reduccmp 'G(false)' 'false'
+  # Basics reduction
+  run 0 $x 'X(true)' 'true'
+  run 0 $x 'X(false)' 'false'
+  run 0 $x 'F(true)' 'true'
+  run 0 $x 'F(false)' 'false'
+  run 0 $x 'G(true)' 'true'
+  run 0 $x 'G(false)' 'false'
 
-run 0 ./reduccmp 'XGF(f)' 'GF(f)'
-run 0 ./reduccmp 'FX(a)' 'XF(a)'
-run 0 ./reduccmp 'G(a R b)' 'G(b)'
-run 0 ./reduccmp 'GX(a)' 'XG(a)'
+  run 0 $x 'XGF(f)' 'GF(f)'
+  case $x in
+   *tau*);;
+   *)
+     run 0 $x 'G(a R b)' 'G(b)'
 
-run 0 ./reduccmp 'X(a) U X(b)' 'X(a U b)'
-run 0 ./reduccmp 'X(a) R X(b)' 'X(a R b)'
+     run 0 $x 'FX(a)' 'XF(a)'
+     run 0 $x 'GX(a)' 'XG(a)'
 
-run 0 ./reduccmp 'Xa & Xb' 'X(a & b)'
-run 0 ./reduccmp '(a U b) & (c U b)' '(a & c) U b'
-run 0 ./reduccmp '(a R b) & (a R c)' 'a R (b & c)'
-run 0 ./reduccmp 'Xa | Xb' 'X(a | b)'
-run 0 ./reduccmp '(a U b) | (a U c)' 'a U (b | c)'
-run 0 ./reduccmp '(a R b) | (c R b)' '(a | c) R b'
+     run 0 $x 'X(a) U X(b)' 'X(a U b)'
+     run 0 $x 'X(a) R X(b)' 'X(a R b)'
+     run 0 $x 'Xa & Xb' 'X(a & b)'
+     run 0 $x 'Xa | Xb' 'X(a | b)'
 
-run 0 ./reduccmp 'X(a & GFb)' 'Xa & GFb'
-run 0 ./reduccmp 'X(a | GFb)' 'Xa | GFb'
-run 0 ./reduccmp 'F(a & GFb)' 'Fa & GFb'
-run 0 ./reduccmp 'G(a | GFb)' 'Ga | GFb'
+     run 0 $x '(a U b) & (c U b)' '(a & c) U b'
+     run 0 $x '(a R b) & (a R c)' 'a R (b & c)'
+     run 0 $x '(a U b) | (a U c)' 'a U (b | c)'
+     run 0 $x '(a R b) | (c R b)' '(a | c) R b'
 
-run 0 ./reduccmp 'X(a & GFb & c)' 'X(a & c) & GFb'
-run 0 ./reduccmp 'X(a | GFb | c)' 'X(a | c) | GFb'
-run 0 ./reduccmp 'F(a & GFb & c)' 'F(a & c) & GFb'
-run 0 ./reduccmp 'G(a | GFb | c)' 'G(a | c) | GFb'
+     run 0 $x 'X(a & GFb)' 'Xa & GFb'
+     run 0 $x 'X(a | GFb)' 'Xa | GFb'
+     run 0 $x 'F(a & GFb)' 'Fa & GFb'
+     run 0 $x 'G(a | GFb)' 'Ga | GFb'
 
-# Eventuality and universality class reduction
-run 0 ./reduccmp 'FFa' 'Fa'
-run 0 ./reduccmp 'FGFa' 'GFa'
-run 0 ./reduccmp 'b U Fa' 'Fa'
-run 0 ./reduccmp 'b U GFa' 'GFa'
-run 0 ./reduccmp 'Ga' 'Ga'
-run 0 ./reduccmp 'GFGa' 'FGa'
-run 0 ./reduccmp 'b R Ga' 'Ga'
-run 0 ./reduccmp 'b R FGa' 'FGa'
+     run 0 $x 'X(a & GFb & c)' 'X(a & c) & GFb'
+     run 0 $x 'X(a | GFb | c)' 'X(a | c) | GFb'
+     run 0 $x 'F(a & GFb & c)' 'F(a & c) & GFb'
+     run 0 $x 'G(a | GFb | c)' 'G(a | c) | GFb'
+     ;;
+  esac
+
+  # Eventuality and universality class reduction
+  run 0 $x 'FFa' 'Fa'
+  run 0 $x 'FGFa' 'GFa'
+  run 0 $x 'b U Fa' 'Fa'
+  run 0 $x 'b U GFa' 'GFa'
+  run 0 $x 'Ga' 'Ga'
+  run 0 $x 'GFGa' 'FGa'
+  run 0 $x 'b R Ga' 'Ga'
+  run 0 $x 'b R FGa' 'FGa'
+
+done
diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc
index f4a463bea..f1e03ed78 100644
--- a/src/ltlvisit/contain.cc
+++ b/src/ltlvisit/contain.cc
@@ -22,10 +22,16 @@
 #include "contain.hh"
 #include "destroy.hh"
 #include "clone.hh"
+#include "tunabbrev.hh"
 #include "ltlast/unop.hh"
+#include "ltlast/binop.hh"
+#include "ltlast/multop.hh"
+#include "ltlast/constant.hh"
 #include "tgba/tgbaproduct.hh"
 #include "tgbaalgos/gtec/gtec.hh"
-
+#include "tgbaalgos/save.hh"
+#include "tostring.hh"
+#include <iostream>
 namespace spot
 {
   namespace ltl
@@ -64,6 +70,32 @@ namespace spot
       return res;
     }
 
+    // Check whether L(!l) is a subset of L(g).
+    bool
+    language_containment_checker::neg_contained(const formula* l,
+						const formula* g)
+    {
+      const formula* nl = unop::instance(unop::Not, clone(l));
+      const record_* rnl = register_formula_(nl);
+      const formula* ng = unop::instance(unop::Not, clone(g));
+      const record_* rng = register_formula_(ng);
+      destroy(nl);
+      destroy(ng);
+      bool res = rnl->incompatible.find(rng) != rnl->incompatible.end();
+      return res;
+    }
+
+    // Check whether L(l) is a subset of L(!g).
+    bool
+    language_containment_checker::contained_neg(const formula* l,
+						const formula* g)
+    {
+      const record_* rl = register_formula_(l);
+      const record_* rg = register_formula_(g);
+      bool res = rl->incompatible.find(rg) != rl->incompatible.end();
+      return res;
+    }
+
     // Check whether L(l) = L(g).
     bool
     language_containment_checker::equal(const formula* l, const formula* g)
@@ -105,5 +137,217 @@ namespace spot
 	}
       return &r;
     }
+
+
+    namespace {
+      struct reduce_tau03_visitor : public clone_visitor {
+	bool stronger;
+	language_containment_checker* lcc;
+
+	reduce_tau03_visitor(bool stronger,
+			     language_containment_checker* lcc)
+	  : stronger(stronger), lcc(lcc)
+	{
+	}
+
+	void
+	visit(unop* uo)
+	{
+	  formula* a = recurse(uo->child());
+	  switch (uo->op())
+	    {
+	    case unop::X:
+	      // if X(a) = a, then keep only a !
+	      if (stronger && lcc->equal(a, uo))
+		{
+		  result_ = a;
+		  break;
+		}
+	    default:
+	      result_ = unop::instance(uo->op(), a);
+	    }
+	}
+
+	void
+	visit(binop* bo)
+	{
+	  formula* a = recurse(bo->first());
+	  formula* b = recurse(bo->second());
+	  switch (bo->op())
+	    {
+	    case binop::U:
+	      // if (a U b) = b, then keep b !
+	      if (stronger && lcc->equal(bo, b))
+		{
+		  destroy(a);
+		  result_ = b;
+		}
+	      // if a => b,  then a U b = b.
+	      else if ((!stronger) && lcc->contained(a, b))
+		{
+		  destroy(a);
+		  result_ = b;
+		}
+	      // if !a => b, then  a U b = Fb
+	      else if (lcc->neg_contained(a, b))
+		{
+		  destroy(a);
+		  result_ = unop::instance(unop::F, b);
+		}
+	      else
+		{
+		  result_ = binop::instance(binop::U, a, b);
+		}
+	      break;
+	    case binop::R:
+	      // if (a R b) = b, then keep b !
+	      if (stronger && lcc->equal(bo, b))
+		{
+		  destroy(a);
+		  result_ = b;
+		}
+	      // if b => a,  then a R b = b.
+	      else if ((!stronger) && lcc->contained(b, a))
+		{
+		  destroy(a);
+		  result_ = b;
+		}
+	      // if a => !b, then  a R b = Gb
+	      else if (lcc->contained_neg(a, b))
+		{
+		  destroy(a);
+		  result_ = unop::instance(unop::G, b);
+		}
+	      else
+		{
+		  result_ = binop::instance(binop::R, a, b);
+		}
+	      break;
+	    default:
+	      result_ = binop::instance(bo->op(), a, b);
+	    }
+	}
+
+	void
+	visit(multop* mo)
+	{
+	  multop::vec* res = new multop::vec;
+	  unsigned mos = mo->size();
+	  for (unsigned i = 0; i < mos; ++i)
+	    res->push_back(recurse(mo->nth(i)));
+	  result_ = 0;
+	  bool changed = false;
+
+	  switch (mo->op())
+	    {
+	    case multop::Or:
+	      for (unsigned i = 0; i < mos; ++i)
+		{
+		  if (!(*res)[i])
+		    continue;
+		  for (unsigned j = i + 1; j < mos; ++j)
+		    {
+		      if (!(*res)[j])
+			continue;
+		      // if !i => j, then i|j = true
+		      if (lcc->neg_contained((*res)[i], (*res)[j]))
+			{
+			  result_ = constant::true_instance();
+			  goto constant_;
+			}
+		      // if i => j, then i|j = j
+		      else if (lcc->contained((*res)[i], (*res)[j]))
+			{
+			  destroy((*res)[i]);
+			  (*res)[i] = 0;
+			  changed = true;
+			  break;
+			}
+		      // if j => i, then i|j = i
+		      else if (lcc->contained((*res)[i], (*res)[j]))
+			{
+			  destroy((*res)[j]);
+			  (*res)[j] = 0;
+			  changed = true;
+			}
+		    }
+		}
+	      break;
+	    case multop::And:
+	      for (unsigned i = 0; i < mos; ++i)
+		{
+		  if (!(*res)[i])
+		    continue;
+		  for (unsigned j = i + 1; j < mos; ++j)
+		    {
+		      if (!(*res)[j])
+			continue;
+		      // if i => !j, then i&j = false
+		      if (lcc->contained_neg((*res)[i], (*res)[j]))
+			{
+			  result_ = constant::false_instance();
+			  goto constant_;
+			}
+		      // if i => j, then i&j = i
+		      else if (lcc->contained((*res)[i], (*res)[j]))
+			{
+			  destroy((*res)[j]);
+			  (*res)[j] = 0;
+			  changed = true;
+			}
+		      // if j => i, then i&j = j
+		      else if (lcc->contained((*res)[i], (*res)[j]))
+			{
+			  destroy((*res)[i]);
+			  (*res)[i] = 0;
+			  changed = true;
+			  break;
+			}
+		    }
+		}
+	      break;
+	    }
+	  if (changed)
+	    {
+	      multop::vec* nres = new multop::vec;
+	      for (unsigned i = 0; i < mos; ++i)
+		if ((*res)[i])
+		  nres->push_back((*res)[i]);
+	      delete res;
+	      res = nres;
+	    }
+	  result_ = multop::instance(mo->op(), res);
+	  return;
+	constant_:
+	  for (unsigned i = 0; i < mos; ++i)
+	    if ((*res)[i])
+	      destroy((*res)[i]);
+	}
+
+	formula*
+	recurse(formula* f)
+	{
+	  reduce_tau03_visitor v(stronger, lcc);
+	  const_cast<formula*>(f)->accept(v);
+	  return v.result();
+	}
+      };
+    }
+
+    formula*
+    reduce_tau03(const formula* f, bool stronger)
+    {
+      bdd_dict b;
+      reduce_tau03_visitor v(stronger,
+			     new language_containment_checker(&b,
+							      true, true,
+							      false, false));
+      // reduce_tau03_visitor does not handle Xor, Implies, and Equiv.
+      f = unabbreviate_ltl(f);
+      const_cast<formula*>(f)->accept(v);
+      destroy(f);
+      delete v.lcc;
+      return v.result();
+    }
   }
 }
diff --git a/src/ltlvisit/contain.hh b/src/ltlvisit/contain.hh
index a0bad63f5..68d3eff00 100644
--- a/src/ltlvisit/contain.hh
+++ b/src/ltlvisit/contain.hh
@@ -54,6 +54,10 @@ namespace spot
 
       /// Check whether L(l) is a subset of L(g).
       bool contained(const formula* l, const formula* g);
+      /// Check whether L(!l) is a subset of L(g).
+      bool neg_contained(const formula* l, const formula* g);
+      /// Check whether L(l) is a subset of L(!g).
+      bool contained_neg(const formula* l, const formula* g);
 
       /// Check whether L(l) = L(g).
       bool equal(const formula* l, const formula* g);
@@ -70,6 +74,32 @@ namespace spot
       /* Translation Maps */
       trans_map translated_;
     };
+
+    /// \brief Reduce a formula using language containment relationships.
+    ///
+    /// The method is taken from table 4.1 in
+    /// \verbatim
+    ///@TechReport{	  tauriainen.03.a83,
+    ///  author	= {Heikki Tauriainen},
+    ///  title = {On Translating Linear Temporal Logic into Alternating and
+    ///		  Nondeterministic Automata},
+    ///  institution	= {Helsinki University of Technology, Laboratory for
+    ///		           Theoretical Computer Science},
+    ///  address	= {Espoo, Finland},
+    ///  month		= dec,
+    ///  number	        = {A83},
+    ///  pages		= {132},
+    ///  type		= {Research Report},
+    ///  year		= {2003},
+    ///  note		= {Reprint of Licentiate's thesis}
+    ///}
+    ///
+    /// (The "dagged" cells in the tables are not handled here.)
+    ///
+    /// If \a stronger is set, additional rules are used to further
+    /// reduce some U, R, and X usages.
+    /// \endverbatim
+    formula* reduce_tau03(const formula* f, bool stronger = false);
   }
 }
 
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index cacd6a2bc..87dc6997b 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -26,6 +26,7 @@
 #include <string>
 #include "ltlvisit/destroy.hh"
 #include "ltlvisit/reduce.hh"
+#include "ltlvisit/contain.hh"
 #include "ltlvisit/tostring.hh"
 #include "ltlvisit/apcollect.hh"
 #include "ltlast/allnodes.hh"
@@ -100,7 +101,10 @@ syntax(char* prog)
 	    << "and universality" << std::endl
 	    << "  -r3   reduce formula using implication between "
 	    << "sub-formulae" << std::endl
-	    << "  -r4   reduce formula using all rules" << std::endl
+	    << "  -r4   reduce formula using all above rules" << std::endl
+	    << "  -r5   reduce formula using tau03" << std::endl
+	    << "  -r6   reduce formula using tau03+" << std::endl
+	    << "  -r7   reduce formula using tau03+ and -r4" << std::endl
 	    << "  -rd   display the reduce formula" << std::endl
 	    << "  -R    same as -r, but as a set" << std::endl
 	    << "  -R1q  merge states using direct simulation "
@@ -163,6 +167,8 @@ main(int argc, char** argv)
   bool from_file = false;
   int reduc_aut = spot::Reduce_None;
   int redopt = spot::ltl::Reduce_None;
+  bool redtau = false;
+  bool stronger = false;
   bool display_reduce_form = false;
   bool display_rel_sim = false;
   bool display_parity_game = false;
@@ -343,6 +349,19 @@ main(int argc, char** argv)
 	{
 	  redopt |= spot::ltl::Reduce_All;
 	}
+      else if (!strcmp(argv[formula_index], "-r5"))
+	{
+	  redtau = true;
+	}
+      else if (!strcmp(argv[formula_index], "-r6"))
+	{
+	  redtau = stronger = true;
+	}
+      else if (!strcmp(argv[formula_index], "-r7"))
+	{
+	  redopt |= spot::ltl::Reduce_All;
+	  redtau = stronger = true;
+	}
       else if (!strcmp(argv[formula_index], "-R"))
 	{
 	  output = 3;
@@ -498,6 +517,14 @@ main(int argc, char** argv)
 	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
 	      spot::ltl::destroy(f);
 	      f = t;
+	      if (display_reduce_form && !redtau)
+		std::cout << spot::ltl::to_string(f) << std::endl;
+	    }
+	  if (redtau)
+	    {
+	      spot::ltl::formula* t = spot::ltl::reduce_tau03(f, stronger);
+	      spot::ltl::destroy(f);
+	      f = t;
 	      if (display_reduce_form)
 		std::cout << spot::ltl::to_string(f) << std::endl;
 	    }
diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test
index 8a168758c..8911ad7cd 100755
--- a/src/tgbatest/spotlbtt.test
+++ b/src/tgbatest/spotlbtt.test
@@ -108,11 +108,19 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), reduction7 of formula (pre reduction)"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spot './ltl2tgba -r7 -F -f -t'"
+   Enabled = yes
+}
+
 Algorithm
 {
    Name = "Spot (Couvreur -- FM) containments + reduction of formula (pre reduction)"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot './ltl2tgba -r4 -F -f -c -t'"
+   Parameters = "--spot './ltl2tgba -r7 -F -f -c -t'"
    Enabled = yes
 }