diff --git a/NEWS b/NEWS
index 8fb613a45..dca4b5b54 100644
--- a/NEWS
+++ b/NEWS
@@ -6,8 +6,9 @@ New in spot 2.3.2.dev (not yet released)
     implemented.
 
   - genltl learned --spec-patterns as an alias for --dac-patterns; it
-    also learned a new set of LTL formulas under --hkrss-patterns
-    (a.k.a. --liberouter-patterns).
+    also learned two new sets of LTL formulas under --hkrss-patterns
+    (a.k.a. --liberouter-patterns) and --p-patterns
+    (a.k.a. --beem-patterns).
 
   Library:
 
diff --git a/bin/genltl.cc b/bin/genltl.cc
index 9d39d894a..dc23f0254 100644
--- a/bin/genltl.cc
+++ b/bin/genltl.cc
@@ -142,6 +142,19 @@
 //    number = 03,
 //    institution = {CESNET}
 // }
+//
+// @InProceedings{pelanek.07.spin,
+//   author = {Radek Pel\'{a}nek},
+//   title = {{BEEM}: benchmarks for explicit model checkers},
+//   booktitle = {Proceedings of the 14th international SPIN conference on
+//     Model checking software},
+//   year = 2007,
+//   pages = {263--267},
+//   numpages = {5},
+//   volume = {4595},
+//   series = {Lecture Notes in Computer Science},
+//   publisher = {Springer-Verlag}
+// }
 
 
 #include "common_sys.hh"
@@ -196,6 +209,7 @@ enum {
   OPT_OR_FG,
   OPT_OR_G,
   OPT_OR_GF,
+  OPT_P_PATTERNS,
   OPT_R_LEFT,
   OPT_R_RIGHT,
   OPT_RV_COUNTER,
@@ -235,6 +249,7 @@ const char* const class_name[LAST_CLASS - FIRST_CLASS] =
     "or-fg",
     "or-g",
     "or-gf",
+    "p-patterns",
     "or-r-left",
     "or-r-right",
     "rv-counter",
@@ -303,6 +318,11 @@ static const argp_option options[] =
     OPT_ALIAS(gh-s),
     { "or-gf", OPT_OR_GF, "RANGE", 0, "GF(p1)|GF(p2)|...|GF(pn)", 0 },
     OPT_ALIAS(gh-c1),
+    { "p-patterns", OPT_P_PATTERNS, "RANGE", OPTION_ARG_OPTIONAL,
+      "Pelánek [Spin'07] patterns from BEEM "
+      "(range should be included in 1..20)", 0 },
+    OPT_ALIAS(beem-patterns),
+    OPT_ALIAS(p),
     { "r-left", OPT_R_LEFT, "RANGE", 0, "(((p1 R p2) R p3) ... R pn)", 0 },
     { "r-right", OPT_R_RIGHT, "RANGE", 0, "(p1 R (p2 R (... R pn)))", 0 },
     { "rv-counter", OPT_RV_COUNTER, "RANGE", 0,
@@ -436,6 +456,12 @@ parse_opt(int key, char* arg, struct argp_state*)
       else
         enqueue_job(key, 1, 12);
       break;
+    case OPT_P_PATTERNS:
+      if (arg)
+        enqueue_job(key, arg);
+      else
+        enqueue_job(key, 1, 20);
+      break;
     case OPT_SB_PATTERNS:
       if (arg)
         enqueue_job(key, arg);
@@ -1142,6 +1168,38 @@ eh_pattern(int n)
   return spot::relabel(parse_formula(formulas[n - 1]), Pnn);
 }
 
+static formula
+p_pattern(int n)
+{
+  static const char* formulas[] = {
+    "G(p0 -> Fp1)",
+    "(GFp1 & GFp0) -> GFp2",
+    "G(p0 -> (p1 & (p2 U p3)))",
+    "F(p0 | p1)",
+    "GF(p0 | p1)",
+    "(p0 U p1) -> ((p2 U p3) | Gp2)",
+    "G(p0 -> (!p1 U (p1 U (!p1 & (p2 R !p1)))))",
+    "G(p0 -> (p1 R !p2))",
+    "G(!p0 -> Fp0)",
+    "G(p0 -> F(p1 | p2))",
+    "!(!(p0 | p1) U p2) & G(p3 -> !(!(p0 | p1) U p2))",
+    "G!p0 -> G!p1",
+    "G(p0 -> (G!p1 | (!p2 U p1)))",
+    "G(p0 -> (p1 R (p1 | !p2)))",
+    "G((p0 & p1) -> (!p1 R (p0 | !p1)))",
+    "G(p0 -> F(p1 & p2))",
+    "G(p0 -> (!p1 U (p1 U (p1 & p2))))",
+    "G(p0 -> (!p1 U (p1 U (!p1 U (p1 U (p1 & p2))))))",
+    "GFp0 -> GFp1",
+    "GF(p0 | p1) & GF(p1 | p2)",
+  };
+
+  constexpr unsigned max = (sizeof formulas)/(sizeof *formulas);
+  if (n < 1 || (unsigned) n > max)
+    bad_number("--p-patterns", n, max);
+  return spot::relabel(parse_formula(formulas[n - 1]), Pnn);
+}
+
 static formula
 sb_pattern(int n)
 {
@@ -1488,6 +1546,9 @@ output_pattern(int pattern, int n)
     case OPT_OR_GF:
       f = GF_n("p", n, false);
       break;
+    case OPT_P_PATTERNS:
+      f = p_pattern(n);
+      break;
     case OPT_R_LEFT:
       f = bin_n("p", n, op::R, false);
       break;
diff --git a/bin/man/genltl.x b/bin/man/genltl.x
index b9f224a71..74fcfb4f2 100644
--- a/bin/man/genltl.x
+++ b/bin/man/genltl.x
@@ -46,6 +46,10 @@ kv
 O. Kupferman and M. Y. Vardi: From Linear Time to Branching Time.
 ACM Transactions on Computational Logic, 6(2):273-294, 2005.
 .TP
+p
+R. Pelánek: BEEM: benchmarks for explicit model checkers
+Proceedings of Spin'07.  LNCS 4595.
+.TP
 rv
 K. Rozier and M. Vardi: LTL Satisfiability Checking.
 Proceedings of Spin'07.  LNCS 4595.
diff --git a/doc/org/genltl.org b/doc/org/genltl.org
index 963b0156a..d7952ad1b 100644
--- a/doc/org/genltl.org
+++ b/doc/org/genltl.org
@@ -133,15 +133,15 @@ This is because most tools using =lbt='s syntax require atomic
 propositions to have the form =pNN=.
 
 
-Four options provide lists of unrelated LTL formulas, taken from the
+Five options provide lists of unrelated LTL formulas, taken from the
 literature (see the [[./man/genltl.1.html][=genltl=]](1) man page for references):
-=--dac-patterns=, =--eh-patterns=, =--hkrss-patterns=, and
-=--sb-patterns=.  With these options, the range is used to select a
-subset of the list of formulas.  Without range, all formulas are used.
-Here is the complete list:
+=--dac-patterns=, =--eh-patterns=, =--hkrss-patterns=, =--p-patterns=,
+and =--sb-patterns=.  With these options, the range is used to select
+a subset of the list of formulas.  Without range, all formulas are
+used.  Here is the complete list:
 
 #+BEGIN_SRC sh :results verbatim :exports both
-  genltl --dac --eh --hkrss --sb --format=%F:%L,%f
+  genltl --dac --eh --hkrss --p --sb --format=%F:%L,%f
 #+END_SRC
 
 #+RESULTS:
@@ -268,6 +268,26 @@ hkrss-patterns:52,XG(p0 -> (G!p1 | (!Xp1 U p2)))
 hkrss-patterns:53,XG((p0 & !p1) -> (G!p1 | (!p1 U p2)))
 hkrss-patterns:54,XG((p0 & p1) -> ((p1 U p2) | Gp1))
 hkrss-patterns:55,Xp0 & G((!p0 & Xp0) -> XXp0)
+p-patterns:1,G(p0 -> Fp1)
+p-patterns:2,(GFp1 & GFp0) -> GFp2
+p-patterns:3,G(p0 -> (p1 & (p2 U p3)))
+p-patterns:4,F(p0 | p1)
+p-patterns:5,GF(p0 | p1)
+p-patterns:6,(p0 U p1) -> ((p2 U p3) | Gp2)
+p-patterns:7,G(p0 -> (!p1 U (p1 U (!p1 & (p2 R !p1)))))
+p-patterns:8,G(p0 -> (p1 R !p2))
+p-patterns:9,G(!p0 -> Fp0)
+p-patterns:10,G(p0 -> F(p1 | p2))
+p-patterns:11,!(!(p0 | p1) U p2) & G(p3 -> !(!(p0 | p1) U p2))
+p-patterns:12,G!p0 -> G!p1
+p-patterns:13,G(p0 -> (G!p1 | (!p2 U p1)))
+p-patterns:14,G(p0 -> (p1 R (p1 | !p2)))
+p-patterns:15,G((p0 & p1) -> (!p1 R (p0 | !p1)))
+p-patterns:16,G(p0 -> F(p1 & p2))
+p-patterns:17,G(p0 -> (!p1 U (p1 U (p1 & p2))))
+p-patterns:18,G(p0 -> (!p1 U (p1 U (!p1 U (p1 U (p1 & p2))))))
+p-patterns:19,GFp0 -> GFp1
+p-patterns:20,GF(p0 | p1) & GF(p1 | p2)
 sb-patterns:1,p0 U p1
 sb-patterns:2,p0 U (p1 U p2)
 sb-patterns:3,!(p0 U (p1 U p2))
diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test
index c5d523401..ae8eb7d2b 100755
--- a/tests/core/ltl2tgba2.test
+++ b/tests/core/ltl2tgba2.test
@@ -27,7 +27,7 @@
 # commonly use as benchmark change, we want to notice it.
 
 set -e
-genltl --dac --eh --sb --hkrss --format=%F,%L,%f >pos
+genltl --dac --eh --sb --hkrss --p --format=%F,%L,%f >pos
 (cat pos; ltlfilt --negate pos/3 --format='!%<,%f') |
     ltlfilt -u -F-/3 >formulas
 
@@ -183,6 +183,24 @@ hkrss-patterns,52, 4,25, 4,25, 5,29, 5,29
 hkrss-patterns,53, 3,22, 3,22, 3,22, 3,22
 hkrss-patterns,54, 3,22, 3,22, 3,22, 3,22
 hkrss-patterns,55, 5,8, 5,8, 5,8, 5,8
+p-patterns,2, 4,36, 4,36, 5,44, 5,44
+p-patterns,3, 2,20, 2,20, 2,20, 2,20
+p-patterns,4, 2,8, 2,8, 2,8, 2,8
+p-patterns,5, 1,4, 1,4, 2,8, 2,8
+p-patterns,6, 4,50, 4,50, 4,50, 4,50
+p-patterns,7, 4,27, 4,27, 4,27, 4,27
+p-patterns,8, 2,10, 2,10, 2,10, 2,10
+p-patterns,9, 1,2, 1,2, 2,4, 2,4
+p-patterns,10, 2,16, 2,16, 2,16, 2,16
+p-patterns,11, 2,20, 2,20, 2,20, 2,20
+p-patterns,12, 3,12, 3,12, 3,12, 3,12
+p-patterns,13, 3,20, 3,20, 3,20, 3,20
+p-patterns,14, 2,13, 2,13, 2,13, 2,13
+p-patterns,15, 2,7, 2,7, 2,7, 2,7
+p-patterns,16, 2,16, 2,16, 2,16, 2,16
+p-patterns,17, 3,20, 3,20, 3,20, 3,20
+p-patterns,18, 5,36, 5,36, 5,36, 5,36
+p-patterns,20, 1,8, 1,8, 3,24, 3,24
 !dac-patterns,1, 2,4, 2,4, 2,4, 2,4
 !dac-patterns,2, 3,10, 3,10, 3,10, 3,10
 !dac-patterns,3, 3,12, 3,12, 3,12, 3,12
@@ -321,6 +339,24 @@ hkrss-patterns,55, 5,8, 5,8, 5,8, 5,8
 !hkrss-patterns,53, 4,32, 4,32, 4,32, 4,32
 !hkrss-patterns,54, 4,32, 4,32, 4,32, 4,32
 !hkrss-patterns,55, 5,12, 6,12, 5,12, 6,12
+!p-patterns,2, 2,15, 2,15, 4,23, 4,23
+!p-patterns,3, 3,41, 3,41, 3,41, 3,41
+!p-patterns,4, 1,1, 1,1, 1,1, 1,1
+!p-patterns,5, 2,6, 2,6, 2,6, 2,6
+!p-patterns,6, 4,42, 4,42, 4,42, 4,42
+!p-patterns,7, 5,34, 5,34, 5,34, 5,34
+!p-patterns,8, 3,24, 3,24, 3,24, 3,24
+!p-patterns,9, 2,4, 2,4, 2,4, 2,4
+!p-patterns,10, 2,11, 2,11, 2,11, 2,11
+!p-patterns,11, 3,48, 3,48, 3,48, 3,48
+!p-patterns,12, 2,4, 2,4, 2,4, 2,4
+!p-patterns,13, 4,32, 4,32, 4,32, 4,32
+!p-patterns,14, 3,24, 3,24, 3,24, 3,24
+!p-patterns,15, 3,12, 3,12, 3,12, 3,12
+!p-patterns,16, 2,17, 2,17, 2,17, 2,17
+!p-patterns,17, 4,31, 4,31, 4,31, 4,31
+!p-patterns,18, 6,43, 6,43, 6,43, 6,43
+!p-patterns,20, 3,16, 3,16, 3,16, 3,16
 EOF
 
 diff output expected