diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc
index bade58393..c230ef979 100644
--- a/src/ltltest/equals.cc
+++ b/src/ltltest/equals.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -99,6 +99,7 @@ main(int argc, char** argv)
   f1 = spot::ltl::reduce(f1);
   tmp->destroy();
   spot::ltl::dump(std::cout, f1);
+  std::cout << std::endl;
 #endif
 #ifdef REDUC_TAU
   spot::ltl::formula* tmp;
@@ -106,6 +107,7 @@ main(int argc, char** argv)
   f1 = spot::ltl::reduce_tau03(f1, false);
   tmp->destroy();
   spot::ltl::dump(std::cout, f1);
+  std::cout << std::endl;
 #endif
 #ifdef REDUC_TAUSTR
   spot::ltl::formula* tmp;
@@ -113,16 +115,23 @@ main(int argc, char** argv)
   f1 = spot::ltl::reduce_tau03(f1, true);
   tmp->destroy();
   spot::ltl::dump(std::cout, f1);
+  std::cout << std::endl;
 #endif
 
   int exit_code = f1 != f2;
 
   f1->destroy();
   f2->destroy();
+
+  spot::ltl::atomic_prop::dump_instances(std::cerr);
+  spot::ltl::unop::dump_instances(std::cerr);
+  spot::ltl::binop::dump_instances(std::cerr);
+  spot::ltl::multop::dump_instances(std::cerr);
+  spot::ltl::automatop::dump_instances(std::cerr);
   assert(spot::ltl::atomic_prop::instance_count() == 0);
   assert(spot::ltl::unop::instance_count() == 0);
   assert(spot::ltl::binop::instance_count() == 0);
   assert(spot::ltl::multop::instance_count() == 0);
-
+  assert(spot::ltl::automatop::instance_count() == 0);
   return exit_code;
 }
diff --git a/src/ltltest/syntimpl.cc b/src/ltltest/syntimpl.cc
index 225f25caf..a6b11f761 100644
--- a/src/ltltest/syntimpl.cc
+++ b/src/ltltest/syntimpl.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -67,12 +67,14 @@ main(int argc, char** argv)
   std::string f2s = spot::ltl::to_string(f2);
 
   int exit_return = 0;
+  spot::ltl::syntactic_implication_cache* c =
+    new spot::ltl::syntactic_implication_cache;
 
   switch (opt)
     {
     case 0:
       std::cout << "Test f1 < f2" << std::endl;
-      if (spot::ltl::syntactic_implication(f1, f2))
+      if (c->syntactic_implication(f1, f2))
 	{
 	  std::cout << f1s << " < " << f2s << std::endl;
 	  exit_return = 1;
@@ -81,7 +83,7 @@ main(int argc, char** argv)
 
     case 1:
       std::cout << "Test !f1 < f2" << std::endl;
-      if (spot::ltl::syntactic_implication_neg(f1, f2, false))
+      if (c->syntactic_implication_neg(f1, f2, false))
 	{
 	  std::cout << "!(" << f1s << ") < " << f2s << std::endl;
 	  exit_return = 1;
@@ -90,7 +92,7 @@ main(int argc, char** argv)
 
     case 2:
       std::cout << "Test f1 < !f2" << std::endl;
-      if (spot::ltl::syntactic_implication_neg(f1, f2, true))
+      if (c->syntactic_implication_neg(f1, f2, true))
 	{
 	  std::cout << f1s << " < !(" << f2s << ")" << std::endl;
 	  exit_return = 1;
@@ -107,6 +109,9 @@ main(int argc, char** argv)
   f2->destroy();
   ftmp1->destroy();
   ftmp2->destroy();
+
+  delete c;
+
   assert(spot::ltl::atomic_prop::instance_count() == 0);
   assert(spot::ltl::unop::instance_count() == 0);
   assert(spot::ltl::binop::instance_count() == 0);
diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc
index eba5ac88c..f9552f946 100644
--- a/src/ltlvisit/reduce.cc
+++ b/src/ltlvisit/reduce.cc
@@ -44,8 +44,8 @@ namespace spot
       {
       public:
 
-	reduce_visitor(int opt)
-	  : opt_(opt)
+	reduce_visitor(int opt, syntactic_implication_cache* c)
+	  : opt_(opt), c_(c)
 	{
 	}
 
@@ -164,14 +164,14 @@ namespace spot
 
 		case binop::U:
 		  /* a < b => a U b = b */
-		  if (syntactic_implication(f1, f2))
+		  if (c_->syntactic_implication(f1, f2))
 		    {
 		      result_ = f2;
 		      f1->destroy();
 		      return;
 		    }
 		  /* !b < a => a U b = Fb */
-		  if (syntactic_implication_neg(f2, f1, false))
+		  if (c_->syntactic_implication_neg(f2, f1, false))
 		    {
 		      result_ = unop::instance(unop::F, f2);
 		      f1->destroy();
@@ -183,7 +183,7 @@ namespace spot
 		    {
 		      binop* bo = static_cast<binop*>(f2);
 		      if ((bo->op() == binop::U || bo->op() == binop::W)
-			  && syntactic_implication(f1, bo->first()))
+			  && c_->syntactic_implication(f1, bo->first()))
 			{
 			  result_ = f2;
 			  f1->destroy();
@@ -194,14 +194,14 @@ namespace spot
 
 		case binop::R:
 		  /* b < a => a R b = b */
-		  if (syntactic_implication(f2, f1))
+		  if (c_->syntactic_implication(f2, f1))
 		    {
 		      result_ = f2;
 		      f1->destroy();
 		      return;
 		    }
 		  /* b < !a => a R b = Gb */
-		  if (syntactic_implication_neg(f2, f1, true))
+		  if (c_->syntactic_implication_neg(f2, f1, true))
 		    {
 		      result_ = unop::instance(unop::G, f2);
 		      f1->destroy();
@@ -213,7 +213,7 @@ namespace spot
 		      /* b < a => a R (b M c) = b M c */
 		      binop* bo = static_cast<binop*>(f2);
 		      if ((bo->op() == binop::R || bo->op() == binop::M)
-			  && syntactic_implication(bo->first(), f1))
+			  && c_->syntactic_implication(bo->first(), f1))
 			{
 			  result_ = f2;
 			  f1->destroy();
@@ -222,7 +222,7 @@ namespace spot
 
 		      /* a < b => a R (b R c) = a R c */
 		      if (bo->op() == binop::R
-			  && syntactic_implication(f1, bo->first()))
+			  && c_->syntactic_implication(f1, bo->first()))
 			{
 			  result_ = binop::instance(binop::R, f1,
 						    bo->second()->clone());
@@ -234,14 +234,14 @@ namespace spot
 
 		case binop::W:
 		  /* a < b => a W b = b */
-		  if (syntactic_implication(f1, f2))
+		  if (c_->syntactic_implication(f1, f2))
 		    {
 		      result_ = f2;
 		      f1->destroy();
 		      return;
 		    }
 		  /* !b < a => a W b = 1 */
-		  if (syntactic_implication_neg(f2, f1, false))
+		  if (c_->syntactic_implication_neg(f2, f1, false))
 		    {
 		      result_ = constant::true_instance();
 		      f1->destroy();
@@ -253,7 +253,7 @@ namespace spot
 		    {
 		      binop* bo = static_cast<binop*>(f2);
 		      if (bo->op() == binop::W
-			  && syntactic_implication(f1, bo->first()))
+			  && c_->syntactic_implication(f1, bo->first()))
 			{
 			  result_ = f2;
 			  f1->destroy();
@@ -264,14 +264,14 @@ namespace spot
 
 		case binop::M:
 		  /* b < a => a M b = b */
-		  if (syntactic_implication(f2, f1))
+		  if (c_->syntactic_implication(f2, f1))
 		    {
 		      result_ = f2;
 		      f1->destroy();
 		      return;
 		    }
 		  /* b < !a => a M b = 0 */
-		  if (syntactic_implication_neg(f2, f1, true))
+		  if (c_->syntactic_implication_neg(f2, f1, true))
 		    {
 		      result_ = constant::false_instance();
 		      f1->destroy();
@@ -283,7 +283,7 @@ namespace spot
 		      /* b < a => a M (b M c) = b M c */
 		      binop* bo = static_cast<binop*>(f2);
 		      if (bo->op() == binop::M
-			  && syntactic_implication(bo->first(), f1))
+			  && c_->syntactic_implication(bo->first(), f1))
 			{
 			  result_ = f2;
 			  f1->destroy();
@@ -293,7 +293,7 @@ namespace spot
 		      /* a < b => a M (b M c) = a M c */
 		      /* a < b => a M (b R c) = a M c */
 		      if ((bo->op() == binop::M || bo->op() == binop::R)
-			  && syntactic_implication(f1, bo->first()))
+			  && c_->syntactic_implication(f1, bo->first()))
 			{
 			  result_ = binop::instance(binop::M, f1,
 						    bo->second()->clone());
@@ -340,9 +340,9 @@ namespace spot
 		      assert(f1 != f2);
 		      // a < b => a + b = b
 		      // a < b => a & b = a
-		      if ((syntactic_implication(*f1, *f2) && // f1 < f2
+		      if ((c_->syntactic_implication(*f1, *f2) && // f1 < f2
 			   (mo->op() == multop::Or)) ||
-			  ((syntactic_implication(*f2, *f1)) && // f2 < f1
+			  ((c_->syntactic_implication(*f2, *f1)) && // f2 < f1
 			   (mo->op() == multop::And)))
 			{
 			  // We keep f2
@@ -351,10 +351,10 @@ namespace spot
 			  removed = true;
 			  break;
 			}
-		      else if ((syntactic_implication(*f2, *f1) && // f2 < f1
-				(mo->op() == multop::Or)) ||
-			       ((syntactic_implication(*f1, *f2)) && // f1 < f2
-				(mo->op() == multop::And)))
+		      else if ((c_->syntactic_implication(*f2, *f1) // f2 < f1
+				&& (mo->op() == multop::Or)) ||
+			       ((c_->syntactic_implication(*f1, *f2)) // f1 < f2
+				&& (mo->op() == multop::And)))
 			{
 			  // We keep f1
 			  (*f2)->destroy();
@@ -372,8 +372,8 @@ namespace spot
 	      for (f1 = res->begin(); f1 != res->end(); f1++)
 		for (f2 = res->begin(); f2 != res->end(); f2++)
 		  if (f1 != f2 &&
-		      syntactic_implication_neg(*f1, *f2,
-						mo->op() !=  multop::Or))
+		      c_->syntactic_implication_neg(*f1, *f2,
+						    mo->op() !=  multop::Or))
 		    {
 		      for (multop::vec::iterator j = res->begin();
 			   j != res->end(); j++)
@@ -400,23 +400,27 @@ namespace spot
 	formula*
 	recurse(formula* f)
 	{
-	  return reduce(f, opt_);
+	  return reduce(f, opt_, c_);
 	}
 
       protected:
 	formula* result_;
 	int opt_;
+	syntactic_implication_cache* c_;
       };
 
     } // anonymous
 
     formula*
-    reduce(const formula* f, int opt)
+    reduce(const formula* f, int opt, syntactic_implication_cache* c)
     {
       formula* f1;
       formula* f2;
       formula* prev = 0;
 
+      syntactic_implication_cache* sic =
+	c ? c : new syntactic_implication_cache;
+
       int n = 0;
 
       while (f != prev)
@@ -449,7 +453,7 @@ namespace spot
 	  if (opt & (Reduce_Syntactic_Implications
 		     | Reduce_Eventuality_And_Universality))
 	    {
-	      reduce_visitor v(opt);
+	      reduce_visitor v(opt, sic);
 	      f2->accept(v);
 	      f1 = v.result();
 	      f2->destroy();
@@ -469,6 +473,10 @@ namespace spot
 	  f = f2;
 	}
       prev->destroy();
+
+      if (c == 0)
+	delete sic;
+
       return const_cast<formula*>(f);
     }
 
diff --git a/src/ltlvisit/reduce.hh b/src/ltlvisit/reduce.hh
index 33326770b..564ff40f0 100644
--- a/src/ltlvisit/reduce.hh
+++ b/src/ltlvisit/reduce.hh
@@ -52,13 +52,16 @@ namespace spot
 	Reduce_All = -1U
       };
 
+    class syntactic_implication_cache;
+
     /// \brief Reduce a formula \a f.
     ///
     /// \param f the formula to reduce
     /// \param opt a conjonction of spot::ltl::reduce_options specifying
     ///            which optimizations to apply.
     /// \return the reduced formula
-    formula* reduce(const formula* f, int opt = Reduce_All);
+    formula* reduce(const formula* f, int opt = Reduce_All,
+		    syntactic_implication_cache* c = 0);
     /// @}
 
     /// \brief Check whether a formula is a pure eventuality.
diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc
index 6c3fc8213..0f5b8fe9b 100644
--- a/src/ltlvisit/syntimpl.cc
+++ b/src/ltlvisit/syntimpl.cc
@@ -40,8 +40,9 @@ namespace spot
       {
       public:
 
-	inf_right_recurse_visitor(const formula *f)
-	  : result_(false), f(f)
+	inf_right_recurse_visitor(const formula *f,
+				  syntactic_implication_cache* c)
+	  : result_(false), f(f), c(c)
 	{
 	}
 
@@ -100,16 +101,16 @@ namespace spot
 		  return;
 		const unop* op = static_cast<const unop*>(f);
 		if (op->op() == unop::X)
-		  result_ = syntactic_implication(op->child(), f1);
+		  result_ = c->syntactic_implication(op->child(), f1);
 	      }
 	      return;
 	    case unop::F:
 	      /* F(a) = true U a */
-	      result_ = syntactic_implication(f, f1);
+	      result_ = c->syntactic_implication(f, f1);
 	      return;
 	    case unop::G:
 	      /* G(a) = false R a */
-	      if (syntactic_implication(f, constant::false_instance()))
+	      if (c->syntactic_implication(f, constant::false_instance()))
 		result_ = true;
 	      return;
 	    case unop::Finish:
@@ -137,7 +138,7 @@ namespace spot
 	      return;
 	    case binop::U:
 	    case binop::W:
-	      if (syntactic_implication(f, f2))
+	      if (c->syntactic_implication(f, f2))
 		result_ = true;
 	      return;
 	    case binop::R:
@@ -145,8 +146,8 @@ namespace spot
 		{
 		  const binop* fb = static_cast<const binop*>(f);
 		  if (fb->op() == binop::R
-		      && syntactic_implication(fb->first(), f1)
-		      && syntactic_implication(fb->second(), f2))
+		      && c->syntactic_implication(fb->first(), f1)
+		      && c->syntactic_implication(fb->second(), f2))
 		    {
 		      result_ = true;
 		      return;
@@ -157,14 +158,14 @@ namespace spot
 		  const unop* fu = static_cast<const unop*>(f);
 		  if (fu->op() == unop::G
 		      && f1 == constant::false_instance()
-		      && syntactic_implication(fu->child(), f2))
+		      && c->syntactic_implication(fu->child(), f2))
 		    {
 		      result_ = true;
 		      return;
 		    }
 		}
-	      if (syntactic_implication(f, f1)
-		  && syntactic_implication(f, f2))
+	      if (c->syntactic_implication(f, f1)
+		  && c->syntactic_implication(f, f2))
 		result_ = true;
 	      return;
 	    case binop::M:
@@ -172,8 +173,8 @@ namespace spot
 		{
 		  const binop* fb = static_cast<const binop*>(f);
 		  if (fb->op() == binop::M
-		      && syntactic_implication(fb->first(), f1)
-		      && syntactic_implication(fb->second(), f2))
+		      && c->syntactic_implication(fb->first(), f1)
+		      && c->syntactic_implication(fb->second(), f2))
 		    {
 		      result_ = true;
 		      return;
@@ -184,14 +185,14 @@ namespace spot
 		  const unop* fu = static_cast<const unop*>(f);
 		  if (fu->op() == unop::F
 		      && f2 == constant::true_instance()
-		      && syntactic_implication(fu->child(), f1))
+		      && c->syntactic_implication(fu->child(), f1))
 		  {
 		    result_ = true;
 		    return;
 		  }
 		}
-	      if (syntactic_implication(f, f1)
-		  && syntactic_implication(f, f2))
+	      if (c->syntactic_implication(f, f1)
+		  && c->syntactic_implication(f, f2))
 		result_ = true;
 	      return;
 	    }
@@ -214,13 +215,13 @@ namespace spot
 	    {
 	    case multop::And:
 	      for (unsigned i = 0; i < mos; ++i)
-		if (!syntactic_implication(f, mo->nth(i)))
+		if (!c->syntactic_implication(f, mo->nth(i)))
 		  return;
 	      result_ = true;
 	      break;
 	    case multop::Or:
 	      for (unsigned i = 0; i < mos && !result_; ++i)
-		if (syntactic_implication(f, mo->nth(i)))
+		if (c->syntactic_implication(f, mo->nth(i)))
 		  result_ = true;
 	      break;
 	    case multop::Concat:
@@ -233,6 +234,7 @@ namespace spot
       protected:
 	bool result_; /* true if f < f1, false otherwise. */
 	const formula* f;
+	syntactic_implication_cache* c;
       };
 
       /////////////////////////////////////////////////////////////////////////
@@ -241,8 +243,9 @@ namespace spot
       {
       public:
 
-	inf_left_recurse_visitor(const formula *f)
-	  : result_(false), f(f)
+	inf_left_recurse_visitor(const formula *f,
+				 syntactic_implication_cache* c)
+	  : result_(false), f(f), c(c)
 	{
 	}
 
@@ -258,8 +261,8 @@ namespace spot
 	    return false;
 	  const binop* fb = static_cast<const binop*>(f);
 	  if (fb->op() == f2->op()
-	      && syntactic_implication(f2->first(), fb->first())
-	      && syntactic_implication(f2->second(), fb->second()))
+	      && c->syntactic_implication(f2->first(), fb->first())
+	      && c->syntactic_implication(f2->second(), fb->second()))
 	    return true;
 	  return false;
 	}
@@ -281,7 +284,7 @@ namespace spot
 	void
 	visit(const atomic_prop* ap)
 	{
-	  inf_right_recurse_visitor v(ap);
+	  inf_right_recurse_visitor v(ap, c);
 	  const_cast<formula*>(f)->accept(v);
 	  result_ = v.result();
 	}
@@ -292,10 +295,10 @@ namespace spot
 	}
 
 	void
-	visit(const constant* c)
+	visit(const constant* cst)
 	{
-	  inf_right_recurse_visitor v(c);
-	  switch (c->val())
+	  inf_right_recurse_visitor v(cst, c);
+	  switch (cst->val())
 	    {
 	    case constant::True:
 	      const_cast<formula*>(f)->accept(v);
@@ -316,7 +319,7 @@ namespace spot
 	visit(const unop* uo)
 	{
 	  const formula* f1 = uo->child();
-	  inf_right_recurse_visitor v(uo);
+	  inf_right_recurse_visitor v(uo, c);
 	  switch (uo->op())
 	    {
 	    case unop::Not:
@@ -328,7 +331,7 @@ namespace spot
 		{
 		  const unop* op = static_cast<const unop*>(f);
 		  if (op->op() == unop::X)
-		    result_ = syntactic_implication(f1, op->child());
+		    result_ = c->syntactic_implication(f1, op->child());
 		}
 	      return;
 	    case unop::F:
@@ -343,7 +346,7 @@ namespace spot
 		    tmp->destroy();
 		    return;
 		  }
-		if (syntactic_implication(tmp, f))
+		if (c->syntactic_implication(tmp, f))
 		  result_ = true;
 		tmp->destroy();
 		return;
@@ -360,7 +363,7 @@ namespace spot
 		    tmp->destroy();
 		    return;
 		  }
-		if (syntactic_implication(tmp, f))
+		if (c->syntactic_implication(tmp, f))
 		  result_ = true;
 		tmp->destroy();
 		return;
@@ -400,8 +403,8 @@ namespace spot
 		{
 		  const binop* fb = static_cast<const binop*>(f);
 		  if (fb->op() == binop::U
-		      && syntactic_implication(f1, fb->first())
-		      && syntactic_implication(f2, fb->second()))
+		      && c->syntactic_implication(f1, fb->first())
+		      && c->syntactic_implication(f2, fb->second()))
 		    {
 		      result_ = true;
 		      return;
@@ -412,14 +415,14 @@ namespace spot
 		  const unop* fu = static_cast<const unop*>(f);
 		  if (fu->op() == unop::F
 		      && f1 == constant::true_instance()
-		      && syntactic_implication(f2, fu->child()))
+		      && c->syntactic_implication(f2, fu->child()))
 		    {
 		      result_ = true;
 		      return;
 		    }
 		}
-	      if (syntactic_implication(f1, f)
-		  && syntactic_implication(f2, f))
+	      if (c->syntactic_implication(f1, f)
+		  && c->syntactic_implication(f2, f))
 		result_ = true;
 	      return;
 	    case binop::W:
@@ -428,8 +431,8 @@ namespace spot
 		{
 		  const binop* fb = static_cast<const binop*>(f);
 		  if (fb->op() == binop::W
-		      && syntactic_implication(f1, fb->first())
-		      && syntactic_implication(f2, fb->second()))
+		      && c->syntactic_implication(f1, fb->first())
+		      && c->syntactic_implication(f2, fb->second()))
 		    {
 		      result_ = true;
 		      return;
@@ -440,14 +443,14 @@ namespace spot
 		  const unop* fu = static_cast<const unop*>(f);
 		  if (fu && fu->op() == unop::G
 		      && f2 == constant::false_instance()
-		      && syntactic_implication(f1, fu->child()))
+		      && c->syntactic_implication(f1, fu->child()))
 		    {
 		      result_ = true;
 		      return;
 		    }
 		}
-	      if (syntactic_implication(f1, f)
-		  && syntactic_implication(f2, f))
+	      if (c->syntactic_implication(f1, f)
+		  && c->syntactic_implication(f2, f))
 		result_ = true;
 	      return;
 	    case binop::R:
@@ -456,13 +459,13 @@ namespace spot
 		  const unop* fu = static_cast<const unop*>(f);
 		  if (fu->op() == unop::G
 		      && f1 == constant::false_instance()
-		      && syntactic_implication(f2, fu->child()))
+		      && c->syntactic_implication(f2, fu->child()))
 		  {
 		    result_ = true;
 		    return;
 		  }
 		}
-	      if (syntactic_implication(f2, f))
+	      if (c->syntactic_implication(f2, f))
 		result_ = true;
 	      return;
 	    case binop::M:
@@ -471,13 +474,13 @@ namespace spot
 		  const unop* fu = static_cast<const unop*>(f);
 		  if (fu->op() == unop::F
 		      && f2 == constant::true_instance()
-		      && syntactic_implication(f1, fu->child()))
+		      && c->syntactic_implication(f1, fu->child()))
 		  {
 		    result_ = true;
 		    return;
 		  }
 		}
-	      if (syntactic_implication(f2, f))
+	      if (c->syntactic_implication(f2, f))
 		result_ = true;
 	      return;
 	    }
@@ -500,12 +503,12 @@ namespace spot
 	    {
 	    case multop::And:
 	      for (unsigned i = 0; (i < mos) && !result_; ++i)
-		if (syntactic_implication(mo->nth(i), f))
+		if (c->syntactic_implication(mo->nth(i), f))
 		  result_ = true;
 	      break;
 	    case multop::Or:
 	      for (unsigned i = 0; i < mos; ++i)
-		if (!syntactic_implication(mo->nth(i), f))
+		if (!c->syntactic_implication(mo->nth(i), f))
 		  return;
 	      result_ = true;
 	      break;
@@ -519,6 +522,7 @@ namespace spot
       protected:
 	bool result_; /* true if f1 < f, 1 otherwise. */
 	const formula* f;
+	syntactic_implication_cache* c;
       };
 
     } // anonymous
@@ -526,7 +530,8 @@ namespace spot
     // This is called by syntactic_implication() after the
     // formulae have been normalized.
     bool
-    syntactic_implication(const formula* f1, const formula* f2)
+    syntactic_implication_cache::syntactic_implication(const formula* f1,
+						       const formula* f2)
     {
       if (f1 == f2)
 	return true;
@@ -534,22 +539,43 @@ namespace spot
 	  || f1 == constant::false_instance())
 	return true;
 
-      inf_left_recurse_visitor v1(f2);
-      inf_right_recurse_visitor v2(f1);
+      // Cache lookup
+      {
+	pairf p(f1, f2);
+	cache_t::const_iterator i = cache_.find(p);
+	if (i != cache_.end())
+	  return i->second;
+      }
 
+      bool result = false;
+
+      inf_left_recurse_visitor v1(f2, this);
       const_cast<formula*>(f1)->accept(v1);
       if (v1.result())
-	return true;
+	{
+	  result = true;
+	}
+      else
+	{
+	  inf_right_recurse_visitor v2(f1, this);
+	  const_cast<formula*>(f2)->accept(v2);
+	  if (v2.result())
+	    result = true;
+	}
 
-      const_cast<formula*>(f2)->accept(v2);
-      if (v2.result())
-	return true;
+      // Cache result
+      {
+	pairf p(f1->clone(), f2->clone());
+	cache_[p] = result;
+      }
 
-      return false;
+      return result;
     }
 
     bool
-    syntactic_implication_neg(const formula* f1, const formula* f2, bool right)
+    syntactic_implication_cache::syntactic_implication_neg(const formula* f1,
+							   const formula* f2,
+							   bool right)
     {
       formula* l = f1->clone();
       formula* r = f2->clone();
@@ -558,6 +584,20 @@ namespace spot
       else
 	l = unop::instance(unop::Not, l);
 
+      // Cache lookup
+      {
+	pairf p(l, r);
+	cache_t::const_iterator i = cache_.find(p);
+	if (i != cache_.end())
+	  {
+	    l->destroy();
+	    r->destroy();
+	    return i->second;
+	  }
+      }
+      // Save the cache key for latter.
+      pairf p(l->clone(), r->clone());
+
       formula* tmp = unabbreviate_logic(l);
       l->destroy();
       l = simplify_f_g(tmp);
@@ -577,7 +617,33 @@ namespace spot
       bool result = syntactic_implication(l, r);
       l->destroy();
       r->destroy();
+
+      // Cache result if is has not be done by syntactic_implication() already.
+      if (l != p.first || r != p.second)
+	{
+	  cache_[p] = result;
+	}
+      else
+	{
+	  p.first->destroy();
+	  p.second->destroy();
+	}
       return result;
     }
+
+    syntactic_implication_cache::~syntactic_implication_cache()
+    {
+      cache_t::const_iterator i = cache_.begin();
+      while (i != cache_.end())
+	{
+	  // Advance the iterator before deleting the key.
+	  pairf p = i->first;
+	  ++i;
+
+	  p.first->destroy();
+	  p.second->destroy();
+	}
+    }
+
   }
 }
diff --git a/src/ltlvisit/syntimpl.hh b/src/ltlvisit/syntimpl.hh
index 12addefe2..a91f18f7c 100644
--- a/src/ltlvisit/syntimpl.hh
+++ b/src/ltlvisit/syntimpl.hh
@@ -1,3 +1,5 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Developpement de
+// l'Epita (LRDE).
 // Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -23,6 +25,7 @@
 # define SPOT_LTLVISIT_SYNTIMPL_HH
 
 #include "ltlast/formula.hh"
+#include <map>
 
 namespace spot
 {
@@ -46,17 +49,35 @@ namespace spot
     /// publisher	= {Springer-Verlag}
     /// }
     /// \endverbatim
-    bool syntactic_implication(const formula* f1, const formula* f2);
+    class syntactic_implication_cache
+    {
+    private:
+      typedef std::pair<const formula*, const formula*> pairf;
+      typedef std::map<pairf, bool> cache_t;
+      cache_t cache_;
+      // Copy disallowed.
+      syntactic_implication_cache(const syntactic_implication_cache&);
+    public:
+      syntactic_implication_cache() {};
+
+      /// \brief Syntactic implication.
+      ///
+      /// Return true if f1 < f2.
+      bool syntactic_implication(const formula* f1, const formula* f2);
+
+      /// \brief Syntactic implication.
+      ///
+      /// If right==false, true if !f1 < f2, false otherwise.
+      /// If right==true, true if f1 < !f2, false otherwise.
+      ///
+      /// \see syntactic_implication
+      bool syntactic_implication_neg(const formula* f1, const formula* f2,
+				     bool right);
+
+      ~syntactic_implication_cache();
+    };
+
 
-    /// \brief Syntactic implication.
-    /// \ingroup ltl_misc
-    ///
-    /// If right==false, true if !f1 < f2, false otherwise.
-    /// If right==true, true if f1 < !f2, false otherwise.
-    ///
-    /// \see syntactic_implication
-    bool syntactic_implication_neg(const formula* f1, const formula* f2,
-				   bool right);
   }
 }