random conjunctions of patterns
https://www.cs.rice.edu/~vardi/papers/time13.pdf suggests building random LTL formulas from conjunctions of known patterns. They use the DAC patterns. We could offer such a service and even generalize it to all the patterns that
I'm not sure what the ideal interface would be. Maybe some
ltlcombine tool that takes a list of formulas as input, some yet-to-be-specified parameters, and outputs combinations of the input formulas.