11 Dec
2018
11 Dec
'18
11 a.m.
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