Dear Team, I am conducting an experiment to determine the performance/capacity of atomic propositions that SPOT can handle when an intersecting run is requested from a Buchi automaton and an LTL formula. The experiment uses standard SPOT functionality: The command line utility 'Randaut' and 'RandLtl'. Finally, I have been able to obtain the desired output and have no obstacles anymore. However, during the setup of the experiment, I observed that at least two random generated formulas resulted in an error: 1. a C++ program I made, eventually resulted in error: " terminate called after throwing an instance of 'std::bad_alloc' what(): std::bad_alloc" 2. The online translator at https://spot.lrde.epita.fr/app/ presented a timeout with the same formula. 3. The spot-sandbox automata notebook at https://spot-sandbox.lrde.epita.fr/notebooks/examples%20(read%20only)/automa... Presented the error: Kernel Restarting. The kernel appears to have died. It will restart automatically. There is no specific use for the specific formulas, so I removed those from the experiment. I successfully ran the remaining batches. The annoying part: It was not immediately obvious that my program actually froze due to a 'questionable' formula instead of doing some heavy lifiting on huge automatons. resulting in some useless waiting time. I am not aware if there is a way to determine upfront whether there such a formula will exist in a set. I did not investigate if the likelihood can be reduced by manipulating a specific operator priority (option of randltl). There are too few formulas that exbibit this behavior. Question: Are such formulas a natural aspect of LTL of is this maybe a bug? Is it an option to avoid or reduce the likelihood of occurrence of such formulas in RandLTL? (making it less random :-) ) The affected formulas were: 1. G((p0) & (((p15) <-> ((G((p5) & (((p14) xor (G(p2))) <-> (G(X(p1)))))) U ((G(p8)) M (p7)))) -> ((p12) M (p6)))) 2. (((G((F(p5)) <-> (G(p7)))) & ((p8) <-> (F(p9)))) xor ((!(p0)) U (p1))) M ((X(p5)) & (F(p4))) Kind regards Carlo Sengers Master Student Software Engineering