Advertisement

Journal of Computer Science and Technology

, Volume 15, Issue 5, pp 423–429 | Cite as

Checking timed automata for linear duration properties

  • Zhao Jianhua Email author
  • Dang Van Hung 
Article

Abstract

It is proved in this paper that checking a timed automaton ℳ with respect to a linear duration property ⊅ can be done by investigating only the integral timed states of ℳ. An equivalence relation is introduced in this paper to divide the infinite number of integral timed states into finite number of equivalence classes. Based on this, a method is proposed for checking whether ℳ satisfies ⊅. In some cases, the number of equivalence classes is too large for a computer to manipulate. A technique for reducing the search-space for checking linear duration property is also described. This technique is more, suitable for the case in this paper than those in the literature because most of those techniques are designed for reachability analysis.

Keywords

model checking duration calculus real-time system 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    Kesten Y, Pnueli A, Sifakis J, Yovine S. Integration graphs: A class of decidable hybrid systems. InHybrid System, No. 736 in LNCS, 1993, pp. 179–208.Google Scholar
  2. [2]
    Zhou Chaochen, Zhang Jingzhong, Yang Lu, Li Xiaoshan. Linear duration invariants. InProc. Formal Techniques in Real-Time and Fault-Tolerant Systems, No. 863 in LNCS, 1994, pp. 373–382.Google Scholar
  3. [3]
    Li Xuandong, Dang Van Hung. Checking linear duration invariants by linear programming. InConcurrency and Parallelism, Programming, Networking, and Security, Joxam Jaffar, Roland H C Yap (eds.), No. 1179 in LNCS, Springer-Verlag, December 1996, pp. 321–332.Google Scholar
  4. [4]
    Li Xuandong, Dang Van Hung, Zheng Tao. Checking hybrid automata for linear duration invariants. InAdvances in Computing Science—ASIAN’97, LNCS 1345, Springer-Verlag, 1997, pp. 166–180.Google Scholar
  5. [5]
    Zhao Jianhua, Dang Van Hung. On checking real-time parallel systems for linear duration properties. InProc. Formal Techniques in Real-Time and Fault-Tolerant Systems 5th International Symposium, No. 1486 in LNCS, Springer-Varlag. September 1998, pp. 241–250.Google Scholar
  6. [6]
    Wang F, Mok A K, Emerson E A. Distributed real-time system specification and verification in APTL.ACM Transactions on Software Engineering and Methodology, 1993, 2(4): 346–378.CrossRefGoogle Scholar

Copyright information

© Science Press, Beijing China and Allerton Press Inc. 2000

Authors and Affiliations

  1. 1.State Key Laboratory of Novel Software Technology, Department of Computer Science and TechnologyNanjing UniversityNanjingP.R. China
  2. 2.International Institute for Software TechnologyUnited Nations UniversityMacauP.R. China

Personalised recommendations