# Regular Separability of One Counter Automata

## TL;DR

This paper proves that the regular separability problem for one counter automata without zero tests is decidable and PSpace-complete, contrasting with the undecidability of related problems for broader classes.

## Contribution

It establishes the decidability and complexity of the regular separability problem specifically for one counter automata without zero tests, a previously unresolved question.

## Key findings

- Decidability and PSpace-completeness for one counter automata without zero tests
- Undecidability results for broader classes of one counter automata
- Contrast with the undecidability of the regularity problem for the same automata

## Abstract

The regular separability problem asks, for two given languages, if there exists a regular language including one of them but disjoint from the other. Our main result is decidability, and PSpace-completeness, of the regular separability problem for languages of one counter automata without zero tests (also known as one counter nets). This contrasts with undecidability of the regularity problem for one counter nets, and with undecidability of the regular separability problem for one counter automata, which is our second result.