*For the most recent entries see the
Petri Nets Newsletter.*

## Reachability analysis for some models of infinite-state transition systems.

Ibarra, O.H.;
Bultan, T.;
Su, J.
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.

*Do you need a refined search? Try our search engine
which allows complex field-based queries.*
*Back to the Petri Nets Bibliography*