On the Verification of Timed Discrete-Event Models

  • Christos Stergiou
  • Stavros Tripakis
  • Eleftherios Matsikoudis
  • Edward A. Lee
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8053)


Timed discrete-event (DE) is an actor-oriented formalism for modeling timed systems. A DE model is a network of actors consuming/producing timed events from/to a set of input/output channels. In this paper we study a basic DE model, called deterministic DE (DDE), where actors are simple constant-delay components, and two extensions of DDE: NDE, where actors are non-deterministic delays, and DETA, where actors are either deterministic delays or timed automata. We investigate verification questions on DE models and examine expressiveness relationships between the DE models and timed automata.


Output Channel Input Channel Reachable State Discrete Transition Input Event 
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.
    Agha, G.: ACTORS: A Model of Concurrent Computation in Distributed Systems. The MIT Press Series in Artificial Intelligence. MIT Press, Cambridge (1986)Google Scholar
  2. 2.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  3. 3.
    Bae, K., Csaba Olveczky, P., Feng, T.H., Lee, E.A., Tripakis, S.: Verifying Hierarchical Ptolemy II Discrete-Event Models using Real-Time Maude. Science of Computer Programming 77(12), 1235–1271 (2012)zbMATHCrossRefGoogle Scholar
  4. 4.
    Cassandras, C., Lafortune, S.: Introduction to Discrete Event Systems. Kluwer Academic Publishers (1999)Google Scholar
  5. 5.
    Cataldo, A., Lee, E., Liu, X., Matsikoudis, E., Zheng, H.: A constructive fixed-point theorem and the feedback semantics of timed sy stems. In: WODES (2006)Google Scholar
  6. 6.
    Chatterjee, K., Henzinger, T.A., Prabhu, V.S.: Finite automata with time-delay blocks. In: EMSOFT 2012, pp. 43–52. ACM (2012)Google Scholar
  7. 7.
    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
  8. 8.
    Eidson, J.C., Lee, E.A., Matic, S., Seshia, S.A., Zou, J.: Distributed real-time software for cyber-physical systems. Proceedings of the IEEE 100(1), 45–59 (2012)CrossRefGoogle Scholar
  9. 9.
    Eker, J., Janneck, J., Lee, E.A., et al.: Taming heterogeneity – the Ptolemy approach. Proc. IEEE 91(1) (2003)Google Scholar
  10. 10.
    Geilen, M., Tripakis, S., Wiggers, M.: The Earlier the Better: A Theory of Timed Actor Interfaces. In: HSCC. ACM (2011)Google Scholar
  11. 11.
    Jonsson, B., Perathoner, S., Thiele, L., Yi, W.: Cyclic dependencies in modular performance analysis. In: EMSOFT 2008, pp. 179–188. ACM (2008)Google Scholar
  12. 12.
    Kahn, G.: The semantics of a simple language for parallel programming (1974)Google Scholar
  13. 13.
    Lampka, K., Perathoner, S., Thiele, L.: Analytic real-time analysis and timed automata: a hybrid method for analyzing embedded real-time systems. In: EMSOFT, pp. 107–116. ACM (2009)Google Scholar
  14. 14.
    Lee, E.A.: Modeling concurrent real-time processes using discrete events. Annals of Software Engineering 7(1), 25–45 (1999)CrossRefGoogle Scholar
  15. 15.
    Liu, X., Lee, E.A.: CPO semantics of timed interactive actor networks. Theoretical Computer Science 409(1), 110–125 (2008)MathSciNetzbMATHCrossRefGoogle Scholar
  16. 16.
    Liu, X., Matsikoudis, E., Lee, E.A.: Modeling timed concurrent systems. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 1–15. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  17. 17.
    Ramadge, P., Wonham, W.: The control of discrete event systems. Proceedings of the IEEE (January 1989)Google Scholar
  18. 18.
    Sirjani, M., Jaghoori, M.M.: Ten Years of Analyzing Actors: Rebeca Experience. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol. 7000, pp. 20–56. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  19. 19.
    Thiele, L., Chakraborty, S., Naedele, M.: Real-time calculus for scheduling hard real-time systems. In: ISCAS, pp. 101–104 (2000)Google Scholar
  20. 20.
    Yates, R.K.: Networks of real-time processes. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 384–397. Springer, Heidelberg (1993)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Christos Stergiou
    • 1
  • Stavros Tripakis
    • 1
  • Eleftherios Matsikoudis
    • 1
  • Edward A. Lee
    • 1
  1. 1.University of CaliforniaBerkeleyUSA

Personalised recommendations