================================================================================
P9424   M.A. Bezem & A. Ponse
        "Two finite specifications of a queue"


Two finite specifications of a queue in ACP with abstraction are proven
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 muCRL, and the only `tau-laws' used are x.tau=x
and x(tau(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.