Skip to main content

2019 | OriginalPaper | Buchkapitel

Approximate Probabilistic Relations for Compositional Abstractions of Stochastic Systems

verfasst von : Abolfazl Lavaei, Sadegh Soudjani, Majid Zamani

Erschienen in: Numerical Software Verification

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

In this paper, we propose a compositional approach for constructing abstractions of general Markov decision processes (gMDPs) using approximate probabilistic relations. The abstraction framework is based on the notion of \(\delta \)-lifted relations, using which one can quantify the distance in probability between the interconnected gMDPs and that of their abstractions. This new approximate relation unifies compositionality results in the literature by allowing abstract models to have either finite or infinite state spaces. To this end, we first propose our compositionality results using the new approximate probabilistic relation which is based on lifting. We then focus on a class of stochastic nonlinear dynamical systems and construct their abstractions using both model order reduction and space discretization in a unified framework. Finally, we demonstrate the effectiveness of the proposed results by considering a network of four nonlinear dynamical subsystems (together 12 dimensions) and constructing finite abstractions from their reduced-order versions (together 4 dimensions) in a unified compositional framework.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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 "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!

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!

Literatur
1.
Zurück zum Zitat Abate, A.: Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey. Electron. Notes Theor. Comput. Sci. 297, 3–25 (2013)CrossRef Abate, A.: Approximation metrics based on probabilistic bisimulations for general state-space Markov processes: a survey. Electron. Notes Theor. Comput. Sci. 297, 3–25 (2013)CrossRef
2.
Zurück zum Zitat Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete-time stochastic hybrid systems. Automatica 44(11), 2724–2734 (2008)MathSciNetCrossRef Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete-time stochastic hybrid systems. Automatica 44(11), 2724–2734 (2008)MathSciNetCrossRef
3.
Zurück zum Zitat Abate, A., Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking of labelled Markov processes via finite approximate bisimulations. In: van Breugel, F., Kashefi, E., Palamidessi, C., Rutten, J. (eds.) Horizons of the Mind. A Tribute to Prakash Panangaden. LNCS, vol. 8464, pp. 40–58. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06880-0_2CrossRef Abate, A., Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic model checking of labelled Markov processes via finite approximate bisimulations. In: van Breugel, F., Kashefi, E., Palamidessi, C., Rutten, J. (eds.) Horizons of the Mind. A Tribute to Prakash Panangaden. LNCS, vol. 8464, pp. 40–58. Springer, Cham (2014). https://​doi.​org/​10.​1007/​978-3-319-06880-0_​2CrossRef
4.
Zurück zum Zitat Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
5.
Zurück zum Zitat Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318(3), 323–354 (2004)MathSciNetCrossRef Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318(3), 323–354 (2004)MathSciNetCrossRef
6.
Zurück zum Zitat Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: logic, simulation and games. In: Proceedings of the 5th International Conference on Quantitative Evaluation of System, pp. 264–273 (2008) Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: logic, simulation and games. In: Proceedings of the 5th International Conference on Quantitative Evaluation of System, pp. 264–273 (2008)
7.
Zurück zum Zitat D’Innocenzo, A., Abate, A., Katoen, J.: Robust PCTL model checking. In: Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control, pp. 275–286 (2012) D’Innocenzo, A., Abate, A., Katoen, J.: Robust PCTL model checking. In: Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control, pp. 275–286 (2012)
8.
Zurück zum Zitat Haesaert, S., Soudjani, S., Abate, A.: Verification of general Markov decision processes by approximate similarity relations and policy refinement. SIAM J. Control Optim. 55(4), 2333–2367 (2017)MathSciNetCrossRef Haesaert, S., Soudjani, S., Abate, A.: Verification of general Markov decision processes by approximate similarity relations and policy refinement. SIAM J. Control Optim. 55(4), 2333–2367 (2017)MathSciNetCrossRef
9.
Zurück zum Zitat Haesaert, S., Soudjani, S., Abate, A.: Temporal logic control of general Markov decision processes by approximate policy refinement. In: Proceedings of the 6th IFAC Conference on Analysis and Design of Hybrid Systems, vol. 51, pp. 73–78 (2018)CrossRef Haesaert, S., Soudjani, S., Abate, A.: Temporal logic control of general Markov decision processes by approximate policy refinement. In: Proceedings of the 6th IFAC Conference on Analysis and Design of Hybrid Systems, vol. 51, pp. 73–78 (2018)CrossRef
10.
Zurück zum Zitat Julius, A.A., Pappas, G.J.: Approximations of stochastic hybrid systems. IEEE Trans. Autom. Control 54(6), 1193–1203 (2009)MathSciNetCrossRef Julius, A.A., Pappas, G.J.: Approximations of stochastic hybrid systems. IEEE Trans. Autom. Control 54(6), 1193–1203 (2009)MathSciNetCrossRef
11.
Zurück zum Zitat Kamgarpour, M., Summers, S., Lygeros, J.: Control design for specifications on stochastic hybrid systems. In: Proceedings of the 16th ACM International Conference on Hybrid Systems: Computation and Control, pp. 303–312 (2013) Kamgarpour, M., Summers, S., Lygeros, J.: Control design for specifications on stochastic hybrid systems. In: Proceedings of the 16th ACM International Conference on Hybrid Systems: Computation and Control, pp. 303–312 (2013)
12.
13.
Zurück zum Zitat Lavaei, A., Soudjani, S., Majumdar, R., Zamani, M.: Compositional abstractions of interconnected discrete-time stochastic control systems. In: Proceedings of the 56th IEEE Conference on Decision and Control, pp. 3551–3556 (2017) Lavaei, A., Soudjani, S., Majumdar, R., Zamani, M.: Compositional abstractions of interconnected discrete-time stochastic control systems. In: Proceedings of the 56th IEEE Conference on Decision and Control, pp. 3551–3556 (2017)
14.
Zurück zum Zitat Lavaei, A., Soudjani, S., Zamani, M.: Compositional synthesis of finite abstractions for continuous-space stochastic control systems: a small-gain approach. In: Proceedings of the 6th IFAC Conference on Analysis and Design of Hybrid Systems, vol. 51, pp. 265–270 (2018)CrossRef Lavaei, A., Soudjani, S., Zamani, M.: Compositional synthesis of finite abstractions for continuous-space stochastic control systems: a small-gain approach. In: Proceedings of the 6th IFAC Conference on Analysis and Design of Hybrid Systems, vol. 51, pp. 265–270 (2018)CrossRef
15.
Zurück zum Zitat Lavaei, A., Soudjani, S., Zamani, M.: From dissipativity theory to compositional construction of finite Markov decision processes. In: Proceedings of the 21st ACM International Conference on Hybrid Systems: Computation and Control, pp. 21–30 (2018) Lavaei, A., Soudjani, S., Zamani, M.: From dissipativity theory to compositional construction of finite Markov decision processes. In: Proceedings of the 21st ACM International Conference on Hybrid Systems: Computation and Control, pp. 21–30 (2018)
16.
Zurück zum Zitat Lavaei, A., Soudjani, S., Zamani, M.: Compositional construction of infinite abstractions for networks of stochastic control systems. Automatica 107, 125–137 (2019)MathSciNetCrossRef Lavaei, A., Soudjani, S., Zamani, M.: Compositional construction of infinite abstractions for networks of stochastic control systems. Automatica 107, 125–137 (2019)MathSciNetCrossRef
17.
Zurück zum Zitat Lavaei, A., Soudjani, S., Zamani, M.: Compositional synthesis of large-scale stochastic systems: a relaxed dissipativity approach. Nonlinear Analysis: Hybrid Systems (2019, accepted) Lavaei, A., Soudjani, S., Zamani, M.: Compositional synthesis of large-scale stochastic systems: a relaxed dissipativity approach. Nonlinear Analysis: Hybrid Systems (2019, accepted)
18.
Zurück zum Zitat Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nordic J. Comput. 2(2), 250–273 (1995)MathSciNetMATH Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nordic J. Comput. 2(2), 250–273 (1995)MathSciNetMATH
19.
Zurück zum Zitat Soudjani, S., Abate, A.: Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM J. Appl. Dyn. Syst. 12(2), 921–956 (2013)MathSciNetCrossRef Soudjani, S., Abate, A.: Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM J. Appl. Dyn. Syst. 12(2), 921–956 (2013)MathSciNetCrossRef
20.
Zurück zum Zitat Soudjani, S., Abate, A., Majumdar, R.: Dynamic Bayesian networks as formal abstractions of structured stochastic processes. In: Proceedings of the 26th International Conference on Concurrency Theory, pp. 1–14 (2015) Soudjani, S., Abate, A., Majumdar, R.: Dynamic Bayesian networks as formal abstractions of structured stochastic processes. In: Proceedings of the 26th International Conference on Concurrency Theory, pp. 1–14 (2015)
21.
Zurück zum Zitat Soudjani, S.E.Z., Gevaerts, C., Abate, A.: FAUST\(^{\sf 2}\): \(\underline{{\rm f}}\)ormal \(\underline{{\rm a}}\)bstractions of \(\underline{{\rm u}}\)ncountable-\(\underline{{\rm st}}\)ate \(\underline{{\rm st}}\)ochastic processes. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 272–286. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_23CrossRef Soudjani, S.E.Z., Gevaerts, C., Abate, A.: FAUST\(^{\sf 2}\): \(\underline{{\rm f}}\)ormal \(\underline{{\rm a}}\)bstractions of \(\underline{{\rm u}}\)ncountable-\(\underline{{\rm st}}\)ate \(\underline{{\rm st}}\)ochastic processes. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 272–286. Springer, Heidelberg (2015). https://​doi.​org/​10.​1007/​978-3-662-46681-0_​23CrossRef
22.
Zurück zum Zitat Soudjani, S.: Formal abstractions for automated verification and synthesis of stochastic systems. Ph.D. thesis, Technische Universiteit Delft, The Netherlands (2014) Soudjani, S.: Formal abstractions for automated verification and synthesis of stochastic systems. Ph.D. thesis, Technische Universiteit Delft, The Netherlands (2014)
23.
Zurück zum Zitat Tkachev, I., Abate, A.: On infinite-horizon probabilistic properties and stochastic bisimulation functions. In: Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC), pp. 526–531 (2011) Tkachev, I., Abate, A.: On infinite-horizon probabilistic properties and stochastic bisimulation functions. In: Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC), pp. 526–531 (2011)
24.
Zurück zum Zitat Zamani, M., Mohajerin Esfahani, P., Majumdar, R., Abate, A., Lygeros, J.: Symbolic control of stochastic systems via approximately bisimilar finite abstractions. IEEE Trans. Autom. Control 59(12), 3135–3150 (2014)MathSciNetCrossRef Zamani, M., Mohajerin Esfahani, P., Majumdar, R., Abate, A., Lygeros, J.: Symbolic control of stochastic systems via approximately bisimilar finite abstractions. IEEE Trans. Autom. Control 59(12), 3135–3150 (2014)MathSciNetCrossRef
Metadaten
Titel
Approximate Probabilistic Relations for Compositional Abstractions of Stochastic Systems
verfasst von
Abolfazl Lavaei
Sadegh Soudjani
Majid Zamani
Copyright-Jahr
2019
DOI
https://doi.org/10.1007/978-3-030-28423-7_7