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