×
Kalyon, Gabriel; Le Gall, Tristan; Marchand, Hervé; Massart, Thierry

Symbolic supervisory control of infinite transition systems under partial observation using abstract interpretation. (English) Zbl 1242.93074

Discrete Event Dyn. Syst. 22, No. 2, 121-161 (2012).
Summary: 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.

Cited in 1 Document

MSC:

93C65 Discrete event control/observation systems
93B50 Synthesis problems
93B52 Feedback control

Keywords:

symbolic transition systems; controller synthesis; partial observation; abstract interpretation

Software:

SMACS; Apron; UMDES; Fixpoint
PDF BibTeX XML Cite
\textit{G. Kalyon} et al., Discrete Event Dyn. Syst. 22, No. 2, 121--161 (2012; Zbl 1242.93074)
Full Text: DOI Link

References:

[1] Balemi S, Hoffmann G, Wong-Toi H, Franklin G (1993) Supervisory control of a rapid thermal multiprocessor. IEEE Trans Automat Contr 38(7):1040–1059 · Zbl 0800.93035
[2] Bourdoncle F (1992) Sémantiques des langages impératifs d’ordre supérieur et interprétation abstraite. PhD thesis, Ecole Polytechnique
[3] Brandt RD, Garg VK, Kumar R, Lin F, Marcus SI, Wonham WM (1990) Formulas for calculating supremal and normal sublanguages. Syst Control Lett 15(8):111–117 · Zbl 0715.93044
[4] Bryant R (1986) Graph-based algorithms for boolean function manipulations. IEEE Trans Comput C-45(8):677–691 · Zbl 0593.94022
[5] Cassandras C, Lafortune S (2008) Introduction to discrete event systems, 2nd edn. Springer · Zbl 1165.93001
[6] Chatterjee K, Doyen L, Henzinger TA, Raskin JF (2007) Algorithms for omega-regular games with imperfect information. Logical Methods in Computer Science 3(3–4):1–23 · Zbl 1125.91028
[7] 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
[8] Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: POPL ’78, pp 84–96. http://doi.acm.org/10.1145/512760.512770
[9] De Wulf M, Doyen L, Raskin JF (2006) A lattice theory for solving games of imperfect information. In: Hespanha J, Tiwari A (eds), Lecture notes in computer science, vol 3927. Springer, Santa Barbara, pp 153–168 · Zbl 1178.93072
[10] Fixpoint (2009) Fixpoint: an OCaml library implementing a generic fix-point engine. http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/fixpoint/ . Accessed March 2011
[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] Henzinger T, Majumdar R, Raskin JF (2005) A classification of symbolic transition systems. ACM Trans Comput Logic 6(1):1–32. http://doi.acm.org/10.1145/1042038.1042039
[13] Hespanha J, Tiwari A (eds) (2006) Hybrid systems: computation and control. In: 9th international workshop, HSCC 2006. Proceedings, lecture notes in computer science, vol 3927. Springer, Santa Barbara · Zbl 1103.68006
[14] Hill R, Tilbury D, Lafortune S (2008) Covering-based supervisory control of partially observed discrete event systems for state avoidance. In: 9th international workshop on discrete event systems, pp 2–8
[15] 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
[16] Jeannet B, Miné A (2009) Apron: a library of numerical abstract domains for static analysis. In: Bouajjani A, Maler O (eds) CAV, lecture notes in computer science, vol 5643. Springer, pp 661–667
[17] 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, Scottland, pp 349–364 · Zbl 1087.68594
[18] Kalyon G, T LG, Marchand H, Massart T (2009) Control of infinite symbolic transition systems under partial observation. In: European control conference. Budapest, Hungary, pp 1456–1462
[19] Kumar R, Garg V (2005) On computation of state avoidance control for infinite state systems in assignment program model. IEEE Trans Autom Sci Eng 2(2):87–91
[20] 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. URL: citeseer.ist.psu.edu/kumar95predicates.html · Zbl 0774.93003
[21] Kupferman O, Madhusudan P, Thiagarajan P, Vardi M (2000) Open systems in reactive environments: Control and synthesis. In: Proc. 11th int. conf. on concurrency theory. Lecture notes in computer science, vol 1877. Springer-Verlag, pp 92–107 · Zbl 0999.68124
[22] Le Gall T, Jeannet B, Marchand H (2005) Supervisory control of infinite symbolic systems using abstract interpretation. In: Decision and control, 2005 and 2005 European control conference. CDC-ECC ’05, pp 30–35
[23] Lin F, Wonham W (1988) On observability of discrete-event systems. Inf Sci 44(3):173–198 · Zbl 0644.93008
[24] Marchand H, Bournai P, Le Borgne M, Le Guernic P (2000) Synthesis of discrete-event controllers based on the signal environment. Discrete Event Dyn Syst: Theory and Applications 10(4):347–368 · Zbl 0976.93057
[25] Miné A (2001) The octagon abstract domain. In: Proc. of the workshop on analysis, slicing, and transformation (AST’01). IEEE CS Press, Stuttgart, IEEE, Gernamy, pp 310–319
[26] Miremadi S, Akesson K, Fabian M, Vahidi A, Lennartson B (2008a) Solving two supervisory control benchmark problems using supremica. In: 9th international workshop on discrete event systems, pp 131–136
[27] Miremadi S, Akesson K, Lennartson B (2008b) Extraction and representation of a supervisor using guards in extended finite automata. In: 9th international workshop on discrete event systems, pp 193–199
[28] OCaml (2005) The programming language Objective CAML. http://caml.inria.fr/ . Accessed August 2010
[29] Pnueli A, Rosner R (1989) On the synthesis of an asynchronous reactive module. In: Ausiello G, Dezani-Ciancaglini M, Rocca SD (eds) ICALP, Springer, Lecture Notes in Computer Science, vol 372, pp 652–671 · Zbl 0686.68015
[30] Ramadge P, Wonham W (1987) Modular feedback logic for discrete event systems. SIAM J Control Optim 25(5):1202–1218 · Zbl 0698.93035
[31] Ramadge P, Wonham W (1989) The control of discrete event systems. Proc IEEE (Special Issue on Dynamics of Discrete Event Systems) 77(1):81–98
[32] Reif J (1984a) The complexity of two-player games of incomplete information. J Comput Syst Sci 29(2):274–301 · Zbl 0551.90100
[33] Reif J (1984b) The complexity of two-player games of incomplete information. J Comput Syst Sci 29(2):274–301 · Zbl 0551.90100
[34] SMACS (2010) The SMACS tool. http://www.smacs.be/ . Accessed March 2011
[35] 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
[36] Takai S, Ushio T (2003) Effective computation of an L m (G)-closed, controllable, and observable sublanguage arising in supervisory control. Syst Control Lett 49(3):191–200 · Zbl 1157.93444
[37] Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5:285–309 · Zbl 0064.26004
[38] Thistle J, Lamouchi H (2009) Effective control synthesis for partially observed discrete-event systems. SIAM J Control Optim 48(3):1858–1887 · Zbl 1282.93178
[39] Wonham W, Ramadge P (1988) Modular supervisory control of discret-event systems. Math Control Signals Syst 1(1):13–30 · Zbl 0661.93053
[40] Yoo T, Lafortune S (2006) Solvability of centralized supervisory control under partial observation. Discrete Event Dyn Syst 16:527–553 · Zbl 1103.93015
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.