diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index b6e5eda59..0bee4a013 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -40,6 +40,10 @@
 
 \newcommand{\uni}[1]{\texttt{\small U+#1}}
 
+% For tables.
+\newcommand{\newfootnotemark}[1]{\addtocounter{footnote}{#1}\footnotemark[\value{footnote}]}
+\newcommand{\newfootnotetext}[2]{\addtocounter{footnote}{#1}\footnotetext[\value{footnote}]{#2}}
+
 
 %% ---------------------- %%
 %% Mathematical symbols.  %%
@@ -991,16 +995,22 @@ instance using the following methods:
 \\\texttt{is\_syntactic\_persistence()}& Whether the formula is a syntactic
   persistence property.
 \\\texttt{is\_marked()}& Whether the formula contains a special
-  ``marked'' version of the $\Esuffix$ or $\nsere{r}$ operators.\footnotemark
+  ``marked'' version of the $\Esuffix$ or $\nsere{r}$ operators.\newfootnotemark{1}
 \\\texttt{accepts\_eword()}& Whether the formula accepts
   $\eword$. (This can only be true for a SERE formula.)
+\\\texttt{has\_lbt\_atomic\_props()}& Whether the atomic
+  propositions of the formula are all of the form ``\texttt{p}$nn$''
+  where $nn$ is a string of digits.  This is required when converting
+  formula into LBT's format.\newfootnotemark{1}
 \end{tabulary}
 
-\footnotetext{These ``marked'' operators are used when
+\newfootnotetext{-1}{These ``marked'' operators are used when
   translating recurring $\Esuffix$ or $\nsere{r}$ operators.  They are
-  rendered as $\EsuffixMarked$ and $\nsereMarked{r}$ and obey the
-  same simplification rules and properties as their unmarked
-  counterpart (except for the \texttt{is\_marked()} property).}
+  rendered as $\EsuffixMarked$ and $\nsereMarked{r}$ and obey the same
+  simplification rules and properties as their unmarked counterpart
+  (except for the \texttt{is\_marked()} property).}
+\newfootnotetext{1}{\url{http://www.tcs.hut.fi/Software/maria/tools/lbt/}}
+
 
 \section{Pure Eventualities and Purely Universal Formul\ae{}}
 \label{sec:eventuniv}
diff --git a/src/bin/genltl.cc b/src/bin/genltl.cc
index bf456e425..e6db3e198 100644
--- a/src/bin/genltl.cc
+++ b/src/bin/genltl.cc
@@ -802,7 +802,7 @@ output_pattern(int pattern, int n)
 
   // Make sure we use only "p42"-style of atomic propositions
   // in lbt's output.
-  if (output_format == lbt_output)
+  if (output_format == lbt_output && !f->has_lbt_atomic_props())
     {
       const spot::ltl::formula* r = spot::ltl::relabel(f, spot::ltl::Pnn);
       f->destroy();
diff --git a/src/bin/ltlcheck.cc b/src/bin/ltlcheck.cc
index a5aba3fca..f65c5cb93 100644
--- a/src/bin/ltlcheck.cc
+++ b/src/bin/ltlcheck.cc
@@ -41,6 +41,7 @@
 #include "ltlvisit/tostring.hh"
 #include "ltlvisit/apcollect.hh"
 #include "ltlvisit/lbt.hh"
+#include "ltlvisit/relabel.hh"
 #include "tgbaalgos/lbtt.hh"
 #include "tgba/tgbaproduct.hh"
 #include "tgbaalgos/gtec/gtec.hh"
@@ -414,6 +415,8 @@ namespace
     // Run-specific variables
     printable_result_filename output;
   public:
+    using spot::formater::has;
+
     translator_runner()
     {
       declare('f', &string_ltl_spot);
@@ -704,6 +707,16 @@ namespace
       pstats->resize(m);
       nstats->resize(m);
 
+      // If we need LBT atomic proposition in any of the input or
+      // output, relabel the formula.
+      if (!f->has_lbt_atomic_props() &&
+	  (runner.has('l') || runner.has('L') || runner.has('T')))
+	{
+	  const spot::ltl::formula* g = spot::ltl::relabel(f, spot::ltl::Pnn);
+	  f->destroy();
+	  f = g;
+	}
+
       // ---------- Positive Formula ----------
 
       runner.round_formula(f, round);
diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc
index 4db0aa8be..220b69d1c 100644
--- a/src/ltlast/atomic_prop.cc
+++ b/src/ltlast/atomic_prop.cc
@@ -52,6 +52,15 @@ namespace spot
       is.syntactic_persistence = true;
       is.not_marked = true;
       is.accepting_eword = false;
+      // is.lbt_atomic_props should be true if the name has the form
+      // pNN where NN is any number of digit.
+      std::string::const_iterator pos = name.begin();
+      is.lbt_atomic_props = (pos != name.end() && *pos++ == 'p');
+      while (is.lbt_atomic_props && pos != name.end())
+	{
+	  char l = *pos++;
+	  is.lbt_atomic_props = (l >= '0' && l <= '9');
+	}
     }
 
     atomic_prop::~atomic_prop()
diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc
index 33421a9e3..96bf22e97 100644
--- a/src/ltlast/formula.cc
+++ b/src/ltlast/formula.cc
@@ -81,7 +81,8 @@ namespace spot
       proprint(is_syntactic_persistence, "p", "syntactic persistence");	\
       proprint(is_syntactic_recurrence, "r", "syntactic recurrence");	\
       proprint(is_marked, "+", "marked");				\
-      proprint(accepts_eword, "0", "accepts the empty word");
+      proprint(accepts_eword, "0", "accepts the empty word");		\
+      proprint(has_lbt_atomic_props, "l", "as LBT-style atomic props");
 
 
     std::list<std::string>
diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh
index ec6b0bf45..0949b6df0 100644
--- a/src/ltlast/formula.hh
+++ b/src/ltlast/formula.hh
@@ -275,6 +275,11 @@ namespace spot
 	return is.accepting_eword;
       }
 
+      bool has_lbt_atomic_props() const
+      {
+	return is.lbt_atomic_props;
+      }
+
       /// The properties as a field of bits.  For internal use.
       unsigned get_props() const
       {
@@ -333,6 +338,7 @@ namespace spot
 	bool syntactic_persistence:1; // Syntactic Persistence Property.
 	bool not_marked:1;	   // No occurrence of EConcatMarked.
 	bool accepting_eword:1;	   // Accepts the empty word.
+	bool lbt_atomic_props:1;   // Use only atomic propositions like p42.
       };
       union
       {