Decision Procedures for Queues with Integer Constraints
Ting Zhang,
Henny B. Sipma,
Zohar Manna
Abstract
Queues are a widely used data structure in programming languages.
They also provide an important synchronization mechanism in modeling distributed protocols.
In this paper we extend the theory of queues with the length function which maps a queue to its size, resulting in a combined theory of queues and Presburger arithmetic.
This arithmetic extension provides a natural but tight coupling
between the two theories, and hence the general Nelson-Oppen
combination method for decision procedures is not applicable.
We present a decision procedure for the quantifier-free theory as well as
a quantifier elimination procedure for the first-order theory
that can remove a block of existential quantifiers in one step.
