Determinization of One-Counter Nets

TL;DR

This paper investigates the problem of converting nondeterministic One-Counter Nets into deterministic ones, revealing undecidability in general but decidability in the case of a single input symbol.

Contribution

The paper introduces four notions of OCN determinization, analyzes their decidability, and identifies a special case where determinization becomes decidable.

Findings

Determinization is undecidable for general OCNs under most notions.

For singleton alphabet OCNs, one determinization notion is decidable.

In the singleton case, an equivalent deterministic OCN always exists.

Abstract

One-Counter Nets (OCNs) are finite-state automata equipped with a counter that is not allowed to become negative, but does not have zero tests. Their simplicity and close connection to various other models (e.g., VASS, Counter Machines and Pushdown Automata) make them an attractive model for studying the border of decidability for the classical decision problems. The deterministic fragment of OCNs (DOCNs) typically admits more tractable decision problems, and while these problems and the expressive power of DOCNs have been studied, the determinization problem, namely deciding whether an OCN admits an equivalent DOCN, has not received attention. We introduce four notions of OCN determinizability, which arise naturally due to intricacies in the model, and specifically, the interpretation of the initial counter value. We show that in general, determinizability is undecidable under most notions, but over a singleton alphabet (i.e., 1 dimensional VASS) one definition becomes decidable, and the rest become trivial, in that there is always an equivalent DOCN.