Undecidability of accordance for open systems with unbounded message queues
Accordance for open nets with unbounded message queues is undecidable for deadlock freedom (with and without final states). Accordance for open nets with unbounded message queues is undecidable for responsiveness (with and without final states). The coarsest precongruence that is contained in the accordance preorder for responsiveness is undecidable. Accordance for open nets with unbounded message queues is undecidable for weak termination.
open nets accordance preorder petri nets theory of computation