Skip to main content
Top
Published in: Acta Informatica 1-2/2020

13-09-2019 | Original Article

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

Authors: Antoine Girard, Gregor Gössler

Published in: Acta Informatica | Issue 1-2/2020

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Literature
1.
go back to reference Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971–984 (2000)CrossRef Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971–984 (2000)CrossRef
2.
go back to reference Angeli, D.: A Lyapunov approach to incremental stability properties. IEEE Trans. Autom. Control 47(3), 410–421 (2002)MathSciNetCrossRef Angeli, D.: A Lyapunov approach to incremental stability properties. IEEE Trans. Autom. Control 47(3), 410–421 (2002)MathSciNetCrossRef
3.
go back to reference 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)MathSciNetCrossRef 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)MathSciNetCrossRef
4.
go back to reference Belta, C., Yordanov, B., Aydin Gol, E.: Formal Methods for Discrete-Time Dynamical Systems, vol. 89. Springer, Berlin (2017)CrossRef Belta, C., Yordanov, B., Aydin Gol, E.: Formal Methods for Discrete-Time Dynamical Systems, vol. 89. Springer, Berlin (2017)CrossRef
5.
go back to reference Bulancea, O.L., Nilsson, P., Ozay, N.: Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings. IFAC-PapersOnLine 51(16), 19–24 (2018)CrossRef Bulancea, O.L., Nilsson, P., Ozay, N.: Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings. IFAC-PapersOnLine 51(16), 19–24 (2018)CrossRef
6.
go back to reference Caines, P.E., Wei, Y.J.: Hierarchical hybrid control systems: a lattice theoretic formulation. IEEE Trans. Autom. Control 43(4), 501–508 (1998)MathSciNetCrossRef Caines, P.E., Wei, Y.J.: Hierarchical hybrid control systems: a lattice theoretic formulation. IEEE Trans. Autom. Control 43(4), 501–508 (1998)MathSciNetCrossRef
7.
go back to reference 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) 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)
8.
go back to reference 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)CrossRef 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)CrossRef
9.
go back to reference Coogan, S., Arcak, M.: Finite abstraction of mixed monotone systems with discrete and continuous inputs. Nonlinear Anal. Hybrid Syst. 23, 254–271 (2017)MathSciNetCrossRef Coogan, S., Arcak, M.: Finite abstraction of mixed monotone systems with discrete and continuous inputs. Nonlinear Anal. Hybrid Syst. 23, 254–271 (2017)MathSciNetCrossRef
10.
go back to reference 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) 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)
11.
go back to reference Girard, A.: Approximately bisimilar abstractions of incrementally stable finite or infinite dimensional systems. In: IEEE Conference on Decision and Control, pp. 824–829 (2014) Girard, A.: Approximately bisimilar abstractions of incrementally stable finite or infinite dimensional systems. In: IEEE Conference on Decision and Control, pp. 824–829 (2014)
12.
go back to reference 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)MathSciNetCrossRef 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)MathSciNetCrossRef
13.
go back to reference Girard, A., Pappas, G.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control 52(5), 782–798 (2007)MathSciNetCrossRef Girard, A., Pappas, G.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control 52(5), 782–798 (2007)MathSciNetCrossRef
14.
go back to reference Girard, A., Pola, G., Tabuada, P.: Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans. Autom. Control 55(1), 116–126 (2010)MathSciNetCrossRef Girard, A., Pola, G., Tabuada, P.: Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans. Autom. Control 55(1), 116–126 (2010)MathSciNetCrossRef
15.
go back to reference Gruber, F., Kim, E.S., Arcak, M.: Sparsity-aware finite abstraction. In: IEEE Conference on Decision and Control, pp. 2366–2371 (2017) Gruber, F., Kim, E.S., Arcak, M.: Sparsity-aware finite abstraction. In: IEEE Conference on Decision and Control, pp. 2366–2371 (2017)
16.
go back to reference Hsu, K., Majumdar, R., Mallik, K., Schmuck, A.K.: Lazy abstraction-based control for safety specifications. arXiv preprint arXiv:1804.02666 (2018) Hsu, K., Majumdar, R., Mallik, K., Schmuck, A.K.: Lazy abstraction-based control for safety specifications. arXiv preprint arXiv:​1804.​02666 (2018)
17.
go back to reference 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) 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)
18.
go back to reference Hussien, O., Ames, A., Tabuada, P.: Abstracting partially feedback linearizable systems compositionally. IEEE Control Syst. Lett. 1(2), 227–232 (2017)CrossRef Hussien, O., Ames, A., Tabuada, P.: Abstracting partially feedback linearizable systems compositionally. IEEE Control Syst. Lett. 1(2), 227–232 (2017)CrossRef
19.
go back to reference 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) 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)
20.
go back to reference 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) 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)
21.
go back to reference Koutsoukos, X.D., Antsaklis, P.J., Stiver, J.A., Lemmon, M.D.: Supervisory control of hybrid systems. Proc. IEEE 88(7), 1026–1049 (2000)CrossRef Koutsoukos, X.D., Antsaklis, P.J., Stiver, J.A., Lemmon, M.D.: Supervisory control of hybrid systems. Proc. IEEE 88(7), 1026–1049 (2000)CrossRef
22.
go back to reference 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) 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)
23.
go back to reference Liu, J., Ozay, N.: Finite abstractions with robustness margins for temporal logic-based control synthesis. Nonlinear Anal. Hybrid Syst. 22, 1–15 (2016)MathSciNetCrossRef Liu, J., Ozay, N.: Finite abstractions with robustness margins for temporal logic-based control synthesis. Nonlinear Anal. Hybrid Syst. 22, 1–15 (2016)MathSciNetCrossRef
24.
go back to reference Lunze, J.: Qualitative modelling of linear dynamical systems with quantized state measurements. Automatica 30(3), 417–431 (1994)MathSciNetCrossRef Lunze, J.: Qualitative modelling of linear dynamical systems with quantized state measurements. Automatica 30(3), 417–431 (1994)MathSciNetCrossRef
25.
go back to reference Maidens, J., Arcak, M.: Reachability analysis of nonlinear systems using matrix measures. IEEE Trans. Autom. Control 60(1), 265–270 (2014)MathSciNetCrossRef Maidens, J., Arcak, M.: Reachability analysis of nonlinear systems using matrix measures. IEEE Trans. Autom. Control 60(1), 265–270 (2014)MathSciNetCrossRef
26.
27.
go back to reference Maler, O.: Control from computer science. Annu. Rev. Control 26(2), 175–187 (2002)CrossRef Maler, O.: Control from computer science. Annu. Rev. Control 26(2), 175–187 (2002)CrossRef
28.
go back to reference 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)MathSciNetCrossRef 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)MathSciNetCrossRef
29.
go back to reference 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) 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)
30.
go back to reference Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Symposium on Principles of Programming Languages, pp. 179–190. ACM (1989) Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Symposium on Principles of Programming Languages, pp. 179–190. ACM (1989)
31.
go back to reference Pola, G., Borri, A., Di Benedetto, M.: Integrated design of symbolic controllers for nonlinear systems. IEEE Trans. Autom. Control 57(2), 534–539 (2012)MathSciNetCrossRef Pola, G., Borri, A., Di Benedetto, M.: Integrated design of symbolic controllers for nonlinear systems. IEEE Trans. Autom. Control 57(2), 534–539 (2012)MathSciNetCrossRef
32.
go back to reference Pola, G., Pepe, P., Di Benedetto, M.D.: Symbolic models for networks of control systems. IEEE Trans. Autom. Control 61(11), 3663–3668 (2016)MathSciNetCrossRef Pola, G., Pepe, P., Di Benedetto, M.D.: Symbolic models for networks of control systems. IEEE Trans. Autom. Control 61(11), 3663–3668 (2016)MathSciNetCrossRef
33.
go back to reference 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)MathSciNetCrossRef 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)MathSciNetCrossRef
34.
go back to reference Raisch, J., O’Young, S.D.: Discrete approximation and supervisory control of continuous systems. IEEE Trans. Autom. Control 43(4), 569–573 (1998)MathSciNetCrossRef Raisch, J., O’Young, S.D.: Discrete approximation and supervisory control of continuous systems. IEEE Trans. Autom. Control 43(4), 569–573 (1998)MathSciNetCrossRef
35.
go back to reference Ramadge, P., Wonham, W.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206–230 (1987)MathSciNetCrossRef Ramadge, P., Wonham, W.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206–230 (1987)MathSciNetCrossRef
36.
37.
go back to reference Reissig, G., Weber, A., Rungger, M.: Feedback refinement relations for the synthesis of symbolic controllers. IEEE Trans. Autom. Control 62(4), 1781–1796 (2017)MathSciNetCrossRef Reissig, G., Weber, A., Rungger, M.: Feedback refinement relations for the synthesis of symbolic controllers. IEEE Trans. Autom. Control 62(4), 1781–1796 (2017)MathSciNetCrossRef
38.
go back to reference 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) 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)
39.
go back to reference Rungger, M., Stursberg, O.: On-the-fly model abstraction for controller synthesis. In: American Control Conference, pp. 2645–2650 (2012) Rungger, M., Stursberg, O.: On-the-fly model abstraction for controller synthesis. In: American Control Conference, pp. 2645–2650 (2012)
40.
go back to reference 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) 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)
41.
go back to reference Swikir, A., Zamani, M.: Compositional synthesis of finite abstractions for networks of systems: a small-gain approach. Automatica 107, 551–561 (2019)MathSciNetCrossRef Swikir, A., Zamani, M.: Compositional synthesis of finite abstractions for networks of systems: a small-gain approach. Automatica 107, 551–561 (2019)MathSciNetCrossRef
42.
go back to reference Tabuada, P.: Verification and Control of Hybrid Systems—A Symbolic Approach. Springer, Berlin (2009)CrossRef Tabuada, P.: Verification and Control of Hybrid Systems—A Symbolic Approach. Springer, Berlin (2009)CrossRef
43.
go back to reference Tabuada, P., Pappas, G.: Linear time logic control of discrete-time linear systems. IEEE Trans. Autom. Control 51(12), 1862–1877 (2006)MathSciNetCrossRef Tabuada, P., Pappas, G.: Linear time logic control of discrete-time linear systems. IEEE Trans. Autom. Control 51(12), 1862–1877 (2006)MathSciNetCrossRef
44.
go back to reference 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)CrossRef 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)CrossRef
45.
go back to reference Yordanov, B., Belta, C.: Formal analysis of discrete-time piecewise affine systems. IEEE Trans. Autom. Control 55(12), 2834–2840 (2010)MathSciNetCrossRef Yordanov, B., Belta, C.: Formal analysis of discrete-time piecewise affine systems. IEEE Trans. Autom. Control 55(12), 2834–2840 (2010)MathSciNetCrossRef
46.
go back to reference Zamani, M., Abate, A., Girard, A.: Symbolic models for stochastic switched systems: a discretization and a discretization-free approach. Automatica 55, 183–196 (2015)MathSciNetCrossRef Zamani, M., Abate, A., Girard, A.: Symbolic models for stochastic switched systems: a discretization and a discretization-free approach. Automatica 55, 183–196 (2015)MathSciNetCrossRef
47.
go back to reference 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)MathSciNetCrossRef 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)MathSciNetCrossRef
48.
go back to reference Zamani, M., Tabuada, P.: Backstepping design for incremental stability. IEEE Trans. Autom. Control 56(9), 2184–2189 (2011)MathSciNetCrossRef Zamani, M., Tabuada, P.: Backstepping design for incremental stability. IEEE Trans. Autom. Control 56(9), 2184–2189 (2011)MathSciNetCrossRef
Metadata
Title
Safety synthesis for incrementally stable switched systems using discretization-free multi-resolution abstractions
Authors
Antoine Girard
Gregor Gössler
Publication date
13-09-2019
Publisher
Springer Berlin Heidelberg
Published in
Acta Informatica / Issue 1-2/2020
Print ISSN: 0001-5903
Electronic ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-019-00341-x

Other articles of this Issue 1-2/2020

Acta Informatica 1-2/2020 Go to the issue

Premium Partner