"Pert, Charles" c.pert22@imperial.ac.uk writes:

I am specifically trying to generate unsatisfiable LTL formulae using the randltl tool in Spot. I am struggling because the default tool is so much more likely to produce consistent and satisfiable formulae. Have you got any tips on how I can alter the generation to produce these types of formulae?

Hi Charles,

I'm not surprised that random formulas are very often satisfiable. With the current state of the tool, I don't know how to build unsatisfiable formulas more efficiently.

However https://gitlab.lre.epita.fr/spot/spot/-/issues/400 links to a paper where they build their benchmark by doing conjunctions of known patterns, and claim to have 50% of unsatisfiable cases. This is a feature we would like to have at some point, but unfortunately not very high priority at the moment.

Alexandre