---
author:
- Shaull Almagor
- Udi Boker
- Piotr Hofman
- Patrick Totzke
bibliography:
- 'autocleaned.bib'
title: 'Parametrized Universality Problems for One-Counter Nets'
---

Introduction {#sec:intro}
============

One-Counter Nets (OCNs) are finite-state machines equipped with an integer counter that cannot decrease below zero and which cannot be explicitly tested for zero. They are the same as 1-dimensional Vector Addition Systems (or Petri nets with exactly one unbounded place). In order to use them as formal language acceptors we assume that transitions are labelled with letters from a finite alphabet and that some states are marked as accepting.

OCNs are a syntactic restriction of One-Counter Automata – Minsky Machines with only one counter, which can have zero-tests, i.e., transitions that depend on the counter value being exactly zero. If counter updates are restricted to $\pm 1$, the model corresponds to Pushdown automata with a single-letter stack alphabet. OCNs are one of the simplest types of discrete infinite-state systems, which makes them suitable for exploring the decidability border of classical decision problems from automata and formal-language theory.

##### Universality Problems. {#universality-problems. .unnumbered}

The universality problem for a class of automata asks if a given automaton accepts all words over its input 