Compositional synthesis of state-dependent switching control. (English) Zbl 1405.93098

Summary: We present a correct-by-design method of state-dependent control synthesis for sampled switching systems. Given a target region \(R\) of the state space, our method builds a capture set \(S\) and a control that steers any element of \(S\) into \(R\). The method works by iterated backward reachability from \(R\). The method is also used to synthesize a recurrence control that makes any state of \(R\) return to \(R\) infinitely often. We explain how the synthesis method can be performed in a compositional manner, and apply it to the synthesis of a compositional control of a concrete floor-heating system with 11 rooms and up to \(2^{11} = 2048\) switching modes.


93B50 Synthesis problems
93C30 Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)
93C55 Discrete-time control/observation systems
93B03 Attainable sets, reachability
93C95 Application models in control theory
93B35 Sensitivity (robustness)


Full Text: DOI


[1] Liberzon, D., Switching in Systems and Control, (2012), Springer Science & Business Media
[2] Asarin, E.; Bournez, O.; Dang, T.; Maler, O.; Pnueli, A., Effective synthesis of switching controllers for linear systems, Proc. IEEE, 88, 7, 1011-1025, (2000)
[3] Gillula, J. H.; Hoffmann, G. M.; Huang, H.; Vitus, M. P.; Tomlin, C., Applications of hybrid reachability analysis to robotic aerial vehicles, Int. J. Robot. Res., 30, 3, 335-354, (2011)
[4] Jaulin, L.; Kieffer, M.; Didrit, O.; Walter, E., Applied Interval Analysis with Examples in Parameter and State Estimation, Robust Control and Robotics, (2001), Springer-Verlag · Zbl 1023.65037
[5] Girard, A., Low-complexity switching controllers for safety using symbolic models, (Proceedings of 4th IFAC Conference on Analysis and Design of Hybrid Systems, (2012)), 82-87
[6] Alur, R.; Henzinger, T. A., Reactive modules, Form. Methods Syst. Des., 15, 1, 7-48, (1999)
[7] Bogomolov, S.; Frehse, G.; Greitschus, M.; Grosu, R.; Pasareanu, C. S.; Podelski, A.; Strump, T., Assume-guarantee abstraction refinement meets hybrid systems, (Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, Proceedings, HVC 2014, Haifa, Israel, November 18-20, 2014, (2014)), 116-131
[8] Dallal, E.; Tabuada, P., On compositional symbolic controller synthesis inspired by small-gain theorems, (54th IEEE Conference on Decision and Control, CDC 2015, Osaka, Japan, December 15-18, 2015, (2015), IEEE), 6133-6138
[9] Fribourg, L.; Kühne, U.; Markey, N., Game-based synthesis of distributed controllers for sampled switched systems, (2nd International Workshop on Synthesis of Complex Parameters, SynCoP’15, OpenAccess Series in Informatics (OASIcs), vol. 44, (2015), Dagstuhl: Dagstuhl Germany), 48-62
[10] Kim, E. S.; Arcak, M.; Seshia, S. A., Compositional controller synthesis for vehicular traffic networks, (54th IEEE Conference on Decision and Control, CDC 2015, Osaka, Japan, December 15-18, 2015, (2015)), 6165-6171
[11] Meyer, P.-J.; Girard, A.; Witrant, E., Safety control with performance guarantees of cooperative systems using compositional abstractions, IFAC-PapersOnLine, 48, 27, 317-322, (2015)
[12] Sangiovanni-Vincentelli, A. L.; Damm, W.; Passerone, R., Taming dr. Frankenstein: contract-based design for cyber-physical systems, Eur. J. Control, 18, 3, 217-238, (2012) · Zbl 1264.93152
[13] Smith, S. W.; Nilsson, P.; Ozay, N., Interdependence quantification for compositional control synthesis with an application in vehicle safety systems, (55th IEEE Conference on Decision and Control, CDC 2016, Las Vegas, NV, USA, December 12-14, 2016, (2016)), 5700-5707
[14] Larsen, K. G.; Mikučionis, M.; Muniz, M.; Srba, J.; Taankvist, J. H., Online and compositional learning of controllers with application to floor heating, (Tools and Algorithms for Construction and Analysis of Systems (TACAS), 22nd International Conference, (2016))
[15] Kühne, U.; Soulat, R., Minimator 1.0, (2015)
[16] L. Fribourg, U. Kühne, R. Soulat, Finite controlled invariants for sampled switched systems, Form. Methods Syst. Des. 45 (3). · Zbl 1303.93121
[17] Octave Web page
[18] Alexandre dit Sandretto, J.; Chapoutot, A., Dynibex library, (2015)
[19] dit Sandretto, J. A.; Chapoutot, A., Validated explicit and implicit Runge-Kutta methods, Reliab. Comput., 22, 79-103, (2016)
[20] Moore, R., Interval Analysis, (1966), Prentice Hall · Zbl 0176.13301
[21] Kühn, W., Zonotope dynamics in numerical quality control, (Hege, H.-C.; Polthier, K., Visualization and Mathematics, (1998), Springer Verlag: Springer Verlag Heidelberg), 125-134 · Zbl 0940.68152
[22] Girard, A., Reachability of uncertain linear systems using zonotopes, (Hybrid Systems: Computation and Control, 8th International Workshop, Proceedings, HSCC 2005, Zurich, Switzerland, March 9-11, 2005, (2005)), 291-305 · Zbl 1078.93005
[23] Althoff, M.; Stursberg, O.; Buss, M., Verification of uncertain embedded systems by computing reachable sets based on zonotopes, (Proc. of the 17th IFAC World Congress, (2008)), 5125-5130
[24] Meyer, P.-J., Invariance and Symbolic Control of Cooperative Systems for Temperature Regulation in Intelligent Buildings, (Sep. 2015), Université Grenoble Alpes, Thesis
[25] Meyer, P.-J.; Nazarpour, H.; Girard, A.; Witrant, E., Experimental implementation of UFAD regulation based on robust controlled invariance, (Proceedings of the 13th European Control Conference, (2014)), 1468-1473
[26] Khatib, M. A.; Girard, A.; Dang, T., Verification and synthesis of timing contracts for embedded controllers, (Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, April 12-14, 2016, (2016)), 115-124 · Zbl 1364.68257
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.