Supervisory control of infinite state systems under partial observation
Gabriel Kalyon, Thierry Massart · 2010
A discrete event system is a system whose state space is given by a discrete set and whose state transition mechanism is event-driven i.e., its state evolution depends only on the occurrence of discrete events over the time. These systems are used in many fields of application (telecommunication networks, aeronautics, aerospace,...). The validity of these systems is then an important issue and to ensure it we can use supervisory control methods. These methods consist in imposing a given specification on a system by means of a controller which runs in parallel with the original system and which restricts its behavior. In this thesis, we develop supervisory control methods where the system can have an infinite state space and the controller has a partial observation of the system (this implies that the controller must define its control policy from an imperfect knowledge of the system). Unfortunately, this problem is generally undecidable. To overcome this negative result, we use abstract interpretation techniques which ensure the termination of our algorithms by overapproximating, however, some computations. The aim of this thesis is to provide the most complete contribution it is possible to bring to this topic. Hence, we consider more and more realistic problems. More precisely, we start our work by considering a centralized framework (i.e., the system is controlled by a single controller) and by synthesizing memoryless controllers (i.e., controllers that define their control policy from the current observation received from the system). Next, to obtain better solutions, we consider the synthesis of controllers that record a part or the whole of the execution of the system and use this information to define the control policy. Unfortunately, these methods cannot be used to control an interesting class of systems: the distributed systems. We have then defined methods that allow to control distributed systems with synchronous communications (decentralized and modular methods) and with asynchronous communications (distributed method). Moreover, we have implemented some of our algorithms to experimentally evaluate the quality of the synthesized controllers. / Un systeme a evenements discrets est un systeme dont l'espace d'etats est un ensemble discret et dont l'evolution de l'etat courant depend de l'occurrence d'evenements discrets a travers le temps. Ces systemes sont presents dans de nombreux domaines critiques tels les reseaux de communications, l'aeronautique, l'aerospatiale... La validite de ces systemes est des lors une question importante et une maniere de l'assurer est d'utiliser des methodes de controle supervise. Ces methodes associent au systeme un dispositif, appele controleur, qui s'execute en parrallele et qui restreint le comportement du systeme de maniere a empecher qu'un comportement errone ne se produise. Dans cette these, on s'interesse au developpement de methodes de controle supervise ou le systeme peut avoir un espace d'etats infini et ou les controleurs ne sont pas toujours capables d'observer parfaitement le systeme; ce qui implique qu'ils doivent definir leur politique de controle a partir d'une connaissance imparfaite du systeme. Malheureusement, ce probleme est generalement indecidable. Pour surmonter cette difficulte, nous utilisons alors des techniques d'interpretation abstraite qui assurent la terminaison de nos algorithmes au prix de certaines sur-approximations dans les calculs. Le but de notre these est de fournir la contribution la plus complete possible dans ce domaine et nous considerons pour cela des problemes de plus en plus realistes. Plus precisement, nous avons commence notre travail en definissant une methode centralisee ou le systeme est controle par un seul controleur qui definit sa politique de controle a partir de la derniere information recue du systeme. Ensuite, pour obtenir de meilleures solutions, nous avons defini des controleurs qui retiennent une partie ou la totalite de l'execution du systeme et qui definissent leur politique de controle a partir de cette information. Malheureusement, ces methodes ne peuvent pas etre utilisees pour controler une classe interessante de systemes: les sytemes distribues. Nous avons alors defini des methodes permettant de controler des systemes distribues dont les communications sont synchrones (methodes decentralisees et modulaires) et asynchrones (methodes distribuees). De plus, nous avons implemente certains de nos algorithmes pour evaluer experimentalement la qualite des controleurs qu'ils synthetisent.