×

Symbolic models for stochastic switched systems: A discretization and a discretization-free approach. (English) Zbl 1377.93156

Summary: Stochastic switched systems are a relevant class of stochastic hybrid systems with probabilistic evolution over a continuous domain and control-dependent discrete dynamics over a finite set of modes. In the past few years several different techniques have been developed to assist in the stability analysis of stochastic switched systems. However, more complex and challenging objectives related to the verification of and the controller synthesis for logic specifications have not been formally investigated for this class of systems as of yet. With logic specifications we mean properties expressed as formulae in linear temporal logic or as automata on infinite strings. This paper addresses these complex objectives by constructively deriving approximately equivalent (bisimilar) symbolic models of stochastic switched systems. More precisely, this paper provides two different symbolic abstraction techniques: one requires state space discretization, but the other one does not require any space discretization which can be potentially more efficient than the first one when dealing with higher dimensional stochastic switched systems. Both techniques provide finite symbolic models that are approximately bisimilar to stochastic switched systems under some stability assumptions on the concrete model. This allows formally synthesizing controllers (switching signals) that are valid for the concrete system over the finite symbolic model, by means of mature automata-theoretic techniques in the literature. The effectiveness of the results are illustrated by synthesizing switching signals enforcing logic specifications for two case studies including temperature control of a six-room building.

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)
93B17 Transformations
93B50 Synthesis problems

Software:

CoSyma
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Abate, A. (2009). A contractivity approach for probabilistic bisimulations of diffusion processes. In Proceedings of 48th IEEE conference on decision and control, December; Abate, A. (2009). A contractivity approach for probabilistic bisimulations of diffusion processes. In Proceedings of 48th IEEE conference on decision and control, December
[2] Abate, A.; Amin, S.; Prandini, M.; Lygeros, J.; Sastry, S., Computational approaches to reachability analysis of stochastic hybrid systems, (Proceedings of the 10th international conference on hybrid systems: computation and control. Proceedings of the 10th international conference on hybrid systems: computation and control, HSCC’07 (2007), Springer-Verlag: Springer-Verlag Berlin, Heidelberg), 4-17 · Zbl 1221.93030
[3] Abate, A.; D’Innocenzo, A.; Di Benedetto, M. D., Approximate abstractions of stochastic hybrid systems, IEEE Transactions on Automatic Control, 56, 11, 2688-2694 (2011) · Zbl 1368.93655
[4] Alur, R.; Henzinger, T.; Lafferriere, G.; Pappas, G. J., Discrete abstractions of hybrid systems, Proceedings of the IEEE, 88, 7, 971-984 (2000)
[5] Angeli, D., A Lyapunov approach to incremental stability properties, IEEE Transactions on Automatic Control, 47, 3, 410-421 (2002) · Zbl 1364.93552
[6] Azuma, S. I., & Pappas, G. J. (2010). Discrete abstraction of stochastic nonlinear systems: a bisimulation function approach. In Proceedings of American control conference, ACC, June; Azuma, S. I., & Pappas, G. J. (2010). Discrete abstraction of stochastic nonlinear systems: a bisimulation function approach. In Proceedings of American control conference, ACC, June
[7] Blom, H. A.P.; Lygeros, J., (Stochastic hybrid systems: theory and safety critical applications. Stochastic hybrid systems: theory and safety critical applications, Lecture notes in control and information sciences (LNCIS), Vol. 337 (2006), Springer-Verlag) · Zbl 1094.93003
[8] Bujorianu, M. L.; Lygeros, J.; Bujorianu, M. C., Hybrid systems: computation and control, (Bisimulation for general stochastic hybrid systems. Bisimulation for general stochastic hybrid systems, LNCS, Vol. 3414 (2005), Springer), 198-214 · Zbl 1078.93062
[9] Chatterjee, D.; Liberzon, D., Stability analysis of deterministic and stochastic switched systems via a comparison principle and multiple Lyapunov functions, SIAM Journal on Control and Optimization, 45, 1, 174-206 (2006) · Zbl 1132.93014
[10] Girard, A.; Pappas, G. J., Approximation metrics for discrete and continuous systems, IEEE Transactions on Automatic Control, 25, 5, 782-798 (2007) · Zbl 1366.93032
[11] Girard, A.; Pola, G.; Tabuada, P., Approximately bisimilar symbolic models for incrementally stable switched systems, IEEE Transactions on Automatic Control, 55, 1, 116-126 (2010) · Zbl 1368.93413
[12] Hoeffding, W., Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association, 58, 301, 13-30 (1963) · Zbl 0127.10602
[13] Julius, A. A.; Pappas, G. J., Approximations of stochastic hybrid systems, IEEE Transactions on Automatic Control, 54, 6, 1193-1203 (2009) · Zbl 1367.93618
[14] Karatzas, I.; Shreve, S. E., (Brownian motion and stochastic calculus. Brownian motion and stochastic calculus, Graduate texts in mathematics, Vol. 113 (1991), Springer-Verlag: Springer-Verlag New York) · Zbl 0734.60060
[15] Lafferriere, G.; Pappas, G. J.; Sastry, S., O-minimal hybrid systems, Mathematics of Control, Signals, and Systems, 13, 1, 1-21 (2000) · Zbl 1059.68073
[16] Le Corronc, E., Girard, A., & Goessler, G. (2013). Mode sequences as symbolic states in abstractions of incrementally stable switched systems. In Proceedings of the 52nd IEEE conference on decision and control, December; Le Corronc, E., Girard, A., & Goessler, G. (2013). Mode sequences as symbolic states in abstractions of incrementally stable switched systems. In Proceedings of the 52nd IEEE conference on decision and control, December
[17] Liberzon, D., (Switching in systems and control. Switching in systems and control, Systems & control: foundations & applications (2003), Birkhäuser) · Zbl 1036.93001
[18] Majumdar, R.; Zamani, M., Approximately bisimilar symbolic models for digital control systems, (Parthasarathy, M.; Seshia, S. A., Computer aided verification (CAV). Computer aided verification (CAV), LNCS, Vol. 7358 (2012), Springer-Verlag), 362-377
[19] Maler, O.; Pnueli, A.; Sifakis, J., On the synthesis of discrete controllers for timed systems, (Mayr, E. W.; Puech, C., Symposium on theoretical aspects of computer science. Symposium on theoretical aspects of computer science, LNCS, Vol. 900 (1995), Springer-Verlag), 229-242 · Zbl 1379.68227
[20] Mouelhi, A., Girard, A., & Goessler, G. (2013). CoSyMA: a tool for controller synthesis using multi-scale abstractions. In Proceedings of the 16th international conference on hybrid systems: computation and control, April; Mouelhi, A., Girard, A., & Goessler, G. (2013). CoSyMA: a tool for controller synthesis using multi-scale abstractions. In Proceedings of the 16th international conference on hybrid systems: computation and control, April
[21] Oksendal, B. K., Stochastic differential equations: an introduction with applications (2002), Springer
[22] Pola, G.; Girard, A.; Tabuada, P., Approximately bisimilar symbolic models for nonlinear control systems, Automatica, 44, 10, 2508-2516 (2008) · Zbl 1155.93322
[23] Pola, G.; Tabuada, P., Symbolic models for nonlinear control systems: alternating approximate bisimulations, SIAM Journal on Control and Optimization, 48, 2, 719-733 (2009) · Zbl 1194.93020
[24] Sproston, J. (2011). Discrete-time verification and control for probabilistic rectangular hybrid automata. In Proceedings of 8th international conference on quantitative evaluation of systems; Sproston, J. (2011). Discrete-time verification and control for probabilistic rectangular hybrid automata. In Proceedings of 8th international conference on quantitative evaluation of systems
[25] Tabuada, P., Verification and control of hybrid systems, a symbolic approach (2009), Springer · Zbl 1195.93001
[26] Zamani, M.; Abate, A., Symbolic control of stochastic switched systems via finite abstractions, (Joshi, K.; Siegle, M.; Stoelinga, M.; D’Argenio, P. R., Quantitative evaluation of systems. Quantitative evaluation of systems, Lecture notes in computer science, Vol. 8054 (2013), Springer: Springer Berlin, Heidelberg), 305-321
[27] Zamani, M.; Abate, A., Approximately bisimilar symbolic models for randomly switched stochastic systems, Systems & Control Letters, 69, 38-46 (2014) · Zbl 1288.93098
[28] Zamani, M.; Mohajerin Esfahani, P.; Majumdar, R.; Abate, A.; Lygeros, J., Symbolic control of stochastic systems via approximately bisimilar finite abstractions, IEEE Transactions on Automatic Control, 59, 12, 3135-3150 (2014) · Zbl 1360.93445
[29] Zamani, M.; Tkachev, I.; Abate, A., Bisimilar symbolic models for stochastic control systems without state-space discretization, (Proceedings of the 17th international conference on hybrid systems: computation and control (2014), ACM: ACM New York, NY, USA), 41-50 · Zbl 1362.93147
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.