Timed Automata with Disjoint Activity

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


The behavior of timed automata consists of idleness and activity, i.e. delay and action transitions. We study a class of timed automata with periodic phases of activity. We show that, if the phases of activity of timed automata in a network are disjoint, then location reachability for the network can be decided using a concatenation of timed automata. This reduces the complexity of verification in Uppaal-like tools from quadratic to linear time (in the number of components) while traversing the same reachable state space. We provide templates which imply, by construction, the applicability of sequential composition, a variant of concatenation, which reflects relevant reachability properties while removing an exponential number of states. Our approach covers the class of TDMA-based (Time Division Multiple Access) protocols, e.g. FlexRay and TTP. We have successfully applied our approach to an industrial TDMA-based protocol of a wireless fire alarm system with more than 100 sensors.


Outgoing Edge Sequential Composition Time Division Multiple Access Parallel Composition Label Transition System 
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.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static Guard Analysis in Timed Automata Verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 254–270. Springer, Heidelberg (2003)CrossRefGoogle 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.
    Daws, C., Yovine, S.: Reducing the number of clock variables of timed automata. In: IEEE Proc. RTSS 1996, pp. 73–81. IEEE Computer Society Press (1996)Google Scholar
  5. 5.
    Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program. 2(3), 155–173 (1982)zbMATHCrossRefGoogle Scholar
  6. 6.
    Haartsen, J.C.: The Bluetooth radio system. IEEE Personal Communications 7(1), 28–36 (2000)CrossRefGoogle Scholar
  7. 7.
    Heiner, G., Thurner, T.: Time-triggered architecture for safety-related distributed real-time systems in transportation systems. In: FTCS, pp. 402–407 (1998)Google Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    Janssen, W., Poel, M., Xu, Q., Zwiers, J.: Layering of Real-Time Distributed Processes. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 393–417. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  10. 10.
    Kopetz, H.: The time-triggered approach to real-time systems design. In: Randell, B., et al. (eds.) Predictably Dependable Computing Systems. Springer (1995)Google Scholar
  11. 11.
    Kopetz, H., Bauer, G.: The Time-Triggered Architecture. Proc. IEEE, 112–126 (2003)Google Scholar
  12. 12.
    Kopetz, H., Grünsteidl, G.: TTP - a time-triggered protocol for fault-tolerant real-time systems. In: FTCS, pp. 524–533 (1993)Google Scholar
  13. 13.
    Olderog, E.R., Dierks, H.: Real-Time Systems - Formal Speci cation and Automatic Veri cation. Cambridge University Press (2008)Google Scholar
  14. 14.
    Kopetz, H., Grünsteidl, G.: TTP - a time-triggered protocol for fault-tolerant real-time systems. In: FTCS, pp. 524–533 (1993)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

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

Personalised recommendations