Efficient symbolic execution of large quantifications in a process algebra

This paper describes three optimization techniques for a process algebra interpreter called EB(3)PAL This interpreter supports the EB3 method, which was developed for the purpose of automating the development of information systems using efficient symbolic execution of abstract specifications. The proposed optimizations allow an interpreter to execute actions on a quantified choice in constant time and on a quantified parallel composition in logarithmic time with respect to the number of entities in a quantified entity type. This time complexity is comparable to that of programmer-derived implementation of process expressions and significantly better than the time complexity of common process algebra simulators, which execute quantifications by computing their expansion into binary expressions.