Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Reachability and Safety in Queue Systems
| |
|
Reachability and Safety in Queue Systems
Oscar H. Ibarra5 
| (5) |
Department of Computer Science, University of California, Santa Barbara, CA 93106, USA |
Abstract
We look at a model of a queue system M that consists of the following components:
| 1. |
Two nondeterministic finite-state machines W and R, each augmented with finitely many reversal-bounded counters (thus, each counter can be incremented or decremented by 1 and
tested for zero, but the number of alternations between nondecreasing mode and nonincreasing mode is bounded by a fixed constant).
W or R (but not both) can also be equipped with an unrestricted pushdown stack.
|
| 2. |
One unrestricted queue that can be used to send messages from W (the “writer”) to R (the “reader”). There is no bound on the length of the queue. When R tries to read from an empty queue, it receives an “empty-queue” signal. When this happens, R can continue doing other computation and can access the queue at a later time..
|
W and R operate at the same clock rate, i.e., each transition (instruction) takes one time unit. There is no central control. Note
that since M is nondeterministic there are, in general, many computation paths starting from a given initial configuration. We investigate
the decidable properties of queue systems. For example, we show that it is decidable to determine, given a system M, whether there is some computation in which R attempts to read from an empty queue. Other verification problems that we show solvable include (binary, forward, and backward)
reachability, safety, invariance, etc. We also consider some reachability questions concerning machines operating in parallel.
Supported in part by NSF grant IRI-9700370.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|