diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc
index e1727a124..536a14c14 100644
--- a/src/ltlast/atomic_prop.cc
+++ b/src/ltlast/atomic_prop.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -42,6 +42,7 @@ namespace spot
       is.ltl_formula = true;
       is.eltl_formula = true;
       is.psl_formula = true;
+      is.sere_formula = true;
       is.eventual = false;
       is.universal = false;
       is.not_marked = true;
diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc
index ab13be12a..303842f40 100644
--- a/src/ltlast/automatop.cc
+++ b/src/ltlast/automatop.cc
@@ -1,5 +1,5 @@
-// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Developpement
-// de l'Epita (LRDE)
+// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
+// Developpement de l'Epita (LRDE)
 //
 // This file is part of Spot, a model checking library.
 //
@@ -38,6 +38,7 @@ namespace spot
       is.ltl_formula = false;
       is.eltl_formula = true;
       is.psl_formula = false;
+      is.sere_formula = false;
       is.eventual = false;
       is.universal = false;
       is.not_marked = true;
diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc
index c3b1bba99..020e33139 100644
--- a/src/ltlast/binop.cc
+++ b/src/ltlast/binop.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -54,6 +54,7 @@ namespace spot
 	case Xor:
 	case Implies:
 	case Equiv:
+	  is.sere_formula = is.boolean;
 	  is.sugar_free_boolean = false;
 	  is.in_nenoform = false;
 	  is.accepting_eword = false;
@@ -66,7 +67,11 @@ namespace spot
 	  is.ltl_formula = false;
 	  is.boolean = false;
 	  is.eltl_formula = false;
+	  is.sere_formula = false;
 	  is.accepting_eword = false;
+	  is.psl_formula = true;
+	  assert(first->is_sere_formula());
+	  assert(second->is_psl_formula());
 	  break;
 	case U:
 	  // 1 U a = Fa
@@ -74,6 +79,7 @@ namespace spot
 	    is.eventual = 1;
 	  is.boolean = false;
 	  is.eltl_formula = false;
+	  is.sere_formula = false;
 	  is.accepting_eword = false;
 	  break;
 	case W:
@@ -82,6 +88,7 @@ namespace spot
 	    is.universal = 1;
 	  is.boolean = false;
 	  is.eltl_formula = false;
+	  is.sere_formula = false;
 	  is.accepting_eword = false;
 	  break;
 	case R:
@@ -90,6 +97,7 @@ namespace spot
 	    is.universal = 1;
 	  is.boolean = false;
 	  is.eltl_formula = false;
+	  is.sere_formula = false;
 	  is.accepting_eword = false;
 	  break;
 	case M:
@@ -98,6 +106,7 @@ namespace spot
 	    is.eventual = 1;
 	  is.boolean = false;
 	  is.eltl_formula = false;
+	  is.sere_formula = false;
 	  is.accepting_eword = false;
 	  break;
 	}
diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc
index 3fa4bfab4..487a5f737 100644
--- a/src/ltlast/bunop.cc
+++ b/src/ltlast/bunop.cc
@@ -35,9 +35,11 @@ namespace spot
     {
       props = child->get_props();
 
+      assert(is.sere_formula);
       is.boolean = false;
       is.ltl_formula = false;
       is.eltl_formula = false;
+      is.psl_formula = false;
       is.eventual = false;
       is.universal = false;
 
diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc
index 2fc89c19f..b98daa377 100644
--- a/src/ltlast/constant.cc
+++ b/src/ltlast/constant.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2009, 2010 Laboratoire de Recherche et D�veloppement
+// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et D�veloppement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
 // 6 (LIP6), d�partement Syst�mes R�partis Coop�ratifs (SRC),
@@ -48,6 +48,7 @@ namespace spot
 	  is.ltl_formula = true;
 	  is.eltl_formula = true;
 	  is.psl_formula = true;
+	  is.sere_formula = true;
 	  is.eventual = true;
 	  is.universal = true;
 	  is.not_marked = true;
@@ -61,7 +62,8 @@ namespace spot
 	  is.sugar_free_ltl = true;
 	  is.ltl_formula = false;
 	  is.eltl_formula = false;
-	  is.psl_formula = true;
+	  is.psl_formula = false;
+	  is.sere_formula = true;
 	  is.eventual = false;
 	  is.universal = false;
 	  is.not_marked = true;
diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc
index 92a36fa1d..494db40c6 100644
--- a/src/ltlast/formula.cc
+++ b/src/ltlast/formula.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -83,6 +83,7 @@ namespace spot
       proprint(is_ltl_formula, "L", "LTL formula");
       proprint(is_eltl_formula, "E", "ELTL formula");
       proprint(is_psl_formula, "P", "PSL formula");
+      proprint(is_sere_formula, "S", "SERE formula");
       proprint(is_eventual, "e", "pure eventuality");
       proprint(is_universal, "u", "purely universal");
       proprint(is_marked, "+", "marked");
diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh
index e19aed201..681deb443 100644
--- a/src/ltlast/formula.hh
+++ b/src/ltlast/formula.hh
@@ -1,5 +1,5 @@
-// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et D�veloppement
-// de l'Epita (LRDE).
+// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
 //
 // This file is part of Spot, a model checking library.
@@ -170,6 +170,12 @@ namespace spot
 	return is.psl_formula;
       }
 
+      /// Whether the formula use only SERE operators.
+      bool is_sere_formula() const
+      {
+	return is.sere_formula;
+      }
+
       /// \brief Whether the formula is purely eventual.
       ///
       /// Pure eventuality formulae are defined in
@@ -279,6 +285,7 @@ namespace spot
 	bool ltl_formula:1;	   // Only LTL operators.
 	bool eltl_formula:1;	   // Only ELTL operators.
 	bool psl_formula:1;	   // Only PSL operators.
+	bool sere_formula:1;	   // Only SERE operators.
 	bool eventual:1;	   // Purely eventual formula.
 	bool universal:1;	   // Purely universal formula.
 	bool not_marked:1;	   // No occurrence of EConcatMarked.
diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc
index df1425507..1cd452592 100644
--- a/src/ltlast/multop.cc
+++ b/src/ltlast/multop.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2009, 2010 Laboratoire de Recherche et D�veloppement
+// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et D�veloppement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -39,6 +39,8 @@ namespace spot
       unsigned s = v->size();
       assert(s > 1);
 
+      props = (*v)[0]->get_props();
+
       switch (op)
 	{
 	case Concat:
@@ -46,6 +48,7 @@ namespace spot
 	  is.boolean = false;
 	  is.ltl_formula = false;
 	  is.eltl_formula = false;
+	  is.psl_formula = false;
 	  is.eventual = false;
 	  is.universal = false;
 	  // fall through
@@ -55,14 +58,12 @@ namespace spot
 	  // Boolean flag, because applied to atomic propositions a&b
 	  // has the same effect as a&&b.
 	case And:
-	  props = (*v)[0]->get_props();
 	  for (unsigned i = 1; i < s; ++i)
 	    props &= (*v)[i]->get_props();
 	  break;
 	case Or:
 	  {
 	    bool ew = (*v)[0]->accepts_eword();
-	    props = (*v)[0]->get_props();
 	    for (unsigned i = 1; i < s; ++i)
 	      {
 		ew |= (*v)[i]->accepts_eword();
diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc
index ab9b9c686..df3661768 100644
--- a/src/ltlast/unop.cc
+++ b/src/ltlast/unop.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -40,17 +40,20 @@ namespace spot
 	{
 	case Not:
 	  is.in_nenoform = (child->kind() == AtomicProp);
+	  is.sere_formula = is.boolean;
 	  is.accepting_eword = false;
 	  break;
 	case X:
 	  is.boolean = false;
 	  is.X_free = false;
 	  is.eltl_formula = false;
+	  is.sere_formula = false;
 	  is.accepting_eword = false;
 	  break;
 	case F:
 	  is.boolean = false;
 	  is.eltl_formula = false;
+	  is.sere_formula = false;
 	  is.sugar_free_ltl = false;
 	  is.eventual = true;
 	  is.accepting_eword = false;
@@ -58,6 +61,7 @@ namespace spot
 	case G:
 	  is.boolean = false;
 	  is.eltl_formula = false;
+	  is.sere_formula = false;
 	  is.sugar_free_ltl = false;
 	  is.universal = true;
 	  is.accepting_eword = false;
@@ -66,6 +70,7 @@ namespace spot
 	  is.boolean = false;
 	  is.ltl_formula = false;
 	  is.psl_formula = false;
+	  is.sere_formula = false;
 	  is.accepting_eword = false;
 	  break;
 	case NegClosure:
@@ -75,7 +80,10 @@ namespace spot
 	  is.boolean = false;
 	  is.ltl_formula = false;
 	  is.eltl_formula = false;
+	  is.psl_formula = true;
+	  is.sere_formula = false;
 	  is.accepting_eword = false;
+	  assert(child->is_sere_formula());
 	  break;
 	}
     }
diff --git a/src/ltltest/kind.test b/src/ltltest/kind.test
index 442625be1..738379378 100755
--- a/src/ltltest/kind.test
+++ b/src/ltltest/kind.test
@@ -1,5 +1,5 @@
 #! /bin/sh
-# Copyright (C) 2010 Laboratoire de Recherche et Developement to
+# Copyright (C) 2010, 2011 Laboratoire de Recherche et Developement to
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -33,10 +33,10 @@ check()
     test "$word" = "$2"
 }
 
-check 'a'         'B&!xfLEP'
-check 'a<->b'     'BxfLEP'
-check '!a'        'B&!xfLEP'
-check '!(a|b)'    'B&xfLEP'
+check 'a'         'B&!xfLEPS'
+check 'a<->b'     'BxfLEPS'
+check '!a'        'B&!xfLEPS'
+check '!(a|b)'    'B&xfLEPS'
 check 'F(a)'      '&!xLPe'
 check 'G(a)'      '&!xLPu'
 check 'a U b'     '&!xfLP'