×

Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems. (English) Zbl 1455.93190

Summary: In this paper, we propose a compositional framework for the construction of discrete-time finite abstractions, also known as finite Markov decision processes, from continuous-time stochastic hybrid systems by quantifying the distance between their outputs in a probabilistic setting. The proposed scheme is based on the notion of stochastic simulation functions, which is used to relate continuous-time stochastic systems with their discrete-time counterparts. Accordingly, one can employ discrete-time abstract systems as substitutions of the continuous-time ones in the controller design process with guaranteed error bounds on their output trajectories. To this end, we first derive sufficient small-gain type conditions for the compositional quantification of the probabilistic distance between the interconnection of original continuous-time stochastic hybrid systems and their discrete-time (finite or infinite) abstractions. We then construct finite abstractions together with their corresponding stochastic simulation functions for a particular class of nonlinear stochastic hybrid systems having some stability property. We illustrate the effectiveness of the proposed results by applying our approaches to the temperature regulation in a circular building and constructing compositionally a discrete-time abstraction from its original continuous-time dynamics in a network containing 1000 rooms. We employ the constructed discrete-time abstractions as substitutes to compositionally synthesize policies regulating the temperature of each room for a bounded time horizon.

MSC:

93E03 Stochastic systems in control theory (general)
93C30 Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)
93C55 Discrete-time control/observation systems
93C10 Nonlinear systems in control theory
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Abate, A.; Prandini, M.; Lygeros, J.; Sastry, S., Probabilistic reachability and safety for controlled discrete-time stochastic hybrid systems, Automatica, 44, 11, 2724-2734 (2008) · Zbl 1152.93051
[2] Baier, C.; Katoen, J.-P.; Larsen, K. G., Principles of Model Checking (2008), MIT press · Zbl 1179.68076
[3] Bertsekas, D. P.; Shreve, S. E., Stochastic Optimal Control: The Discrete-Time Case (1996), Athena Scientific
[4] Cauchi, N.; Abate, A., StocHy: Automated verification and synthesis of stochastic processes, Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 247-264 (2019), Springer · Zbl 07120162
[5] Dashkovskiy, S.; Rüffer, B. S.; Wirth, F. R., An ISS small gain theorem for general networks, Math. Control, Signals, Syst. (MCSS), 19, 2, 93-122 (2007) · Zbl 1125.93062
[6] Dashkovskiy, S. N.; Rüffer, B. S.; Wirth, F. R., Small gain theorems for large scale systems and construction of ISS Lyapunov functions, SIAM J. Control Opt., 48, 6, 4089-4118 (2010) · Zbl 1202.93008
[7] Dynkin, E. B., Markov Processes, 77-104 (1965), Springer
[8] Gielen, R. H.; Hermans, R. M.; Lazar, M.; Teel, A. R., On the application of the small-gain theorem to the stability analysis of large-scale power systems with delay, Proceedings of the American Control Conference (ACC), 1476-1481 (2012)
[9] Girard, A.; Pappas, G. J., Hierarchical control system design using approximate simulation, Automatica, 45, 2, 566-571 (2009) · Zbl 1158.93301
[10] Girard, A.; Pola, G.; Tabuada, P., Approximately bisimilar symbolic models for incrementally stable switched systems, IEEE Trans. Autom. Control, 55, 1, 116-126 (2009) · Zbl 1368.93413
[11] Girard, A.; Gössler, G.; Mouelhi, S., Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models, IEEE Trans. Autom. Control, 61, 6, 1537-1549 (2016) · Zbl 1359.93350
[12] Goedel, R.; Sanfelice, R. G.; Teel, A. R., Hybrid dynamical systems: modeling stability, and robustness (2012), Princeton University Press: Princeton University Press Princeton, NJ · Zbl 1241.93002
[13] Gronwall, T. H., Note on the derivatives with respect to a parameter of the solutions of a system of differential equations, Ann. Math., 292-296 (1919) · JFM 47.0399.02
[14] Haesaert, S.; Soudjani, S.; Abate, A., Verification of general Markov decision processes by approximate similarity relations and policy refinement, SIAM J. Control Opt., 55, 4, 2333-2367 (2017) · Zbl 1367.93615
[15] Haesaert, S.; Soudjani, S.; Abate, A., Verification of general Markov decision processes by approximate similarity relations and policy refinement, SIAM Journal on Control and Optimization, 55, 2333-2367 (2017) · Zbl 1367.93615
[16] Julius, A. A.; Pappas, G. J., Approximations of stochastic hybrid systems, IEEE Trans. Autom. Control, 54, 6, 1193-1203 (2009) · Zbl 1367.93618
[17] Kamgarpour, M.; Summers, S.; Lygeros, J., Control design for specifications on stochastic hybrid systems, Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control. Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, HSCC ’13, 303-312 (2013), ACM: ACM New York, NY, USA · Zbl 1364.93263
[18] Laurenti, L.; Abate, A.; Bortolussi, L.; Cardelli, L.; Ceska, M.; Kwiatkowska, M., Reachability computation for switching diffusions: finite abstractions with certifiable and tuneable precision, Proceedings of the 20th ACM International Conference on Hybrid Systems: Computation and Control, 55-64 (2017) · Zbl 1369.93728
[19] Lavaei, A.; Soudjani, S.; Majumdar, R.; Zamani, M., Compositional abstractions of interconnected discrete-time stochastic control systems, Proceedings of the 56th IEEE Conference on Decision and Control, 3551-3556 (2017)
[20] Lavaei, A.; Soudjani, S.; Zamani, M., From dissipativity theory to compositional construction of finite Markov decision processes, Proceedings of the 21st ACM International Conference on Hybrid Systems: Computation and Control, 21-30 (2018) · Zbl 1422.90067
[21] A. Lavaei, S. Soudjani, M. Zamani, Compositional abstraction-based synthesis of general MDPs via approximate probabilistic relations, Nonlinear Anal. Hybrid Syst. arXiv:1906.02930 (2019). · Zbl 1429.93139
[22] Liberzon, D.; Nešić, D.; Teel, A. R., Small-gain theorems of lasalle type for hybrid systems, Proceedings of the 51st IEEE Conference on Decision and Control (CDC), 6825-6830 (2012)
[23] Liberzon, D.; Nešić, D.; Teel, A. R., Lyapunov-based small-gain theorems for hybrid systems, IEEE Trans. Autom. Control, 59, 6, 1395-1410 (2014) · Zbl 1360.93639
[24] Mallik, K.; Soudjani, S.; Schmuck, A.; Majumdar, R., Compositional construction of finite state abstractions for stochastic control systems, 2017 IEEE 56th Annual Conference on Decision and Control (CDC), 550-557 (2017)
[25] Nejati, A.; Soudjani, S.; Zamani, M., Abstraction-based synthesis of continuous-time stochastic control systems, Proceedings of the 18th European Control Conference, 3212-3217 (2019)
[26] Øksendal, B. K.; Sulem, A., Applied Stochastic Control of Jump Diffusions, 498 (2005), Springer · Zbl 1074.93009
[27] A. Papachristodoulou, J. Anderson, G. Valmorbida, S. Prajna, P. Seiler, P. Parrilo, SOSTOOLS version 3.00 sum of squares optimization toolbox for MATLAB, arXiv:1310.4716 (2013).
[28] Pnueli, A., The temporal logic of programs, Proceedings of the 18th IEEE Annual Symposium on Foundations of Computer Science, 46-57 (1977)
[29] Pola, G.; Girard, A.; Tabuada, P., Approximately bisimilar symbolic models for nonlinear control systems, Automatica, 44, 10, 2508-2516 (2008) · Zbl 1155.93322
[30] Rüffer, B. S., Monotone inequalities, dynamical systems, and paths in the positive orthant of Euclidean n-space, Positivity, 14, 2, 257-283 (2010) · Zbl 1211.47091
[31] Rungger, M.; Zamani, M., SCOTS: a tool for the synthesis of symbolic controllers, Proceedings of the 19th ACM International Conference on Hybrid Systems: Computation and Control, 99-104 (2016) · Zbl 1364.93267
[32] Soudjani, S.; Abate, A., Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes, SIAM J. Appl. Dyn. Syst., 12, 2, 921-956 (2013) · Zbl 1278.93243
[33] Soudjani, S., Formal Abstractions for Automated Verification and Synthesis of Stochastic Systems (2014), Technische Universiteit Delft: Technische Universiteit Delft The Netherlands, Ph.D. thesis
[34] Soudjani, S.; Abate, A.; Majumdar, R., Dynamic Bayesian networks as formal abstractions of structured stochastic processes, Proceedings of the 26th International Conference on Concurrency Theory, 1-14 (2015)
[35] Soudjani, S.; Gevaerts, C.; Abate, A., \( \textsf{FAUST}{}^2\): Formal abstractions of uncountable-state stochastic processes, TACAS’15. TACAS’15, Lecture Notes in Computer Science, 9035, 272-286 (2015), Springer
[36] Soudjani, S.; Abate, A.; Majumdar, R., Dynamic Bayesian networks for formal verification of structured stochastic processes, Acta Inform., 54, 2, 217-242 (2017) · Zbl 1364.68262
[37] Swikir, A.; Girard, A.; Zamani, M., From dissipativity theory to compositional synthesis of symbolic models, Proceedings of the 4th Indian Control Conference (ICC), 30-35 (2018)
[38] Tkachev, I.; Mereacre, A.; Katoen, J.-P.; Abate, A., Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems, Proceedings of the 16th ACM International Conference on Hybrid Systems: Computation and Control, 293-302 (2013) · Zbl 1362.68189
[39] Tolić, D.; Sanfelice, R. G.; Fierro, R., Self-triggering in nonlinear systems: a small gain theorem approach, Proceedings of the 20th Mediterranean Conference on Control & Automation (MED), 941-947 (2012)
[40] Tolic, D.; Sanfelice, R. G.; Fierro, R., Input-output triggered control via the small gain theorem and switched systems modeling, Int. J. Robust Nonlinear Control, 1-27 (2014)
[41] Young, W. H., On classes of summable functions and their Fourier series, Proc. R. Soc. Lond. A: Math., Phys. Eng. Sci., 87, 594, 225-229 (1912) · JFM 43.1114.12
[42] 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 (2011) · Zbl 1369.93002
[43] Zamani, M.; Abate, A., Approximately bisimilar symbolic models for randomly switched stochastic systems, Syst. Control Lett., 69, 38-46 (2014) · Zbl 1288.93098
[44] Zamani, M.; Mohajerin Esfahani, P.; Majumdar, R.; Abate, A.; Lygeros, J., Symbolic control of stochastic systems via approximately bisimilar finite abstractions, IEEE Trans. Autom. Control, 59, 12, 3135-3150 (2014) · Zbl 1360.93445
[45] Zamani, M.; Abate, A.; Girard, A., Symbolic models for stochastic switched systems: a discretization and a discretization-free approach, Automatica, 55, 183-196 (2015) · Zbl 1377.93156
[46] Zamani, M.; Rungger, M.; Mohajerin Esfahani, P., Approximations of stochastic hybrid systems: a compositional approach, IEEE Trans. Autom. Control, 62, 6, 2838-2853 (2017) · Zbl 1369.60045
[47] Lavaei, A.; Soudjani, S.; Zamani, M., Compositional construction of infinite abstractions for networks of stochastic control systems, Automatica., 107, 125-137 (2019) · Zbl 1429.93139
[48] Lavaei, A.; Soudjani, S.; Zamani, M., Compositional abstraction-based synthesis for networks of stochastic switched systems, Automatica., 114 (2020) · Zbl 1441.93322
[49] Lavaei, A.; Zamani, M., Compositional construction of finite MDPs for large-scale stochastic switched systems: A dissipativity approach, Proceedings of the 15th IFAC Symposium on Large Scale Complex Systems: Theory and Applications, 52 (3), 31-36 (2019)
[50] Lavaei, A.; Soudjani, S.; Zamani, M., Compositional synthesis of finite abstractions for continuous-space stochastic control systems: A small-gain approach, Proceedings of the 6th IFAC Conference on Analysis and Design of Hybrid Systems, 51, 265-270 (2018)
[51] Lavaei, A.; Soudjani, S.; Zamani, M., Compositional (in)finite abstractions for large-scale interconnected stochastic systems, IEEE Trans. Autom. Control (2020)
[52] Lavaei, A., Automated Verification and Control of Large-Scale Stochastic Cyber-Physical Systems: Compositional Techniques (2019), Universität München: Universität München Germany, PhD thesis
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.