Sciweavers

Share
CONCUR
2000
Springer

Reachability Analysis for Some Models of Infinite-State Transition Systems

10 years 6 months ago
Reachability Analysis for Some Models of Infinite-State Transition Systems
We introduce 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). We extend a CM 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 qu...
Oscar H. Ibarra, Tevfik Bultan, Jianwen Su
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where CONCUR
Authors Oscar H. Ibarra, Tevfik Bultan, Jianwen Su
Comments (0)
books