## Abstract

In this chapter we concentrate on timed models of DES. We also explore what happens when a system combines time-driven dynamics with event-driven dynamics giving rise to what are referred to as *hybrid systems*, which were introduced at the end of Chap. 1. The simplest instance of time-driven dynamics is the case of adjoining one or more clocks to the untimed DES model, resulting in a *timed model*. In the case of timed DES models, the sample paths are no longer specified as event sequences {*e* _{1} *e* _{2}, …} or state sequences {*x* _{0},*x* _{1},….}, but they must include some form of timing information. For example, let *t* _{ k }, *k*= 1, 2, …, denote the time instant when the *k*th event and state transition occurs (with *t* _{0} given); then a timed sample path of a DES may be described by the sequence {(*x* _{0},*t* _{0}), (*x* _{1} *t* _{1}), …}. Similarly, a timed sequence of events would look like {(*e* _{1} *t* _{1}), (*e* _{2},*t* _{2}), …}. Creating a framework for timed DES models will enable us to address questions such as “how many events of a particular type can occur in a given time interval?”, “is the time interval between occurrences of two different events always greater than a given lower bound?” or “how long does the system spend in a given state?” These issues are of critical importance in analyzing the behavior of many classes of DES since they provide us with particularly useful measures of system performance. The next step is to consider more complicated time-driven dynamics than clocks. Namely, at each discrete state of the system, we can associate a set of differential equations that describe the evolution of continuous variables of interest. This brings us to the realm of hybrid systems.

## Keywords

Hybrid Model Sample Path Parallel Composition Hybrid Automaton State Transition Diagram## Preview

Unable to display preview. Download preview PDF.

## Selected References

## ∎ Timed Automata and Time(d) Petri Nets

- — Alur, R., and D.L. Dill, “A Theory of Timed Automata,”
*Theoretical Computer Science*, No. 126, pp. 183–235, 1994.Google Scholar - — Brandin, B., and W.M. Wonham, “Supervisory Control of Timed Discrete-Event Systems,”
*IEEE Transactions on Automatic Control*, Vol. 39, No. 2, pp. 329–342, February 1994.MATHCrossRefMathSciNetGoogle Scholar - — Berthomieu, B., and M. Diaz, “Modeling and Verification of Time Dependent Systems Using Time Petri Nets,”
*IEEE Transactions on Software Engineering*, Vol. 17, No. 3, pp. 259–273, 1991.CrossRefMathSciNetGoogle Scholar - — Clarke, E.M., O. Grumberg, and D. A. Peled,
*Model Checking*, The MIT Press, Cambridge, MA, 1999.Google Scholar - — Kaynar, D.K., N. Lynch, R. Segala, and F. Vaandrager,
*The Theory of Timed I/O Automata*, Synthesis Lectures on Computer Science, Vol. 1, No. 1, pp. 1—114, Morgan & Claypool Publishers, 2006.Google Scholar - — Merlin, P.M., and D.J. Farber, “Recoverability of Communication Protocols-Implications of a Theoretical Study,”
*IEEE Transactions on Communications*, Vol. 24, No. 9, pp. 1036–1043, 1976.MATHCrossRefMathSciNetGoogle Scholar - — Sifakis, J., “Use of Petri Nets for Performance Evaluation,”
*Acta Cybernetica*, Vol. 4, No. 2, pp. 185–202, 1978.MathSciNetGoogle Scholar - — Tripakis, S., and S. Yovine, “Analysis of Timed Systems Using Time-Abstracting Bisimulations,”
*Formal Methods in Systems Design*, Vol. 18, No. 1, pp. 25–68, 2001.MATHCrossRefGoogle Scholar - — Wang, J.,
*Timed Petri Nets - Theory and Application*, Kluwer Academic Pub lishers, Boston, 1998.MATHGoogle Scholar

## ∎*Max-Plus Algebra*

- — Heidergott, B., G.J. Olsder, and J. van der Woude,
*Max Plus at Work - Modeling and Analysis of Synchronized Systems: A Course on Max-Plus Algebra and Its Applications*, Princeton University Press, 2006Google Scholar - — Baccelli, F., G. Cohen, G.J. Olsder, and J.P. Quadrat,
*Synchronization and Lin earity*, Wiley, 1992.Google Scholar - — Cohen, G., P. Moller, J.P. Quadrat, and M. Viot, “Algebraic Tools for the Perfor mance Evaluation of Discrete Event Systems,”
*Proceedings of the IEEE*, Vol. 77, No. 1, pp. 39–58, 1989.CrossRefGoogle Scholar - — Cunningham-Greene, R.A.,
*Minimax Algebra*, Springer-Verlag, Berlin, 1979.Google Scholar

## ∎ Hybrid Systems

- — Alur, R., C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, “The algorithmic analysis of hybrid sys tems,”
*Theoretical Computer Science*, Vol. 138, No. 1, pp. 3–34, 1995.MATHCrossRefMathSciNetGoogle Scholar - — Bemporad, A., and M. Morari, “Control of Systems Integrating Logic Dynamics and Constraints,”
*Automatica*, Vol. 35, No. 3, pp. 407–427, 1999.MATHCrossRefMathSciNetGoogle Scholar - — Branicky, M.S., V.S. Borkar, and S.K. Mitter, “A Unified Framework for Hy brid Control: Model and Optimal Control Theory,”
*IEEE Trans. on Automatic Control*, Vol. 43, No. 1, pp. 31–45, 1998.MATHCrossRefMathSciNetGoogle Scholar - — Grossman, R., A. Nerode, A. Ravn, and H. Rischel, (Eds),
*Hybrid Systems*, Springer, New York, 1993.Google Scholar - — Hristu-Varsakelis, D., and W.S. Levine,
*Handbook of Networked and Embedded Control Systems*, Birkhauser, Boston, 2005.MATHCrossRefGoogle Scholar

## ∎ Miscellaneous

- — Benveniste, A., and P. Le Guernic, “Hybrid Dynamical Systems Theory and the SIGNAL Language,”
*IEEE Transactions on Automatic Control*, Vol. 35, No. 5, pp. 535–546, May 1990.MATHCrossRefGoogle Scholar - — Bérard, B., M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, Ph. Sch- noebelen, with P. McKenzie,
*Systems and Software Verification. Model-Checking Techniques and Tools*, Springer, 2001.Google Scholar - — Manna, Z., and A. Pnueli,
*The Temporal Logic of Reactive and Concurrent Sys-tems: Specification*, Springer-Verlag, New York, 1992.Google Scholar - — Manna, Z., and A. Pnueli,
*Temporal Verification of Reactive Systems: Safety*, Springer-Verlag, New York, 1995.Google Scholar - — Ostroff, J.S.,
*Temporal Logic for Real-Time Systems*, Research Studies Press and John Wiley & Sons, New York, 1989.Google Scholar