Bounded Stacks, Bags and Queues

摘要

We prove that a bounded stack can be specified in process algebra with just the211u001eoperators alternative and sequential composition and iteration. The bounded bag 211u001ecannot be specified with these operators, but can be specified if we add the 211u001eparallel composition operator without communication (free merge). The bounded 211u001equeue cannot even be specified in this signature; we need a form of variable 211u001ebinding such as given by general communication and encapsulation, the state 211u001eoperator, or abstraction.