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