Advertisement

Symbolic Control of Stochastic Switched Systems via Finite Abstractions

  • Majid Zamani
  • Alessandro Abate
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8054)

Abstract

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.

Keywords

Lyapunov Function Linear Matrix Inequality Linear Temporal Logic Switching Signal Symbolic Model 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    Angeli, D.: A Lyapunov approach to incremental stability properties. IEEE Transactions on Automatic Control 47(3), 410–421 (2002)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Blom, H.A.P., Lygeros, J.: Stochastic Hybrid Systems: Theory and Safety Critical Applications. LNCIS, vol. 337. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Bujorianu, M.L., Lygeros, J., Bujorianu, M.C.: Bisimulation for General Stochastic Hybrid Systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 198–214. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    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)MathSciNetzbMATHCrossRefGoogle Scholar
  7. 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
  8. 8.
    Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. IEEE Transactions on Automatic Control 25(5), 782–798 (2007)MathSciNetCrossRefGoogle Scholar
  9. 9.
    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)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Julius, A.A., Pappas, G.J.: Approximations of stochastic hybrid systems. IEEE Transaction on Automatic Control 54(6), 1193–1203 (2009)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Karatzas, I., Shreve, S.E.: Brownian Motion and Stochastic Calculus, 2nd edn. Graduate Texts in Mathematics, vol. 113. Springer, New York (1991)zbMATHGoogle Scholar
  12. 12.
    Liberzon, D.: Switching in Systems and Control. Systems & Control: Foundations & Applications. Birkhäuser (2003)Google Scholar
  13. 13.
    Majumdar, R., Zamani, M.: Approximately bisimilar symbolic models for digital control systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 362–377. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  14. 14.
    Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 229–242. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  15. 15.
    Mazo Jr., M., Davitian, A., Tabuada, P.: PESSOA: A tool for embedded controller synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 566–569. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  16. 16.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Inc. (1989)Google Scholar
  17. 17.
    Oksendal, B.K.: Stochastic differential equations: An introduction with applications, 5th edn. Springer (November 2002)Google Scholar
  18. 18.
    Pola, G., Tabuada, P.: Symbolic models for nonlinear control systems: Alternating approximate bisimulations. SIAM Journal on Control and Optimization 48(2), 719–733 (2009)MathSciNetzbMATHCrossRefGoogle Scholar
  19. 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. 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. 21.
    Tabuada, P.: Verification and Control of Hybrid Systems, A symbolic approach, 1st edn. Springer (June 2009)Google Scholar
  22. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Majid Zamani
    • 1
  • Alessandro Abate
    • 1
  1. 1.Delft Center for Systems and ControlDelft University of TechnologyThe Netherlands

Personalised recommendations