Decentralized control of infinite systems. (English) Zbl 1226.93013

Summary: We propose algorithms for the synthesis of decentralized state-feedback controllers with partial observation of infinite state systems, which are modeled by symbolic transition systems. We first consider the computation of safe controllers ensuring the avoidance of a set of forbidden states and then extend this result to the deadlock free case. The termination of the algorithms solving these problems is ensured by the use of abstract interpretation techniques, but at the price of overapproximations, in particular, in the computation of the states which must be avoided. We then extend our algorithms to the case where the system to be controlled is given by a collection of subsystems (modules). This structure is exploited to locally compute a controller for each module. Our tool SMACS gives an empirical evaluation of our methods by showing their feasibility, usability and efficiency.


93A14 Decentralized systems
93B52 Feedback control
93B50 Synthesis problems


SMACS; Fixpoint; UMDES; Apron
Full Text: DOI Link


[1] Akesson K, Flordal H, Fabian M (2002) Exploiting modularity for synthesis and verification of supervisors. In: Proc. of the IFAC. Barcelona, Spain
[2] APRON (2009) The APRON library. http://apron.cri.ensmp.fr/
[3] Brandin B, Malik R, Dietrich P (2000) Incremental system verification and synthesis of minimally restrictive behaviours. In: Proceedings of the American control conference. Chicago, Illinois, pp 4056–4061
[4] Cassandras C, Lafortune S (2008) Introduction to discrete event systems, 2nd edn. Springer · Zbl 1165.93001
[5] Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL’77, pp 238–252
[6] Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: POPL ’78, pp 84–96
[7] FixPoint (2009) Fixpoint: an OCaml library implementing a generic fix-point engine. http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/fixpoint/
[8] Gaudin, B, Deussen P (2007) Supervisory control on concurrent discrete event systems with variables. In: 26th American control conference, ACC’07
[9] Gaudin B, Marchand H (2005) Efficient computation of supervisors for loosely synchronous discrete event systems: a state-based approach. In: 6th IFAC World congress. Prague, Czech Republic
[10] Gaudin B, Marchand H (2007) An efficient modular method for the control of concurrent discrete event systems: a language-based approach. Discrete Event Dyn Syst 17(2):179–209 · Zbl 1116.93038
[11] Halbwachs N, Proy Y, Roumanoff P (1997) Verification of real-time systems using linear relation analysis. Form Methods Syst Des 11(2):157–185
[12] Jeannet B (2003) Dynamic partitioning in linear relation analysis. Application to the verification of reactive systems. Form Methods Syst Des 23(1):5–37 · Zbl 1067.68091
[13] Jeannet B, Jéron T, Rusu V, Zinovieva E (2005) Symbolic test selection based on approximate analysis. In: TACAS’05, vol 3440 of LNCS. Edinburgh, pp 349–364 · Zbl 1087.68594
[14] Kalyon G, Le Gall T, Marchand H, Massart T (2009) Control of infinite symbolic transition systems under partial observation. In: European control conference. Hungary, pp 1456–1462 · Zbl 1242.93074
[15] Kumar R, Garg V (2005) On computation of state avoidance control for infinite state systems in assignment program model. IEEE Trans Automat Sci Eng 2(2):87–91
[16] Kumar R, Garg V, Marcus S (1993) Predicates and predicate transformers for supervisory control of discrete event dynamical systems. IEEE Trans Automat Contr 38(2):232–247 · Zbl 0774.93003
[17] Le Gall T, Jeannet B, Marchand H (2005) Supervisory control of infinite symbolic systems using abstract interpretation. In: CDC/ECC’05, pp 31–35
[18] Miné A (2001) The octagon abstract domain. In: Proc. of the workshop on analysis, slicing, and transformation (AST’01). IEEE. IEEE CS Press, Stuttgart, Germany, pp 310–319
[19] OCaml (2009) The programming language Objective CAML. http://caml.inria.fr/
[20] Ramadge P, Wonham W (1989) The control of discrete event systems. Proc IEEE 77(1):81–98 (Special issue on Dynamics of Discrete Event Systems)
[21] Rudie K, Wonham W (1992a) Think globally, act locally: decentralized supervisory control. IEEE Trans Automat Contr 31(11):1692–1708 · Zbl 0778.93002
[22] Rudie K, Wonham WM (1992b) An automata-theoretic approach to automatic program verification. In: Proceedings of the IEEE Conference on Decision and Control (CDC). Tucson, Arizona, pp 3770–3777
[23] SMACS (2010) The SMACS tool. http://www.smacs.be/
[24] Takai S (1998) On the languages generated under fully decentralized supervision. IEEE Trans Automat Contr 43(9):1253–1256 · Zbl 0957.93055
[25] Takai S, Kodama S (1997) M-controllable subpredicates arising in state feedback control of discrete event systems. Int J Control 67(4):553–566 · Zbl 0883.93034
[26] Takai S, Kodama S (1998) Characterization of all m-controllable subpredicates of a given predicate. Int J Control 70(9):541–549 · Zbl 0930.93055
[27] Takai S, Kodama S, Ushio T (1994) Decentralized state feedback control of discrete event systems. Syst Control Lett 22(5):369–375 · Zbl 0827.93004
[28] Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5:285–309 · Zbl 0064.26004
[29] Willner Y, Heymann M (1991) Supervisory control of concurrent discrete-event systems. Int J Control 54(5):1143–1169 · Zbl 0752.93043
[30] Wonham W, Ramadge P (1988) Modular supervisory control of discrete-event systems. Math Control Signals Syst 1(1):13–30 · Zbl 0661.93053
[31] Yoo T-S, Lafortune S (2002) A general architecture for decentralized supervisory control of discrete-event systems. Discrete Event Dyn Syst 12:335–377 · Zbl 1048.93067
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.