线性半代数变迁系统的近似互模拟等价  

Approximate bisimulation for linear semi-algebraic transition systems

作　　者：邓辉[1] 吴尽昭[2] 

机构地区：[1]北京交通大学计算机与信息技术学院,北京100044 [2]广西民族大学广西混杂计算与集成电路设计分析重点实验室,南宁530006

出　　处：《吉林大学学报（工学版）》2013年第4期1052-1058,共7页Journal of Jilin University:Engineering and Technology Edition

基　　金：国家自然科学基金项目(60973147;60873118);高等学校博士学科点专项科研基金项目(20090009110006);广西自然科学基金项目(2011GXNSFA018154);广西壮族自治区主席科技基金项目(10169-1);广西教育厅科研项目(201012MS274)

摘　　要：针对软件程序状态间转移关系存在不等式约束的问题,给出一种形式化的程序描述系统,即线性半代数变迁系统。在该系统的基础上,为简化软件程序结构,采用特征列的方法,提出了基于线性半代数系统共同零点的互模拟等价概念及计算方法。但在工程应用中大多数实验所得数据仅为给定误差范围内的近似值,精确的系统等价关系缺乏容错性及灵活性。为获得更恰当的系统关系,利用奇异值分解对系统进行近似处理,建立了系统的近似互模拟等价概念及计算方法。通过符号与数值混合计算,实现误差可计算及可控制。最终选取近似等价系统代替原复杂系统。并发通信程序中的实例分析表明,该方法在简化软件程序设计中具有合理性及有效性。As the transitions of states for software program have inequality constraints, a formal description, named linear semi-algebraic transition system, is proposed for program. With using characteristic set, a novel notion of bisimulation is established to simplify the structure of programs on the basis of common zeros of linear semi-algebraic systems. However, in applications, most of experimental data only have approximate values within an given error range. Therefore, the exact equivalence relations lack fault tolerance and flexibility. To obtain more appropriate relations for software programs, Singular Value Decomposition （SVD） is used to approximately process the systems and achieve the notion and calculation of approximate bisimulation. By symbolic and numerical hybrid computation, the error is computed and controlled. Finally, the approximate system is used to replace the original complex system. A case analysis of concurrent communication programshows that our approach is reasonable and effective for simplifying software program design.

关 键 词：计算机软件 近似互模拟 线性半代数变迁系统 特征列 奇异值分解 并发通信程序 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]