more families of LTL formulas for genltl
The page http://www.schuppan.de/viktor/atva11/ has a link to a tarball with 3723 formulas (each of them is expressed in various syntax and also in negated form, so the total appears to be much larger). All these formulas comes with references to their sources, and many of them are actually scalable patterns (manually?) instantiated for multiple values. I suspect that many of those scalable patterns would fit well in
genltl; and it might make sense to also consider some of the non-scalable satisfiability formulas even if these are not model-checking properties.