SMACS is a tool aiming at the supervisory control of infinite state systems under partial observation. We consider a system modelled by a Symbolic Transition System (i.e. an automaton extended with variables). The controller can observe the system by knowing the valuation of the variables. However, this observation is not completely accurate; a mask models this partial observation of the system. According to this observation, the controller comes to a decision and disables some controllable actions so that the system satisfies a given specification.

This software is curently developped by Gabriel Kalyon and Tristan Le Gall.

to be done

SMACS code source is available under GNU Lesser General Public Licence. It requires three libraries: APRON (with the OCAML interface), Camllib and Fixpoint. Moreover, the graphical ouput requires two additional softwares: Graphviz and Ghostview.

SMACS v1.0: first release.

SMACS modular v1.0m: modular version. The modular version does not have the same input and output than the main version; The experimental section of the article Decentralized Control of Infinite Systems was done with SMACS v1.0 and SMACS modular v1.0m.

[2010] G. Kalyon, Le Gall T, H. Marchand and T. Massart. Decentralized Control of Infinite Systems, submitted to Journal of Discrete Event Systems

[2010] G. Kalyon, Le Gall T, H. Marchand and T. Massart. Covering-Based Supervisory Control of Infinite Symbolic Transition Systems under Partial Observation, submitted to Journal of Discrete Event Systems

[2009] G. Kalyon, T. Le Gall, H. Marchand and T. Massart. Contrôle décentralisé de systèmes symboliques infinis sous observation partielle, in 7ème Colloque Francophone sur la Modélisation des Systèmes Réactifs, Nantes, France, november 2009. (more)

[2009] G. Kalyon, Le Gall T, H. Marchand and T. Massart. Control of Infinite Symbolic Transition Systems under Partial Observation, in European Control Conference, Budapest, Hungary, August 2009. (more)