Checking timed automata for linear duration properties
- 18 Downloads
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.
Keywordsmodel checking duration calculus real-time system
Unable to display preview. Download preview PDF.
- 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
- 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
- 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
- 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
- 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