Symbolic Supervisory Control of Infinite Transition Systems under Partial Observation using Abstract Interpretation

Abstract : We propose algorithms for the synthesis of state-feedback controllers with partial observation of infinite state discrete event systems modelled by Symbolic Transition Systems. We provide models of safe memoryless controllers both for potentially deadlocking and deadlock free controlled systems. The termination of the algorithms solving these problems is ensured using abstract interpretation techniques which provide an overapproximation of the transitions to disable. We then extend our algorithms to controllers with memory and to online controllers. We also propose improvements in the synthesis of controllers in the finite case which, to our knowledge, provide more permissive solutions than what was previously proposed in the literature. Our tool SMACS gives an empirical validation of our methods by showing their feasibility, usability and efficiency.
Type de document :
Article dans une revue
Discrete Event Dynamic Systems, Springer Verlag, 2012, 22 (2), pp.121-161. 〈10.1007/s10626-011-0101-3〉
Liste complète des métadonnées

Littérature citée [34 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00586169
Contributeur : Hervé Marchand <>
Soumis le : vendredi 15 avril 2011 - 10:46:12
Dernière modification le : mercredi 29 novembre 2017 - 15:08:13
Document(s) archivé(s) le : jeudi 8 novembre 2012 - 16:36:13

Fichier

JDEDS.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Gabriel Kalyon, Tristan Le Gall, Hervé Marchand, Thierry Massart. Symbolic Supervisory Control of Infinite Transition Systems under Partial Observation using Abstract Interpretation. Discrete Event Dynamic Systems, Springer Verlag, 2012, 22 (2), pp.121-161. 〈10.1007/s10626-011-0101-3〉. 〈inria-00586169〉

Partager

Métriques

Consultations de la notice

206

Téléchargements de fichiers

167