LOCAL OPTIMIZATION ALGORITHMS FOR SYMBOLIC TRANSITION GRAPHS WITH ASSIGNMENT

Symbolic transition graph with assignment（STGA） is a new model for value passing processes. An algorithm with “on the fly instantiation” has already been proposed to automatically check bisimulation equivalence between value passing processes represented by STGAs. As a single node in an STGA corresponds to many nodes in the “instantiated” transition graph, optimization on STGA will significantly improve the time and space efficiencies of bisimulation checking algorithms. A group of local optimization algorithms are introduced in this paper, with their correctness proof outlined, and some examples from applications are presented to illustrate their effectiveness.