In this tutorial we propose the model of timed automata, originating from the verification of real-time systems, as a model for posing and solving time-dependent planning and scheduling problems. We believe that in the same sense as automata are used as the major vehicle for verification of systems where the model of time is qualitative, timed automata can be the center of a a unifying mathematical modeling framework for quantitative time, having the following attractive features:

  1. It is sufficiently expressive to describe the essential aspects of time-dependent real-life problems in a variety of application domains.
  2. It provides for models with well-defined and clear dynamic semantics.
  3. These models are amenable to computer-aided design methods such as simulation, testing, verification and automatic synthesis of (optimal) schedules and plans.
  4. These methods are currently supported by tools of various levels of maturity, that treat the specific computational problems of time-related reasoning.

Information about the authors

Oded Maler Oded Maler was born in 1957 in Haifa, Israel. He obtained his B.A. in Computer Science from the Technion, Haifa in 1979 and his M.Sc. in Management Science from the University of Tel-Aviv at 1984. In 1989 he finished his Ph.D. thesis ( Finite Automata: Infinite Behavior, Learnability and Decomposition ), under the supervision of A. Pnueli in the department of Applied Mathematics and Computer Science, Weizmann Institute, Rehovot. After two years of post-doc at IRISA, Rennes, he moved to Grenoble at 1992 and obtained a research position (CR1) at the CNRS (French National Center of Scientific Research) in 1994. He has been promoted to "research director" (DR2) in 2001. Dr. Maler's research is centered around the theory of automata and its various extensions, most notably timed automata, hybrid automata and their application to control, embedded systems, scheduling and circuit timing analysis.

back to tutorials list