Towards Efficient Partition Refinement for Checking Reachability in Timed Automata

  • Agata Półrola
  • Wojciech Penczek
  • Maciej Szreter
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2791)


The paper presents a new method for building abstract models for Timed Automata, enabling on-the-fly reachability analysis. Our pseudo-simulating models, generated by a modified partitioning algorithm, are in many cases much smaller than forward-reachability graphs commonly applied for this kind of verification. A theoretical description of the method is supported by some preliminary experimental results.


Model Check Abstract Model Reachability Analysis Concrete State Bound Model Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Courcoubetis, C., Dill, D., Halbwachs, N., Wong-Toi, H.: An implementation of three algorithms for timing verification based on automata emptiness. In: Proc. of the 13th IEEE Real-Time Systems Symposium (RTSS 1992), pp. 157–166. IEEE Comp. Soc. Press, Los Alamitos (1992)Google Scholar
  2. 2.
    Alur, R., Courcoubetis, C., Dill, D., Halbwachs, N., Wong-Toi, H.: Minimization of timed transition systems. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 340–354. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  3. 3.
    Audemard, G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: Bounded model checking for timed systems. Technical Report 0201-05, ITC-IRST, Sommarive 16, 38050 Povo, Trento, Italy (January 2002)Google Scholar
  4. 4.
    Beyer, D.: Improvements in BDD-based reachability analysis of Timed Automata. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 318–343. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. 5.
    Bouajjani, A., Fernandez, J.-C., Halbwachs, N., Raymond, P., Ratel, C.: Minimal state graph generation. Science of Computer Programming 18, 247–269 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Bouajjani, A., Tripakis, S., Yovine, S.: On-the-fly symbolic model checking for real-time systems. In: Proc. of the 18th IEEE Real-Time Systems Symposium (RTSS 1997), pp. 232–243. IEEE Comp. Soc. Press, Los Alamitos (1997)Google Scholar
  7. 7.
    D’Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reachability analysis of probabilistic systems by successive refinements. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 39–56. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  8. 8.
    Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313–329. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  9. 9.
    Dembiński, P., Janowska, A., Janowski, P., Penczek, W., Półrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: VerICS: A tool for verifying Timed Automata and Estelle specifications. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 278–283. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  10. 10.
    Dembiński, P., Penczek, W., Półrola, A.: Automated verification of infinite state concurrent systems: an improvement in model generation. In: Wyrzykowski, R., Dongarra, J., Paprzycki, M., Waśniewski, J. (eds.) PPAM 2001. LNCS, vol. 2328, pp. 247–255. Springer, Heidelberg (2002)Google Scholar
  11. 11.
    Dembiński, P., Penczek, W., Półrola, A.: Verification of Timed Automata based on similarity. Fundamenta Informaticae 51(1-2), 59–89 (2002)zbMATHMathSciNetGoogle Scholar
  12. 12.
    Henzinger, T., Majumdar, R.: A classification of symbolic transition systems. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 13–34. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  13. 13.
    Kang, I., Lee, I.: An efficient state space generation for the analysis of real-time systems. In: Proc. of Int. Symposium on Software Testing and Analysis (1996)Google Scholar
  14. 14.
    Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of realtime systems: Compact data structures and state-space reduction. In: Proc. of the 18th IEEE Real-Time System Symposium (RTSS 1997), pp. 14–24. IEEE Comp. Soc. Press, Los Alamitos (1997)Google Scholar
  15. 15.
    Lee, D., Yannakakis, M.: On-line minimization of transition systems. In: Proc. of the 24th ACM Symp. on the Theory of Computing, May 1992, pp. 264–274 (1992)Google Scholar
  16. 16.
    Niebert, P., Tripakis, S., Yovine, S.: Minimum-time reachability for Timed Automata. In: Proc. of the 8th IEEE Mediterranean Conf. on Control and Automation (MED 2000), Patros, Greece, IEEE Comp. Soc. Press, Los Alamitos (2000)Google Scholar
  17. 17.
    Penczek, W.: Partial order reductions for checking branching properties of Time Petri Nets. In: Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P 2000). Informatik-Berichte, vol. 140, pp. 189–202. Humboldt University (2000)Google Scholar
  18. 18.
    Półrola, A., Penczek, W., Szreter, M.: Towards efficient partition refinement for checking reachability in Timed Automata, An electronic version of this paper available at
  19. 19.
    Półrola, A., Penczek, W., Szreter, M.: Reachability analysis for Timed Automata based on partitioning. Technical Report 961, ICS PAS, Ordona 21, 01-237 Warsaw (June 2003)Google Scholar
  20. 20.
    Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design 18(1), 25–68 (2001)zbMATHCrossRefGoogle Scholar
  21. 21.
    Woźna, B., Penczek, W., Zbrzezny, A.: Checking reachability properties for Timed Automata via SAT. Technical Report 949, ICS PAS, Ordona 21, 01 – 237 Warsaw (October 2002)Google Scholar
  22. 22.
    Yannakakis, M., Lee, D.: An efficient algorithm for minimizing real-time transition systems. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 210–224. Springer, Heidelberg (1993)Google Scholar
  23. 23.
    Yovine, S.: KRONOS: A verification tool for real-time systems. Springer International Journal of Software Tools for Technology Transfer 1(1/2), 123–133 (1997)zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Agata Półrola
    • 1
  • Wojciech Penczek
    • 2
    • 3
  • Maciej Szreter
    • 2
  1. 1.Faculty of MathematicsUniversity of LodzLodzPoland
  2. 2.Institiute of Computer Science, PASWarsawPoland
  3. 3.Institute of InformaticsPodlasie AcademySiedlcePoland

Personalised recommendations