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.

We study asynchronously communicating open systems modeled as Petri nets with an interface. An accordance preorder describes when one open system can be safely replaced by another open system without affecting some behavioral property of the overall system. Although accordance is decidable for several behavioral properties if we assume a previously known bound on the maximal number of pending messages, we show that it is not decidable without this assumption.