稠密时间表示及冗余消除
作者:
基金项目:

Supported by the National Natural Science Foundation of China under Grant Nos.69833020, 60203028 (国家自然科学基金)


Dense Time Representation and Redundancy Elimination
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [14]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

    算法的效率在很大程度上依赖于实际采用的数据结构.对无用数据的处理不仅会带来空间存储上的浪费,而且也会进一步造成时间上的浪费.因此,消除信息冗余一直是算法研究的一个重点.在当前实时领域(尤其是在基于稠密/连续时间语义)的算法研究中,该问题十分突出.从信息之间的依赖关系入手,分析了在对连续时间进行有穷表示和操作中存在的问题,通过改进"范式化"处理过程,给出了进行冗余信息消除的一种方法以及其正确性证明,并通过实验测试了改进的效率.

    Abstract:

    The efficiency of an algorithm depends greatly on the data structure adopted in practice, while the processing of useless data can cause not only much waste of memory but also much waste of time. Hence to eliminate redundant information is one of the main focuses in the research of algorithms, and the issue has received extensive attention in real-time field (especially those based on dense/continuous time semantics) for many years. After investigating existing problems in finite representation and operations, and by analyzing the dependence relation in information, a method is presented for eliminating redundant information in representation of dense time, which is developed based on an modification of the procedure of ‘Normalization’. The correctness of the method is proved and the efficiency is tested by experiences.

    参考文献
    [1]Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science, 1994,126(2):183~235.
    [2]Dill DL. Timing assumptions and verification of finite-state concurrent systems. In: Sifakis J, ed. Proceedings of the Automatic Verification Methods for Finite State Systems. LNCS 407, Berlin: Springer-Verlag, 197~212.
    [3]Behrmann G, Larsen KG, Pearson J, Weise C, Wang Y. Efficient timed reachability analysis using clock difference diagrams. In: Proceedings of the CAV'99. LNCS 1633, Trento, 1999. 341~353.
    [4]Asarin E, Bozga M, Kerbrat A, Maler O, Pnueli A, Rasse A. Data-Structures for the verification of timed automata. In: Proceedings of the HART'97. LNCS 1201, Grenoble, 1997. 346~360.
    [5]Wang F. Region encoding diagram for fully symbolic verification of real-time systems. In: Martin R, ed. Proceedings of the 24th IEEE COMPSAC 2000 (Computer Software and Applications Conference). Taipei: IEEE Computer Society, 2000. 509~515.
    [6]Cerans,K. Decidability of bisimulation equivalences for parallel timer processes. In: Proceedings of the CAV'92. LNCS 663, Montercal, 1992. 302~315.
    [7]Weise C, Lenzkes D. Efficient scaling-invariant checking of timed bisimulation. In: Proceedings of the STACS'97. Hansestadt Lubeck, LNCS 1200, 1997. 177~188.
    [8]Chen J, Lin HM. Timed bisimulation over timed symbolic transition graph. Chinese Journal of Computers, 2002,25(2):113~121 (in Chinese with English abstract)
    [9]Alur R, Courcoubetis C, Dill D. Model-Checking in dense real-time. Information and Computation, 1993,104(1):2~34.
    [10]Henzinger TA, Nicollin X, Sifakis J, Yovine S. Symbolic model checking for real-time systems. Information and Computation, 1994,111(2):193~244.
    [11]Wang Y, Pettersson P, Daniels, M. Automatic verification of real-time communicating systems by constraint solving. In: Hogrefe D, Leue S, eds. Proceedings of the 7th International Conference on Formal Description Techniques. Berne, Chapman & Hall, 1994. 223~238.
    [12]Backhouse RC, Gasteren AJM. Calculating a path algorithm. In: Proceedings of the Mathematics of Program Construction, the 2nd International Conference (MPC'92). LNCS 669, Oxford, 1992. 32~44.
    [13]Sedgewick, R. Algorithms. 2nd ed. Massachusetts: Addison-Wesley, 1988.
    [14]陈靖,林惠民.时间符号迁移图及其互模拟判定.计算机学报,2002,25(2):113~121.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

陈靖.稠密时间表示及冗余消除.软件学报,2003,14(10):1681-1691

复制
分享
文章指标
  • 点击次数:4201
  • 下载次数: 5394
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2002-09-03
  • 最后修改日期:2003-04-14
文章二维码
您是第19868246位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号