×

Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. (English) Zbl 1152.93051

Summary: Probabilistic reachability over a finite horizon is investigated for a class of discrete time stochastic hybrid systems with control inputs. A suitable embedding of the reachability problem in a stochastic control framework reveals that it is amenable to two complementary interpretations, leading to dual algorithms for reachability computations. In particular, the set of initial conditions providing a certain probabilistic guarantee that the system will keep evolving within a desired ‘safe’ region of the state space is characterized in terms of a value function, and ‘maximally safe’ Markov policies are determined via dynamic programming. These results are of interest not only for safety analysis and design, but also for solving those regulation and stabilization problems that can be reinterpreted as safety problems. The temperature regulation problem presented in the paper as a case study is one such case.

MSC:

93E03 Stochastic systems in control theory (general)
93B03 Attainable sets, reachability
93C55 Discrete-time control/observation systems
49L20 Dynamic programming in optimal control and differential games

Software:

ToolboxLS; MATISSE
Full Text: DOI

References:

[1] Abate, A., Amin, S., Prandini, M., Lygeros, J., & Sastry, S. (2006). Probabilistic reachability and safe sets computation for discrete time stochastic hybrid systems. In Proceedings of the 45th IEEE conference on decision and control; Abate, A., Amin, S., Prandini, M., Lygeros, J., & Sastry, S. (2006). Probabilistic reachability and safe sets computation for discrete time stochastic hybrid systems. In Proceedings of the 45th IEEE conference on decision and control · Zbl 1178.93069
[2] Alur, R.; Henzinger, T.; Lafferriere, G.; Pappas, G. J., Discrete abstractions of hybrid systems, Proceedings of the IEEE, 88, 2, 971-984 (2000)
[3] Asarin, E.; Bournez, O.; Dang, T.; Maler, O., Approximate reachability analysis of piecewise linear dynamical systems, (Lynch, N.; Krogh, B., Hybrid systems: Computation and control. Hybrid systems: Computation and control, Lecture notes in computer science, Vol. 1790 (2000), Springer Verlag), 21-31 · Zbl 0938.93502
[4] Balluchi, A.; Benvenuti, L.; Di Benedetto, M. D.; Miconi, G. M.; Pozzi, U.; Villa, T., Maximal safe set computation for idle speed control of an automotive engine, (Lynch, N.; Krogh, B., Hybrid systems: Computation and control. Hybrid systems: Computation and control, Lecture notes in computer science, Vol. 1790 (2000), Springer Verlag), 32-44 · Zbl 0962.93070
[5] Belta, C.; Finin, P.; Habets, L.; Halász, A.; Imielinski, M.; Kumar, V., Understanding the bacterial stringent response using reachability analysis of hybrid systems, (Alur, R.; Pappas, G. J., Hybrid systems: Computation and control. Hybrid systems: Computation and control, Lecture notes in computer science, Vol. 2993 (2004), Springer Verlag), 111-126 · Zbl 1135.93334
[6] Bertsekas, D. P., Infinite-time reachability of state-space regions using feedback control, IEEE Transactions on Automatic Control, AC-17, 5, 604-613 (1972) · Zbl 0264.93011
[7] Bertsekas, D. P.; Shreve, S. E., Stochastic optimal control: The discrete-time case (1996), Athena Scientific
[8] Bujorianu, M. L., Extended stochastic hybrid systems and their reachability problem, (Alur, R.; Pappas, G., Hybrid systems: Computation and control. Hybrid systems: Computation and control, Lecture notes in computer science, Vol. 2993 (2004), Springer Verlag), 234-249 · Zbl 1135.93373
[9] Bujorianu, M. L., & Lygeros, J. (2004). General stochastic hybrid systems: Modelling and optimal control. In Proceedings of the 43rd IEEE conference on decision and control; Bujorianu, M. L., & Lygeros, J. (2004). General stochastic hybrid systems: Modelling and optimal control. In Proceedings of the 43rd IEEE conference on decision and control
[10] Davis, M. H.A., Markov models and optimization (1993), Chapman & Hall/CRC Press: Chapman & Hall/CRC Press London · Zbl 0780.60002
[11] Digailova, I. A., & Kurzhanski, A. B. (2005). Reachability analysis under control-dependent stochastic noise. In Proceedings of the 16th IFAC world congress; Digailova, I. A., & Kurzhanski, A. B. (2005). Reachability analysis under control-dependent stochastic noise. In Proceedings of the 16th IFAC world congress
[12] Fehnker, A.; Ivančić, F., Benchmarks for hybrid systems verifications, (Alur, R.; Pappas, G. J., Hybrid systems: Computation and control. Hybrid systems: Computation and control, Lecture notes in computer science, Vol. 2993 (2004), Springer Verlag), 326-341 · Zbl 1135.93324
[13] Ghosh, M. K.; Araposthasis, A.; Marcus, S. I., Ergodic control of switching diffusions, SIAM Journal of Control and Optimization, 35, 6, 1952-1988 (1997) · Zbl 0891.93081
[14] Girard, A., Reachability of uncertain linear systems using zonotopes, (Morari, M.; Thiele, L., Hybrid systems: Computation and control. Hybrid systems: Computation and control, Lecture notes in computer science, Vol. 3414 (2005), Springer Verlag), 291-305 · Zbl 1078.93005
[15] Girard, A., Julius, A., & Pappas, G. J. (2006). Approximate simulation relations for hybrid systems. In Proceedings of the 2nd IFAC conference on analysis and design of hybrid systems; Girard, A., Julius, A., & Pappas, G. J. (2006). Approximate simulation relations for hybrid systems. In Proceedings of the 2nd IFAC conference on analysis and design of hybrid systems · Zbl 1395.93113
[16] Hu, J.; Lygeros, J.; Sastry, S., Towards a theory of stochastic hybrid systems, (Lynch, N.; Krogh, B., Hybrid systems: Computation and control. Hybrid systems: Computation and control, Lecture notes in computer science, Vol. 1790 (2000), Springer Verlag), 160-173 · Zbl 0962.93082
[17] Hu, J.; Prandini, M.; Sastry, S., Aircraft conflict prediction in the presence of a spatially correlated wind field, IEEE Transactions on Intelligent Transportation Systems, 3, 326-340 (2005)
[18] Katoen, J. P., Stochastic model checking, (Cassandras, C. G.; Lygeros, J., Stochastic hybrid systems. Stochastic hybrid systems, Automation and control engineering series, Vol. 24 (2006), Taylor & Francis Group/CRC Press), 79-106
[19] Kumar, P. R.; Varaiya, P. P., Stochastic systems: Estimation, identification, and adaptive control (1986), Prentice Hall, Inc: Prentice Hall, Inc New Jersey · Zbl 0706.93057
[20] Kurzhanski, A. B.; Varaiya, P., On reachability under uncertainty, SIAM Journal of Control and Optimization, 41, 1, 181-216 (2002) · Zbl 1025.34061
[21] Kushner, H. J.; Dupuis, P. G., Numerical methods for stochastic control problems in continuous time (2001), Springer-Verlag: Springer-Verlag New York · Zbl 0968.93005
[22] Lygeros, J., On reachability and minimum cost optimal control, Automatica, 40-6, 317-927 (2004) · Zbl 1068.93011
[23] Lygeros, J.; Tomlin, C.; Sastry, S., Controllers for reachability specifications for hybrid systems, Automatica, 35, 3, 349-370 (1999) · Zbl 0943.93043
[24] Lygeros, J., & Watkins, O. (2003). Stochastic reachability for discrete time systems: an application to aircraft collision avoidance. In Proceedings of the 42nd IEEE conference of decision and control; Lygeros, J., & Watkins, O. (2003). Stochastic reachability for discrete time systems: an application to aircraft collision avoidance. In Proceedings of the 42nd IEEE conference of decision and control
[25] Malhame, R.; Chong, C.-Y., Electric load model synthesis by diffusion approximation of a high-order hybrid-state stochastic system, IEEE Transactions on Automatic Control, 30, 9, 854-860 (1985) · Zbl 0566.93050
[26] Mitchell, I.; Templeton, J., A toolbox of Hamilton-Jacobi solvers for analysis of nondeterministic continuous and hybrid systems, (Morari, M.; Thiele, L., Hybrid systems: Computation and control. Hybrid systems: Computation and control, LNCIS, Vol. 3414 (2005), Springer Verlag), 480-494 · Zbl 1078.93522
[27] Mitchell, I.; Tomlin, C., Level set methods for computation in hybrid systems, (Krogh, B.; Lynch, N., Hybrid systems: Computation and control. Hybrid systems: Computation and control, Lecture notes in computer science (2000), Springer Verlag), 310-323 · Zbl 0952.93006
[28] Picasso, B.; Bicchi, A., Control synthesis for practical stabilization of quantized linear systems, Rendiconti Seminario Matematico Università di Torino, 63, 4, 397-410 (2005) · Zbl 1150.93007
[29] Prajna, S.; Jadbabaie, A.; Pappas, G. J., A framework for worst-case and stochastic safety verification using barrier certificates, IEEE Transactions on Automatic Control, 52, 8, 1415-1429 (2007) · Zbl 1366.93711
[30] Prandini, M.; Hu, J., A stochastic approximation method for reachability computations, (Blom, H. A.P.; Lygeros, J., Stochastic hybrid systems: Theory and safety applications. Stochastic hybrid systems: Theory and safety applications, Lecture notes in control and informations sciences, Vol. 337 (2006), Springer), 107-139 · Zbl 1130.93050
[31] Prandini, M.; Hu, J., Stochastic reachability: Theory and numerical approximation, (Cassandras, C. G.; Lygeros, J., Stochastic hybrid systems. Stochastic hybrid systems, Automation and control engineering series, Vol. 24 (2006), Taylor & Francis Group/CRC Press), 107-138
[32] Prandini, M.; Hu, J.; Lygeros, J.; Sastry, S., A probabilistic approach to aircraft conflict detection, IEEE Transactions on Intelligent Transportation Systems, 1, 4, 199-220 (2000)
[33] Puterman, M. L., Markov decision processes (1994), John Wiley & Sons, Inc · Zbl 0336.93047
[34] Stursberg, O.; Krogh, B. H., Effcient representation and computation of reachable sets for hybrid systems, (Pnueli, A.; Maler, O., Hybrid systems: Computation and control. Hybrid systems: Computation and control, Lecture notes in computer science, Vol. 2623 (2003), Springer Verlag), 482-497 · Zbl 1032.93037
[35] Tomlin, C.; Lygeros, J.; Sastry, S., Synthesizing controllers for nonlinear hybrid systems, (Henzinger, T.; Sastry, S., Hybrid systems: Computation and control. Hybrid systems: Computation and control, Lecture notes in computer science, Vol. 1386 (1998), Springer Verlag), 360-373
[36] Tomlin, C.; Mitchell, I.; Bayen, A.; Oishi, M., Computational techniques for the verification and control of hybrid systems, Proceedings of the IEEE, 91, 7, 986-1001 (2003)
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.