diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 03f1e7a06..5f562ed2f 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -10,9 +10,8 @@
 \usepackage{url}
 \usepackage{xspace}
 \usepackage{dsfont}
-\usepackage{mathabx}
+\usepackage{mathabx}  % vDash
 \usepackage{showlabels}
-\usepackage{chngpage}
 \usepackage{tabulary}
 \usepackage[numbers]{natbib}
 \usepackage{rotating}
@@ -646,9 +645,11 @@ denote arbitrary SERE and $b$ denotes a Boolean formula.
 \end{tabular}
 \end{center}
 
-The character \samp{\$} can also be used as value for $\mvar{j}$ in
-the above operators to denote an unbounded range.  For instance
-`$a\STAR{i,\texttt{\$}}$' and `$a\STAR{i..}$' represent the same SERE.
+The character \samp{\$} or the string \samp{inf} can also be used as
+value for $\mvar{j}$ in the above operators to denote an unbounded
+range.\footnote{SVA uses \samp{\$} while PSL uses \samp{inf}.}  For
+instance `$a\STAR{i,\texttt{\$}}$', `$a\STAR{i\texttt{:inf}}$' and
+`$a\STAR{i..}$' all represent the same SERE.
 
 \subsection{Semantics}
 
diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll
index 063021cfc..072341dde 100644
--- a/src/ltlparse/ltlscan.ll
+++ b/src/ltlparse/ltlscan.ll
@@ -123,9 +123,10 @@ flex_set_buffer(const char* buf, int start_tok)
    , is from Perl */
 <sqbracket>","|".."|":"|"to"	return token::OP_SQBKT_SEP;
 
-  /* In SVA  you use [=1:$] instead of [=1..].  We will also
-     accept [=1..$] and [=1:].  */
-<sqbracket>"$"			return token::OP_UNBOUNDED;
+  /* In SVA you use [=1:$] instead of [=1..].  We will also accept
+     [=1..$] and [=1:].  The PSL LRM shows examples like [=1:inf]
+     instead, so will accept this too.  */
+<sqbracket>"$"|"inf"		return token::OP_UNBOUNDED;
 
   /* & and | come from Spin.  && and || from LTL2BA.
      /\, \/, and xor are from LBTT.
diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test
index b6b3c2c6a..a2e0a886e 100755
--- a/src/ltltest/equals.test
+++ b/src/ltltest/equals.test
@@ -158,12 +158,12 @@ run 0 ../equals '{a[*][*2..3]}' '{a[*]}'
 run 0 ../equals '{a[*..3][*2]}' '{a[*..6]}'
 run 0 ../equals '{a[*..3][*to2]}' '{a[*:6]}'
 run 0 ../equals '{a[*..3][*2..$]}' '{a[*]}'
-run 0 ../equals '{a[*..3][*2:]}' '{a[*]}'
+run 0 ../equals '{a[*..3][*2:]}' '{a[*:inf]}'
 run 0 ../equals '{a[*1..]}' '{a[+]}'
 run 0 ../equals '{a[+][*1..3]}' '{a[+]}'
 run 0 ../equals '{a[*1..3][+]}' '{a[+]}'
 run 0 ../equals '{[*2][+]}' '{[*2][+]}'
-run 0 ../equals '{[+][*2]}' '{[*2..]}'
+run 0 ../equals '{[+][*2]}' '{[*2..inf]}'
 
 run 0 ../equals '{0[=2]}' '0'
 run 0 ../equals '{0[=2..]}' '0'