Advertisement

Checking ACTL* Properties of Discrete Timed Automata via Bounded Model Checking

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

Abstract

The main contribution of the paper consists in showing that the BMC method is feasible for ACTL * (the universal fragment of CTL * which subsumes both ACTL and LTL. The extension to ACTL * is obtained by redefining the function returning the sufficient number of executions over which an ACTL * formula is checked, and then by combining two known translations to SAT for ACTL  and LTL formulas. The proposed translation of ACTL * formulas is essentially different from the existing translations of both ACTL and LTL formulas. Moreover, ACTL * seems to be the largest set of temporal properties which can be verified by means of BMC. We have implemented our new BMC algorithm for discrete timed automata and we have presented a preliminary experimental results, which prove the efficiency of the method. The formal treatment is the basis for the implementation of the technique in the symbolic model checker \(\surd\)erics.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Courcoubetis, C., Dill, D.: Model checking in dense real-time. Information and Computation 104(1), 2–34 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Audemard, G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: Bounded model checking for timed systems. In: Proc. of RT-TOOLS 2002 (2002)Google Scholar
  3. 3.
    Benedetti, M., Cimatti, A.: Bounded Model checking for Past LTL. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 18–33. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  4. 4.
    Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 485–500. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  5. 5.
    Beyer, D.: Improvements in BDD-based reachability analysis of Timed Automata. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, p. 318. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. 6.
    Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proc. of DAC 1999 (1999)Google Scholar
  7. 7.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  8. 8.
    Bozga, M., Maler, O., Tripakis, S.: Efficient verification of Timed Automata using dense and discrete time semantics. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 125–141. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  9. 9.
    Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)zbMATHCrossRefGoogle Scholar
  10. 10.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  11. 11.
    Dams, D., Grumberg, O., Gerth, R.: Abstract interpretation of reactive systems: Abstractions preserving ACTL*, ECTL* and CTL*. In: Proceedings of PROCOMET 1994, Elsevier Science Publishers, Amsterdam (1994)Google Scholar
  12. 12.
    Daws, C., Tripakis, 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
  13. 13.
    Dembiński, P., Janowska, A., Janowski, P., Penczek, W., Półrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: \(\surd\)erics: 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
  14. 14.
    de Moura, L., Rueß, H., Sorea, M.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, p. 438. Springer, Heidelberg (2002)Google Scholar
  15. 15.
    Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods in System Design 9, 105–131 (1995)CrossRefGoogle Scholar
  16. 16.
    Grumberg, O., Long, D.E.: Model checking and modular verification. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527, Springer, Heidelberg (1991)Google Scholar
  17. 17.
    Heljanko, K.: Bounded reachability checking with process semantics. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, p. 218. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  18. 18.
    Heljanko, K., Niemelä, I.: Bounded LTL model checking with stable models. In: Eiter, T., Faber, W., Truszczyński, M. (eds.) LPNMR 2001. LNCS (LNAI), vol. 2173, p. 200. Springer, Heidelberg (2001)Google Scholar
  19. 19.
    McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)Google Scholar
  20. 20.
    Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of Timed Automata via Satisfiability Checking. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, p. 225. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  21. 21.
    Peled, D.: Partial order reduction: Linear and branching temporal logics and process algebras. In: Proc. of POMIV 1996. ACM/AMS DIMACS Series, vol. 29, Amer. Math. Soc., Providence (1996)Google Scholar
  22. 22.
    Penczek, W., Szreter, M., Gerth, R., Kuiper, R.: Improving partial order reductions for universal branching time properties. Fundamenta Informaticae 43, 245–267 (2000)zbMATHMathSciNetGoogle Scholar
  23. 23.
    Penczek, W., Woźna, B., Zbrzezny, A.: Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae 51(1-2), 135–156 (2002)zbMATHMathSciNetGoogle Scholar
  24. 24.
    Penczek, W., Woźna, B., Zbrzezny, A.: SAT-Based Bounded Model Checking for the Universal Fragment of TCTL. Technical Report 947, ICS PAS (2002)Google Scholar
  25. 25.
    Penczek, W., Woźna, B., Zbrzezny, A.: Towards bounded model checking for the universal fragment of TCTL. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, p. 265. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  26. 26.
    Sorea, M.: Bounded model checking for timed automata. In: Proc. of MTCS 2002. ENTCS, vol. 68(5), Elsevier Science Publishers, Amsterdam (2002)Google Scholar
  27. 27.
    Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design 18(1), 25–68 (2001)zbMATHCrossRefGoogle Scholar
  28. 28.
    Wolper, P., Godefroid, P.: Partial-order methods for temporal verification. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, Springer, Heidelberg (1993)Google Scholar
  29. 29.
    Woźna, B., Penczek, W., Zbrzezny, A.: Reachability for timed systems based on SAT-solvers. In: Proc. of CS&P 2002. Informatik-Berichte Nr 161, vol. II. Humboldt University (2002)Google Scholar
  30. 30.
    Woźna, B., Zbrzezny, A.: Reaching the limits for Bounded Model Checking. Technical Report 958, ICS PAS (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Bożena Woźna
    • 1
  • Andrzej Zbrzezny
    • 1
  1. 1.Institute of Mathematics and Computer Science, PU of CzȩstochowaCzȩstochowaPoland

Personalised recommendations