×

zbMATH — the first resource for mathematics

Refinements of behavioural abstractions for the supervisory control of hybrid systems. (English) Zbl 07242395
A class of hybrid systems is described in the framework of Willems’ behavioral system theory. The authors focus their attention on time-invariant systems with an external discrete-event input/output interface. The requirement of a uniform length of the discrete-valued external signals is dropped. The concept of experiments is briefly discussed as well as the concept a finite state machine realization. An algorithm for solving the supervisory controller synthesis problem is proposed. Also, it is proved, under suitable assumptions, that this algorithm terminates with success after finitely many iterations. This is the main result of the paper. Moreover, six examples are provided to illustrate the proposed approach.
MSC:
93C30 Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)
93C65 Discrete event control/observation systems
93B50 Synthesis problems
Software:
HyTech; PHAVer; PPL
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Althoff, M.; Stursberg, O.; Buss, M., Computing reachable sets of hybrid systems using a combination of zonotopes and polytopes, Nonlinear Analysis: Hybrid Systems, 4, 2, 233-249 (2010) · Zbl 1201.93017
[2] Alur, R.; Henzinger, TA; Ho, P-H, Automatic symbolic verification of embedded systems, IEEE Trans Softw Eng, 22, 3, 181-201 (1996)
[3] Alur, R.; Henzinger, T.; Lafferriere, G.; Pappas, G., Discrete abstractions of hybrid systems, Proc IEEE, 88, 7, 971-984 (2000)
[4] Bagnara, R.; Hill, PM; Zaffanella, E., The Parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems, Sci Comput Program, 72, 1-2, 3-21 (2008)
[5] Chutinan A, Krogh BH (1998) Computing polyhedral approximations to flow pipes for dynamic systems. In: IEEE 37th international conference on decision and control, pp 2089-2094
[6] Clarke, E.; Fehnker, A.; Han, Z.; Krogh, B.; Ouaknine, J.; Stursberg, O.; Theobald, M., Abstraction and counterexample-guided refinement in model checking of hybrid systems, Int J Found Comput Sci, 14, 4, 583-604 (2003) · Zbl 1101.68678
[7] Frehse, G., PHAVEr: algorithmic verification of hybrid systems past HyTech, Int J Softw Tools Technol Transfer, 10, 3, 263-279 (2008)
[8] Gol, EA; Ding, X.; Lazar, M.; Belta, C., Finite bisimulations for switched linear systems, IEEE Trans Autom Control, 59, 12, 3122-3134 (2014) · Zbl 1360.93461
[9] Halbwachs, N.; Proy, Y-E; Roumanoff, P., Verification of real-time systems using linear relation analysis, Formal Methods in System Design, 11, 157-185 (1997)
[10] Henzinger TA (2000) The theory of hybrid automata. In: Inan MK, Kurshan RP (eds) Verification of digital and hybrid systems. NATO ASI Series (Series F: Computer and Systems Sciences), vol 170. Springer · Zbl 0959.68073
[11] Henzinger, TA; Horowitz, B.; Majumdar, R.; Wong-Toi, H., Beyond HyTech: Hybrid systems analysis using interval numerical methods. Hybrid Systems: Computation and Control, LNCS, 1790, 130-144 (2000) · Zbl 0938.93552
[12] Lafferriere, G.; Pappas, GJ; Sastry, S., O-minimal hybrid systems, Mathematics of Control, Signals and Systems, 13, 1, 1-21 (2000) · Zbl 1059.68073
[13] Liu, J.; Ozay, N., Finite abstractions with robustness margins for temporal logic-based control synthesis, Nonlinear Analysis: Hybrid Systems, 22, 1-15 (2016) · Zbl 1344.93046
[14] Maler, O.; Dang, T., Reachability analysis via face lifting. Hybrid Systems: Computation and Control, LNCS, 1386, 96-109 (1998)
[15] Mitchell, IM; Bayen, AM; Tomlin, CJ, A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games, IEEE Trans Autom Control, 50, 7, 947-957 (2005) · Zbl 1366.91022
[16] Moor, T.; Davoren, JM; Raisch, J., Learning by doing: systematic abstraction refinement for hybrid control synthesis, IEE Proceedings: Control Theory and Applications, 153, 5, 591-599 (2006)
[17] Moor T, Götz S (2018) Deterministic finite-automata abstractions of time-variant sequential behaviours. In: 14th Workshop on discrete event systems (WODES’18), p 399
[18] Moor, T.; Raisch, J., Supervisory control of hybrid systems within a behavioural framework, Syst Control Lett, 38, 3, 157-166 (1999) · Zbl 0948.93037
[19] Moor T, Raisch J (2002) Abstraction based supervisory controller synthesis for high order monotone continuous systems. Modelling, Analysis, and Design of Hybrid Systems, LNCIS 279, pp 247-265
[20] Moor, T.; Raisch, J.; O’Young, S., Discrete supervisory control of hybrid systems based on l-complete approximations, Discrete Event Dynamic Systems: Theory and Applications, 12, 1, 83-107 (2002) · Zbl 1002.93016
[21] Park, SJ; Raisch, J., Supervisory control of hybrid systems under partial observation based on l-complete approximations, IEEE Trans Autom Control, 60, 5, 1404-1409 (2015) · Zbl 1360.93435
[22] Pola, G.; Tabuada, P., Symbolic models for nonlinear control systems: alternating approximate bisimulations, SIAM J Control Optim, 48, 2, 719-733 (2009) · Zbl 1194.93020
[23] Ramadge, PJ; Wonham, WM, Supervisory control of a class of discrete event systems, SIAM J Control Optim, 25, 1, 206-230 (1987) · Zbl 0618.93033
[24] Ramadge, PJ; Wonham, WM, The control of discrete event systems, Proc IEEE, 77, 1, 81-98 (1989)
[25] Reissig, G., Computing abstractions of nonlinear systems, IEEE Trans Autom Control, 56, 11, 2583-2598 (2011) · Zbl 1368.93178
[26] Reissig, G.; Weber, A.; Rungger, M., Feedback refinement relations for the synthesis of symbolic controllers, IEEE Trans Autom Control, 62, 4, 1781-1796 (2017) · Zbl 1366.93363
[27] Schmuck, AK; Raisch, J., Asynchronous l-complete approximations, Syst Control Lett, 73, 67-75 (2014) · Zbl 1297.93044
[28] Schmuck AK, Tabuada P, Raisch J (2015) Comparing asynchronous l-complete approximations and quotient based abstractions. In: IEEE 54th international conference on decision and control, pp 6823-6829
[29] Stiver, JA; Antsaklis, PJ; Lemmon, MD, Interface and controller design for hybrid systems, Hybrid Systems II. LNCS, 999, 462-492 (1995)
[30] Stursberg, O., Supervisory control of hybrid systems based on model abstraction and guided search, Nonlinear Anal Theory Methods Appl, 65, 6, 1168-1187 (2006) · Zbl 1121.93046
[31] Tabuada, P., Verification and control of hybrid systems: a symbolic approach (2009), New York: Springer, New York · Zbl 1195.93001
[32] Thistle JG, Wonham WM (1994a) Control of infinite behavior of finite automata. SIAM J Control Opt 32(4):1075-1097 · Zbl 0925.93233
[33] Thistle JG, Wonham WM (1994b) Supervision of infinite behavior of discrete event systems. SIAM J Control Optim 32(4):1098-1113 · Zbl 0925.93234
[34] Willems, JC, Paradigms and puzzles in the theory of dynamic systems, IEEE Trans Autom Control, 36, 3, 258-294 (1991) · Zbl 0737.93004
[35] Yang JM, Moor T, Raisch J (2018) Local refinement of l-complete approximations for supervisory control of hybrid systems. In: 14th Workshop on discrete event systems (WODES’18), p 496
[36] Zamani, M.; Pola, G.; Mazo, M.; Tabuada, P., Symbolic models for nonlinear control systems without stability assumptions, IEEE Trans Autom Control, 57, 7, 1804-1809 (2012) · Zbl 1369.93002
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.