SMACS swMATH ID: 6144 Software Authors: Kalyon, Gabriel; Le Gall, Tristan; Marchand, Herv’e; Massart, Thierry Description: Symbolic supervisory control of infinite transition systems under partial observation using abstract interpretation. 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. Homepage: http://www.ulb.ac.be//di/verif/tlegall/smacs/index.html Keywords: symbolic transition systems; controller synthesis; partial observation; abstract interpretation Related Software: Fixpoint; UMDES; Apron Cited in: 2 Documents Further Publications: http://www.smacs.be/papers.html Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Symbolic supervisory control of infinite transition systems under partial observation using abstract interpretation. Zbl 1242.93074Kalyon, Gabriel; Le Gall, Tristan; Marchand, Hervé; Massart, Thierry 2012 Cited by 4 Authors 2 Kalyon, Gabriel 2 Le Gall, Tristan 2 Marchand, Hervé 2 Massart, Thierry Jacques Cited in 1 Serial 2 Discrete Event Dynamic Systems Cited in 1 Field 2 Systems theory; control (93-XX) Citations by Year