一句话：证明连续计数器系统到达目标配置的指令序列语言为正则，从而为多类无限状态系统保持可达性可判定。
计数器广泛用于建模与验证软件系统，如并发程序中的资源创建与使用，但离散计数器常导致极高复杂度。连续计数器将计数值松弛为非负有理数，是对离散计数器的高效过近似。本文研究连续计数器系统的可判定性，主要结果表明：尽管系统是无限状态，能够到达给定目标配置的计数器指令序列语言仍是正则的，且可有效构造其有限自动机。由此，多种迁移系统可在加入连续计数器后保持可达性可判定，包括高阶递归方案、良结构迁移系统以及离散计数器系统的可判定扩展。作者还证明了所得有限自动机规模的非初等下界。
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 higherorder 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-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 = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776661}
}