Advertisement

Removing Irrelevant Atomic Formulas for Checking Timed Automata Efficiently

  • Jianhua Zhao
  • Xuandong Li
  • Tao Zheng
  • Guoliang Zheng
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2791)

Abstract

Reachability analysis for timed automata can be done by enumeration of time zones, which are conjunctions of atomic formulas of the form x-y≤(<)n. This paper shows that some of the atomic formulas in a generated time zone can be removed while the reachability analysis algorithm generates the same set of reachable locations. We call such formulas irrelevant ones. By removing the irrelevant formulas, the number of symbolic states associated with each location is reduced. We present two methods to detect irrelevant formulas. Case studies show that, for some kind of timed automata, these methods may significantly reduce the space requirement for reachability analysis.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL: Status & Developments. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 456–459. Springer, Heidelberg (1997)Google Scholar
  2. 2.
    Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool Kronos. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, Springer, Heidelberg (1996)CrossRefGoogle Scholar
  3. 3.
    Henzinger, T.A., Ho, P.-H.: Hytech: The Cornell hybrid technology tool. In: Proc. of Workshop on Tools and Algorithms for the Construction and Analysis of Systems, BRICS report series NS-95-2 (1995)Google Scholar
  4. 4.
    Wang-Toi, H.: Symbolic Approximations for Verifying Real-Time Systems. PhD thesis, Stanford University (1994)Google Scholar
  5. 5.
    Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient Verification of Real-Time Systems: Compact Data Structures and State-Space Reduction. In: Proc. of the 18th IEEE Real-Time Systems Symposium, IEEE Computer Society Press, Los Alamitos (1997)Google Scholar
  6. 6.
    Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial Order Reductions for Timed Systems. In: Proc. of the 9th International Conference on Concurrency Theory (September 1998)Google Scholar
  7. 7.
    Zhao, J., Xu, H., Li, X., Zheng, T., Zheng, G.: Partial Order Path Technique for Checking Parallel Timed Automata. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, p. 417. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. 8.
    Daws, C., Yovine, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, p. 313. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  9. 9.
    Havelund, K., Skou, A., Larsen, K.G., Lund, K.: 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, Los Alamitos (1997)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Jianhua Zhao
    • 1
  • Xuandong Li
    • 1
  • Tao Zheng
    • 1
  • Guoliang Zheng
    • 1
  1. 1.State Key Laboratory of Novel Software Technology Dept. of Computer Sci. and Tech.Nanjing UniversityNanjingP.R.China

Personalised recommendations