Efficient symbolic computation of process expressions

This paper describes three optimization techniques for the eb process algebra. The optimizations are expressed in a new deterministic operational semantics which is shown to be trace-equivalent to a traditional non-deterministic operational semantics. Internal action transitions are eliminated by an efficient preruntime analysis of the structure of a process expression. Execution environments are used to optimize variable instantiation using lazy evaluation. Non-determinism is eliminated by returning a choice between possible transitions. This new operational semantics is implemented in the ebpai process algebra interpreter to support the eb method. The goal of this method is to automate the development of information systems using, among other mechanisms, efficient symbolic computation of process expressions.