Two finite specifications of a queue

AbstractIt is known that a queue is not finitely definable in ACP with handshaking communication (Baeten and Bergstra, 1988). In this paper, two finite specifications of a queue in ACP with abstraction and handshaking are proved correct relative to a standard specification of a queue that employs an infinite data type for representing its contents. The proofs are given in the proof theory of μCRL, and the only ‘τ-laws’ used are xτ = x and x(τ(y + z) + y) = x(y + z). Therefore the proofs are adequate for both ‘branching bisimilarity’ and ‘observation equivalence’. Additionally, it is shown that standard concurrency follows from RSP for a class of processes guardedly specifiable in ACP with abstraction