TCTL Inevitability Analysis of Dense-Time Systems

  • Farn Wang
  • Geng-Dian Hwang
  • Fang Yu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2759)


Inevitability properties in branching temporal logics are of the syntax ∀◊φ, where φ is an arbitrary (timed) CTL formula. Such inevitability properties in dense-time logics can be analyzed with greatest fixpoint calculation. We present algorithms to model-check inevitability properties both with and without non-Zeno computation requirement. We discuss a technique for early decision on greatest fixpoint calculation. Our algorithms come with a d-parameter for the measurement of time-progress. We have experimented with various issues, which may affect the performance of TCTL inevitability analysis. Specifically, we report the performance of our implementation w.r.t. various d-parameter values and with or without the non-Zeno computation requirement in the evaluation of greatest fixpoints. We have also experimented with safe abstration techniques for model-checking TCTL inevitability properties. Analysis of experiment data helps clarify how various techniques can be used to improve verification of inevitability properties.


Branching temporal logics TCTL real-time systems inevitability model-checking greatest fixpoint abstraction 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    R. Alur, C. Courcoubetis, D.L. Dill. Model Checking for Real-Time Systems, IEEE LICS, 1990.Google Scholar
  2. [2]
    R. Alur, D. L. Dill. Automata for modelling real-time systems. ICALP’ 1990, LNCS 443, Springer-Verlag, pp.322–335.Google Scholar
  3. [3]
    B. Alpern, F.B. Schneider. Defining Liveness. Information Processing Letters 21,4 (October 1985), 181–185.zbMATHCrossRefMathSciNetGoogle Scholar
  4. [4]
    F. Balarin. Approximate Reachability Analysis of Timed Automata. IEEE RTSS, 1996.Google Scholar
  5. [5]
    G. Behrmann, K. G. Larsen, J. Pearson, C. Weise, Wang Yi. Efficient Timed Reachability Analysis Using Clock Difference Diagrams. CAV’99, July, Trento, Italy, LNCS 1633, Springer-Verlag.Google Scholar
  6. [6]
    P. Cousot, R. Cousot. Abstract Interpretation and application to logic programs. Journal of Logic Programming, 13(2–3):103–179, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  7. [7]
    E. Clarke, E.A. Emerson, A.P. Sistla. Automatic Verification of Finite-State Concurrent Systems using Temporal-Logic Specifications, ACM Trans. Programming, Languages, and Systems, 8, Nr. 2, pp. 244–263.Google Scholar
  8. [8]
    E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. Counterexample-guided Abstraction Refinement. CAV’2000.Google Scholar
  9. [9]
    D.L. Dill. Timing Assumptions and Verification of Finite-state Concurrent Systems. CAV’89, LNCS 407, Springer-Verlag.Google Scholar
  10. [10]
    C. Daws, A. Olivero, S. Tripakis, S. Yovine. The tool KRONOS. The 3rd Hybrid Systems, 1996, LNCS 1066, Springer-Verlag.CrossRefGoogle Scholar
  11. [11]
    E.A. Emerson. Uniform Inevitability is tree automataon ineffable. Information Processing Letters 24(2), Jan 1987, pp.77–79.zbMATHCrossRefMathSciNetGoogle Scholar
  12. [12]
    T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine. Symbolic Model Checking for Real-Time Systems, IEEE LICS 1992.Google Scholar
  13. [13]
    P.-A. Hsiung, F. Wang. User-Friendly Verification. Proceedings of 1999 FORTE/PSTV, October, 1999, Beijing. Formal Methods for Protocol Engineering and Distributed Systems, editors: J. Wu, S.T. Chanson, Q. Gao; Kluwer Academic Publishers.Google Scholar
  14. [14]
    F. Laroussinie, K. G. Larsen. CMC: A Tool for Compositional Model-Checking of Real-Time Systems. FORTE/PSTV’98, Kluwer.Google Scholar
  15. [15]
    K.G. Larsen, F. Larsson, P. Pettersson, Y. Wang. Efficient Verification of Real-Time Systems: Compact Data-Structure and State-Space Reduction. IEEE RTSS, 1998.Google Scholar
  16. [16]
    J. Moller, J. Lichtenberg, H.R. Andersen, H. Hulgaard. Difference Decision Diagrams, in proceedings of Annual Conference of the European Association for Computer Science Logic (CSL), Sept. 1999, Madreid, Spain.Google Scholar
  17. [17]
    Z. Manna, A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.Google Scholar
  18. [18]
    M.O. Moller. Parking Can Get You There Faster — Model Augmentation to Speed up Real-Time Model Checking. Electronic Notes in Theoretical Computer Science 65(6), 2002.Google Scholar
  19. [19]
    A.W. Mazurkiewicz, E. Ochmanski, W. Penczek. Concurrent Systems and Inevitability. TCS 64(3): 281–304, 1989.zbMATHCrossRefMathSciNetGoogle Scholar
  20. [20]
    P. Pettersson, K. G. Larsen, UPPAAL2k. in Bulletin of the European Association for Theoretical Computer Science, volume 70, pages 40–44, 2000.Google Scholar
  21. [21]
    A. Pnueli, The Temporal Logic of Programs, 18th annual IEEE-CS Symp. on Foundations of Computer Science, pp. 45–57, 1977.Google Scholar
  22. [22]
    F. Wang. Efficient Data-Structure for Fully Symbolic Verification of Real-Time Software Systems. TACAS’2000, March, Berlin, Germany. in LNCS 1785, Springer-Verlag.Google Scholar
  23. [23]
    F. Wang. Region Encoding Diagram for Fully Symbolic Verification of Real-Time Systems. the 24th COMPSAC, Oct. 2000, Taipei, Taiwan, ROC, IEEE press.Google Scholar
  24. [24]
    F. Wang. RED: Model-checker for Timed Automata with Clock-Restriction Diagram. Workshop on Real-Time Tools, Aug. 2001, Technical Report 2001-014, ISSN 1404-3203, Dept. of Information Technology, Uppsala University.Google Scholar
  25. [25]
    F. Wang. Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram, Proceedings of FORTE, August 2001, Cheju Island, Korea.Google Scholar
  26. [26]
    F. Wang. Efficient Verification of Timed Automata with BDD-like Data-Structures. proceedings of VMCAI’2003, LNCS 2575, Springer-Verlag.Google Scholar
  27. [27]
    F. Wang, P.-A. Hsiung. Automatic Verification on the Large. Proceedings of the 3rd IEEE HASE, November 1998.Google Scholar
  28. [28]
    F. Wang, P.-A. Hsiung. Efficient and User-Friendly Verification. IEEE Transactions on Computers, Jan. 2002.Google Scholar
  29. [29]
    F. Wang, G.-D. Hwang, F. Yu. Symbolic Simulation of Real-Time Concurrent Systems. to appear in proceedings of RTCSA’2003, Feb. 2003, Tainan, Taiwan, ROC.Google Scholar
  30. [30]
    H. Wong-Toi. Symbolic Approximations for Verifying Real-Time Systems. Ph.D. thesis, Stanford University, 1995.Google Scholar
  31. [31]
    S. Yovine. Kronos: A Verification Tool for Real-Time Systems. International Journal of Software Tools for Technology Transfer, Vol. 1, Nr. 1/2, October 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Farn Wang
    • 1
  • Geng-Dian Hwang
    • 2
  • Fang Yu
    • 2
  1. 1.Dept. of Electrical EngineeringNational Taiwan UniversityTaipeiTaiwan, Republic of China
  2. 2.Institute of Information ScienceAcademia SinicaTaipeiTaiwan, Republic of China

Personalised recommendations