Skip to main content
main-content
Top

Hint

Swipe to navigate through the chapters of this book

2019 | OriginalPaper | Chapter

Approximate Probabilistic Relations for Compositional Abstractions of Stochastic Systems

Authors : Abolfazl Lavaei, Sadegh Soudjani, Majid Zamani

Published in: Numerical Software Verification

Publisher: Springer International Publishing

share
SHARE

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.
Literature
1.
go back to reference 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.
go back to reference 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.
go back to reference 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_​2 CrossRef 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_​2 CrossRef
4.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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)
13.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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.
go back to reference 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_​23 CrossRef 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_​23 CrossRef
22.
go back to reference 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.
go back to reference 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.
go back to reference 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
Metadata
Title
Approximate Probabilistic Relations for Compositional Abstractions of Stochastic Systems
Authors
Abolfazl Lavaei
Sadegh Soudjani
Majid Zamani
Copyright Year
2019
DOI
https://doi.org/10.1007/978-3-030-28423-7_7

Premium Partner