main-content

## Swipe to navigate through the chapters of this book

Published in:

2019 | OriginalPaper | Chapter

# Approximate Probabilistic Relations for Compositional Abstractions of Stochastic Systems

Authors : Abolfazl Lavaei, Sadegh Soudjani, Majid Zamani

Published in:

Publisher:

## 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.
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.
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)
3.
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.
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008) MATH
5.
Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318(3), 323–354 (2004)
6.
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.
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.
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)
9.
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.
Julius, A.A., Pappas, G.J.: Approximations of stochastic hybrid systems. IEEE Trans. Autom. Control 54(6), 1193–1203 (2009)
11.
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.
Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)
13.
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.
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.
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.
Lavaei, A., Soudjani, S., Zamani, M.: Compositional construction of infinite abstractions for networks of stochastic control systems. Automatica 107, 125–137 (2019)
17.
Lavaei, A., Soudjani, S., Zamani, M.: Compositional synthesis of large-scale stochastic systems: a relaxed dissipativity approach. Nonlinear Analysis: Hybrid Systems (2019, accepted)
18.
Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nordic J. Comput. 2(2), 250–273 (1995)
19.
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)
20.
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.
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.
Soudjani, S.: Formal abstractions for automated verification and synthesis of stochastic systems. Ph.D. thesis, Technische Universiteit Delft, The Netherlands (2014)
23.
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.
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)