Symbolic Model Checking of Finite Precision Timed Automata

  • Rongjie Yan
  • Guangyuan Li
  • Zhisong Tang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)


This paper introduces the notion of finite precision timed automata (FPTAs) and proposes a data structure to represent its symbolic states. To reduce the state space, FPTAs only record the integer values of clock variables together with the order of their most recent resets. We provide constraints under which the reachability checking of a timed automaton can be reduced to that of the corresponding FPTA, and then present an algorithm for reachability analysis. Finally, the paper reports some preliminary experimental results, and analyzes the advantages and disadvantages of the new data structure.


Finite precision timed automata model checking symbolic methods 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Alur, R., Henzinger, T.A.: A Really Temproal Logic. In: IEEE FOCS, pp. 164–169 (1989)Google Scholar
  3. 3.
    Asarin, E., Bozga, M., Kerbrat, A., Maler, O., Pnueli, A., Rasse, A.: Data-Structures for the Verification of Timed Automata. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 346–360. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  4. 4.
    Behrmann, G., Larsen, K.G., Weise, C., Wang, Y., Pearson, J.: Efficient Timed Reachability Analysis Using Clock Difference Diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 341–353. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  5. 5.
    Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)zbMATHGoogle Scholar
  6. 6.
    Bengtsson, J., Jonsson, B., Lilius, J., Wang, Y.: Partial Order Reductions for Timed System. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 485–500. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  7. 7.
    Bengtsson, J., Wang, Y.: Timed Automata: Semantics, Algorithms and Tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer, Heidelberg (2001)zbMATHGoogle Scholar
  9. 9.
    Beyer, D., Lewerentz, C., Noack, A.: Rabbit: A Tool for BDD-based Verification of Real-Time Systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 122–125. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  10. 10.
    Bosnacki, D., Dams, D., Holenderski, L.: A Heuristic for Symmetry Reductions with Scalarsets. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 518–533. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  11. 11.
    Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a Model-Checking Tool for Real-Time Systems. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 298–302. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  12. 12.
    Bozga, M., Maler, O., Pnueli, A., Yovine, S.: Some Progress in the Symbolic Verification of Timed Automata. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 179–190. Springer, Heidelberg (1997)Google Scholar
  13. 13.
    Bryant, R.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)zbMATHCrossRefGoogle Scholar
  14. 14.
    Dang, Z., Ibarra, O.H., Bultan, T., Kemmerer, R.A., Su, J.: Binary Reachability Analysis of Discrete Pushdown Timed Automata. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 69–84. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  15. 15.
    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, pp. 208–219. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  16. 16.
    Daws, C., Yovine, S.: Reducing the Number of Clock Variables of Timed Automata. In: IEEE RTSS, pp. 73–81 (1996)Google Scholar
  17. 17.
    Gerd, B., Johan, B., Alexandre, D., Larsen, K.G., Paul, P., Wang, Y.: UPPAAL Implementation Secrets. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 3–22. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  18. 18.
    Hendriks, M., Behrmann, G., Larsen, K.G., Vaandrager, F.: Adding Symmetry Reduction to Uppaal. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 46–59. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  19. 19.
    Lamport, L.: A Fast Mutual Exclusion Algorithm. ACM Transactions on Computer Systems 5(1), 1–11 (1987)CrossRefGoogle Scholar
  20. 20.
    Larsen, K.G., Pettersson, P., Wang, Y.: UPPAAL in a Nutshell. International Journal on Software Tools for Technology Transfer 1(1/2), 134–152 (1997)zbMATHGoogle Scholar
  21. 21.
    Raskin, J.F., Schoebbens, P.: Real-Time Logics: Fictitious Clock as an Abstraction of Dense Time. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 165–182. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  22. 22.
    Wang, F.: Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 157–171. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  23. 23.
    Wang, F.: Region Encoding Diagram for Fully Symbolic Verification of Real-Time Systems. In: COMPSAC, pp. 509–515 (2000)Google Scholar
  24. 24.
    Wang, F.: Efficient Verification of Timed Automata with BDD-like Data-Structures. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 189–205. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  25. 25.
    Wang, F.: Formal Verification of Timed Systems: A Survery and Perspective. Proceedings of the IEEE 92(8), 1283–1307 (2004)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Rongjie Yan
    • 1
    • 2
  • Guangyuan Li
    • 1
  • Zhisong Tang
    • 1
  1. 1.Laboratory of Computer Science, Institute of SoftwareChinese Academy of SciencesBeijingChina
  2. 2.Graduate School of the Chinese Academy of SciencesBeijingChina

Personalised recommendations