diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc
index df9962855..823a74c8e 100644
--- a/src/ltlast/atomic_prop.cc
+++ b/src/ltlast/atomic_prop.cc
@@ -43,6 +43,7 @@ namespace spot
       is.eltl_formula = true;
       is.psl_formula = true;
       is.sere_formula = true;
+      is.finite = true;
       is.eventual = false;
       is.universal = false;
       is.syntactic_safety = true;
diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc
index 826e97480..fe7551eeb 100644
--- a/src/ltlast/automatop.cc
+++ b/src/ltlast/automatop.cc
@@ -39,6 +39,7 @@ namespace spot
       is.eltl_formula = true;
       is.psl_formula = false;
       is.sere_formula = false;
+      is.finite = false;
       is.eventual = false;
       is.universal = false;
       is.syntactic_safety = false;
diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc
index 765652084..f0547692e 100644
--- a/src/ltlast/binop.cc
+++ b/src/ltlast/binop.cc
@@ -64,16 +64,17 @@ namespace spot
 	      // Only formula that are in the intersection of
 	      // guarantee and safety are closed by Xor and <=>.
 	      bool sg = is.syntactic_safety && is.syntactic_guarantee;
-	      bool rp = is.syntactic_recurrence && is.syntactic_persistence;
 	      is.syntactic_safety = sg;
 	      is.syntactic_guarantee = sg;
-	      is.syntactic_recurrence = rp;
-	      is.syntactic_persistence = rp;
+	      assert(is.syntactic_recurrence == true);
+	      assert(is.syntactic_persistence == true);
 	    }
 	  else
 	    {
 	      is.syntactic_safety = false;
 	      is.syntactic_guarantee = false;
+	      is.syntactic_recurrence = false;
+	      is.syntactic_persistence = false;
 	    }
 	  break;
 	case Implies:
@@ -102,16 +103,20 @@ namespace spot
 	  is.accepting_eword = false;
 	  is.psl_formula = true;
 
-	  // FIXME: if we know that the SERE has a finite language.
-	  // (i.e. no star).  Then
-	  // is.syntactic_safety = second->is_syntactic_safety();
-	  // is.syntactic_obligation = second->is_syntactic_obligation();
-	  // is.syntactic_recurrence = second->is_syntactic_recurrence();
-	  is.syntactic_safety = false;
 	  is.syntactic_guarantee = second->is_syntactic_guarantee();
-	  is.syntactic_obligation = second->is_syntactic_guarantee();
-	  is.syntactic_recurrence = second->is_syntactic_guarantee();
 	  is.syntactic_persistence = second->is_syntactic_persistence();
+	  if (first->is_finite())
+	    {
+	      is.syntactic_safety = second->is_syntactic_safety();
+	      is.syntactic_obligation = second->is_syntactic_obligation();
+	      is.syntactic_recurrence = second->is_syntactic_recurrence();
+	    }
+	  else
+	    {
+	      is.syntactic_safety = false;
+	      is.syntactic_obligation = second->is_syntactic_guarantee();
+	      is.syntactic_recurrence = second->is_syntactic_guarantee();
+	    }
 
 	  assert(first->is_sere_formula());
 	  assert(second->is_psl_formula());
@@ -124,16 +129,20 @@ namespace spot
 	  is.accepting_eword = false;
 	  is.psl_formula = true;
 
-	  // FIXME: if we know that the SERE has a finite language.
-	  // (i.e. no star).  Then
-	  // is.syntactic_guarantee = second->is_syntactic_guarantee();
-	  // is.syntactic_obligation = second->is_syntactic_obligation();
-	  // is.syntactic_persistence = second->is_syntactic_persistence();
 	  is.syntactic_safety = second->is_syntactic_safety();
-	  is.syntactic_guarantee = false;
-	  is.syntactic_obligation = second->is_syntactic_safety();
 	  is.syntactic_recurrence = second->is_syntactic_recurrence();
-	  is.syntactic_persistence = second->is_syntactic_safety();
+	  if (first->is_finite())
+	    {
+	      is.syntactic_guarantee = second->is_syntactic_guarantee();
+	      is.syntactic_obligation = second->is_syntactic_obligation();
+	      is.syntactic_persistence = second->is_syntactic_persistence();
+	    }
+	  else
+	    {
+	      is.syntactic_guarantee = false;
+	      is.syntactic_obligation = second->is_syntactic_safety();
+	      is.syntactic_persistence = second->is_syntactic_safety();
+	    }
 
 	  assert(first->is_sere_formula());
 	  assert(second->is_psl_formula());
@@ -145,6 +154,7 @@ namespace spot
 	  is.boolean = false;
 	  is.eltl_formula = false;
 	  is.sere_formula = false;
+	  is.finite = false;
 	  is.accepting_eword = false;
 
 	  is.syntactic_safety = false;
@@ -164,6 +174,7 @@ namespace spot
 	  is.boolean = false;
 	  is.eltl_formula = false;
 	  is.sere_formula = false;
+	  is.finite = false;
 	  is.accepting_eword = false;
 
 	  // is.syntactic_safety = Safety W Safety;
@@ -183,6 +194,7 @@ namespace spot
 	  is.boolean = false;
 	  is.eltl_formula = false;
 	  is.sere_formula = false;
+	  is.finite = false;
 	  is.accepting_eword = false;
 
 	  // is.syntactic_safety = Safety R Safety;
@@ -202,6 +214,7 @@ namespace spot
 	  is.boolean = false;
 	  is.eltl_formula = false;
 	  is.sere_formula = false;
+	  is.finite = false;
 	  is.accepting_eword = false;
 
 	  is.syntactic_safety = false;
diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc
index e59e18d81..a99d86d63 100644
--- a/src/ltlast/bunop.cc
+++ b/src/ltlast/bunop.cc
@@ -51,11 +51,14 @@ namespace spot
       switch (op_)
 	{
 	case Star:
+	  if (max_ == unbounded)
+	    is.finite = false;
 	  if (min_ == 0)
 	    is.accepting_eword = true;
 	  break;
 	case Equal:
 	case Goto:
+	  is.finite = false;
 	  is.accepting_eword = (min_ == 0);
 	  // Equal and Goto can only apply to Boolean formulae.
 	  assert(child->is_boolean());
diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc
index 60bcb70e4..8ce6a9307 100644
--- a/src/ltlast/constant.cc
+++ b/src/ltlast/constant.cc
@@ -49,6 +49,7 @@ namespace spot
 	  is.eltl_formula = true;
 	  is.psl_formula = true;
 	  is.sere_formula = true;
+	  is.finite = true;
 	  is.eventual = true;
 	  is.universal = true;
 	  is.syntactic_safety = true;
@@ -69,6 +70,7 @@ namespace spot
 	  is.eltl_formula = false;
 	  is.psl_formula = false;
 	  is.sere_formula = true;
+	  is.finite = true;
 	  is.eventual = false;
 	  is.syntactic_safety = false;
 	  is.syntactic_guarantee = false;
diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc
index d2624a072..8e906f977 100644
--- a/src/ltlast/formula.cc
+++ b/src/ltlast/formula.cc
@@ -84,6 +84,7 @@ namespace spot
       proprint(is_eltl_formula, "E", "ELTL formula");
       proprint(is_psl_formula, "P", "PSL formula");
       proprint(is_sere_formula, "S", "SERE formula");
+      proprint(is_finite, "F", "finite");
       proprint(is_eventual, "e", "pure eventuality");
       proprint(is_universal, "u", "purely universal");
       proprint(is_syntactic_safety, "s", "syntactic safety");
diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh
index f9d32bb88..b9c2ef179 100644
--- a/src/ltlast/formula.hh
+++ b/src/ltlast/formula.hh
@@ -152,30 +152,37 @@ namespace spot
 	return is.sugar_free_ltl;
       }
 
-      /// Whether the formula use only LTL operators.
+      /// Whether the formula uses only LTL operators.
       bool is_ltl_formula() const
       {
 	return is.ltl_formula;
       }
 
-      /// Whether the formula use only ELTL operators.
+      /// Whether the formula uses only ELTL operators.
       bool is_eltl_formula() const
       {
 	return is.eltl_formula;
       }
 
-      /// Whether the formula use only PSL operators.
+      /// Whether the formula uses only PSL operators.
       bool is_psl_formula() const
       {
 	return is.psl_formula;
       }
 
-      /// Whether the formula use only SERE operators.
+      /// Whether the formula uses only SERE operators.
       bool is_sere_formula() const
       {
 	return is.sere_formula;
       }
 
+      /// Whether a SERE describes a finite language, or an LTL
+      /// formula uses no temporal operator but X.
+      bool is_finite() const
+      {
+	return is.finite;
+      }
+
       /// \brief Whether the formula is purely eventual.
       ///
       /// Pure eventuality formulae are defined in
@@ -316,6 +323,7 @@ namespace spot
 	bool eltl_formula:1;	   // Only ELTL operators.
 	bool psl_formula:1;	   // Only PSL operators.
 	bool sere_formula:1;	   // Only SERE operators.
+	bool finite:1;		   // Finite SERE formulae, or Bool+X forms.
 	bool eventual:1;	   // Purely eventual formula.
 	bool universal:1;	   // Purely universal formula.
 	bool syntactic_safety:1;   // Syntactic Safety Property.
diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc
index 72df7b3d0..369c4d23a 100644
--- a/src/ltlast/unop.cc
+++ b/src/ltlast/unop.cc
@@ -66,6 +66,7 @@ namespace spot
 	  is.boolean = false;
 	  is.eltl_formula = false;
 	  is.sere_formula = false;
+	  is.finite = false;
 	  is.sugar_free_ltl = false;
 	  is.eventual = true;
 	  is.syntactic_safety = false;
@@ -79,6 +80,7 @@ namespace spot
 	  is.boolean = false;
 	  is.eltl_formula = false;
 	  is.sere_formula = false;
+	  is.finite = false;
 	  is.sugar_free_ltl = false;
 	  is.universal = true;
 	  // is.syntactic_safety inherited
@@ -93,6 +95,7 @@ namespace spot
 	  is.ltl_formula = false;
 	  is.psl_formula = false;
 	  is.sere_formula = false;
+	  is.finite = false;
 	  is.syntactic_safety = false;
 	  is.syntactic_guarantee = false;
 	  is.syntactic_obligation = false;
@@ -107,7 +110,7 @@ namespace spot
 	  is.eltl_formula = false;
 	  is.psl_formula = true;
 	  is.sere_formula = false;
-	  is.syntactic_safety = true;
+	  is.syntactic_safety = is.finite;
 	  is.syntactic_guarantee = true;
 	  is.syntactic_obligation = true;
 	  is.syntactic_recurrence = true;
@@ -121,7 +124,7 @@ namespace spot
 	  is.psl_formula = true;
 	  is.sere_formula = false;
 	  is.syntactic_safety = true;
-	  is.syntactic_guarantee = true;
+	  is.syntactic_guarantee = is.finite;
 	  is.syntactic_obligation = true;
 	  is.syntactic_recurrence = true;
 	  is.syntactic_persistence = true;
diff --git a/src/ltltest/kind.test b/src/ltltest/kind.test
index ec4f79886..8e7bb4ed3 100755
--- a/src/ltltest/kind.test
+++ b/src/ltltest/kind.test
@@ -33,10 +33,10 @@ check()
     test "$word" = "$2"
 }
 
-check 'a'         'B&!xfLEPSsgopr'
-check 'a<->b'     'BxfLEPSsgopr'
-check '!a'        'B&!xfLEPSsgopr'
-check '!(a|b)'    'B&xfLEPSsgopr'
+check 'a'         'B&!xfLEPSFsgopr'
+check 'a<->b'     'BxfLEPSFsgopr'
+check '!a'        'B&!xfLEPSFsgopr'
+check '!(a|b)'    'B&xfLEPSFsgopr'
 check 'F(a)'      '&!xLPegopr'
 check 'G(a)'      '&!xLPusopr'
 check 'a U b'     '&!xfLPgopr'
@@ -61,12 +61,28 @@ check '{a;c*;b}|->!Gb' '&xPr'
 check '{a;c*;b}|->F!b' '&!xPr'
 check '{a;c*;b}|->GFa' '&!xPr'
 check '{a;c*;b}|->FGa' '&!xP'
+check '{a;c;b|(d;e)}|->!Xb' '&fPFsgopr'
+check '{a;c;b|(d;e)}|->X!b' '&!fPFsgopr'
+check '{a;c;b|(d;e)}|->!Fb' '&xPsopr'
+check '{a;c;b|(d;e)}|->G!b' '&!xPsopr'
+check '{a;c;b|(d;e)}|->!Gb' '&xPgopr'
+check '{a;c;b|(d;e)}|->F!b' '&!xPgopr'
+check '{a;c;b|(d;e)}|->GFa' '&!xPr'
+check '{a;c;b|(d;e)}|->FGa' '&!xPp'
 check '{a;c*;b}<>->!Gb' '&xPgopr'
 check '{a;c*;b}<>->F!b' '&!xPgopr'
 check '{a;c*;b}<>->FGb' '&!xPp'
 check '{a;c*;b}<>->!GFb' '&xPp'
-check '{a:b:c:d}!' 'B&!xfLEPSsgopr'  # Equivalent to a&b&c&d
-check 'a&b&c&d'    'B&!xfLEPSsgopr'
+check '{a;c*;b}<>->GFb' '&!xP'
+check '{a;c*;b}<>->!FGb' '&xP'
+check '{a;c|d;b}<>->!Gb' '&xPgopr'
+check '{a;c|d;b}<>->G!b' '&!xPsopr'
+check '{a;c|d;b}<>->FGb' '&!xPp'
+check '{a;c|d;b}<>->!GFb' '&xPp'
+check '{a;c|d;b}<>->GFb' '&!xPr'
+check '{a;c|d;b}<>->!FGb' '&xPr'
+check '{a:b:c:d}!' 'B&!xfLEPSFsgopr'  # Equivalent to a&b&c&d
+check 'a&b&c&d'    'B&!xfLEPSFsgopr'
 check '(Xa <-> XXXc) U (b & Fe)' 'LPgopr'
 check '(!X(a|X(!b))&(FX(g xor h)))U(!G(a|b))' 'LPgopr'
 check '(!X(a|X(!b))&(GX(g xor h)))R(!F(a|b))' 'LPsopr'
@@ -88,6 +104,11 @@ check 'Fa  M GFb' '&!xLPer'
 check 'GFa W GFb' '&!xLPeur'
 check 'FGa W FGb' '&!xLPeu'
 check 'Ga  W FGb' '&!xLPup'
+check '{a;b*;c}' '&!xfPsopr'
+check '{a;b*;c}!' '&!xfPgopr'
+check '!{a;b*;c}!' '&xfPsopr'  # The negative normal form is {a;b*;c}[]->0
+check '{a;b*;c}[]->0' '&!xfPsopr'
+check '!{a;b*;c}' '&!xfPgopr+'
 
 run 0 ../consterm '1'
 run 0 ../consterm '0'