Semantics of Timed Discrete-Event Systems

Eleftherios Matsikoudis and Edward A. Lee

Center for Hybrid and Embedded Software Systems (CHESS), National Science Foundation 0720882 (CSR-EHS: PRET), National Science Foundation 1035672 (CPS: PTIDES), National Science Foundation 0931843 (ActionWebs), Army Research Office W911NF-07-2-0019 (SCOS), Air Force Office of Scientific Research FA9550-06-0312 (HCDDES MURI), Air Force Research Lab, Multiscale Systems Center (MuSyC), Robert Bosch GmBH, National Instruments, Thales and Toyota

In the context of timed discrete-event systems, processes are allowed to realize functions that are not order-preserving with respect to the prefix ordering relation on the communicated sequences of values. This property renders naive applications of traditional domain-theoretic models inadequate for the semantic interpretation of such systems. Yet, interesting results have been obtained by imposing a fixed lower bound on the reaction time of the involved processes, effectively precluding Zeno behavior [1,2,3,4].

This work focuses on relaxing this requirement to obtain semantic interpretations even in the presence of Zeno conditions. The underlying aim is to establish a canonical denotational definition of timed discrete-event programming languages, thereby providing the means for reasoning about the correctness of the individual implementations, as well as allowing hidden commonalities of seemingly different timed systems to emerge.

[1]
R. K. Yates, "Networks of Real-Time Processes," CONCUR 93: Proc. Int. Conf. Concurrency Theory, Springer-Verlag, 1993, pp. 384-397.
[2]
E. A. Lee, "Modeling Concurrent Real-Time Processes Using Discrete Events," Annals of Software Engineering, Vol. 7, No. 3, 1999, pp. 25-45 (invited paper).
[3]
Xiaojun Liu, Edward A. Lee, "CPO Semantics of Timed Interactive Actor Networks," EECS Department, University of California, Berkeley, Technical Report No. UCB/EECS-2007-131, November 5, 2007.
[4]
A. Cataldo, E. A. Lee, X. Liu, E. Matsikoudis and H. Zheng, "Discrete-Event Systems: Generalizing Metric Spaces and Fixed Point Semantics," UCB/ERL M05/12, April 8, 2005.