Recursive process definitions with the state operator

Abstract

We investigate the defining power of finite recursive specifications over the theory with + (alternative composition) and • (sequential composition) and λ (the state operator) over a finite set of states, and find that it is greater than that of the same theory without state operator. Thus, adding the state operator is an essential extension of BPA (the theory of processes over +, •). On the other hand, applying the state operator to a regular process again gives a regular process. As a limiting result in the other direction, we find that not all PA-processes (where also parallel composition λ is present) can be defined over BPA plus state operator.