Computational Mathematics and Modeling

, Volume 30, Issue 2, pp 99–106 | Cite as

A Flattening Algorithm for Hierarchical Timed Automata

  • V. V. PodymovEmail author

We propose a coherent algorithm for the translation of hierarchical timed automata into networks of (planar) timed automata. This kind of translation is called flattening. The two types of timed automata are used in formal verification of real-time systems: systems of parallel interacting components whose execution essentially depends not only on the order of the events in the system, but also on the real time of these events. The concept of hierarchical timed automaton covers the syntactic variations that are used in existing studies and are non-comparable by their expressive power. The number of states in a flattened network of time automata is of the least order among the flattening results of existing studies.


timed automata formal verification real-time systems translation 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    G. Behrmann, A. David, and K. G. Larsen, “A tutorial on Uppaal,” Formal methods in the design of real-time systems, in: 4th Int. School of Formal Methods for the Design of Computer, Communication, and Software Systems, 3185, SFM-RT 2004, LNCS (2004), pp. 200–236.Google Scholar
  2. 2.
    A. David, M. O. Moeller, and W. Yi, “Formal verification of UML statecharts with real-time extensions,” Fund. Appr. to Software Eng., 218–232 (2002).Google Scholar
  3. 3.
    C. Baker and J.-P. Katoen, Principles of Model Checking, MIT Press (2008).Google Scholar
  4. 4.
    A. David and M. O. Moller, “From HUppaal to Uppaal: A translation from hierarchical times automata to flat timed automata,” Research Series RS-01-11, BRICS, Dept. Computer Sci., Univ. Aarhus (March 2001).Google Scholar
  5. 5.
    D. Yu. Volkanov, V. A. Zakharov, D. A. Zorin, I. V. Konnov, and V. V. Podymov, “How to develop a simple verification tool for real-time systems,” Model. i Anal. Inform. Sist., 19, No. 6, 45–56 (2012).CrossRefGoogle Scholar
  6. 6.
    D. Yu. Volkanov, V. A. Zakharov, D. A. Zorin, V. V. Podymov, and I. V. Konnov, “A combined toolset for the verification of real-time distributed systems,” Programm., No. 6, 73–82 (2015).Google Scholar

Copyright information

© Springer Science+Business Media, LLC, part of Springer Nature 2019

Authors and Affiliations

  1. 1.Faculty of Computational Mathematics and CyberneticsLomonosov Moscow State UniversityMoscowRussia

Personalised recommendations