Towards Bounded Model Checking for the Universal Fragment of TCTL

  • Wojciech Penczek
  • Bożena Woźna
  • Andrzej Zbrzezny
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2469)


Bounded Model Checking (BMC) based on SAT methods consists in searching for a counterexample of a particular length and to generate a propositional formula that is satisfiable iff such a counterexample exists. Our paper shows how the concept of bounded model checking can be extended to deal with TACTL (the universal fragment of TCTL) properties of Timed Automata.


Model Check Transition Relation Propositional Variable Propositional Formula Region Graph 
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.


  1. 1.
    R. Alur, C. Courcoubetis, and D. Dill. Model checking in dense real-time. Information and Computation, 104(1):2–34, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. An implementation of three algorithms for timing verification based on automata emptiness. In Proc. of RTSS’92, p. 157–166. IEEE Comp. Soc. Press, 1992.Google Scholar
  3. 3.
    R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. Minimization of timed transition systems. In Proc. of CONCUR’92, volume 630 of LNCS, p. 340–354. Springer-Verlag, 1992.Google Scholar
  4. 4.
    R. Alur and D. Dill. A theory of Timed Automata. Theoretical Computer Science, 126(2):183–235, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    R. Alur, T. Feder, and T. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1):116–146, 1996.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    E. Asarin, M. Bozga, A. Kerbrat, O. Maler, A. Pnueli, and A. Rasse. Data-structures for the verification of Timed Automata. In Proc. of HART’97, volume 1201 of LNCS, p. 346–360. Springer-Verlag, 1997.Google Scholar
  7. 7.
    J. Bengtsson, B. Jonsson, J. Lilius, and W. Yi. Partial order reductions for timed systems. In Proc. of CONCUR’98, volume 1466 of LNCS, p. 485–500. Springer-Verlag, 1998.Google Scholar
  8. 8.
    A. Biere, A. Cimatti, E. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proc. of DAC’99, p. 317–320, 1999.Google Scholar
  9. 9.
    A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of TACAS’99, volume 1579 of LNCS, p. 193–207. Springer-Verlag, 1999.Google Scholar
  10. 10.
    A. Bouajjani, S. Tripakis, and S. Yovine. On-the-fly symbolic model checking for real-time systems. In Proc. of RTSS’97, p. 232–243. IEEE Comp. Soc. Press, 1997.Google Scholar
  11. 11.
    R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transaction on Computers, 35(8):677–691, 1986.zbMATHCrossRefGoogle Scholar
  12. 12.
    E. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. In Formal Methods in System Designe, volume 19(1), p. 7–34, 2001.zbMATHCrossRefGoogle Scholar
  13. 13.
    E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.Google Scholar
  14. 14.
    D. Dams, R. Gerth, B. Knaack, and R. Kuiper. Partial-order reduction techniques for real-time model checking. In Proc. of the 3rd Int. Workshop on Formal Methods for Industrial Critical Systems, p. 157–169, 1998.Google Scholar
  15. 15.
    D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems: Abstractions preserving ACTL*, ECTL* and CTL*. In Proc. of PROCOMET’94. Elsevier Science Publishers, 1994.Google Scholar
  16. 16.
    C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In Proc. of TACAS’98, volume 1384 of LNCS, p. 313–329. Springer-Verlag, 1998.Google Scholar
  17. 17.
    Richard H. Eckhouse. Minicomputer systems. Organization and programming. Prentice-Hall, 1975.Google Scholar
  18. 18.
    E. A. Emerson. Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter Temporal and Modal Logic, p. 995–1067. Elsevier Science Publishers, 1990.Google Scholar
  19. 19.
    E. A. Emerson and E. M. Clarke. Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241–266, 1982.zbMATHCrossRefGoogle Scholar
  20. 20.
    E. A. Emerson and A. P. Sistla. Symmetry and model checking. Formal Methods in System Design, 9:105–131, 1995.CrossRefGoogle Scholar
  21. 21.
    O. Grumberg and D. E. Long. Model checking and modular verification. In Proc. of CONCUR’91, volume 527 of LNCS, p. 250–265. Springer-Verlag, 1991.Google Scholar
  22. 22.
    K. Heljanko and I. Niemelä. Bounded LTL model checking with stable models. In Proc. of LPNMR’2001, volume 2173 of LNCS, p. 200–212. Springer-Verlag, 2001.Google Scholar
  23. 23.
    D. S. Johnson and M. A. Trick, editors. Cliques, Coloring and Satisfiability: The Second DIMACS Implementation Challenge, volume 26 of ACM/AMS DIMACS Series. Amer. Math. Soc., 1996.Google Scholar
  24. 24.
    I. Kang and I. Lee. An Efficient State Space Generation for the Analysis of Realtime Systems. In Proc. of Int. Symposium on Software Testing and Analysis, 1996.Google Scholar
  25. 25.
    O. Kupferman, T. A. Henzinger, and M. Y. Vardi. A space-efficient on-the-fly algorithm for real-time model checking. In Proc. of CONCUR’96, volume 1119 of LNCS, p. 514–529. Springer-Verlag, 1996.Google Scholar
  26. 26.
    J. Lilius. Efficient state space search for Time Petri Nets. In Proc. of MFCS, volume 18 of ENTCS. Elsevier Science Publishers, 1999.Google Scholar
  27. 27.
    K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.Google Scholar
  28. 28.
    M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient sat solver. In Proc. of DAC’01, June 2001.Google Scholar
  29. 29.
    F. Pagani. Partial orders and verification of real-time systems. In Proc. of FTRTFT’96, volume 1135 of LNCS, p. 327–346. Springer-Verlag, 1996.Google Scholar
  30. 30.
    D. Peled. Partial order reduction: Linear and branching temporal logics and process algebras. In Proc. of POMIV’96, volume 29 of ACM/AMS DIMACS Series, p. 79–88. Amer. Math. Soc., 1996.Google Scholar
  31. 31.
    W. Penczek and A. Półrola. Abstractions and partial order reductions for checking branching properties of Time Petri Nets. In Proc. of ICATPN’01, volume 2075 of LNCS, p. 323–342. Springer-Verlag, 2001.Google Scholar
  32. 32.
    W. Penczek, M. Szreter, R. Gerth, and R. Kuiper. Improving partial order reductions for universal branching time properties. Fundamenta Informaticae, 43:245–267, 2000.zbMATHMathSciNetGoogle Scholar
  33. 33.
    W. Penczek and B. Woźna. Towards bounded model checking for Timed Automata. In Proc. of CS&P’01, p. 195–209, 2001.Google Scholar
  34. 34.
    W. Penczek, B. Woźna, and A. Zbrzezny. Bounded Model Checking for the Universal Fragment of CTL. Fundamenta Informaticae, 2002. to appear.Google Scholar
  35. 35.
    W. Penczek, B. Woźna, and A. Zbrzezny. Branching Time Bounded Model Checking for Elementary Net Systems. Report ICS PAS, 940, January 2002.Google Scholar
  36. 36.
    S. Tripakis and S. Yovine. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design, 18(1):25–68, 2001.zbMATHCrossRefGoogle Scholar
  37. 37.
    P. Wolper and P. Godefroid. Partial-order methods for temporal verification. In Proc. of CONCUR’93, volume 715 of LNCS, p. 233–246. Springer-Verlag, 1993.Google Scholar
  38. 38.
    T. Yoneda and B.H. Schlingloff. Efficient verification of parallel real-time systems. Formal Methods in System Design, 11(2):197–215, 1997.CrossRefGoogle Scholar
  39. 39.
    L. Zhang, C. Madigan, M. Moskewicz, and S. Malik. Efficient conflict driven learning in a boolean satisfiability solver. In Proc. of ICCAD’01, Nov. 2001.Google Scholar
  40. 40.

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Wojciech Penczek
    • 1
    • 2
  • Bożena Woźna
    • 3
  • Andrzej Zbrzezny
    • 3
  1. 1.Institute of Computer SciencePASWarsawPoland
  2. 2.Podlasie Academy Institute of InformaticsSiedlcePoland
  3. 3.Institute of Mathematics and Computer SciencePUCzcestochowaPoland

Personalised recommendations