带赋值符号迁移图的局部优化算法  

LOCAL OPTIMIZATION ALGORITHMS FOR SYMBOLIC TRANSITION GRAPHS WITH ASSIGNMENT

作　　者：方海[1] 许文[1] 林惠民[1] 

机构地区：[1]中国科学院软件研究所计算机科学实验室,北京100080

出　　处：《计算机研究与发展》2000年第1期95-101,共7页Journal of Computer Research and Development

基　　金：国家自然科学基金重点项目!(项目编号69833020)和中国科学院"九五"基础研究重点项目

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

关 键 词：传值进程 符号迁移图 赋值 局部优化算法 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]