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.