Timed IMDS

  • Wiktor B. DaszczukEmail author
Part of the Studies in Computational Intelligence book series (SCI, volume 817)


The behavior of a distributed system may depend on real time flow (as opposed to succession of events in discrete systems), because changes in the system may take some time. As a result, deadlock situations may depend on relations between periods of time associated with individual changes.


  1. Alur, R., & Dill, D. L. (1994). A theory of timed automata. Theoretical Computer Science, 126(2), 183–235. Scholar
  2. Behrmann, G., Cougnard, A., David, A., Fleury, E., Gulstrand Larsen, K., & Lime, D. (2006). Uppaal-Tiga: Timed games for everyone. In Nordic Workshop on Programming Theory (NWPT’06), Reykjavik, Iceland, October 18–20, 2006. URL:
  3. Behrmann, G., David, A., & Larsen, K. G. (2006). A tutorial on Uppaal 4.0. Aalborg, Denmark. URL:
  4. Benghazi Akhlaki, K., Capel Tuñón, M. I., Holgado Terriza, J. A., & Mendoza Morales L E. (2007). A methodological approach to the formal specification of real-time systems by transformation of UML-RT design models. Science of Computer Programming, 65(1), 41–56.
  5. Bérard, B. (2013). An introduction to timed automata. In Control of discrete-event systems (pp. 169–187). London, UK: Springer.
  6. Bérard, B., Cassez, F., Haddad, S., Lime, D., & Roux, O. H. (2005). Comparison of the expressiveness of timed automata and time Petri nets. In Third International Conference FORMATS 2005, Uppsala, Sweden (pp. 211–225), September 26–28, 2005. Berlin: Springer.
  7. Bowman, H. (2001). Time and action lock freedom properties for timed automata. In 21st International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2001, Cheju Island, Korea (pp. 119–134), August 28–31, 2001. Boston: Kluwer Academic Publishers.
  8. Bowman, H., Gomez, R., & Su, L. (2005). A tool for the syntactic detection of zeno-timelocks in timed automata. Electronic Notes in Theoretical Computer Science, 139(1), 25–47. Scholar
  9. Cassez, F., & Roux, O. H. (2006). Structural translation from time Petri nets to timed automata. Journal of Systems and Software, 79(10), 1456–1468. Scholar
  10. Emerson, E. A., Mok, A. K., Sistla, P., & Srinivasan, J. (1992). Quantitative temporal reasoning. Real-Time Systems, 4(4), 331–352.
  11. Frossl, J., Gerlach, J, & Kropf, T. (1996). An efficient algorithm for real-time symbolic model checking. In Proceedings ED&TC European Design and Test Conference, Paris, France (pp. 15–20), March 11–14, 1996. New York, NY: IEEE Computer Society Press.
  12. Gluchowski, P. (2009). Languages of CTL and RTCTL Calculi in real-time analysis of a system described by a fault tree with time dependencies. In 2009 Fourth International Conference on Dependability of Computer Systems, DepCoS–RELCOMEX ’09, Brunów, Poland (pp. 33–41), June 30–July 2, 2009. New York, NY: IEEE.
  13. Gómez, R., & Bowman, H. (2007). Efficient detection of zeno runs in timed automata. In 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2007), Salzburg, Austria (pp. 195–210), October 3–5, 2007, LNCS 4763. Berlin, Heidelberg: Springer.
  14. Hadjidj, R., Boucheneb, H., & Hadjidj, D. (2007). Zenoness detection and timed model checking for real time systems. In K. Barkaoui & M. Ioualalen (Eds.), First International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS’07), Algiers, Algeria (pp. 120–134), May 5–6, 2007. Swinton, UK: British Computer Society. url:
  15. Holzmann, G. J. (1995). Tutorial: Proving properties of concurrent systems with SPIN. In 6th International Conference on Concurrency Theory (CONCUR’95, Philadelphia, PA) (pp. 453–455), August 21–24, 1995. Berlin, Heidelberg: Springer.
  16. Krystosik, A., & Turlej, D. (2006). EMLAN: A language for model checking of embedded systems software. In IFAC Workshop on Programmable Devices and Embedded Systems, Brno, Czech Republic (pp. 126–131), February 14–16, 2006. Amsterdam: Elsevier Science.
  17. Lime, D., & Roux, O. H. (2006). Model checking of time petri nets using the state class timed automaton. Discrete Event Dynamic Systems, 16(2), 179–205. Scholar
  18. Lindahl, M., Pettersson, P., & Yi, W. (2001). Formal design and analysis of a gear controller. International Journal on Software Tools for Technology Transfer, 3, 353–368.
  19. Popescu, C., & Martinez Lastra, J. L. (2010). Formal methods in factory automation. In J. Silvestre-Blanes (Ed.), Factory automation (pp. 463–475). Rijeka, Croatia: InTech.
  20. Ruf, J., & Kropf, T. (2003). Symbolic verification and analysis of discrete timed systems. Formal Methods in System Design, 23(1), 67–108. Scholar
  21. Winskel, G., & Nielsen, M. (1995). Models for concurrency. In S. Abramsky, D. M. Gabbay, & T. S. E. Maibaum (Eds.), Handbook of logic in computer science (Vol. 4, pp. 1–148). Oxford, UK: Oxford University Press. ISBN: 0-19-853780-8Google Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Institute of Computer ScienceWarsaw University of TechnologyWarsawPoland

Personalised recommendations