Advertisement

Can Decision Diagrams Overcome State Space Explosion in Real-Time Verification?

  • Dirk Beyer
  • Andreas Noack
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2767)

Abstract.

In this paper we analyze the efficiency of binary decision diagrams (BDDs) and clock difference diagrams (CDDs) in the verification of timed automata. Therefore we present analytical and empirical complexity results for three communication protocols. The contributions of the analyses are: Firstly, they show that BDDs and CDDs of polynomial size exist for the reachability sets of the three protocols. This is the first evidence that CDDs can grow only polynomially for models with non-trivial state space explosion. Secondly, they show that CDD-based tools, which currently use at least exponential space for two of the protocols, will only find polynomial-size CDDs if they use better variable orders, as the BDD-based tool Rabbit does. Finally, they give insight into the dependency of the BDD and CDD size on properties of the model, in particular the number of automata and the magnitude of the clock values.

Keywords

Variable Order Outgoing Edge Binary Decision Diagram Reachability Analysis State Space Explosion 
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.

References

  1. 1.
    Alur, R.: Timed automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8–22. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Alur, R., Itai, A., Kurshan, R.P., Yannakakis, M.: Timing verification by successive approximation. Information and Computation 118(1), 142–157 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Amnell, T., Behrmann, G., Bengtsson, J., D’Argenio, P.R., David, A., Fehnker, A., Hune, T., Jeannet, B., Larsen, K.G., Möller, M.O., Pettersson, P., Weise, C., Yi, W.: Uppaal - now, next, and future. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 99–124. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  5. 5.
    Asarin, E., Maler, O., Pnueli, A.: On discretization of delays in timed automata and digital circuits. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 470–484. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  6. 6.
    Aziz, A., Tasiran, S., Brayton, R.K.: BDD variable ordering for interacting finite state machines. In: Proc. DAC 1994, pp. 283–288. ACM Press, New York (1994)Google Scholar
  7. 7.
    Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: 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
  8. 8.
    Beyer, D.: Efficient reachability analysis and refinement checking of timed automata using BDDs. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 86–91. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  9. 9.
    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
  10. 10.
    Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Transactions on Computers 45(9), 993–1002 (1996)CrossRefzbMATHGoogle Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transaction on Computers C-35(8), 677–691 (1986)CrossRefzbMATHGoogle Scholar
  13. 13.
    Burch, J.R., Clarke, E.M., Long, D.E., McMillan, K.L., Dill, D.L.: Symbolic model checking for sequential circuit verification. IEEE Transactions on CAD 13(4), 401–424 (1994)CrossRefGoogle Scholar
  14. 14.
    Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  15. 15.
    Göllü, A., Puri, A., Varaiya, P.: Discretization of timed automata. In: Proc. Decision and Control, pp. 957–958 (1994)Google Scholar
  16. 16.
    Thomas, A., Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  17. 17.
    Møller, J.B., Lichtenberg, J., Andersen, H.R., Hulgaard, H.: Difference Decision Diagrams. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 111–125. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  18. 18.
    Wang, F.: Symbolic verification of complex real-time systems with clockrestriction diagram. In: Proc. FORTE 2001, pp. 235–250. Kluwer, Dordrecht (2001)Google Scholar
  19. 19.
    Yovine, S.: Kronos: A verification tool for real-time systems. Software Tools for Technology Transfer 1(1-2), 123–133 (1997)CrossRefzbMATHGoogle Scholar
  20. 20.
    Yovine, S.: Model checking timed automata. In: Rozenberg, G. (ed.) EEF School 1996. LNCS, vol. 1494, pp. 114–152. Springer, Heidelberg (1998)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Dirk Beyer
    • 1
  • Andreas Noack
    • 1
  1. 1.Software Systems Engineering Research GroupBrandenburg Technical University at CottbusGermany

Personalised recommendations