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

• paper • Previous Articles     Next Articles

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

CLC Number: 

  • 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] MA Jian, FAN Jian-ping, LIU Feng, LI Hong-hui. The evolution model of objective-oriented software system [J]. 吉林大学学报(工学版), 2018, 48(2): 545-550.
[2] LUO Yang-xia, GUO Ye. Software recognition based on features of data dependency [J]. 吉林大学学报(工学版), 2017, 47(6): 1894-1902.
[3] LI Juan, MENG Ke-xin, LI Yue, LIU Hui-li. Seismic signal noise suppression based on similarity matched Wiener filtering [J]. 吉林大学学报(工学版), 2017, 47(6): 1964-1968.
[4] ZHENG Ming, ZHUO Mu-gui, ZHANG Shu-gong, ZHOU You, LIU Gui-xia. Reconstruction for gene regulatory network based on hybrid parallel genetic algorithm and threshold value method [J]. 吉林大学学报(工学版), 2017, 47(2): 624-631.
[5] YING Huan, WANG Dong-hui, WU Cheng-gang, WANG Zhe, TANG Bo-wen, LI Jian-jun. Efficient deterministic replay technique on commodity system environment [J]. 吉林大学学报(工学版), 2017, 47(1): 208-217.
[6] LI Yong, HUANG Zhi-qiu, WANG Yong, FANG Bing-wu. New approach of cross-project defect prediction based on multi-source data [J]. 吉林大学学报(工学版), 2016, 46(6): 2034-2041.
[7] WANG Nian-bin, ZHU Guan-wen, ZHOU Lian-ke, WANG Hong-wei. Novel dataspace index for efficient processing of path query [J]. 吉林大学学报(工学版), 2016, 46(3): 911-916.
[8] TE Ri-gen, JIANG Sheng, LI Xiong-fei, LI Jun. Document compression scheme based on integer data [J]. 吉林大学学报(工学版), 2016, 46(1): 228-234.
[9] CHEN Peng-fei, TIAN Di, YANG Guang. Design and implementation of LIBS software based on MVC architecture [J]. 吉林大学学报(工学版), 2016, 46(1): 242-245.
[10] LIU Lei, WANG Yan-yan, SHEN Chun, LI Yu-xiang, LIU Lei. Performance portable GPU parallel optimization technique on Bellman-Ford algorithm [J]. 吉林大学学报(工学版), 2015, 45(5): 1559-1564.
[11] FENG Xiao-ning, WANG Zhuo, ZHANG Xu. Formal method for routing protocol of WSN based on L-π calculus [J]. 吉林大学学报(工学版), 2015, 45(5): 1565-1571.
[12] LI Ming-zhe, WANG Jin-lin, CHEN Xiao, CHEN Jun. Architecture model of streaming media applications on network processors(VPL) [J]. 吉林大学学报(工学版), 2015, 45(5): 1572-1580.
[13] WANG Ke-chao, WANG Tian-tian, SU Xiao-hong, MA Pei-jun. Plagiarism detection in student programs based on frequent closed sequence mining [J]. 吉林大学学报(工学版), 2015, 45(4): 1260-1265.
[14] HUANG Hong-tao,WANG Jing,YE Hai-zhi,HUANG Shao-bin. Lazy slicing based method for verifying linear temporal logic property [J]. 吉林大学学报(工学版), 2015, 45(1): 245-251.
[15] FAN Da-juan, HUANG Zhi-qiu, XIAO Fang-xiong, ZHU Yi, WANG Jin. Compatibility analysis and adaptor generation for multi-service interaction [J]. 吉林大学学报(工学版), 2014, 44(4): 1094-1103.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
Copyright © Journal of Jilin University(Engineering and Technology Edition), All Rights Reserved.
Tel: +86-431-85095297　Fax: +86-431-85094074　E-mail: xbgxb@jlu.edu.cn
Powered by Beijing Magtech Co. Ltd