Advertisement

Diamonds Are a Girl’s Best Friend: Partial Order Reduction for Timed Automata with Abstractions

  • Henri Hansen
  • Shang-Wei Lin
  • Yang Liu
  • Truong Khanh Nguyen
  • Jun Sun
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)

Abstract

A major obstacle for using partial order reduction in the context of real time verification is that the presence of clocks and clock constraints breaks the usual diamond structure of otherwise independent transitions. This is especially true when information of the relative values of clocks is preserved in the form of diagonal constraints. However, when diagonal constraints are relaxed by a suitable abstraction, some diamond structure is re-introduced in the zone graph. In this article, we introduce a variant of the stubborn set method for reducing an abstracted zone graph. Our method works with all abstractions, but especially targets situations where one abstract execution can simulate several permutations of the corresponding concrete execution, even though it might not be able to simulate the permutations of the abstract execution. We define independence relations that capture this “hidden” diamond structure, and define stubborn sets using these relations. We provide a reference implementation for verifying timed language inclusion, to demonstrate the effectiveness of our method.

References

  1. 1.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Alur, R., Itai, A., Kurshan, R.P., Yannakakis, M.: Timing verification by successive approximation. Inf. Comput. 118(1), 142–157 (1995)CrossRefzbMATHMathSciNetGoogle Scholar
  3. 3.
    Behrmann, G., Bouyer, P., Larsen, K., Pelanek, R.: Lower and upper bounds in zone-based abstractions of timed automata. International Journal on Software Tools for Technology Transfer (STTT) 8, 204–215 (2006)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.
    Dams, D., Gerth, R., Knaack, B., Kuiper, R.: Partial-order reduction techniques for real-time model checking. Formal Aspects of Computing 10, 469–482 (1998)CrossRefzbMATHGoogle Scholar
  6. 6.
    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
  7. 7.
    Evangelista, S., Pajault, C.: Solving the ignoring problem for partial order reduction. International Journal on Software Tools for Technology Transfer 12(2), 155–170 (2010)CrossRefGoogle Scholar
  8. 8.
    Hansen, H., Kwiatkowska, M., Qu, H.: Partial order reduction for model checking markov decision processes under unconditional fairness. In: QEST 2011, pp. 203–212. IEEE CS Press (2011)Google Scholar
  9. 9.
    Hansen, H., Wang, X.: Compositional analysis for weak stubborn sets. In: Caillaud, K.H.B., Carmona, J. (eds.) Proceedings of ACSD 2011, pp. 36–43. IEEE CS Press (2011)Google Scholar
  10. 10.
    Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Better Abstractions for Timed Automata. In: LICS, pp. 375–384 (2012)Google Scholar
  11. 11.
    Lugiez, D., Niebert, P., Zennou, S.: A partial order semantics approach to the clock explosion problem of timed automata. Theoretical Computer Science 345(1), 27–59 (2005)CrossRefzbMATHMathSciNetGoogle Scholar
  12. 12.
    Minea, M.: Partial order reduction for model checking of timed automata. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 431–446. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  13. 13.
    Niebert, P., Qu, H.: Adding invariants to event zone automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 290–305. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  14. 14.
    Salah, R., Bozga, M., Maler, O.: On interleaving in timed automata. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 465–476. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  16. 16.
    Valmari, A.: A stubborn attack on state explosion. Formal Methods in System Design 1(1), 297–322 (1992)CrossRefzbMATHGoogle Scholar
  17. 17.
    Valmari, A.: Stubborn set methods for process algebras. In: Proceedings of the DIMACS Workshop on Partial Order Methods in Verification, POMIV 1996, pp. 213–231. AMS Press, Inc., New York (1997)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Henri Hansen
    • 1
  • Shang-Wei Lin
    • 2
  • Yang Liu
    • 3
  • Truong Khanh Nguyen
    • 4
  • Jun Sun
    • 5
  1. 1.Department of MathematicsTampere University of TechnologyFinland
  2. 2.Temasek LaboratoriesNational University of SingaporeSingapore
  3. 3.School of Computer EngineeringNanyang Technological UniversitySingapore
  4. 4.National University of SingaporeSingapore
  5. 5.Singapore University of Technology and DesignSingapore

Personalised recommendations