Reducing Quasi-Equal Clocks in Networks of Timed Automata

  • Christian Herrera
  • Bernd Westphal
  • Sergio Feo-Arenis
  • Marco Muñiz
  • Andreas Podelski
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7595)


We introduce the novel notion of quasi-equal clocks and use it to improve the verification time of networks of timed automata. Intuitively, two clocks are quasi-equal if, during each run of the system, they have the same valuation except for those points in time where they are reset. We propose a transformation that takes a network of timed automata and yields a network of timed automata which has a smaller set of clocks and preserves properties up to those not comparing quasi-equal clocks. Our experiments demonstrate that the verification time in three transformed real world examples is much lower compared to the original.


Model Check Sink Node Transition Sequence Computation Path Broadcast Channel 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Dill, D.: A theory of timed automata. TCS 126(2), 183–235 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Rappaport, T.S.: Wireless communications: principles and practice, vol 2. Prentice Hall (2002)Google Scholar
  3. 3.
    Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  4. 4.
    Braberman, V., Garbervestky, D., Kicillof, N., Monteverde, D., Olivero, A.: Speeding Up Model Checking of Timed-Models by Combining Scenario Specialization and Live Component Analysis. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 58–72. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  5. 5.
    Braberman, V.A., Garbervetsky, D., Olivero, A.: Improving the Verification of Timed Systems Using Influence Information. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 21–36. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  6. 6.
    Bozga, M., Fernandez, J.-C., Ghirvu, L.: State Space Reduction Based on Live Variables Analysis. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 164–178. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  7. 7.
    Lugiez, D., Niebert, P., Zennou, S.: A Partial Order Semantics Approach to the Clock Explosion Problem of Timed Automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 296–311. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  8. 8.
    Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: RTSS, pp. 73–81. IEEE (1996)Google Scholar
  9. 9.
    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
  10. 10.
    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)Google Scholar
  11. 11.
    Salah, R., Bozga, M., Maler, O.: Compositional timing analysis. In: EMSOFT, pp. 39–48. ACM (2009)Google Scholar
  12. 12.
    Olderog, E.-R., Dierks, H.: Real-time systems - formal specification and automatic verification. Cambridge University Press (2008)Google Scholar
  13. 13.
    Gobriel, S., Khattab, S., Mossé, D., Brustoloni, J., Melhem, R.: Ridesharing: Fault tolerant aggregation in sensor networks using corrective actions. the 3rd annual. In: IEEE Communications Society Conference on Sensor, Mesh and Ad Hoc Communications and Networks (SECON), pp. 595–604 (2006)Google Scholar
  14. 14.
    Jensen, H., Larsen, K., Skou, A.: Modelling and analysis of a collision avoidance protocol using SPIN and Uppaal. In: 2nd SPIN Workshop (1996)Google Scholar
  15. 15.
    Dietsch, D., Feo-Arenis, S., Westphal, B., Podelski, A.: Disambiguation of industrial standards through formalization and graphical languages. In: RE, pp. 265–270 (2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Christian Herrera
    • 1
  • Bernd Westphal
    • 1
  • Sergio Feo-Arenis
    • 1
  • Marco Muñiz
    • 1
  • Andreas Podelski
    • 1
  1. 1.Albert-Ludwigs-Universität FreiburgFreiburgGermany

Personalised recommendations