You are in: Contents/ Tutorials     Timed Automata for Planning and Scheduling   Oded Maler (VERIMAG, France) Oded.Maler@imag.fr   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: It is sufficiently expressive to describe the essential aspects of time-dependent real-life problems in a variety of application domains. It provides for models with well-defined and clear dynamic semantics. These models are amenable to computer-aided design methods such as simulation, testing, verification and automatic synthesis of (optimal) schedules and plans. These methods are currently supported by tools of various levels of maturity, that treat the specific computational problems of time-related reasoning.     Practical Approaches to Handling Uncertainty in Planning and Scheduling   J. Christopher Beck (Univ. College Cork, Ireland) c.beck@4c.ucc.ie Thierry Vidal (ENIT, France) thierry@enit.fr   This tutorial presents techniques for dealing with the fact that the execution of plans and schedules in the real world cannot assume a static environment: the world changes non-deterministically during problem solving and execution. We present techniques from the Artificial Intelligence and Operations Research literature for handling uncertainty in planning and scheduling with emphasis on practical techniques. Such techniques include reactive, on-line scheduling and planning, and proactive, off-line techniques that build solutions that can cope with uncertain events, as well as intermediate approaches between these extremes.     Model Checking --- A Hands-on Introduction   Alessandro Cimatti (ITC-Irst, Italy) cimatti@irst.itc.it Marco Pistore (Univ. of Trento, Italy) pistore@dit.unitn.it Marco Roveri (ITC-Irst, Italy) roveri@irst.itc.it   Model Checking is a formal technique for the verification of designs of concurrent systems. It is based on the representation of the system being analyzed as a (finite state) transition systems (e.g. Kripke models), while the requirements are typically expressed in temporal logics. A system satisfies a given property amounts to checking if the corresponding temporal formula is true in the Kripke model. Model checking is very effective in pinpointing design errors that are extremely hard to detect by means of testing, and is therefore being applied in the industrial development of reactive systems, hardware designs, and communication protocols. Furthermore, model checking techniques and tools are gaining interest in several fields of Artificial Intelligence (e.g. Planning, Multi-agent systems, and Model-based Diagnosis) and Engineering (e.g. Requirement Verification, Safety Analysis). Of particular interest is Symbolic Model Checking, which makes it is possible to analyze extremely large finite-state systems by means of symbolic representation techniques (e.g. Binary Decision Diagrams, propositional satisfiability).     Resource-Bounded And Time-Critical Reasoning   Lloyd Greenwald (Drexel Univ., USA) lgreenwald@cs.drexel.edu Shlomo Zilberstein (Univ. of Massachusetts, USA) shlomo@cs.umass.edu   A central problem in artificial intelligence is how to develop computational models that allow decision-support systems or autonomous agents to react to a situation after performing the right amount of deliberation. Frequently, the complexity of problem solving makes it beneficial to use approximate solutions rather than try to compute the optimal answer. This issue arises in a wide range of application domains including medical trauma management, Bayesian inference, sequence alignment, graphics rendering, web page prefetching, autonomous space exploration, real-time avionics, and robot navigation. This tutorial explores the theory and practice of building intelligent systems that reason explicitly about employing limited computational resources to generate timely solutions to difficult combinatorial optimization, planning and scheduling problems. Solution techniques go beyond simple greedy or reactive algorithms to achieve high-quality solutions while meeting both hard and soft real-time deadlines. We will explore over fifteen years of progress in this area, covering historical perspectives, state-of-the-art solution techniques, and current and future challenges.