Introduction
Our project addresses the controller synthesis problem for real-time open systems. Most of the safety critical systems nowadays include a control program to supervise a plant. Such systems are often called embedded systems (e.g. nuclear plant, transport software, communication protocols, etc). They are critical in the sense that error can lead to the loss of lives or a major loss of money. This is why a great deal of research has been devoted to the formal verification of such systems. Among other techniques, model-checking consists in verifying that a model (of the plant and the control program running concurrently) meets some specification. It is now widely used in an industrial context and has turned out very successful in the design of critical systems. However, model-checking requires that the whole system is designed and the control program is given a priori.
A more difficult task consists in building a control program that supervises the plant in order to meet some requirements. In the automatic control community this problem has been extensively studied since the seminal work of Ramadge and Wonham about the supervisory control of discrete systems. How to build a controller for finite discrete event systems and when it can be done, are now well understood questions. This is not yet the case for timed systems, which involve real-time constraints. During the last decade, the model of timed automata (Alur and Dill) made it possible to reason about quantitative time. Model-checking was lifted to timed automata and is now supported by various tools (KRONOS, UPPAAL, CMC), which have been applied successfully to the verification of many industrial cases. The control synthesis problem for timed systems is of course more difficult, particularly because of the dense nature of time. It has been studied quite a lot recently but only partial results exist and there is no unified theory for the control of timed systems.
Objectives
If we try to summarize the results about control synthesis for timed systems we find the following features:
- the systems are usually timed automata or hybrid automata where the transitions are partitioned into controllable and uncontrollable ones; another way of tackling the control problem is to assume that discrete transitions are controllable (triggered by the controller) while continuous transitions correspond to the evolution of the environment;
- there are different (un)decidability results according to the class of timed systems involved (timed automata, rectangular automata, hybrid automata) and the logic used for specifying the desired property of the system;
- different types of timed control can be defined: dense-time control, sampling control, and again different decidability results follow from the type of control involved;
- the controller synthesis problem is solved using a backward reachability algorithm on the model of the plant: this means that the synthetised controller (when there is one) has a structure (discrete part) determined by the model of the plant.
In this project, our main objectives are to increase the knowledge about control problems for timed systems and provide new methods for controller synthesis.
Partners
VERIMAG People involved
- Karine Altisen
- Thao Dang
- Moez Krichen
- Stavros Tripakis
