Trace Inclusion for One-Counter Nets Revisited

TL;DR

This paper investigates the complexity of trace inclusion problems in One-Counter Nets, showing decidability in certain cases and establishing high complexity bounds for others, thus clarifying the computational limits of these models.

Contribution

It demonstrates that trace inclusion between an OCN and a deterministic OCN is NL-complete, and proves Ackermannian completeness for the trace universality problem in nondeterministic OCN.

Findings

Trace inclusion between OCN and deterministic OCN is NL-complete.

Trace universality for nondeterministic OCN is Ackermannian complete.

Decidability varies significantly depending on restrictions applied to OCNs.

Abstract

One-Counter nets (OCN) consist of a nondeterministic finite control and a single integer counter that cannot be fully tested for zero. They form a natural subclass of both One-Counter Automata, which allow zero-tests and Petri Nets/VASS, which allow multiple such weak counters. The trace inclusion problem has recently been shown to be undecidable for OCN. In this paper, we contrast the complexity of two natural restrictions which imply decidability. First, we show that trace inclusion between an OCN and a deterministic OCN is NL-complete, even with arbitrary binary-encoded initial counter-values as part of the input. Secondly, we show Ackermannian completeness of for the trace universality problem of nondeterministic OCN. This problem is equivalent to checking trace inclusion between a finite and a OCN-process.