Global renaming operators in concrete process algebra (Q1106660)

Renaming operators are introduced in concrete process algebra (concrete means that abstraction and silent moves are not considered). Examples of renaming operators are given: encapsulation, pre-abstraction, and localization. We show that renamings enhance the defining power of concrete process algebra by using the example of a queue. We give a definition of the trace set of a process, see when equality of trace sets implies equality of processes, and use trace sets to define the restriction of a process. Finally, we describe processes with actions that have a side effect on a state space and show how to use this for a translation of computer programs into process algebra.