Decidability of Weak Simulation on One-counter Nets

TL;DR

This paper proves that weak simulation preorder is decidable for one-counter nets, revealing a unique convergence property at omega^2, while other relations remain undecidable.

Contribution

It establishes the decidability of weak simulation on one-counter nets and characterizes the convergence level of weak simulation approximants.

Findings

Weak simulation is decidable for OCN.

Weak simulation approximants converge at level omega^2.

Weak bisimulation and trace inclusion are undecidable for OCN.

Abstract

One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with only a weak test for zero. We show that weak simulation preorder is decidable for OCN and that weak simulation approximants do not converge at level omega, but only at omega^2. In contrast, other semantic relations like weak bisimulation are undecidable for OCN, and so are weak (and strong) trace inclusion.