The web page https://spot.lrde.epita.fr/ipynb/stutter-inv.html shows how to use Spot to highlight the states in a Büchi automaton which have a stutter invariant language. It says "Such a procedure gives us map of where POR can be enabled when model checking using such an automaton.” Does anyone know a reference for this technique? I mean specifically the idea that POR is something that can be turned on or off depending on the current state of the property automaton. I feel I’ve seen that somewhere, but don’t remember where. Thanks! -Steve
Dear Stephen,
Stephen Siegel writes:
Does anyone know a reference for this technique? I mean specifically the idea that POR is something that can be turned on or off depending on the current state of the property automaton. I feel I’ve seen that somewhere, but don’t remember where.
As far as I know, this is original and not yet implemented in any model checker. It's part of some work that we started earlier this year with some colleagues. The plan was that Spot would implement the stutter-invariant state detection, and LTSmin would use that to switch on POR dynamically. The latter has not been implemented yet.
If you know of some previous work similar to that, I'm very interested.
Best regards, Alexandre
-
Alexandre Duret-Lutz -
Stephen Siegel