Document Open Access Logo

From Dissipativity Theory to Compositional Construction of Control Barrier Certificates

Authors Ameneh Nejati , Majid Zamani

PDF
Thumbnail PDF

File

LITES.8.2.6.pdf
  • Filesize: 2.02 MB
  • 17 pages

Document Identifiers

Author Details

Ameneh Nejati
  • Department of Electrical Engineering, Technical University of Munich, Germany
  • Department of Computer Science, LMU Munich, Germany
Majid Zamani
  • Department of Computer Science, University of Colorado Boulder, USA
  • Department of Computer Science, LMU Munich, Germany

Cite AsGet BibTex

Ameneh Nejati and Majid Zamani. From Dissipativity Theory to Compositional Construction of Control Barrier Certificates. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 06:1-06:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LITES.8.2.6

Abstract

This paper proposes a compositional framework based on dissipativity approaches to construct control barrier certificates for networks of continuous-time stochastic hybrid systems. The proposed scheme leverages the structure of the interconnection topology and a notion of so-called control storage certificates to construct control barrier certificates compositionally. By utilizing those certificates, one can compositionally synthesize state-feedback controllers for interconnected systems enforcing safety specifications over a finite-time horizon. In particular, we leverage dissipativity-type compositionality conditions to construct control barrier certificates for interconnected systems based on corresponding control storage certificates computed for subsystems. Using those constructed control barrier certificates, one can quantify upper bounds on probabilities that interconnected systems reach certain unsafe regions in finite-time horizons. We employ a systematic technique based on the sum-of-squares optimization program to search for storage certificates of subsystems together with their corresponding safety controllers. We demonstrate our proposed results by applying them to a temperature regulation in a circular building containing 1000 rooms. To show the applicability of our approaches to dense networks, we also apply our proposed techniques to a fully-interconnected network.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Embedded and cyber-physical systems
  • Mathematics of computing → Stochastic processes
  • Theory of computation → Timed and hybrid models
Keywords
  • Compositional barrier certificates
  • Stochastic hybrid systems
  • Dissipativity theory
  • Large-scale networks
  • Formal controller synthesis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. M. Ahmadi, B. Wu, H. Lin, and U. Topcu. Privacy verification in POMDPs via barrier certificates. In Proceedings of the 57th IEEE Conference on Decision and Control (CDC), pages 5610-5615, 2018. Google Scholar
  2. M. Anand, A. Lavaei, and M. Zamani. Compositional construction of control barrier certificates for large-scale interconnected stochastic systems. Proceedings of the 21st IFAC World Congress, 53(2):1862-1867, 2020. Google Scholar
  3. M. Arcak, C. Meissen, and A. Packard. Networks of dissipative systems. SpringerBriefs in Electrical and Computer Engineering. Springer, 2016. Google Scholar
  4. H. E. Bell. Gershgorin’s theorem and the zeros of polynomials. The American Mathematical Monthly, 72(3):292-295, 1965. Google Scholar
  5. A. Clark. Control barrier functions for complete and incomplete information stochastic systems. In Proceedings of the American Control Conference (ACC), pages 2928-2935, 2019. Google Scholar
  6. A. Girard, G. Gössler, and S. Mouelhi. Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models. IEEE Transactions on Automatic Control, 61(6):1537-1549, 2016. Google Scholar
  7. C. Godsil and G. Royle. Algebraic graph theory. Graduate Texts in Mathematics. Springe, 2001. Google Scholar
  8. C. Huang, X. Chen, W. Lin, Z. Yang, and X. Li. Probabilistic safety verification of stochastic hybrid systems using barrier certificates. ACM Transactions on Embedded Computing Systems (TECS), 16(5s):186, 2017. Google Scholar
  9. P. Jagtap, S. Soudjani, and M. Zamani. Formal synthesis of stochastic systems via control barrier certificates. IEEE Transactions on Automatic Control, 66(7):3097-3110, 2020. Google Scholar
  10. H. J. Kushner. Stochastic Stability and Control. Mathematics in Science and Engineering. Elsevier Science, 1967. Google Scholar
  11. A. Lavaei. Automated Verification and Control of Large-Scale Stochastic Cyber-Physical Systems: Compositional Techniques. PhD thesis, Technische Universität München, Germany, 2019. Google Scholar
  12. A. Lavaei, S. Soudjani, A. Abate, and M. Zamani. Automated verification and synthesis of stochastic hybrid systems: A survey. Automatica, 2022. Google Scholar
  13. A. Lavaei, S. Soudjani, and M. Zamani. Compositional construction of infinite abstractions for networks of stochastic control systems. Automatica, 107:125-137, 2019. Google Scholar
  14. A. Lavaei, S. Soudjani, and M. Zamani. Compositional abstraction-based synthesis for networks of stochastic switched systems. Automatica, 114, 2020. Google Scholar
  15. A. Lavaei, S. Soudjani, and M. Zamani. Compositional abstraction of large-scale stochastic systems: A relaxed dissipativity approach. Nonlinear Analysis: Hybrid Systems, 36, 2020. Google Scholar
  16. A. Lavaei, S. Soudjani, and M. Zamani. Compositional (in)finite abstractions for large-scale interconnected stochastic systems. IEEE Transactions on Automatic Control, 65(12):5280-5295, 2020. Google Scholar
  17. A. Nejati, S. Soudjani, and M. Zamani. Compositional construction of control barrier certificates for large-scale stochastic switched systems. IEEE Control Systems Letters, 4(4):845-850, 2020. Google Scholar
  18. A. Nejati, S. Soudjani, and M. Zamani. Compositional construction of control barrier functions for networks of continuous-time stochastic systems. Proceedings of the 21st IFAC World Congress, 53(2):1856-1861, 2020. Google Scholar
  19. A. Nejati, S. Soudjani, and M. Zamani. Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems. European Journal of Control, 57:82-94, 2021. Google Scholar
  20. A. Nejati and M. Zamani. Compositional construction of finite MDPs for continuous-time stochastic systems: A dissipativity approach. Proceedings of the 21st IFAC World Congress, 53(2):1962-1967, 2020. Google Scholar
  21. B. Oksendal. Stochastic differential equations: an introduction with applications. Springer Science & Business Media, 2013. Google Scholar
  22. B. K. Øksendal and A. Sulem. Applied stochastic control of jump diffusions, volume 498. Springer, 2005. Google Scholar
  23. A. Papachristodoulou, J. Anderson, G. Valmorbida, S. Prajna, P. Seiler, and P. Parrilo. SOSTOOLS version 3.00 sum of squares optimization toolbox for MATLAB. arXiv:1310.4716, 2013. Google Scholar
  24. P. A. Parrilo. Semidefinite programming relaxations for semialgebraic problems. Mathematical programming, 96(2):293-320, 2003. Google Scholar
  25. A. Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pages 46-57, 1977. Google Scholar
  26. S. Prajna, A. Jadbabaie, and G. J. Pappas. A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Transactions on Automatic Control, 52(8):1415-1428, 2007. Google Scholar
  27. K. Ross. Stochastic control in continuous time. Lecture Notes on Continuous Time Stochastic Control, pages P33-P37, 2008. Google Scholar
  28. J. F. Sturm. Using sedumi 1.02, a matlab toolbox for optimization over symmetric cones. Optimization methods and software, 11(1-4):625-653, 1999. Google Scholar
  29. R. Wisniewski and M. L. Bujorianu. Stochastic safety analysis of stochastic hybrid systems. In Proceedings of the 56th IEEE Conference on Decision and Control, pages 2390-2395, 2017. Google Scholar
  30. T. Wongpiromsarn, U. Topcu, and A. Lamperski. Automata theory meets barrier certificates: Temporal logic verification of nonlinear systems. IEEE Transactions on Automatic Control, 61(11):3344-3355, 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact