Vol. 8 No. 2 (2022): Special Issue on Distributed Hybrid Systems
Special Issue on Distributed Hybrid Systems

From Dissipativity Theory to Compositional Construction of Control Barrier Certificates

PDF
  • Ameneh Nejati,
  • Majid Zamani
Ameneh Nejati
Department of Electrical Engineering, Technical University of Munich, Germany; Department of Computer Science, LMU Munich, Germany
Bio
Majid Zamani
Department of Computer Science, University of Colorado Boulder, USA; Department of Computer Science, LMU Munich, Germany
Bio
DOI: https://doi.org/10.4230/LITES.8.2.6

Published 2022-12-07

Keywords

  • Compositional barrier certificates,
  • Stochastic hybrid systems,
  • Dissipativity theory,
  • Large-scale networks,
  • Formal controller synthesis

How to Cite

[1]
Nejati, A. and Zamani, M. 2022. From Dissipativity Theory to Compositional Construction of Control Barrier Certificates. Leibniz Transactions on Embedded Systems. 8, 2 (Dec. 2022), 06:1–06:17. DOI:https://doi.org/10.4230/LITES.8.2.6.

Copyright (c) 2022 Ameneh Nejati and Majid Zamani

Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

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.

PDF

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.
  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.
  3. M. Arcak, C. Meissen, and A. Packard. Networks of dissipative systems. SpringerBriefs in Electrical and Computer Engineering. Springer, 2016.
  4. H. E. Bell. Gershgorin’s theorem and the zeros of polynomials. The American Mathematical Monthly, 72(3):292-295, 1965.
  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.
  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.
  7. C. Godsil and G. Royle. Algebraic graph theory. Graduate Texts in Mathematics. Springe, 2001.
  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.
  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.
  10. H. J. Kushner. Stochastic Stability and Control. Mathematics in Science and Engineering. Elsevier Science, 1967.
  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.
  12. A. Lavaei, S. Soudjani, A. Abate, and M. Zamani. Automated verification and synthesis of stochastic hybrid systems: A survey. Automatica, 2022.
  13. A. Lavaei, S. Soudjani, and M. Zamani. Compositional construction of infinite abstractions for networks of stochastic control systems. Automatica, 107:125-137, 2019.
  14. A. Lavaei, S. Soudjani, and M. Zamani. Compositional abstraction-based synthesis for networks of stochastic switched systems. Automatica, 114, 2020.
  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.
  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.
  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.
  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.
  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.
  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.
  21. B. Oksendal. Stochastic differential equations: an introduction with applications. Springer Science & Business Media, 2013.
  22. B. K. Øksendal and A. Sulem. Applied stochastic control of jump diffusions, volume 498. Springer, 2005.
  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.
  24. P. A. Parrilo. Semidefinite programming relaxations for semialgebraic problems. Mathematical programming, 96(2):293-320, 2003.
  25. A. Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pages 46-57, 1977.
  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.
  27. K. Ross. Stochastic control in continuous time. Lecture Notes on Continuous Time Stochastic Control, pages P33-P37, 2008.
  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.
  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.
  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.