Advertisement

Detecting Quasi-equal Clocks in Timed Automata

  • Marco Muñiz
  • Bernd Westphal
  • Andreas Podelski
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8053)

Abstract

A recent optimizations technique for timed model checking starts with a given specification of quasi-equal clocks. In principle, the zone graph can used to detect which clocks are quasi-equal; the construction of the zone graph would, however, defeat its very purpose (which is the optimization of this construction). In this paper, we present an abstraction that is effective for the goal of the optimization based on quasi-equal clocks: it is coarse enough to yield a drastic reduction of the size of the zone graph. Still, it is precise enough to identify a large class of quasi-equal clocks. The abstraction is motivated by an intuition about the way quasi-equalities can be tracked. We have implemented the corresponding reasoning method in the Jahob framework using an SMT solver. Our experiments indicate that our intuition may lead to a useful abstraction.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Behrmann, G., Bouyer, P., Larsen, K.G., Pelánek, R.: Lower and upper bounds in zone based abstractions of timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 312–326. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  3. 3.
    Behrmann, G., Bouyer, P., Larsen, K.G., Pelánek, R.: Lower and upper bounds in zone-based abstractions of timed automata. International Journal on Software Tools for Technology Transfer 8(3), 204–215 (2006)CrossRefGoogle Scholar
  4. 4.
    Bellman, R., Kalaba, R.E.: Dynamic programming and modern control theory. Academic Press, New York (1965)Google Scholar
  5. 5.
    Bengtsson, J., Yi, W.: On clock difference constraints and termination in reachability analysis of timed automata. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 491–503. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  6. 6.
    Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  7. 7.
    Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: Proc. RTSS 1996, pp. 73–81. IEEE Computer Society Press (1996)Google 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.
    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  10. 10.
    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
  11. 11.
    Herrera, C., Westphal, B., Feo-Arenis, S., Muñiz, M., Podelski, A.: Reducing quasi-equal clocks in networks of timed automata. In: Jurdziński, M., Ničković, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 155–170. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  12. 12.
    Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer (STTT) 1(1), 134–152 (1997)zbMATHGoogle Scholar
  13. 13.
    Muñiz, M., Westphal, B., Podelski, A.: Timed automata with disjoint activity. In: Jurdziński, M., Ničković, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 188–203. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  14. 14.
    Olderog, E.R., Dierks, H.: Real-Time Systems - Formal Specification and Automatic Verification. Cambridge University Press (2008)Google Scholar
  15. 15.
    Pettersson, P.: Modelling and verification of real-time systems using timed automata: theory and practice. Ph.D. thesis, Citeseer (1999)Google Scholar
  16. 16.
    Podelski, A., Wies, T.: Counterexample-guided focus. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 249–260. ACM, New York (2010), http://doi.acm.org/10.1145/1706299.1706330 CrossRefGoogle Scholar
  17. 17.
    Wies, T., Muñiz, M., Kuncak, V.: An efficient decision procedure for imperative tree data structures. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 476–491. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  18. 18.
    Yovine, S.: Kronos: A verification tool for real-time systems. International Journal on Software Tools for Technology Transfer (STTT) 1(1), 123–133 (1997)zbMATHGoogle Scholar
  19. 19.
    Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, pp. 349–361. ACM, New York (2008), http://doi.acm.org/10.1145/1375581.1375624 CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Marco Muñiz
    • 1
  • Bernd Westphal
    • 1
  • Andreas Podelski
    • 1
  1. 1.Albert-Ludwigs-Universität FreiburgFreiburgGermany

Personalised recommendations