General Decidability Results for Systems with Continuous Counters

TL;DR

This paper demonstrates that systems with continuous counters, as an over-approximation of discrete counters, have decidable reachability properties and can be effectively analyzed using finite automata, despite their infinite state space.

Contribution

It proves that the language of sequences leading to a target configuration is regular and can be effectively recognized by a finite automaton, extending decidability to systems with continuous counters.

Findings

The language of sequences to a target configuration is regular.

Finite automata for these languages can be effectively constructed.

Decidability of reachability is maintained in 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.