On Saturday, November 19, 2016 at 11:00:30 AM UTC+2, Stephan Merz wrote:
The idea of machine closure is that the state machine executing the safety part of the specification does not need "prescience" in order to make those choices that will be compatible with the liveness condition: any choice allowed by the next-state relation can be completed to an infinite behavior satisfying the overall specification, using a fair scheduler.
OK! So now I understand the importance of machine closure much better (and should probably go back and read about it more carefully), and I guess this is one more reason for the importance of stuttering invariance. Anyway, this precisely addresses my question. If algorithms that are not machine-closed are discarded as "invalid", they do not muddle the equivalence. The only problem is (I think) that such formulas cannot themselves be detected within the logic, correct?
Thanks!