Bherer, Hans; Desharnais, Jules; St-Denis, Richard Control of parameterized discrete event systems. (English) Zbl 1169.93018 Discrete Event Dyn. Syst. 19, No. 2, 213-265 (2009). Summary: This paper investigates the control of parameterized discrete event systems when specifications are given in terms of predicates and satisfy a similarity assumption. This study is motivated by a weakness in current synthesis methods that do not scale well to huge systems. For systems consisting of similar processes under total or partial observation, conditions are given to deduce properties of a system of \(n\) processes (arbitrary size) from properties of a system of \(n _{0}\) processes (bounded size), with \(n \geq n _{0}\). Furthermore, it is shown how to infer a control policy for the former from the latter’s, while taking into account interconnections between processes. Cited in 3 Documents MSC: 93C65 Discrete event control/observation systems 93B52 Feedback control 93B50 Synthesis problems 93A15 Large-scale systems 39A13 Difference equations, scaling (\(q\)-differences) Keywords:parameterized discrete event system; state feedback control; scalable control policy; interconnection relation; weak and strong soundness Software:CalcCheck; UMDES PDFBibTeX XMLCite \textit{H. Bherer} et al., Discrete Event Dyn. Syst. 19, No. 2, 213--265 (2009; Zbl 1169.93018) Full Text: DOI References: [1] Attie PC, Emerson EA (1998) Synthesis of concurrent systems with many similar processes. ACM Trans Program Lang Syst 20(1):1–65 · doi:10.1145/271510.271519 [2] Balemi S, Hoffmann GJ, Gyugyi P, Wong-Toi H, Franklin GF (1993) Supervisory control of a rapid thermal multiprocessor. IEEE Trans Autom Contr 38(7):1040–1059 · Zbl 0800.93035 · doi:10.1109/9.231459 [3] Barbeau M, Kabanza F, St-Denis, R (1997) An efficient algorithm for controller synthesis under full observation. J Algorithms 25(1):144–161 · Zbl 0888.68064 · doi:10.1006/jagm.1997.0877 [4] Barrett G, Lafortune S (1998) Bisimulation, the supervisory control problem and strong model matching for finite state machines. Discret Event Dyn Syst Theory Appl 8(4):377–429 · Zbl 0919.93005 · doi:10.1023/A:1008301317459 [5] Ben Hadj-Alouane N, Lafortune S, Lin F (1994) Variable lookahead supervisory control with state information. IEEE Trans Autom Contr 39(12):2398–2410 · Zbl 0812.93003 · doi:10.1109/9.362854 [6] Ben Hadj-Alouane N, Lafortune S, Lin F (1996) Centralized and distributed algorithms for on-line synthesis of maximal control policies under partial observation. Discret Event Dyn Syst Theory Appl 6(4): 379–427 · Zbl 0880.93016 · doi:10.1007/BF01797138 [7] Bherer H, Desharnais J, Frappier M, St-Denis R (2003) Intégration d’une technique de vérification dans une procédure de synthèse de contrôleurs de systèmes paramétrés. In: Méry D, Rezg N, Xie X (eds) Modélisation des systèmes réactifs (MSR 2003), pp 553–566 [8] Bherer H, Desharnais J, Frappier M, St-Denis R (2004) Synthesis of state feedback controllers for parameterized discrete event systems. In: Wang F (ed) Automated technology for verification and analysis (ATVA’2004). Lecture notes in computer science, vol 3299. Springer, Berlin Heidelberg New York, pp 487–490 · Zbl 1108.93311 [9] Bherer H, Desharnais J, St-Denis R (2005) Synthesis of state feedback controllers for parameterized discrete event systems under partial observation. In: Proceedings of the 44th IEEE conference on decision and control and European control conference 2005. IEEE, Seville, pp 3499–3506 [10] Bherer H, Desharnais J, St-Denis R (2006a) Parameterized discrete event systems under partial observation revisited. In: Proceedings of the 8th IASTED international conference on control and applications. IASTED, Montréal, pp 273–280 [11] Bherer H, Desharnais J, St-Denis R (2006b) On the reachability and nonblocking properties for parameterized discrete event systems. In: Proceedings of the 8th international workshop on discrete event systems. Ann Arbor, MI, 10–12 July 2006, pp 113–118 [12] Cassandras CG, Lafortune S (1999) Introduction to discrete event systems. Kluwer, Boston · Zbl 0934.93001 [13] Chung S-L, Lafortune S, Lin F (1992) Limited lookahead policies in supervisory control of discrete event systems. IEEE Trans Autom Contr 37(12):1921–1935 · Zbl 0773.93004 · doi:10.1109/9.182478 [14] Davey BA, Priestley HA (1990) Introduction to lattices and order. Cambridge University Press, Cambridge · Zbl 0701.06001 [15] de Queiroz MH, Cury JER (2000) Modular supervisory control of large scale discrete event systems. In: Boel R, Stremersch G (eds) Discrete event systems: analysis and control. The international series in engineering and computer science, vol 569. Springer, Berlin Heidelberg New York, pp 103–110 · Zbl 1051.93066 [16] Dreschsler R, Sieling D (2001) Binary decision diagrams in theory and practice. Int J Softw Tools Technol Transf 3(2):112–136 · Zbl 1002.68583 [17] Emerson EA, Kahlon V (2000) Reducing model checking of the many to the few. In: McAllester DA (ed) Automated deduction (CADE’2000). Lecture notes in computer science, vol 1831. Springer, Berlin Heidleberg New York, pp 236–354 · Zbl 0963.68109 [18] Emerson EA, Sistla AP (1997) Utilizing symmetry when model-checking under fairness assumptions: an automata-theoretic approach. ACM Trans Program Lang Syst 19(4):617–638 · doi:10.1145/262004.262008 [19] Eyzell JM, Cury JER (2001) Exploiting symmetry in the synthesis of supervisors for discrete event systems. IEEE Trans Autom Contr 46(9):1500–1505 · Zbl 1011.93070 · doi:10.1109/9.948486 [20] Frappier M, St-Denis R (2001) Towards a computer-aided design of reactive systems. In: Moreno-Díaz R, Buchberger B, Freire J-L (eds) Computer aided systems theory – EUROCAST 2001. Lecture notes in computer science, vol 2178. Springer, Berlin Heidelberg New York, pp 421–436 · Zbl 1023.93511 [21] Gohari P, Wonham WM (2005) Efficient implementation of fairness in discrete-event systems using queues. IEEE Trans Autom Contr 50(11):1845–1849 · Zbl 1365.93289 · doi:10.1109/TAC.2005.858658 [22] Gries D, Schneider FB (1995) A logical approach to discrete math. Springer, Berlin Heidelberg New York [23] Giua A, DiCesare F (1994) Petri net structural analysis for supervisory control. IEEE Trans Robot Autom 10(2):185–195 · Zbl 0812.93004 · doi:10.1109/70.282543 [24] Harel D (1987) Statecharts: a visual formalism for complex systems. Sci Comput Program 8(3):231–274 · Zbl 0637.68010 · doi:10.1016/0167-6423(87)90035-9 [25] Heymann M, Lin F (1994) On-line control of partially observed discrete event systems. Discret Event Dyn Syst 4(3):221–236 · Zbl 0811.93004 · doi:10.1007/BF01438708 [26] Holloway LE, Krogh BH, Giua A (1997) A survey of Petri net methods for controlled discrete event systems. Discret Event Dyn Syst Theory Appl 7(2):151–190 · Zbl 0968.93053 · doi:10.1023/A:1008271916548 [27] Kerjean S, Kabanza F, St-Denis R, Thiébaux S (2006) Analyzing LTL model checking techniques for plan synthesis and controller synthesis. Electron Notes Theor Comput Sci 149(2):91–104 · doi:10.1016/j.entcs.2005.07.028 [28] Komenda J, van Schuppen JH (2005) Supremal sublanguages of general specification languages arising in modular control of dicrete-event systems. In: Proceedings of the 44th IEEE conference on decision and control and European control conference 2005. IEEE, Seville, pp 2275–2780 [29] Komenda J, van Schuppen JH, Gaudin B, Marchand H (2005) Modular supervisory control with general indecomposable specification languages. In: Proceedings of the 44th IEEE conference on decision and control and European control conference 2005. IEEE, Seville, pp 3474–3479 [30] Kumar R, Garg VK (1995) Modeling and control of logical discrete event systems. Kluwer, Boston · Zbl 0875.68980 [31] Kumar R, Garg V, Marcus SI (1993) Predicates and predicate transformers for supervisory control of discrete event dynamical systems. IEEE Trans Autom Contr 38(2):232–247 · Zbl 0774.93003 · doi:10.1109/9.250512 [32] Leduc RJ, Brandin BA, Lawford M, Wonham WM (2005) Hierarchical interface-based supervisory control–part I: serial case. IEEE Trans Autom Contr 50(9):1322–1335 · Zbl 1365.93296 · doi:10.1109/TAC.2005.854586 [33] Li Y (1991) Control of vector discrete-event systems. Ph.D. thesis, University of Toronto, Toronto [34] Li Y, Wonham WM (1988) Controllability and observability in the state-feedback control of discrete-event systems. In: Proceedings of 27th IEEE conference on decision and control. IEEE, Austin, pp 203–208 [35] Li Y, Wonham WM (1993) Control of vector discrete-event systems I–the base model. IEEE Trans Autom Contr 38(8):1214–1227 · Zbl 0784.93007 · doi:10.1109/9.233154 [36] Li Y, Wonham WM (1994) Control of vector discrete-event systems II–controller synthesis. IEEE Trans Autom Contr 39(3):512–531 · Zbl 0823.93003 · doi:10.1109/9.280750 [37] Ma C, Wonham WM (2005) Nonblocking supervisory control of state tree structures. Lecture notes in control and information sciences, vol 317. Springer, Berlin Heidelberg New York · Zbl 1114.93002 [38] Makungu M, Barbeau M, St-Denis R (1999) Synthesis of controllers of processes modeled as colored Petri nets. Discret Event Dyn Syst Theor Appl 9(2):147–169 · Zbl 0952.93040 · doi:10.1023/A:1008371814442 [39] Pena PN, Cury JER, Lafortune S (2006) Testing modularity of local supervisors: an approach based on abstractions. In: Proceedings of the 8th international workshop on discrete event systems. Ann Arbor, MI, 10–12 July 2006, pp 107–112 [40] Pnueli A, Ruah S, Zuck L (2001) Automatic deductive verification with invisible invariants. In: Margaria T, Yi W (eds) Tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol 2031. Springer, Berlin Heidelberg New York, pp 82–97 · Zbl 0978.68539 [41] Prosser JH, Kam M, Kwatny HG (1998) Online supervisor synthesis for partially observed discrete-event systems. IEEE Trans Autom Contr 43(11):1630–1634 · Zbl 0981.93044 · doi:10.1109/9.728885 [42] Ramadge PJG, Wonham WM (1987) Modular feedback logic for discrete event systems. SIAM J Contr Optim 25(5):1202–1218 · Zbl 0698.93035 · doi:10.1137/0325066 [43] Schmidt K, Marchand H, Gaudin B (2006) Modular and decentralized supervisory control of concurrent discrete event systems using reduced system models. In: Proceedings of the 8th international workshop on discrete event systems. Ann Arbor, MI, 10–12 July 2006, pp 149–154 [44] Song R, Leduc RJ (2006) Symbolic synthesis and verification of hierarchical interface-based supervisory control. In: Proceedings of the 8th international workshop on discrete event systems. Ann Arbor, MI, 10–12 July 2006, pp 419–426 [45] St-Denis R (2002) Designing reactive systems: integration of abstraction techniques into a synthesis procedure. J Syst Softw 60(2):103–112 · Zbl 05433809 · doi:10.1016/S0164-1212(01)00083-8 [46] Takai S, Kodama S (1997) M-controllable subpredicates arising in state feedback control of discrete event systems. Int J Contr 67(4):553–566 · Zbl 0883.93034 · doi:10.1080/002071797224072 [47] Takai S, Kodama, S (1998) Characterization of all M-controllable subpredicates of a given predicate. Int J Contr 70(4):541–549 · Zbl 0930.93055 · doi:10.1080/002071798222190 [48] Takai S, Ushio T, Kodama S (1995) Static-state feedback control of discrete-event systems under partial observation. IEEE Trans Autom Contr 40(11):1950–1954 · Zbl 0841.93023 · doi:10.1109/9.471222 [49] Thistle JG, Nazari S (2005) Analysis of arbitrarily large networks of discrete-event systems. In: Proceedings of the 44th IEEE conference on decision and control and European control conference 2005. IEEE, Seville, pp 3468–3473 [50] Wonham WM (2006) Supervisory control of discrete-event systems. ECE 1636F/1637S, System control group. University of Toronto, Toronto [51] Wonham WM, Ramadge PJG (1988) Modular supervisory control of discrete event systems. Math Contr Signals Syst 1(1):13–30 · Zbl 0661.93053 · doi:10.1007/BF02551233 [52] Zhong H, Wonham WM (1990) On the consistency of hierarchical supervision in discrete-event systems. IEEE Trans Autom Contr 35(10):1125–1134 · Zbl 0724.93051 · doi:10.1109/9.58555 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.