General Decidability Results for Systems with Continuous Counters
Abstract
Counters that hold natural numbers are ubiquitous in modeling and verifying software systems; for example, they model dynamic creation and use of resources in concurrent programs. Unfortunately, such discrete counters often lead to extremely high complexity. Continuous counters are an efficient over-approximation of discrete counters. They are obtained by relaxing the original counters to hold values over the non-negative rational numbers. This work shows that continuous counters are extraordinarily well-behaved in terms of decidability. Our main result is that, despite continuous counters being infinite-state, the language of sequences of counter instructions that can arrive in a given target configuration, is regular. Moreover, a finite automaton for this language can be computed effectively. This implies that a wide variety of transition systems can be equipped with continuous counters, while maintaining decidability of reachability properties. Examples include higher-order recursion schemes, well-structured transition systems, and decidable extensions of discrete counter systems. We also prove a non-elementary lower bound for the size of the resulting finite automaton.
Cite
@article{arxiv.2511.21559,
title = {General Decidability Results for Systems with Continuous Counters},
author = {A. R. Balasubramanian and Matthew Hague and Rupak Majumdar and Ramanathan S. Thinniyam and Georg Zetzsche},
journal= {arXiv preprint arXiv:2511.21559},
year = {2025}
}