Abstract
In this paper, we present an efficient nondeterministic algorithm to decide nonemptiness for reversal-bounded multicounter machines. This algorithm executes in time polynomial in the size of the input and the number of reversals the counters are allowed. Previously the best known upper bound required space logarithmic in the size of the input and linear in the number of reversals. We argue that our algorithm is within some polynomial function of the optimal nondeterministic run time for many classes of these machines. Furthermore, we show that in most cases, the complexity of the nonemptiness problem does not change significantly when the reversal bound is dropped for one of the counters. In addition, we explore the changes in the complexity of the nonemptiness problem for these classes as different parameters are fixed or are given in either unary or binary. Our results yield as corollaries the answers to several unanswered questions regarding the disjointness, equivalence, and containment problems for reversal-bounded multicounter machines. Finally, we use our results to solve several problems regarding deadlock detection and unboundedness detection for systems of communicating finite state machines.
