吉林大学学报(工学版) ›› 2013, Vol. 43 ›› Issue (04): 1052-1058.doi: 10.7964/jdxbgxb201304033

• 论文 • 上一篇    下一篇

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

邓辉1, 吴尽昭2   

  1. 1. 北京交通大学 计算机与信息技术学院, 北京 100044;
    2. 广西民族大学 广西混杂计算与集成电路设计分析重点实验室, 南宁 530006
  • 收稿日期:2012-03-27 出版日期:2013-07-01 发布日期:2013-07-01
  • 通讯作者: 吴尽昭(1965-),男,教授,博士生导师.研究方向:形式化方法.E-mail:jinzhaowu205@gmail.com E-mail:jinzhaowu205@gmail.com
  • 作者简介:邓辉(1985-),女,博士研究生.研究方向:形式化方法.E-mail:hedy.h.deng@gmail.com
  • 基金资助:

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

Approximate bisimulation for linear semi-algebraic transition systems

DENG Hui1, WU Jin-zhao2   

  1. 1. School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China;
    2. Guangxi Key Laboratory of Hybrid Computation and IC Design Analysis, Guangxi University for Nationalities, Nanning 530006, China
  • Received:2012-03-27 Online:2013-07-01 Published:2013-07-01

RICH HTML

0   

PDF (PC)

255

摘要：

针对软件程序状态间转移关系存在不等式约束的问题,给出一种形式化的程序描述系统,即线性半代数变迁系统。在该系统的基础上,为简化软件程序结构,采用特征列的方法,提出了基于线性半代数系统共同零点的互模拟等价概念及计算方法。但在工程应用中大多数实验所得数据仅为给定误差范围内的近似值,精确的系统等价关系缺乏容错性及灵活性。为获得更恰当的系统关系,利用奇异值分解对系统进行近似处理,建立了系统的近似互模拟等价概念及计算方法。通过符号与数值混合计算,实现误差可计算及可控制。最终选取近似等价系统代替原复杂系统。并发通信程序中的实例分析表明,该方法在简化软件程序设计中具有合理性及有效性。

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

Abstract:

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 program shows that our approach is reasonable and effective for simplifying software program design.

Key words: computer software, approximate bisimulation, linear semi-algebraic transition systems, characteristic set, singular value decomposition, concurrent communication program

中图分类号: 

  • TP301

[1] Sankaranarayanan S, Sipma H B, Manna Z. Non-linear loop invariant generation using groebner bases[J]. Contemporary Mathematics, 2004, 39(1):318-329.

[2] 邓辉,吴尽昭. 多项式程序模型的互模拟等价[J]. 北京交通大学学报, 2011, 35(4):73-77. Deng Hui, Wu Jin-zhao. Bisimulation equivalen-ce for polynomial program model[J]. Journal of Beijing Jiaotong University,2011, 35(4): 73-77.

[3] Deng Hui, Wu Jin-zhao, Zhou Ning. Approximate equivalence and optimization for high-level data-path[J]. Journal of Information and Computationnal Science,2011, 8(16): 4131-4142.

[4] Van Glabbeek R J. The linear time-branching time spectrum[J]. Lecture Notes in Computer Science, 1990, 458: 278-297.

[5] Pappas G J. Bisimulation linear systems[J]. Automatica, 2003, 39(12): 2035-2047.

[6] Van der schaft A J. Bisimulation of dynamical systems[J]. Lecture Notes in Computer Science, 2004, 2293: 291-294.

[7] Haghverdi E,Tabuada P,Pappas G J.Bisimulation relations for dynamical control and hybrid systems[J].Theoretical Computer Science, 2005,342(2-3):229-261.

[8] Alter O, Brown P O, Botstein D. Singular value decomposition for genome-wide expression data processing and modeling[J]. The National Academy of Sciences, 2000, 97(18):10101-10106.

[9] 王东明. 消去法及其应用[M]. 北京:科学出版社, 2002.

[10] 吴文俊. 数字机械化[M]. 北京:科学出版社, 2003.

[11] Buchberger B. A View on the Future of Symbolic Computation[M]. New York: ACM press, 2005.

[12] Zhou Chao-chen. Program verification through computer algebra. Formal Method and Software Engineering. USA: Lecture Notes in Computer Science, 2006.

[13] 宋光艾. 高等代数[M]. 北京:清华大学出版社, 2012.
[1] 马健, 樊建平, 刘峰, 李红辉. 面向对象软件系统演化模型[J]. 吉林大学学报(工学版), 2018, 48(2): 545-550.
[2] 罗养霞, 郭晔. 基于数据依赖特征的软件识别[J]. 吉林大学学报(工学版), 2017, 47(6): 1894-1902.
[3] 李娟, 孟可心, 李月, 刘慧力. 基于相似匹配维纳滤波的地震资料噪声压制[J]. 吉林大学学报(工学版), 2017, 47(6): 1964-1968.
[4] 郑明, 卓慕瑰, 张树功, 周柚, 刘桂霞. 基于混合并行遗传算法和阈值限定法的基因调控网络构建[J]. 吉林大学学报(工学版), 2017, 47(2): 624-631.
[5] 应欢, 王东辉, 武成岗, 王喆, 唐博文, 李建军. 适用于商用系统环境的低开销确定性重放技术[J]. 吉林大学学报(工学版), 2017, 47(1): 208-217.
[6] 李勇, 黄志球, 王勇, 房丙午. 基于多源数据的跨项目软件缺陷预测[J]. 吉林大学学报(工学版), 2016, 46(6): 2034-2041.
[7] 王念滨, 祝官文, 周连科, 王红卫. 支持高效路径查询的数据空间索引方法[J]. 吉林大学学报(工学版), 2016, 46(3): 911-916.
[8] 特日跟, 江晟, 李雄飞, 李军. 基于整数数据的文档压缩编码方案[J]. 吉林大学学报(工学版), 2016, 46(1): 228-234.
[9] 康辉, 王家琦, 梅芳. 基于Pi演算的并行编程语言[J]. 吉林大学学报(工学版), 2016, 46(1): 235-241.
[10] 陈鹏飞, 田地, 杨光. 基于MVC架构的LIBS软件设计与实现[J]. 吉林大学学报(工学版), 2016, 46(1): 242-245.
[11] 刘磊, 王燕燕, 申春, 李玉祥, 刘雷. Bellman-Ford算法性能可移植的GPU并行优化[J]. 吉林大学学报(工学版), 2015, 45(5): 1559-1564.
[12] 冯晓宁, 王卓, 张旭. 基于L-π演算的WSN路由协议形式化方法[J]. 吉林大学学报(工学版), 2015, 45(5): 1565-1571.
[13] 李明哲, 王劲林, 陈晓, 陈君. 基于网络处理器的流媒体应用架构模型(VPL)[J]. 吉林大学学报(工学版), 2015, 45(5): 1572-1580.
[14] 王克朝, 王甜甜, 苏小红, 马培军. 基于频繁闭合序列模式挖掘的学生程序雷同检测[J]. 吉林大学学报(工学版), 2015, 45(4): 1260-1265.
[15] 黄宏涛，王静，叶海智，黄少滨. 基于惰性切片的线性时态逻辑性质验证[J]. 吉林大学学报(工学版), 2015, 45(1): 245-251.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
版权所有 © 《吉林大学学报(工学版)》编辑部
地址：长春市人民大街5988号　电话：+86-431-85095297　传真：+86-431-85094074　E-mail: xbgxb@jlu.edu.cn
本系统由北京玛格泰克科技发展有限公司设计开发