Journal of Computer Science and Technology

, Volume 21, Issue 1, pp 41–51 | Cite as

Remove Irrelevant Atomic Formulas for Timed Automaton Model Checking

  • Jian-Hua ZhaoEmail author
  • Xuan-Dong Li
  • Tao Zheng
  • Guo-Liang Zheng


Most of the timed automata reachability analysis algorithms in the literature explore the state spaces by enumeration of symbolic states, which use time constraints to represent a set of concrete states. A time constraint is a conjunction of atomic formulas which bound the differences of clock values. In this paper, it is shown that some atomic formulas of symbolic states generated by the algorithms can be removed to improve the model checking time- and space-efficiency. Such atomic formulas are called as irrelevant atomic formulas. A method is also presented to detect irrelevant formulas based on the test-reset information about clock variables. An optimized model-checking algorithm is designed based on these techniques. The case studies show that the techniques presented in this paper significantly improve the space- and time-efficiency of reachability analysis.


formal method model checking timed automaton 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Kim G Larsen, Paul Pettersson, Wang Yi. UPPAAL: Status & Developments. In Proc. the 9th International Conference on Computer-Aided Verification, Orna Grumberg, (ed.), Haifa, Israel, Springer-Verlag, June 1997, LNCS 1254, pp.456–459.Google Scholar
  2. 2.
    Daws C, Olivero A, Tripakis S, Yovine S. The tool Kronos. In DIMACS Workshop on Verification and Control of Hybrid Systems, LNCS 1066, Springer-Verlag, October 1995.Google Scholar
  3. 3.
    Henzinger T A, Ho P H. Hytech: The Cornell hybrid technology tool. In Proc. Workshop on Tools and Algorithms for the Construction and Analysis of Systems, 1995, BRICS report series NS-95-2.Google Scholar
  4. 4.
    Rajeev Alur, David L Dill. A theory of timed automata. Journal of Theoretical Computer Science, 1994, 126(2): 183–235.Google Scholar
  5. 5.
    Gerd Behrmann, Alexandre David, Kim Guldstrand Larsen. A Tutorial on UPPAAL. In Formal Methods for the Design of Real-Time Systems, International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13–18, 2004, Revised Lectures, Lecture Notes in Computer Science 3185, Springer 2004, ISBN 3-540-23068-8.Google Scholar
  6. 6.
    Tomas Gerhard Rokicki. Representing and modeling digital circuits [Dissertation]. Stanford University, 1993.Google Scholar
  7. 7.
    Johan Bengtsson. Clocks, DBMs and states in timed systems, [Dissertation], Uppsala University, 2002.Google Scholar
  8. 8.
    Zhao Jianhua, Dang Van Hung. Checking timed automata for linear duration properties. Journal of Computer Science and Technology, Sept. 2000, 15(5): 423–429.Google Scholar
  9. 9.
    Li Yong, Dang Van Hung. Checking temporal duration properties of timed automata. Journal of Computer Science and Technology, Nov. 2002, 17(6): 689–698.Google Scholar
  10. 10.
    Zhao Jianhua, Li Xuandong, Zheng Tao, Zheng Guoliang. Removing irrelevant atomic formulas for checking timed automata efficiently. In Proc. FORMATS'03, Marseille, France, September 6–7, 2003, LNCS 2791, pp.34–45.Google Scholar
  11. 11.
    Kalus Havelund, Arne Skou, Kim G Larsen, Kristian Lund. Formal modelling and analysis of an audio/video protocol: An industrial case study using UPPAAL. In Proc. of 18th IEEE Real-Time Systems Symposium, IEEE Computer Society Press, December 1997, pp.2–13.Google Scholar
  12. 12.
    Daws C, Yovine S. Reducing the number of clock variables of timed automata. In Proc. the 17th IEEE Real Time Systems Symposium, RTSS'96, Washington DC, USA, December 1996, IEEE Computer Society Press, pp.73–81.Google Scholar

Copyright information

© Springer Science + Business Media, Inc. 2006

Authors and Affiliations

  • Jian-Hua Zhao
    • 1
    • 2
    Email author
  • Xuan-Dong Li
    • 1
    • 2
  • Tao Zheng
    • 2
  • Guo-Liang Zheng
    • 1
    • 2
  1. 1.State Key Laboratory of Novel Software TechnologyNanjing UniversityNanjingP.R. China
  2. 2.Department of Computer Science and TechnologyNanjing UniversityNanjingP.R. China

Personalised recommendations