@article{10.1145_3776661,
    author = {Balasubramanian, A. R. and Hague, Matthew and Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg},
    title = {General Decidability Results for Systems with Continuous Counters},
    year = {2026},
    issue_date = {January 2026},
    publisher = {Association for Computing Machinery},
    address = {New York, NY, USA},
    volume = {10},
    number = {POPL},
    url = {https://doi.org/10.1145/3776661},
    doi = {10.1145/3776661},
    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.},
    journal = {Proc. ACM Program. Lang.},
    month = {jan},
    articleno = {19},
    numpages = {28},
    keywords = {Continuous Counters, Decidability, Regular Language, Vector Addition System},
    date-added = {2026-1-9 11:4:36 +0100}
}

@article{10.1145_3776661, author = {Balasubramanian, A. R. and Hague, Matthew and Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg}, title = {General Decidability Results for Systems with Continuous Counters}, year = {2026}, issue_date = {January 2026}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = {10}, number = {POPL}, url = {https://doi.org/10.1145/3776661}, doi = {10.1145/3776661}, 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.}, journal = {Proc. ACM Program. Lang.}, month = {jan}, articleno = {19}, numpages = {28}, keywords = {Continuous Counters, Decidability, Regular Language, Vector Addition System}, date-added = {2026-1-9 11:4:36 +0100} }