Hi Alexandre and thanks for your response.

It's good you found Spot, then. So far, most people contacting us have been using only it's LTL->Büchi translator. So I'll be very interested to get any kind of feedback about your use case.

I will let you know if I manage to put something together!

Do you mean

1. that you want to reuse part of the information that have already

been computed by the emptiness check during the first run, and just invalidate anything related to the SCC that has been altered afterwards?

2. that you want the start a fresh emptiness check from scratch, but

just without deleting and re-building a new the emptiness_check instance?

I believe none of the emptiness_checks presently support either scenarios. The second one could be achieved by adding a reset() method to all emptiness_check sub classes (should be easy), but that reset() method would not bring a huge speed-up over the delete/new approach. The first approach would require much more invasive changes, and it might not be suitable with all emptiness check algorithms. Maybe an emptiness-check could be tuned to support such a "partial restart" ; it seems worth a though. Has anybody done such a thing before?

I believe I want to do (1), but I stil exploring ideas and options so it's not entirely clear how this would be done and what restrictions there will be on the modifications of the automaton. Briefly, the automaton will be a proof in some system that allows cyclic proofs (think induction) and the soundness of the proof depends on some "infinitely often" style of property. So I thought that (a) real on-the-fly model checking can be combined with proof search quite nicely and (b) when the checker comes up with a counterexample, use it to modify the proof and carry on.

I have no idea if anyone has done the partial restart before; it does not fit the standard use case for model checking, so I would not be surprised if it's never been done.

Thanks! Nikos