diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc
index 915a11db8..7cf62be89 100644
--- a/src/ltlast/binop.cc
+++ b/src/ltlast/binop.cc
@@ -121,6 +121,10 @@ namespace spot
 	  return "W";
 	case M:
 	  return "M";
+	case EConcat:
+	  return "EConcat";
+	case UConcat:
+	  return "UConcat";
 	}
       // Unreachable code.
       assert(0);
@@ -136,7 +140,7 @@ namespace spot
       // example the formula instance for 'a xor b' is the same as
       // that for 'b xor a'.
 
-      /// Trivial identities:
+      // Trivial identities:
       switch (op)
 	{
 	case Xor:
@@ -176,10 +180,10 @@ namespace spot
 	  assert(second != constant::true_instance());
 	  break;
 	case Implies:
-	  ///   - (1 => Exp) = Exp
-	  ///   - (0 => Exp) = 0
-	  ///   - (Exp => 1) = 1
-	  ///   - (Exp => 0) = !Exp
+	  //   - (1 => Exp) = Exp
+	  //   - (0 => Exp) = 0
+	  //   - (Exp => 1) = 1
+	  //   - (Exp => 0) = !Exp
 	  if (first == constant::true_instance())
 	    return second;
 	  if (first == constant::false_instance())
@@ -196,9 +200,9 @@ namespace spot
 	    return unop::instance(unop::Not, first);
 	  break;
 	case U:
-	  ///   - (Exp U 1) = 1
-	  ///   - (Exp U 0) = 0
-	  ///   - (0 U Exp) = Exp
+	  //   - (Exp U 1) = 1
+	  //   - (Exp U 0) = 0
+	  //   - (0 U Exp) = Exp
 	  if (second == constant::true_instance()
 	      || second == constant::false_instance()
 	      || first == constant::false_instance())
@@ -208,9 +212,9 @@ namespace spot
 	    }
 	  break;
 	case W:
-	  ///   - (Exp W 1) = 1
-	  ///   - (0 W Exp) = Exp
-	  ///   - (1 W Exp) = 1
+	  //   - (Exp W 1) = 1
+	  //   - (0 W Exp) = Exp
+	  //   - (1 W Exp) = 1
 	  if (second == constant::true_instance()
 	      || first == constant::false_instance())
 	    {
@@ -224,9 +228,9 @@ namespace spot
 	    }
 	  break;
 	case R:
-	  ///   - (Exp R 1) = 1
-	  ///   - (Exp R 0) = 0
-	  ///   - (1 R Exp) = Exp
+	  //   - (Exp R 1) = 1
+	  //   - (Exp R 0) = 0
+	  //   - (1 R Exp) = Exp
 	  if (second == constant::true_instance()
 	      || second == constant::false_instance()
 	      || first == constant::true_instance())
@@ -236,9 +240,9 @@ namespace spot
 	    }
 	  break;
 	case M:
-	  ///   - (Exp M 0) = 0
-	  ///   - (1 M Exp) = Exp
-	  ///   - (0 M Exp) = 0
+	  //   - (Exp M 0) = 0
+	  //   - (1 M Exp) = Exp
+	  //   - (0 M Exp) = 0
 	  if (second == constant::false_instance()
 	      || first == constant::true_instance())
 	    {
@@ -251,6 +255,28 @@ namespace spot
 	      return first;
 	    }
 	  break;
+	case EConcat:
+	  //   - 0 <>-> Exp = 0
+	  //   - 1 <>-> Exp = Exp
+	  if (first == constant::false_instance())
+	    return second;
+	  if (first == constant::true_instance())
+	    {
+	      second->destroy();
+	      return first;
+	    }
+	  break;
+	case UConcat:
+	  //   - 0 []-> Exp = 1
+	  //   - 1 []-> Exp = Exp
+	  if (first == constant::false_instance())
+	    return constant::true_instance();
+	  if (first == constant::true_instance())
+	    {
+	      second->destroy();
+	      return first;
+	    }
+	  break;
 	}
 
       pairf pf(first, second);
diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh
index 1731b1d67..de97074c9 100644
--- a/src/ltlast/binop.hh
+++ b/src/ltlast/binop.hh
@@ -53,7 +53,9 @@ namespace spot
 		  U, //< until
 		  R, //< release (dual of until)
 		  W, //< weak until
-		  M  //< strong release (dual of weak until)
+		  M,  //< strong release (dual of weak until)
+		  EConcat, // Existential Concatenation
+		  UConcat // Universal Concatenation
       };
 
       /// \brief Build a unary operator with operation \a op and
diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy
index 4c1dca2c2..939dad973 100644
--- a/src/ltlparse/ltlparse.yy
+++ b/src/ltlparse/ltlparse.yy
@@ -1,7 +1,5 @@
 /* Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
 ** de l'Epita (LRDE).
-/* Copyright (C) 2010 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),
 ** Université Pierre et Marie Curie.
@@ -29,6 +27,7 @@
 %name-prefix "ltlyy"
 %debug
 %error-verbose
+%expect 0
 
 %code requires
 {
@@ -76,12 +75,15 @@ using namespace spot::ltl;
 /* All tokens.  */
 
 %token PAR_OPEN "opening parenthesis" PAR_CLOSE "closing parenthesis"
+%token BRACE_OPEN "opening brace" BRACE_CLOSE "closing brace"
 %token OP_OR "or operator" OP_XOR "xor operator" OP_AND "and operator"
 %token OP_IMPLIES "implication operator" OP_EQUIV "equivalent operator"
 %token OP_U "until operator" OP_R "release operator"
 %token OP_W "weak until operator" OP_M "strong release operator"
 %token OP_F "sometimes operator" OP_G "always operator"
 %token OP_X "next operator" OP_NOT "not operator"
+%token OP_UCONCAT "universal concat operator"
+%token OP_ECONCAT "existential concat operator"
 %token <str> ATOMIC_PROP "atomic proposition"
 %token OP_STAR "star operator" OP_CONCAT "concat operator"
 %token CONST_TRUE "constant true" CONST_FALSE "constant false"
@@ -91,6 +93,8 @@ using namespace spot::ltl;
 /* Priorities.  */
 
 /* Low priority regex operator. */
+%left OP_UCONCAT OP_ECONCAT
+
 %left OP_CONCAT
 
 /* Logical operators.  */
@@ -112,7 +116,7 @@ using namespace spot::ltl;
 
 %nonassoc OP_POST_NEG OP_POST_POS
 
-%type <ltl> subformula
+%type <ltl> subformula booleanatom rationalexp bracedrationalexp
 
 %destructor { delete $$; } <str>
 %destructor { $$->destroy(); } <ltl>
@@ -145,7 +149,7 @@ result:       subformula END_OF_INPUT
 /* The reason we use `constant::false_instance()' for error recovery
    is that it isn't reference counted.  (Hence it can't leak references.)  */
 
-subformula: ATOMIC_PROP
+booleanatom: ATOMIC_PROP
 	      {
 		$$ = parse_environment.require(*$1);
 		if (! $$)
@@ -201,8 +205,63 @@ subformula: ATOMIC_PROP
 	      { $$ = constant::true_instance(); }
 	    | CONST_FALSE
 	      { $$ = constant::false_instance(); }
+
+rationalexp: booleanatom
 	    | CONST_EMPTYWORD
 	      { $$ = constant::empty_word_instance(); }
+	    | PAR_OPEN rationalexp PAR_CLOSE
+	      { $$ = $2; }
+	    | PAR_OPEN error PAR_CLOSE
+	      { error_list.push_back(parse_error(@$,
+		 "treating this parenthetical block as false"));
+		$$ = constant::false_instance();
+	      }
+	    | PAR_OPEN rationalexp END_OF_INPUT
+	      { error_list.push_back(parse_error(@1 + @2,
+				      "missing closing parenthesis"));
+		$$ = $2;
+	      }
+	    | PAR_OPEN error END_OF_INPUT
+	      { error_list.push_back(parse_error(@$,
+                    "missing closing parenthesis, "
+		    "treating this parenthetical block as false"));
+		$$ = constant::false_instance();
+	      }
+	    | rationalexp OP_AND rationalexp
+	      { $$ = multop::instance(multop::And, $1, $3); }
+	    | rationalexp OP_AND error
+              { missing_right_binop($$, $1, @2, "and operator"); }
+	    | rationalexp OP_OR rationalexp
+	      { $$ = multop::instance(multop::Or, $1, $3); }
+	    | rationalexp OP_OR error
+              { missing_right_binop($$, $1, @2, "or operator"); }
+	    | rationalexp OP_CONCAT rationalexp
+	      { $$ = multop::instance(multop::Concat, $1, $3); }
+	    | rationalexp OP_CONCAT error
+              { missing_right_binop($$, $1, @2, "concat operator"); }
+	    | rationalexp OP_STAR
+	      { $$ = unop::instance(unop::Star, $1); }
+
+bracedrationalexp: BRACE_OPEN rationalexp BRACE_CLOSE
+              { $$ = $2; }
+            | BRACE_OPEN error BRACE_CLOSE
+	      { error_list.push_back(parse_error(@$,
+		 "treating this brace block as false"));
+		$$ = constant::false_instance();
+	      }
+            | BRACE_OPEN rationalexp END_OF_INPUT
+	      { error_list.push_back(parse_error(@1 + @2,
+				      "missing closing brace"));
+		$$ = $2;
+	      }
+	    | BRACE_OPEN error END_OF_INPUT
+	      { error_list.push_back(parse_error(@$,
+                    "missing closing brace, "
+		    "treating this brace block as false"));
+		$$ = constant::false_instance();
+	      }
+
+subformula: booleanatom
 	    | PAR_OPEN subformula PAR_CLOSE
 	      { $$ = $2; }
 	    | PAR_OPEN error PAR_CLOSE
@@ -229,10 +288,6 @@ subformula: ATOMIC_PROP
 	      { $$ = multop::instance(multop::Or, $1, $3); }
 	    | subformula OP_OR error
               { missing_right_binop($$, $1, @2, "or operator"); }
-	    | subformula OP_CONCAT subformula
-	      { $$ = multop::instance(multop::Concat, $1, $3); }
-	    | subformula OP_CONCAT error
-              { missing_right_binop($$, $1, @2, "concat operator"); }
 	    | subformula OP_XOR subformula
 	      { $$ = binop::instance(binop::Xor, $1, $3); }
 	    | subformula OP_XOR error
@@ -277,8 +332,14 @@ subformula: ATOMIC_PROP
 	      { $$ = unop::instance(unop::Not, $2); }
 	    | OP_NOT error
 	      { missing_right_op($$, @1, "not operator"); }
-	    | subformula OP_STAR
-	      { $$ = unop::instance(unop::Star, $1); }
+            | bracedrationalexp OP_UCONCAT subformula
+	      { $$ = binop::instance(binop::UConcat, $1, $3); }
+            | bracedrationalexp OP_UCONCAT error
+	      { missing_right_binop($$, $1, @2, "universal concat operator"); }
+            | bracedrationalexp OP_ECONCAT subformula
+	      { $$ = binop::instance(binop::EConcat, $1, $3); }
+            | bracedrationalexp OP_ECONCAT error
+	      { missing_right_binop($$, $1, @2, "universal concat operator"); }
 ;
 
 %%
diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll
index 5732c686e..863d77dd9 100644
--- a/src/ltlparse/ltlscan.ll
+++ b/src/ltlparse/ltlscan.ll
@@ -65,6 +65,8 @@ flex_set_buffer(const char* buf)
 
 "("				BEGIN(0); return token::PAR_OPEN;
 ")"				BEGIN(not_prop); return token::PAR_CLOSE;
+"{"                             BEGIN(0); return token::BRACE_OPEN;
+"}"				BEGIN(not_prop); return token::BRACE_CLOSE;
 
   /* Must go before the other operators, because the F of FALSE
      should not be mistaken with a unary F. */
@@ -87,6 +89,8 @@ flex_set_buffer(const char* buf)
 "<=>"|"<->"|"<-->"		BEGIN(0); return token::OP_EQUIV;
 "*"				BEGIN(0); return token::OP_STAR;
 ";"				BEGIN(0); return token::OP_CONCAT;
+"[]->"				BEGIN(0); return token::OP_UCONCAT;
+"<>->"				BEGIN(0); return token::OP_ECONCAT;
 
   /* <>, [], and () are used in Spin.  */
 "F"|"<>"			BEGIN(0); return token::OP_F;
diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc
index e31dd83bc..d94dedfc5 100644
--- a/src/ltlvisit/basicreduce.cc
+++ b/src/ltlvisit/basicreduce.cc
@@ -261,6 +261,8 @@ namespace spot
 	    case binop::Xor:
 	    case binop::Equiv:
 	    case binop::Implies:
+	    case binop::EConcat:
+	    case binop::UConcat:
 	      result_ = binop::instance(bo->op(),
 					basic_reduce(f1),
 					basic_reduce(f2));
diff --git a/src/ltlvisit/consterm.cc b/src/ltlvisit/consterm.cc
index f2816b6c5..cd9fb416c 100644
--- a/src/ltlvisit/consterm.cc
+++ b/src/ltlvisit/consterm.cc
@@ -62,7 +62,9 @@ namespace spot
 	    case binop::W:
 	    case binop::M:
 	    case binop::R:
-	      result_ = false;
+	    case binop::EConcat:
+	    case binop::UConcat:
+	      assert(!"unsupported operator");
 	      break;
 	    }
 	}
@@ -77,7 +79,7 @@ namespace spot
 	    case unop::F:
 	    case unop::G:
 	    case unop::Finish:
-	      result_ = false;
+	      assert(!"unsupported operator");
 	      break;
 	    case unop::Star:
 	      result_ = true;
@@ -89,7 +91,6 @@ namespace spot
 	visit(const automatop*)
 	{
 	  assert(!"automatop not supported for constant term");
-	  result_ = false;
 	}
 
 	void
diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc
index f5d588772..76ddbf01d 100644
--- a/src/ltlvisit/lunabbrev.cc
+++ b/src/ltlvisit/lunabbrev.cc
@@ -81,10 +81,14 @@ namespace spot
 	  /* f1 R f2 == f1 R f2 */
           /* f1 W f2 == f1 W f2 */
 	  /* f1 M f2 == f1 M f2 */
+	  /* f1 UConcat f2 == f1 UConcat f2 */
+	  /* f1 EConcat f2 == f1 EConcat f2 */
    	case binop::U:
 	case binop::R:
 	case binop::W:
 	case binop::M:
+	case binop::UConcat:
+	case binop::EConcat:
 	  result_ = binop::instance(op, f1, f2);
 	  return;
 	}
diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc
index e455dcfc6..1f573dfd9 100644
--- a/src/ltlvisit/nenoform.cc
+++ b/src/ltlvisit/nenoform.cc
@@ -174,6 +174,18 @@ namespace spot
 	      result_ = binop::instance(negated_ ? binop::W : binop::M,
 					recurse(f1), recurse(f2));
 	      return;
+	    case binop::UConcat:
+	      /* !(a []-> b) == a<>-> !b */
+	      result_ = binop::instance(negated_ ?
+					binop::EConcat : binop::UConcat,
+					recurse_(f1, false), recurse(f2));
+	      return;
+	    case binop::EConcat:
+	      /* !(a <>-> b) == a[]-> !b */
+	      result_ = binop::instance(negated_ ?
+					binop::UConcat : binop::EConcat,
+					recurse_(f1, false), recurse(f2));
+	      return;
 	    }
 	  /* Unreachable code.  */
 	  assert(0);
diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc
index 36bad8e36..8bae2b143 100644
--- a/src/ltlvisit/reduce.cc
+++ b/src/ltlvisit/reduce.cc
@@ -156,6 +156,9 @@ namespace spot
 	      if (f2 == constant::false_instance())
 		ret_.is.universal = true;
 	      return;
+	    case binop::UConcat:
+	    case binop::EConcat:
+	      return;
 	    }
 	  /* Unreachable code.  */
 	  assert(0);
@@ -313,6 +316,8 @@ namespace spot
 		case binop::Xor:
 		case binop::Equiv:
 		case binop::Implies:
+		case binop::UConcat:
+		case binop::EConcat:
 		  break;
 
 		case binop::U:
diff --git a/src/ltlvisit/simpfg.cc b/src/ltlvisit/simpfg.cc
index f4a0f9210..e6da46304 100644
--- a/src/ltlvisit/simpfg.cc
+++ b/src/ltlvisit/simpfg.cc
@@ -1,7 +1,5 @@
 // Copyright (C) 2010 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
-// département Systèmes Répartis Coopératifs (SRC), Université Pierre
-// et Marie Curie.
 // Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -53,6 +51,8 @@ namespace spot
 	case binop::Xor:
 	case binop::Implies:
 	case binop::Equiv:
+	case binop::UConcat:
+	case binop::EConcat:
 	  result_ = binop::instance(op, f1, f2);
 	  return;
 	  /* true U f2 == F(f2) */
diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc
index 2013af89d..3888e287b 100644
--- a/src/ltlvisit/syntimpl.cc
+++ b/src/ltlvisit/syntimpl.cc
@@ -126,6 +126,8 @@ namespace spot
 	    case binop::Xor:
 	    case binop::Equiv:
 	    case binop::Implies:
+	    case binop::UConcat:
+	    case binop::EConcat:
 	      return;
 	    case binop::U:
 	    case binop::W:
@@ -359,6 +361,8 @@ namespace spot
 	    case binop::Xor:
 	    case binop::Equiv:
 	    case binop::Implies:
+	    case binop::UConcat:
+	    case binop::EConcat:
 	      return;
 	    case binop::U:
 	      /* (a < c) && (c < d) => a U b < c U d */
diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc
index cedb8b61b..ec968f82a 100644
--- a/src/ltlvisit/tostring.cc
+++ b/src/ltlvisit/tostring.cc
@@ -103,11 +103,23 @@ namespace spot
 	visit(const binop* bo)
 	{
 	  bool top_level = top_level_;
-	  top_level_ = false;
 	  if (!top_level)
 	    os_ << "(";
 
-	  bo->first()->accept(*this);
+	  switch (bo->op())
+	    {
+	    case binop::UConcat:
+	    case binop::EConcat:
+	      os_ << "{ ";
+	      top_level_ = true;
+	      bo->first()->accept(*this);
+	      top_level_ = false;
+	      break;
+	    default:
+	      top_level_ = false;
+	      bo->first()->accept(*this);
+	      break;
+	    }
 
 	  switch (bo->op())
 	    {
@@ -132,6 +144,12 @@ namespace spot
 	    case binop::M:
 	      os_ << " M ";
 	      break;
+	    case binop::UConcat:
+	      os_ << " }[]-> ";
+	      break;
+	    case binop::EConcat:
+	      os_ << " }<>-> ";
+	      break;
 	    }
 
 	  bo->second()->accept(*this);
@@ -311,7 +329,17 @@ namespace spot
 	      break;
 	    case binop::R:
 	      bo->first()->accept(*this);
-	     os_ << " V ";
+	      os_ << " V ";
+	      bo->second()->accept(*this);
+	      break;
+	    case binop::UConcat:
+	      bo->first()->accept(*this);
+	      os_ << " []-> ";
+	      bo->second()->accept(*this);
+	      break;
+	    case binop::EConcat:
+	      bo->first()->accept(*this);
+	      os_ << " <>-> ";
 	      bo->second()->accept(*this);
 	      break;
 	      /* W and M are not supported by Spin */
diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc
index 0607a6a1b..6db6b8ece 100644
--- a/src/tgba/formula2bdd.cc
+++ b/src/tgba/formula2bdd.cc
@@ -112,6 +112,8 @@ namespace spot
 	  case binop::R:
 	  case binop::W:
 	  case binop::M:
+	  case binop::UConcat:
+	  case binop::EConcat:
 	    assert(!"unsupported operator");
 	  }
 	/* Unreachable code.  */
diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc
index 78b67c7b7..03842d756 100644
--- a/src/tgbaalgos/eltl2tgba_lacim.cc
+++ b/src/tgbaalgos/eltl2tgba_lacim.cc
@@ -129,6 +129,8 @@ namespace spot
 	  case binop::R:
 	  case binop::W:
 	  case binop::M:
+	  case binop::UConcat:
+	  case binop::EConcat:
 	    assert(!"unsupported operator");
 	  }
 	/* Unreachable code.  */
diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc
index 31795fe95..c57ad9927 100644
--- a/src/tgbaalgos/ltl2taa.cc
+++ b/src/tgbaalgos/ltl2taa.cc
@@ -247,6 +247,9 @@ namespace spot
 	case binop::Implies:
 	case binop::Equiv:
 	  assert(0); // TBD
+	case binop::UConcat:
+	case binop::EConcat:
+	  assert(!"unsupported operator");
 	}
 	/* Unreachable code.  */
 	assert(0);
diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index ea14853a4..49f67a3e8 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -418,6 +418,10 @@ namespace spot
 	      res_ = (f1 & f2) | (bdd_ithvar(a) & f2 & bdd_ithvar(x));
 	      return;
 	    }
+	  case binop::UConcat:
+	  case binop::EConcat:
+	    assert(!"unsupported operator");
+	    break;
 	  }
 	/* Unreachable code.  */
 	assert(0);
@@ -527,6 +531,10 @@ namespace spot
 	  case binop::W:
 	    res_ = true;
 	    return;
+	  case binop::UConcat:
+	  case binop::EConcat:
+	    node->second()->accept(*this);
+	    return;
 	  }
 	/* Unreachable code.  */
 	assert(0);
diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc
index 1fdfd23a6..2fa3eedc8 100644
--- a/src/tgbaalgos/ltl2tgba_lacim.cc
+++ b/src/tgbaalgos/ltl2tgba_lacim.cc
@@ -220,6 +220,10 @@ namespace spot
 	      res_ = now;
 	      return;
 	    }
+	  case binop::UConcat:
+	  case binop::EConcat:
+	    assert(!"unsupported operator");
+	    break;
 	  }
 	/* Unreachable code.  */
 	assert(0);