【摘要】 带赋值符号迁移图（ＳＴＧＡ）是刻画一般传值进程的抽象计算模型，在ＳＴＧＡ 上可以用“ｏｎ－ｔｈｅ－ｆｌｙ”实例化算法来验证传值进程之间的互模拟等价．由于ＳＴＧＡ 的一个结点对应于具体迁移图的许多结点，在ＳＴＧＡ 上所作的优化对提高互模拟判定算法的时间和空间效率会产生很大的影响．文中介绍了ＳＴＧＡ 上的一组局部优化算法，证明其正确性，并通过应用实例说明对提高效率的作用．更多还原

【Abstract】 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.更多还原