Related, I found this write-up of machine closure by William Schultz which was very good. We care about machine closure because if we allow non-machine-closed liveness assumptions, our algorithm has to have prescience about whether it's about to enter a dead-end state from which it will not be able to satisfy the liveness assumption. Since algorithms don't really work that way, we want to restrict liveness assumptions to being of a particular form so that our algorithm can make simple decisions based on its current state, not on future states.
https://will62794.github.io/tlaplus/formal-methods/2020/08/05/machine-closure.html
On Monday, December 16, 2024 at 10:02:43 AM UTC-5 Andrew Helwer wrote:
Like it takes as parameters the formulas S and L and it determines whether their conjunction is machine-closed; or is such a problem undecidable?
Andrew