diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy
index 6d55e5111..25afbe18c 100644
--- a/src/ltlparse/ltlparse.yy
+++ b/src/ltlparse/ltlparse.yy
@@ -87,6 +87,8 @@ using namespace spot::ltl;
 %token OP_X "next operator" OP_NOT "not operator" OP_STAR "star operator"
 %token OP_UCONCAT "universal concat operator"
 %token OP_ECONCAT "existential concat operator"
+%token OP_UCONCAT_NONO "universal non-overlapping concat operator"
+%token OP_ECONCAT_NONO "existential non-overlapping concat operator"
 %token <str> ATOMIC_PROP "atomic proposition"
 %token OP_CONCAT "concat operator" OP_FUSION "fusion operator"
 %token CONST_TRUE "constant true" CONST_FALSE "constant false"
@@ -96,7 +98,7 @@ using namespace spot::ltl;
 /* Priorities.  */
 
 /* Low priority regex operator. */
-%left OP_UCONCAT OP_ECONCAT
+%left OP_UCONCAT OP_ECONCAT OP_UCONCAT_NONO OP_ECONCAT_NONO
 
 %left OP_CONCAT OP_FUSION
 
@@ -386,12 +388,34 @@ subformula: booleanatom
             | bracedrationalexp parenthesedsubformula
 	      { $$ = binop::instance(binop::UConcat, $1, $2); }
             | bracedrationalexp OP_UCONCAT error
-	      { missing_right_binop($$, $1, @2, "universal concat operator"); }
+	      { missing_right_binop($$, $1, @2,
+				    "universal overlapping concat operator"); }
             | bracedrationalexp OP_ECONCAT subformula
 	      { $$ = binop::instance(binop::EConcat, $1, $3); }
             | bracedrationalexp OP_ECONCAT error
-	      { missing_right_binop($$, $1, @2, "universal concat operator"); }
-
+	      { missing_right_binop($$, $1, @2,
+				    "existential overlapping concat operator");
+	      }
+            | bracedrationalexp OP_UCONCAT_NONO subformula
+	      /* {SERE}[]=>EXP = {SERE;1}[]->EXP */
+	      { $$ = binop::instance(binop::UConcat,
+		       multop::instance(multop::Concat, $1,
+					constant::true_instance()), $3);
+	      }
+            | bracedrationalexp OP_UCONCAT_NONO error
+	      { missing_right_binop($$, $1, @2,
+				  "universal non-overlapping concat operator");
+	      }
+            | bracedrationalexp OP_ECONCAT_NONO subformula
+	      /* {SERE}<>=>EXP = {SERE;1}<>->EXP */
+	      { $$ = binop::instance(binop::EConcat,
+		       multop::instance(multop::Concat, $1,
+					constant::true_instance()), $3);
+	      }
+            | bracedrationalexp OP_ECONCAT_NONO error
+	      { missing_right_binop($$, $1, @2,
+				"existential non-overlapping concat operator");
+	      }
 ;
 
 %%
diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll
index 5f90c0864..0db5ddc5f 100644
--- a/src/ltlparse/ltlscan.ll
+++ b/src/ltlparse/ltlscan.ll
@@ -89,6 +89,8 @@ flex_set_buffer(const char* buf, int start_tok)
 "[*0]"				BEGIN(0); return token::CONST_EMPTYWORD;
 "[]->"|"|->"			BEGIN(0); return token::OP_UCONCAT;
 "<>->"				BEGIN(0); return token::OP_ECONCAT;
+"[]=>"|"|=>"			BEGIN(0); return token::OP_UCONCAT_NONO;
+"<>=>"				BEGIN(0); return token::OP_ECONCAT_NONO;
 "*"|"[*]"			BEGIN(0); return token::OP_STAR;
 ";"				BEGIN(0); return token::OP_CONCAT;
 ":"				BEGIN(0); return token::OP_FUSION;
diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test
index bb77e43af..52e872601 100755
--- a/src/tgbatest/ltl2tgba.test
+++ b/src/tgbatest/ltl2tgba.test
@@ -76,13 +76,14 @@ check_psl '{a;b}'
 check_psl '{(a;b)*}'
 check_psl 'G{(a;b)*}'
 check_psl '{a*}[]->{b*}'
+check_psl '{a*}[]=>{b*}'
 check_psl '{a*&b}'
 check_psl '{a*&b*}'
 check_psl '{((!c;b*) & d);e}'
 check_psl '{(a* & (c;b*) & d);e}'
 # Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni,
 # Ruah, Zarpas (2007).
-check_psl '{1[*];req;ack;1}[]->{start;busy[*];done}'
+check_psl '{1[*];req;ack}|=>{start;busy[*];done}'
 
 # Make sure 'a U (b U c)' has 3 states and 6 transitions,
 # before and after degeneralization.