Symbolic Control of Stochastic Switched Systems via Finite Abstractions
Stochastic switched systems are a class of continuous-time dynamical models with probabilistic evolution over a continuous domain and control-dependent discrete dynamics over a finite set of modes. As such, they represent a subclass of general stochastic hybrid systems. While the literature has witnessed recent progress in the dynamical analysis and controller synthesis for the stability of stochastic switched systems, more complex and challenging objectives related to the verification of and the synthesis for logic specifications (properties expressed as formulas in linear temporal logic or as automata on infinite strings) have not been formally investigated as of yet. This paper addresses these complex objectives by constructively deriving approximately equivalent (bisimilar) symbolic models of stochastic switched systems. More precisely, a finite symbolic model that is approximately bisimilar to a stochastic switched system is constructed under some dynamical stability assumptions on the concrete model. This allows to formally synthesize controllers (switching signals) over the finite symbolic model that are valid for the concrete system, by means of mature techniques in the literature.
KeywordsLyapunov Function Linear Matrix Inequality Linear Temporal Logic Switching Signal Symbolic Model
Unable to display preview. Download preview PDF.
- 1.Abate, A.: A contractivity approach for probabilistic bisimulations of diffusion processes. In: Proceedings of 48th IEEE Conference on Decision and Control, pp. 2230–2235 (December 2009)Google Scholar
- 7.Girard, A.: Low-complexity switching controllers for safety using symbolic models. In: Proceedings of 4th IFAC Conference on Analysis and Design of Hybrid Systems, pp. 82–87 (2012)Google Scholar
- 12.Liberzon, D.: Switching in Systems and Control. Systems & Control: Foundations & Applications. Birkhäuser (2003)Google Scholar
- 16.Milner, R.: Communication and Concurrency. Prentice-Hall, Inc. (1989)Google Scholar
- 17.Oksendal, B.K.: Stochastic differential equations: An introduction with applications, 5th edn. Springer (November 2002)Google Scholar
- 19.Prajna, S., Papachristodoulou, A., Seiler, P., Parrilo, P.A.: SOSTOOLS: Control applications and new developments. In: Proceedings of IEEE International Symposium on Computer Aided Control Systems Design, pp. 315–320 (2004)Google Scholar
- 20.Sproston, J.: Discrete-time verification and control for probabilistic rectangular hybrid automata. In: Proceedings of 8th International Conference on Quantitative Evaluation of Systems, pp. 79–88 (2011)Google Scholar
- 21.Tabuada, P.: Verification and Control of Hybrid Systems, A symbolic approach, 1st edn. Springer (June 2009)Google Scholar
- 22.Zamani, M., Mohajerin Esfahani, P., Majumdar, R., Abate, A., Lygeros, J.: Symbolic control of stochastic systems via approximately bisimilar finite abstractions. arXiv: 1302.3868 (2013)Google Scholar