Is there a decision procedure for telling whether a spec is machine-closed?

[Andrew Helwer]

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

[Andrew Helwer]

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

Andrew

[Stephan Merz]

Hi Andrew,

the problem is certainly decidable for finite-state systems. In automata-theoretic terms, it corresponds to deciding if every prefix of a run of a Büchi automaton can be extended to an accepting run, and this question can be expressed in monadic second-order logic, which is decidable. However, I do not know of any tool that implements such a check.

In practice, machine closure is important for system specifications that describe how a system is expected to work (in contrast to problem specifications such as linearizability). I don’t remember having encountered a system specification for which the sufficient condition of requiring only assume weak or strong fairness conditions on sub-actions of the next-state relation would be unsatisfactory. Do you have a concrete example of a machine-closed system specification that requires a more complex liveness assumption?

Stephan

On 16 Dec 2024, at 16:02, Andrew Helwer <andrew...@gmail.com> 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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/2ff9a5af-baff-4382-81c9-3328f746e57dn%40googlegroups.com.