×

Compositional abstraction of large-scale stochastic systems: a relaxed dissipativity approach. (English) Zbl 1441.93293

Summary: In this paper, we propose a compositional approach for the construction of finite abstractions (a.k.a. finite Markov decision processes (MDPs)) for networks of discrete-time stochastic control subsystems that are not necessarily stabilizable. The proposed approach leverages the interconnection topology and a notion of finite-step stochastic storage functions, that describes joint dissipativity-type properties of subsystems and their abstractions, and establishes a finite-step stochastic simulation function as a relation between the network and its abstraction. To this end, we first develop a new type of compositionality conditions which is less conservative than the existing ones. In particular, using a relaxation via a finite-step stochastic simulation function, it is possible to construct finite abstractions such that stabilizability of each subsystem is not necessarily required. We then propose an approach to construct finite MDPs together with their corresponding finite-step storage functions for general discrete-time stochastic control systems satisfying an incremental passivability property. We also construct finite MDPs for a particular class of nonlinear stochastic control systems. To demonstrate the effectiveness of the proposed results, we first apply our approach to an interconnected system composed of 4 subsystems such that 2 of them are not stabilizable. We then consider a road traffic network in a circular cascade ring composed of 50 cells, and construct compositionally a finite MDP of the network. We employ the constructed finite abstractions as substitutes to compositionally synthesize policies keeping the density of the traffic lower than 20 vehicles per cell. Finally, we apply our proposed technique to a fully interconnected network of 500 nonlinear subsystems and construct their finite MDPs with guaranteed error bounds on the probabilistic distance between their output trajectories.

MSC:

93E03 Stochastic systems in control theory (general)
93A15 Large-scale systems
93C55 Discrete-time control/observation systems
90C40 Markov and semi-Markov decision processes

Software:

FAUST2

References:

[1] Baier, C.; Katoen, J., Principles of Model Checking (2008), MIT press · Zbl 1179.68076
[2] Larsen, K. G.; Skou, A., Bisimulation through probabilistic testing, Inform. and Comput., 94, 1, 1-28 (1991) · Zbl 0756.68035
[3] Segala, R.; Lynch, N., Probabilistic simulations for probabilistic processes, Nordic J. Comput., 2, 2, 250-273 (1995) · Zbl 0839.68067
[4] J. Desharnais, F. Laviolette, M. Tracol, Approximate analysis of probabilistic processes: logic, simulation and games, in: Proceedings of the 5th International Conference on Quantitative Evaluation of System, 2008, pp. 264-273.
[5] A. D’Innocenzo, A. Abate, J. Katoen, Robust PCTL model checking, in: Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, 2012, pp. 275-286. · Zbl 1361.68140
[6] Hahn, E. M.; Hartmanns, A.; Hermanns, H.; Katoen, J.-P., A compositional modelling and analysis framework for stochastic hybrid systems, Form. Methods Syst. Des., 43, 2, 191-232 (2013) · Zbl 1291.68293
[7] N. Basset, M. Kwiatkowska, C. Wiltsche, Compositional controller synthesis for stochastic games, in: Proceedings of the International Conference on Concurrency Theory, 2014, pp. 173-187. · Zbl 1421.93053
[8] Kwiatkowska, M.; Norman, G.; Parker, D.; Qu, H., Compositional probabilistic verification through multi-objective model checking, Inform. and Comput., 232, 38-65 (2013) · Zbl 1277.68138
[9] Zamani, M.; Abate, A., Approximately bisimilar symbolic models for randomly switched stochastic systems, Systems Control Lett., 69, 38-46 (2014) · Zbl 1288.93098
[10] 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
[11] Zamani, M.; Mohajerin Esfahani, P.; Majumdar, R.; Abate, A.; Lygeros, J., Symbolic control of stochastic systems via approximately bisimilar finite abstractions, IEEE Trans. Automat. Control, 59, 12, 3135-3150 (2014) · Zbl 1360.93445
[12] Julius, A. A.; Pappas, G. J., Approximations of stochastic hybrid systems, IEEE Trans. Automat. Control, 54, 6, 1193-1203 (2009) · Zbl 1367.93618
[13] Zamani, M.; Rungger, M.; Mohajerin Esfahani, P., Approximations of stochastic hybrid systems: a compositional approach, IEEE Trans. Automat. Control, 62, 6, 2838-2853 (2017) · Zbl 1369.60045
[14] 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
[15] 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
[16] I. Tkachev, A. Mereacre, J. Katoen, A. Abate, Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems, in: Proceedings of the 16th ACM International Conference on Hybrid Systems: Computation and Control, 2013, pp. 293-302. · Zbl 1362.68189
[17] I. Tkachev, A. Abate, On infinite-horizon probabilistic properties and stochastic bisimulation functions, in: Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference, CDC-ECC, 2011, pp. 526-531.
[18] 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
[19] A. Lavaei, S. Soudjani, M. Zamani, Compositional synthesis of finite abstractions for continuous-space stochastic control systems: A small-gain approach, in: Proceedings of the 6th IFAC Conference on Analysis and Design of Hybrid Systems, vol. 51, no. 16, 2018, pp. 265-270.
[20] A. Lavaei, S. Soudjani, R. Majumdar, M. Zamani, Compositional abstractions of interconnected discrete-time stochastic control systems, in: Proceedings of the 56th IEEE Conference on Decision and Control, 2017, pp. 3551-3556.
[21] 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
[22] Lavaei, A.; Soudjani, S.; Zamani, M., Compositional (in)finite abstractions for large-scale interconnected stochastic systems, IEEE Transactions on Automatic Control, to appear as a full paper, arXiv: 1808.00893 (2020) · Zbl 1536.93850
[23] Lavaei, A.; Soudjani, S.; Zamani, M., Approximate probabilistic relations for compositional synthesis of stochastic systems, Proceedings of the Numerical Software Verification, 101-109 (2019), Lecture Notes in Computer Science 11652
[24] Lavaei, A.; Soudjani, S.; Zamani, M., Compositional abstraction-based synthesis of general MDPs via approximate probabilistic relations, arXiv:1906.02930 (2019)
[25] Lavaei, A.; Soudjani, S.; Zamani, M., Compositional abstraction-based synthesis for networks of stochastic switched systems, Automatica, 114 (2020) · Zbl 1441.93322
[26] 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)
[27] Lavaei, A.; Soudjani, S.; Zamani, M., Compositional synthesis of not necessarily stabilizable stochastic systems via finite abstractions, Proceedings of the 18th European Control Conference, 2802-2807 (2019)
[28] Lavaei, A.; Zamani, M., Compositional verification of large-scale stochastic systems via relaxed small-gain conditions, Proceedings of the 58th IEEE Conference on Decision and Control (2020)
[29] Nejati, A.; Soudjani, S.; Zamani, M., Abstraction-based synthesis of continuous-time stochastic control systems, Proceedings of the 18th Eorupean Control Conference, 3212-3217 (2019)
[30] Aeyels, D.; Peuteman, J., A new asymptotic stability criterion for nonlinear time-variant differential equations, IEEE Trans. Autom. Control, 43, 7, 968-971 (1998) · Zbl 0982.34044
[31] R.H. Gielen, M. Lazar, Non-conservative dissipativity and small-gain conditions for stability analysis of interconnected systems, in: Proceedings of the 51st IEEE Conference on Decision and Control, CDC, 2012, pp. 4187-4192.
[32] N. Noroozi, B.S. Rüffer, Non-conservative dissipativity and small-gain theory for ISS networks, in: Proceedings of the 53rd IEEE Conference on Decision and Control, 2014, pp. 3131-3136.
[33] Gielen, R. H.; Lazar, M., On stability analysis methods for large-scale discrete-time systems, Automatica, 55, 66-72 (2015) · Zbl 1378.93092
[34] Noroozi, N.; Geiselhart, R.; Grüne, L.; Rüffer, B. S.; Wirth, F. R., Nonconservative discrete-time ISS small-gain conditions for closed sets, IEEE Trans. Automat. Control, 63, 5, 1231-1242 (2018) · Zbl 1395.93506
[35] N. Noroozi, A. Swikir, F.R. Wirth, M. Zamani, Compositional construction of abstractions via relaxed small-gain conditions Part II: discrete case, in: 2018 European Control Conference, ECC, 2018, pp. 1-4.
[36] A. Lavaei, S. Soudjani, M. Zamani, From dissipativity theory to compositional construction of finite Markov decision processes, in: Proceedings of the 21st ACM International Conference on Hybrid Systems: Computation and Control, 2018, pp. 21-30. · Zbl 1422.90067
[37] Bertsekas, D. P.; Shreve, S. E., Stochastic Optimal Control: The Discrete-Time Case (1996), Athena Scientific
[38] Haesaert, S.; Soudjani, S.; Abate, A., Verification of general Markov decision processes by approximate similarity relations and policy refinement, SIAM J. Control Optim., 55, 4, 2333-2367 (2017) · Zbl 1367.93615
[39] Haesaert, S.; Soudjani, S., Robust dynamic programming for temporal logic control of stochastic systems, CoRR, abs/1811.11445 (2018)
[40] Soudjani, S.; Abate, A., Quantitative approximation of the probability distribution of a Markov process by formal abstractions, Log. Methods Comput. Sci., 11, 3 (2015) · Zbl 1342.60120
[41] Geiselhart, R.; Gielen, R. H.; Lazar, M.; Wirth, F. R., An alternative converse Lyapunov theorem for discrete-time systems, Systems Control Lett., 70, 49-59 (2014) · Zbl 1290.93149
[42] Arcak, M.; Meissen, C.; Packard, A., (Networks of Dissipative Systems. Networks of Dissipative Systems, SpringerBriefs in Electrical and Computer Engineering (2016), Springer) · Zbl 1343.93001
[43] Angeli, D., A Lyapunov approach to incremental stability properties, IEEE Trans. Automat. Control, 47, 3, 410-421 (2002) · Zbl 1364.93552
[44] Pham, Q. C.; Tabareau, N.; Slotine, J. J., A contraction theory approach to stochastic incremental stability, IEEE Trans. Automat. Control, 54, 4, 816-820 (2009) · Zbl 1367.60073
[45] Soudjani, S.; Gevaerts, C.; Abate, A., \( \text{FAUST}^{\text{2}} \): formal abstractions of uncountable-state stochastic processes, (TACAS’15. TACAS’15, Lecture Notes in Computer Science, vol. 9035 (2015), Springer), 272-286
[46] E. Le Corronc, A. Girard, G. Goessler, Mode sequences as symbolic states in abstractions of incrementally stable switched systems, in: Proceedings of the 52th IEEE Conference on Decision and Control, 2013, pp. 3225-3230.
[47] Bell, H. E., Gershgorin’s theorem and the zeros of polynomials, Amer. Math. Monthly, 72, 3, 292-295 (1965) · Zbl 0134.02003
[48] M. Kamgarpour, J. Ding, S. Summers, A. Abate, J. Lygeros, C. Tomlin, Discrete time stochastic hybrid dynamical games: verification & controller synthesis, in: Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference, 2011, pp. 6122-6127.
[49] T.A. Henzinger, S. Qadeer, S.K. Rajamani, You assume, we guarantee: Methodology and case studies, in: International Conference on Computer Aided Verification, 1998, pp. 440-451.
[50] A. Saoud, A. Girard, L. Fribourg, On the composition of discrete and continuous-time assume-guarantee contracts for invariance, in: 2018 European Control Conference, ECC, 2018, pp. 435-440.
[51] Godsil, C.; Royle, G., (Algebraic Graph Theory. Algebraic Graph Theory, Graduate Texts in Mathematics (2001), Springer, New York) · Zbl 0968.05002
[52] Young, W. H., On classes of summable functions and their fourier series, Proc. R. Soc. Lond. Ser. A Math. Phys. Eng. Sci., 87, 594, 225-229 (1912) · JFM 43.0334.09
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.