| 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
--
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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion visit https://groups.google.com/d/msgid/tlaplus/E85CB80A-32E3-49F3-973F-CFA522358D03%40gmail.com. |