In: Lecture Notes in Computer Science, Vol. 1877: Concurrency Theory, Proceedings of CONCUR 2000, pages 183-198. Springer-Verlag, 2000.
Abstract: The paper introduces some new models of infinite-state transition systems. The basic model, called a (reversal-bounded) counter machine (CM), is a nondeterministic finite automaton augmented with finitely many reversal-bounded counters (i.e., each counter can be incremented or decremented by 1 and tested for zero, but the number of times it can change mode from nondecreasing to nonincreasing and vice-versa is bounded by a constant, independent of the computation). A CM is extended by augmenting it with some familiar data structures: (i) A pushdown counter machine (PCM) is a CM augmented with an unrestricted pushdown stack. (ii) A tape counter machine (TCM) is a CM augmented with a two-way read/write worktape that is restricted in that the number of times the head crosses the boundary between any two adjacent cells of the worktape is bounded by a constant, independent of the computation (thus, the worktape is finite-crossing). There is no bound on how long the head can remain on a cell. (iii) A queue counter machine (QCM) is a CM augmented with a queue that is restricted in that the number of alternations between non-deletion phase and non-insertion phase is bounded by a constant. A non-deletion (non-insertion) phase is a period consisting of insertions (deletions) and no-changes, i.e., the queue is idle. The paper shows that emptiness, (binary, forward, and backward) reachability, nonsafety, and invariance for these machines are solvable. It also looks at extensions of the models that allow the use of linear-relation tests among the counters and parameterized constants as ``primitive'' predicates. The conditions under which these problems are still solvable are investigated.
Keywords: infinite-state transition systems, reachability analysis.