Abstract Finite automata with counters are often used to specify families of constraints. The addition of counters provides more power than membership in regular languages that is possible with finite automata. All available propagation algorithms for counter automata based constraints maintain only bounds consistency on counter variables, and although it is possible to maintain domain consistency it can be computationally very costly. In this paper we give an algorithm that decides when maintaining bounds consistency for an automata with a single counter implies domain consistency.
展开▼