Automata-based controller synthesis for stochastic systems: a game framework via approximate probabilistic relations. (English) Zbl 1505.93257
Summary: In this work, we propose an abstraction and refinement methodology for the controller synthesis of discrete-time stochastic systems to enforce complex logical properties expressed by deterministic finite automata (DFA). Our proposed scheme is based on a notion of so-called \(( \epsilon , \delta )\)-approximate probabilistic relations, allowing one to quantify the similarity between stochastic systems modeled by discrete-time stochastic games and their corresponding finite abstractions. Leveraging this type of relations, the lower bound for the probability of satisfying the desired specifications can be well ensured by refining controllers synthesized over abstract systems to the original games. Moreover, we propose an algorithmic procedure to construct such a relation for a particular class of nonlinear stochastic systems with slope restrictions on the nonlinearity. The proposed methods are demonstrated on a quadrotor example, and the results indicate that the desired lower bound for the probability of satisfaction is guaranteed.
MSC:
| 93E03 | Stochastic systems in control theory (general) |
| 93C55 | Discrete-time control/observation systems |
| 93B50 | Synthesis problems |
| 68Q45 | Formal languages and automata |
| 91A15 | Stochastic games, stochastic differential games |
Keywords:
stochastic games; automata-based controller synthesis; approximate probabilistic relation; policy refinement; finite abstractionReferences:
| [1] | Abate, A.; Katoen, J.-P.; Lygeros, J.; Prandini, M., Approximate model checking of stochastic hybrid systems, European Journal of Control, 16, 6, 624-641 (2010) · Zbl 1216.93091 |
| [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) · Zbl 1152.93051 |
| [3] | Aberkane, S.; Dragan, V., On a solution to the problem of time-varying zero-sum LQ stochastic difference game: A Riccati equation approach, (Proceedings of the 18th European control conference (2019)), 388-393 |
| [4] | Arcak, M.; Kokotovic, P., Observer-based control of systems with slope-restricted nonlinearities, IEEE Transactions on Automatic Control, 46, 7, 1146-1150 (2001) · Zbl 1014.93033 |
| [5] | Asselborn, L.; Stursberg, O., Probabilistic control of uncertain linear systems using stochastic reachability, IFAC-PapersOnLine, 48, 14, 167-173 (2015) |
| [6] | Baier, C.; Katoen, J.-P., Principles of model checking (2008), MIT Press · Zbl 1179.68076 |
| [7] | Basset, N.; Kwiatkowska, M.; Wiltsche, C., Compositional strategy synthesis for stochastic games with multiple objectives, Information and Computation, 261, 536-587 (2018) · Zbl 1395.68265 |
| [8] | Bernardo, J. M.; Smith, A. F.M., Bayesian theory, Vol. 405 (2009), John Wiley & Sons |
| [9] | Borkar, V. S., Probability theory: An advanced course (2012), Springer Science & Business Media |
| [10] | Boyd, S.; Boyd, S. P.; Vandenberghe, L., Convex optimization (2004), Cambridge University Press · Zbl 1058.90049 |
| [11] | Breton, M.; Alj, A.; Haurie, A., Sequential Stackelberg equilibria in two-person games, Journal of Optimization Theory and Applications, 59, 1, 71-97 (1988) · Zbl 0631.90100 |
| [12] | Buzhinsky, I., Formalization of natural language requirements into temporal logics: a survey, (2019 IEEE 17th international conference on industrial informatics, Vol. 1. 2019 IEEE 17th international conference on industrial informatics, Vol. 1, INDIN (2019), IEEE), 400-406 |
| [13] | Cannon, M.; Cheng, Q.; Kouvaritakis, B.; Raković, S. V., Stochastic tube MPC with state estimation, Automatica, 48, 3, 536-541 (2012) · Zbl 1244.93181 |
| [14] | Chatterjee, K.; Doyen, L., Perfect-information stochastic games with generalized mean-payoff objectives, (Proceedings of the 31st annual ACM/IEEE symposium on logic in computer science (2016)), 247-256 · Zbl 1401.68238 |
| [15] | Chatterjee, K.; Ibsen-Jensen, R., Qualitative analysis of concurrent mean-payoff games, Information and Computation, 242, 2-24 (2015) · Zbl 1318.91039 |
| [16] | Chatterjee, K.; Katoen, J.-P.; Weininger, M.; Winkler, T., Stochastic games with lexicographic reachability-safety objectives, (International conference on computer aided verification (2020), Springer), 398-420 · Zbl 1478.68151 |
| [17] | Ding, J.; Kamgarpour, M.; Summers, S.; Abate, A.; Lygeros, J.; Tomlin, C., A stochastic games framework for verification and control of discrete time stochastic hybrid systems, Automatica, 49, 9, 2665-2674 (2013) · Zbl 1364.93857 |
| [18] | Duret-Lutz, A.; Lewkowicz, A.; Fauchille, A.; Michaud, T.; Renault, E.; Xu, L., Spot 2.0: A framework for LTL and \(\omega \)-automata manipulation, (International symposium on automated technology for verification and analysis (2016), Springer), 122-129 |
| [19] | Fan, X.; Arcak, M., Observer design for systems with multivariable monotone nonlinearities, Systems & Control Letters, 50, 4, 319-330 (2003) · Zbl 1157.93330 |
| [20] | Faruq, F.; Parker, D.; Laccrda, B.; Hawes, N., Simultaneous task allocation and planning under uncertainty, (Proceedings of the IEEE/RSJ international conference on intelligent robots and systems (2018)), 3559-3564 |
| [21] | Frederiksen, S. K.S.; Miltersen, P. B., Monomial strategies for concurrent reachability games and other stochastic games, (International workshop on reachability problems (2013), Springer), 122-134 · Zbl 1407.68289 |
| [22] | Girard, A.; Pappas, G. J., Hierarchical control system design using approximate simulation, Automatica, 45, 2, 566-571 (2009) · Zbl 1158.93301 |
| [23] | González-Trejo, J. I.; Hernández-Lerma, O.; Hoyos-Reyes, L. F., Minimax control of discrete-time stochastic systems, SIAM Journal on Control and Optimization, 41, 5, 1626-1659 (2002) · Zbl 1045.90083 |
| [24] | Haesaert, S.; Soudjani, S., Robust Dynamic Programming for Temporal Logic Control of Stochastic Systems, IEEE Transactions on Automatic Control, 66, 2496-2511 (2020) · Zbl 1467.93292 |
| [25] | Haesaert, S.; Soudjani, S.; Abate, A., Verification of general markov decision processes by approximate similarity relations and policy refinement, SIAM Journal on Control and Optimization, 55, 4, 2333-2367 (2017) · Zbl 1367.93615 |
| [26] | Haesaert, S.; Soudjani, S.; Abate, A., Temporal logic control of general Markov decision processes by approximate policy refinement, IFAC-PapersOnLine, 51, 16, 73-78 (2018) |
| [27] | Henzinger, T. A.; de Alfaro, L.; Chatterjee, K., Strategy improvement for concurrent reachability games, (Third international conference on the quantitative evaluation of systems (2006), IEEE), 291-300 |
| [28] | Herceg, M.; Kvasnica, M.; Jones, C. N.; Morari, M., Multi-Parametric Toolbox 3.0, (Proceedings of the European control conference (2013)), 502-510 |
| [29] | Hou, T.; Zhang, W.; Ma, H., A game-based control design for discrete-time Markov jump systems with multiplicative noise, IET Control Theory & Applications, 7, 5, 773-783 (2013) |
| [30] | Kamgarpour, M.; Ding, J.; Summers, S.; Abate, A.; Lygeros, J.; Tomlin, C., Discrete time stochastic hybrid dynamical games: Verification & controller synthesis, (Proceedings of the 50th IEEE conference on decision and control and European control conference (2011)), 6122-6127 |
| [31] | Kamgarpour, M.; Summers, S.; Lygeros, J., Control design for specifications on stochastic hybrid systems, (Proceedings of the 16th international conference on hybrid systems: Computation and control (2013)), 303-312 · Zbl 1364.93263 |
| [32] | Kamgarpour, M.; Wood, T. A.; Summers, S.; Lygeros, J., Control synthesis for stochastic systems given automata specifications defined by stochastic sets, Automatica, 76, 177-182 (2017) · Zbl 1352.93045 |
| [33] | Kattenbelt, M.; Kwiatkowska, M.; Norman, G.; Parker, D., A game-based abstraction-refinement framework for Markov decision processes, Formal Methods in System Design, 36, 3, 246-280 (2010) · Zbl 1233.90276 |
| [34] | Kupferman, O.; Vardi, M. Y., Model checking of safety properties, Formal Methods in System Design, 19, 3, 291-314 (2001) · Zbl 0995.68061 |
| [35] | Kwiatkowska, M. Z., Model checking and strategy synthesis for stochastic games: From theory to practice, (Proceedings of the 43rd international colloquium on automata, languages, and programming (2016)) · Zbl 1388.68186 |
| [36] | Kwiatkowska, M.; Norman, G.; Parker, D., Verification and control of turn-based probabilistic real-time games, (The art of modelling computational systems: A journey from logic and concurrency to security and privacy (2019)), 379-396 · Zbl 1535.68140 |
| [37] | Lavaei, A., Automated verification and control of large-scale stochastic cyber-physical systems: Compositional techniques, 1-268 (2019), Department of Electrical Engineering, Technische Universität München: Department of Electrical Engineering, Technische Universität München Germany, (Ph.D. thesis) |
| [38] | Lavaei, A.; Khaled, M.; Soudjani, S.; Zamani, M., AMYTISS: Parallelized automated controller synthesis for large-scale stochastic systems, (International conference on computer aided verification (2020), Springer), 461-474 · Zbl 1481.93037 |
| [39] | Lavaei, A.; Soudjani, S.; Abate, A.; Zamani, M., Automated verification and synthesis of stochastic hybrid systems: A survey (2022), Automatica · Zbl 1504.93389 |
| [40] | Lavaei, A.; Soudjani, S.; Zamani, M., Compositional construction of infinite abstractions for networks of stochastic control systems, Automatica, 107, 125-137 (2019) · Zbl 1429.93139 |
| [41] | Lavaei, A.; Soudjani, S.; Zamani, M., Compositional abstraction-based synthesis for networks of stochastic switched systems, Automatica, 114 (2020) · Zbl 1441.93322 |
| [42] | Lavaei, A.; Soudjani, S.; Zamani, M., Compositional abstraction of large-scale stochastic systems: A relaxed dissipativity approach, Nonlinear Analysis. Hybrid Systems, 36 (2020) · Zbl 1441.93293 |
| [43] | Lavaei, A.; Soudjani, S.; Zamani, M., Compositional (in)finite abstractions for large-scale interconnected stochastic systems, IEEE Transactions on Automatic Control, 65, 12, 5280-5295 (2020) · Zbl 1536.93850 |
| [44] | Lavaei, A.; Soudjani, S.; Zamani, M., Compositional abstraction-based synthesis of general MDPs via approximate probabilistic relations, Nonlinear Analysis. Hybrid Systems, 39 (2021) · Zbl 1478.93665 |
| [45] | Moon, J.; Başar, T., Discrete-time stochastic Stackelberg dynamic games with a large number of followers, (Proceedings of the IEEE 55th conference on decision and control (2016)), 3578-3583 |
| [46] | Mukaidani, H.; Xu, H., Infinite horizon linear-quadratic Stackelberg games for discrete-time stochastic systems, Automatica, 76, 301-308 (2017) · Zbl 1352.93106 |
| [47] | Nejati, A.; Soudjani, S.; Zamani, M., Compositional abstraction-based synthesis for continuous-time stochastic hybrid systems, European Journal of Control, 57, 82-94 (2021) · Zbl 1455.93190 |
| [48] | Nejati, A.; Zamani, M., Compositional construction of finite MDPs for continuous-time stochastic systems: A dissipativity approach, IFAC-PapersOnLine, 53, 2, 1962-1967 (2020) |
| [49] | Rieder, U., Non-Cooperative Dynamic Games with General Utility Functions, (Stochastic games and related topics: In Honor of Professor L. S. Shapley (1991), Springer Netherlands: Springer Netherlands Dordrecht), 161-174 · Zbl 0742.90098 |
| [50] | Saha, I.; Ramaithitima, R.; Kumar, V.; Pappas, G. J.; Seshia, S. A., Automated composition of motion primitives for multi-robot systems from safe LTL specifications, (Proceedings of the IEEE/RSJ international conference on intelligent robots and systems (2014)), 1525-1532 |
| [51] | Schilders, W., Introduction to model order reduction, (Schilders, W. H.A.; van der Vorst, H. A.; Rommes, J., Model order reduction: Theory, research aspects and applications (2008), Springer), 3-32 · Zbl 1154.93322 |
| [52] | Shreve, S. E., Stochastic optimal control: The discrete time case (1978), Academic Press · Zbl 0471.93002 |
| [53] | Soudjani, S., Formal abstractions for automated verification and synthesis of stochastic systems (2014), Delft Center for Systems and Control, TU Delft, (Ph.D. thesis) |
| [54] | Soudjani, S.; Abate, A.; Majumdar, R., Dynamic Bayesian networks as formal abstractions of structured stochastic processes, (Proceedings of the 26th international conference on concurrency theory, Vol. 42 (2015)), 169-183 · Zbl 1374.68301 |
| [55] | Svoreňová, M.; Křetínskỳ, J.; Chmelík, M.; Chatterjee, K.; Černá, I.; Belta, C., Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games, Nonlinear Analysis. Hybrid Systems, 23, 230-253 (2017) · Zbl 1351.93138 |
| [56] | Tkachev, I.; Mereacre, A.; Katoen, J.-P.; Abate, A., Quantitative Automata-based Controller Synthesis for Non-Autonomous Stochastic Hybrid Systems, (Proceedings of the 16th international conference on hybrid systems: Computation and control (2013)), 293-302 · Zbl 1362.68189 |
| [57] | Toh, K.-C.; Todd, M. J.; Tütüncü, R. H., SDPT3 —a MATLAB software package for semidefinite programming, version 1.3, Optimization Methods & Software, 11, 1-4, 545-581 (1999) · Zbl 0997.90060 |
| [58] | van Huijgevoort, B. C.; Haesaert, S., Similarity quantification for linear stochastic systems as a set-theoretic control problem (2020), arXiv:2007.09052 |
| [59] | Wiltsche, C., Assume-guarantee strategy synthesis for stochastic games (2015), University of Oxford, (Ph.D. thesis) |
| [60] | Zamani, M.; Arcak, M., Compositional abstraction for networks of control systems: A dissipativity approach, IEEE Transactions on Control of Network Systems, 5, 3, 1003-1015 (2018) · Zbl 1515.93137 |
| [61] | Zhong, B.; Lavaei, A.; Zamani, M.; Caccamo, M., Automata-based controller synthesis for stochastic systems: A game framework via approximate probabilistic relations (2022), arXiv:2104.11803v3 |
| [62] | Zhu, Q.; Basar, T., Game-theoretic methods for robustness, security, and resilience of cyberphysical control systems: Games-in-games principle for optimal cross-layer resilient control systems, IEEE Control Systems Magazine, 35, 1, 46-65 (2015) · Zbl 1476.93098 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
