General Decidability Results for Systems with Continuous Counters
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866909926746488832 |
|---|---|
| author | Balasubramanian, A. R. Hague, Matthew Majumdar, Rupak Thinniyam, Ramanathan S. Zetzsche, Georg |
| author_facet | Balasubramanian, A. R. Hague, Matthew Majumdar, Rupak Thinniyam, Ramanathan S. Zetzsche, Georg |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_21559 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | General Decidability Results for Systems with Continuous Counters Balasubramanian, A. R. Hague, Matthew Majumdar, Rupak Thinniyam, Ramanathan S. Zetzsche, Georg Formal Languages and Automata Theory Logic in Computer Science 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. |
| title | General Decidability Results for Systems with Continuous Counters |
| topic | Formal Languages and Automata Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2511.21559 |