Advertisement

Safety synthesis for incrementally stable switched systems using discretization-free multi-resolution abstractions

  • Antoine GirardEmail author
  • Gregor Gössler
Original Article

Abstract

Control of continuous and hybrid systems using discrete abstractions often suffers from scalability issues, due to the use of state space partitions as symbolic states. In this paper, for incrementally stable switched systems, we introduce a class of abstractions that do not rely on state space partitions but use mode sequences as symbolic states. Our approach differs from existing works by the possibility of considering sequences of varying length, giving the possibility to adjust locally the resolution of the abstraction. Temporal constraints on the switching signal can also be taken into account. We thus define multi-resolution bisimilar abstractions that enjoy interesting properties that can be used to design specific algorithms to synthesize safety controllers. These algorithms need not compute the full abstraction that is built incrementally during controller synthesis, exploring finer resolutions only when the specification cannot be enforced at the coarser level. We illustrate the approach by a numerical example inspired by road traffic regulation.

Notes

References

  1. 1.
    Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971–984 (2000)CrossRefGoogle Scholar
  2. 2.
    Angeli, D.: A Lyapunov approach to incremental stability properties. IEEE Trans. Autom. Control 47(3), 410–421 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Aylward, E.M., Parrilo, P.A., Slotine, J.J.E.: Stability and robustness analysis of nonlinear systems via contraction metrics and SOS programming. Automatica 44(8), 2163–2170 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Belta, C., Yordanov, B., Aydin Gol, E.: Formal Methods for Discrete-Time Dynamical Systems, vol. 89. Springer, Berlin (2017)CrossRefzbMATHGoogle Scholar
  5. 5.
    Bulancea, O.L., Nilsson, P., Ozay, N.: Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings. IFAC-PapersOnLine 51(16), 19–24 (2018)CrossRefGoogle Scholar
  6. 6.
    Caines, P.E., Wei, Y.J.: Hierarchical hybrid control systems: a lattice theoretic formulation. IEEE Trans. Autom. Control 43(4), 501–508 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Cámara, J., Girard, A., Gössler, G.: Synthesis of switching controllers using approximately bisimilar multiscale abstractions. In: Hybrid Systems: Computation and Control, pp. 191–200 (2011)Google Scholar
  8. 8.
    Canudas De Wit, C., Ojeda, L.L., Kibangou, A.Y.: Graph constrained-CTM observer design for the Grenoble south ring. IFAC Proc. Vol. 45(24), 197–202 (2012)CrossRefGoogle Scholar
  9. 9.
    Coogan, S., Arcak, M.: Finite abstraction of mixed monotone systems with discrete and continuous inputs. Nonlinear Anal. Hybrid Syst. 23, 254–271 (2017)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Dallal, E., Tabuada, P.: On compositional symbolic controller synthesis inspired by small-gain theorems. In: IEEE Conference on Decision and Control, pp. 6133–6138 (2015)Google Scholar
  11. 11.
    Girard, A.: Approximately bisimilar abstractions of incrementally stable finite or infinite dimensional systems. In: IEEE Conference on Decision and Control, pp. 824–829 (2014)Google Scholar
  12. 12.
    Girard, A., Gössler, G., Mouelhi, S.: Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models. IEEE Trans. Autom. Control 61(6), 1537–1549 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Girard, A., Pappas, G.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control 52(5), 782–798 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Girard, A., Pola, G., Tabuada, P.: Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans. Autom. Control 55(1), 116–126 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Gruber, F., Kim, E.S., Arcak, M.: Sparsity-aware finite abstraction. In: IEEE Conference on Decision and Control, pp. 2366–2371 (2017)Google Scholar
  16. 16.
    Hsu, K., Majumdar, R., Mallik, K., Schmuck, A.K.: Lazy abstraction-based control for safety specifications. arXiv preprint arXiv:1804.02666 (2018)
  17. 17.
    Hsu, K., Majumdar, R., Mallik, K., Schmuck, A.K.: Multi-layered abstraction-based controller synthesis for continuous-time systems. In: International Conference on Hybrid Systems: Computation and Control, pp. 120–129 (2018)Google Scholar
  18. 18.
    Hussien, O., Ames, A., Tabuada, P.: Abstracting partially feedback linearizable systems compositionally. IEEE Control Syst. Lett. 1(2), 227–232 (2017)CrossRefGoogle Scholar
  19. 19.
    Kim, E.S., Arcak, M., Seshia, S.A.: Compositional controller synthesis for vehicular traffic networks. In: IEEE Conference on Decision and Control, pp. 6165–6171 (2015)Google Scholar
  20. 20.
    Kim, E.S., Arcak, M., Zamani, M.: Constructing control system abstractions from modular components. In: International Conference on Hybrid Systems: Computation and Control, pp. 137–146 (2018)Google Scholar
  21. 21.
    Koutsoukos, X.D., Antsaklis, P.J., Stiver, J.A., Lemmon, M.D.: Supervisory control of hybrid systems. Proc. IEEE 88(7), 1026–1049 (2000)CrossRefGoogle Scholar
  22. 22.
    Le Corronc, E., Girard, A., Gössler, G.: Mode sequences as symbolic states in abstractions of incrementally stable switched systems. In: IEEE Conference on Decision and Control, pp. 3225–3230 (2013)Google Scholar
  23. 23.
    Liu, J., Ozay, N.: Finite abstractions with robustness margins for temporal logic-based control synthesis. Nonlinear Anal. Hybrid Syst. 22, 1–15 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Lunze, J.: Qualitative modelling of linear dynamical systems with quantized state measurements. Automatica 30(3), 417–431 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Maidens, J., Arcak, M.: Reachability analysis of nonlinear systems using matrix measures. IEEE Trans. Autom. Control 60(1), 265–270 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Majumdar, R., Mallik, K., Schmuck, A.K.: Compositional synthesis of finite state abstractions. arXiv preprint arXiv:1612.08515 (2016)
  27. 27.
    Maler, O.: Control from computer science. Annu. Rev. Control 26(2), 175–187 (2002)CrossRefGoogle Scholar
  28. 28.
    Meyer, P.J., Girard, A., Witrant, E.: Compositional abstraction and safety synthesis using overlapping symbolic models. IEEE Trans. Autom. Control 63(6), 1835–1841 (2018)MathSciNetCrossRefzbMATHGoogle Scholar
  29. 29.
    Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive (1) designs. In: International Workshop on Verification, Model Checking, and Abstract Interpretation, pp. 364–380 (2006)Google Scholar
  30. 30.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Symposium on Principles of Programming Languages, pp. 179–190. ACM (1989)Google Scholar
  31. 31.
    Pola, G., Borri, A., Di Benedetto, M.: Integrated design of symbolic controllers for nonlinear systems. IEEE Trans. Autom. Control 57(2), 534–539 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    Pola, G., Pepe, P., Di Benedetto, M.D.: Symbolic models for networks of control systems. IEEE Trans. Autom. Control 61(11), 3663–3668 (2016)MathSciNetCrossRefzbMATHGoogle Scholar
  33. 33.
    Pola, G., Pepe, P., Di Benedetto, M.D.: Decentralized supervisory control of networks of nonlinear control systems. IEEE Trans. Autom. Control 63(9), 2803–2817 (2018)MathSciNetCrossRefzbMATHGoogle Scholar
  34. 34.
    Raisch, J., O’Young, S.D.: Discrete approximation and supervisory control of continuous systems. IEEE Trans. Autom. Control 43(4), 569–573 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  35. 35.
    Ramadge, P., Wonham, W.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206–230 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  36. 36.
    Reißig, G.: Computing abstractions of nonlinear systems. IEEE Trans. Autom. Control 56(11), 2583–2598 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  37. 37.
    Reissig, G., Weber, A., Rungger, M.: Feedback refinement relations for the synthesis of symbolic controllers. IEEE Trans. Autom. Control 62(4), 1781–1796 (2017)MathSciNetCrossRefzbMATHGoogle Scholar
  38. 38.
    Rungger, M., Mazo, M., Tabuada, P.: Scaling up controller synthesis for linear systems and safety specifications. In: IEEE Conference on Decision and Control, pp. 7638–7643 (2012)Google Scholar
  39. 39.
    Rungger, M., Stursberg, O.: On-the-fly model abstraction for controller synthesis. In: American Control Conference, pp. 2645–2650 (2012)Google Scholar
  40. 40.
    Saoud, A., Girard, A., Fribourg, L.: Contract based design of symbolic controllers for interconnected multiperiodic sampled-data systems. In: IEEE Conference on Decision and Control, pp. 1–9 (2018)Google Scholar
  41. 41.
    Swikir, A., Zamani, M.: Compositional synthesis of finite abstractions for networks of systems: a small-gain approach. Automatica 107, 551–561 (2019)MathSciNetCrossRefGoogle Scholar
  42. 42.
    Tabuada, P.: Verification and Control of Hybrid Systems—A Symbolic Approach. Springer, Berlin (2009)CrossRefzbMATHGoogle Scholar
  43. 43.
    Tabuada, P., Pappas, G.: Linear time logic control of discrete-time linear systems. IEEE Trans. Autom. Control 51(12), 1862–1877 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  44. 44.
    Tazaki, Y., Imura, J.: Discrete-state abstractions of nonlinear systems using multi-resolution quantizer. In: Hybrid Systems: Computation and Control, vol. 5469, pp. 351–365 (2009)Google Scholar
  45. 45.
    Yordanov, B., Belta, C.: Formal analysis of discrete-time piecewise affine systems. IEEE Trans. Autom. Control 55(12), 2834–2840 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  46. 46.
    Zamani, M., Abate, A., Girard, A.: Symbolic models for stochastic switched systems: a discretization and a discretization-free approach. Automatica 55, 183–196 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  47. 47.
    Zamani, M., Pola, G., Mazo, M., Tabuada, P.: Symbolic models for nonlinear control systems without stability assumptions. IEEE Trans. Autom. Control 57(7), 1804–1809 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  48. 48.
    Zamani, M., Tabuada, P.: Backstepping design for incremental stability. IEEE Trans. Autom. Control 56(9), 2184–2189 (2011)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2019

Authors and Affiliations

  1. 1.Laboratoire des signaux et systèmes (L2S)CNRS, CentraleSupélec, Université Paris-Sud, Université Paris-SaclayGif-sur-YvetteFrance
  2. 2.Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIGGrenobleFrance
  3. 3.Inria, Centre de Grenoble - Rhône-AlpesMontbonnot St IsmierFrance

Personalised recommendations