Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems

ABSTRACT

This work deals with Markov processes that are defined over an uncountable state space (possibly hybrid) and embedding non-determinism in the shape of a control structure. The contribution looks at the problem of optimization, over the set of allowed controls, of probabilistic specifications defined by automata - in particular, the focus is on deterministic finite-state automata. This problem can be reformulated as an optimization of a probabilistic reachability property over a product process obtained from the model for the specification and the model of the system. Optimizing over automata-based specifications thus leads to maximal or minimal probabilistic reachability properties. For both setups, the contribution shows that these problems can be sufficiently tackled with history-independent Markov policies. This outcome has relevant computational repercussions: in particular, the work develops a discretization procedure leading into standard optimization problems over Markov decision processes. Such procedure is associated with exact error bounds and is experimentally tested on a case study.

References

1. MoVeS website. http://www.movesproject.eu.
2. A. Abate, S. Amin, M. Prandini, J. Lygeros, and S. Sastry. Computational approaches to reachability analysis of stochastic hybrid systems. In Hybrid Systems: Computation and Control, pages 4--17. Springer Verlag, 2007.
3. A. Abate, J.-P. Katoen, J. Lygeros, and M. Prandini. Approximate model checking of stochastic hybrid systems. European Journal of Control, 16(6):1--18, 2010.
4. A. Abate, J.-P. Katoen, and A. Mereacre. Quantitative automata model checking of autonomous stochastic hybrid systems. In Proceedings of the 14th ACM international conference on Hybrid Systems: Computation and Control, pages 83--92, Chicago, IL, April 2011.
5. A. Abate, M. Prandini, J. Lygeros, and S. Sastry. Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica, 44(11):2724--2734, 2008.
6. C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
7. D. Bertsekas and S. Shreve. Stochastic Optimal Control: The Discrete Time Case, volume 139. Academic Press, 1978.
8. H. Blom and J. Lygeros (Eds.). Stochastic Hybrid Systems: Theory and Safety Critical Applications. Number 337 in Lecture Notes in Control and Information Sciences. Springer Verlag, Berlin Heidelberg, 2006.
9. C. Cassandras and J. E. Lygeros. Stochastic hybrid systems, volume 24. CRC Press, 2007.
10. D. Chatterjee, E. Cinquemani, and J. Lygeros. Maximizing the probability of attaining a target prior to extinction. Nonlinear Analysis: Hybrid Systems, 5(2):367--381, 2011.
11. J. Ding, A. Abate, and C. Tomlin. Optimal control of partially observable discrete time stochastic hybrid systems for safety specifications. Proceedings of the 32nd American Control Conference, 2013.
12. V. Forejt, M. Kwiatkowska, G. Norman, and D. Parker. Automated verification techniques for probabilistic systems. Formal Methods for Eternal Networked Software Systems, pages 53--113, 2011.
13. O. Hernández-Lerma and J. B. Lasserre. Discrete-time Markov control processes, volume 30 of Applications of Mathematics (New York). Springer Verlag, New York, 1996.
14. A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker. PRISM: A tool for automatic verification of probabilistic systems. In H. Hermanns and J. Palsberg, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 3920 of Lecture Notes in Computer Science, pages 441--444. Springer Verlag, 2006.
15. S. Meyn and R. Tweedie. Markov Chains and Stochastic Stability. Springer Verlag, 1993.
16. W. Rudin. Real and complex analysis. McGraw-Hill Book Co., New York, third edition, 1987.
17. S. Soudjani and A. Abate. Adaptive gridding for abstraction and verification of stochastic hybrid systems. In Quantitative Evaluation of Systems (QEST), pages 59--68, Aachen, DE, 2011.
18. S. Summers and J. Lygeros. A Probabilistic Reach-Avoid Problem for Controlled Discrete Time Stochastic Hybrid Systems. In IFAC Conference on Analysis and Design of Hybrid Systems, ADHS, Zaragoza, Spain, September 2009.
19. S. Summers and J. Lygeros. Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem. Automatica, 46(12):1951--1961, 2010.
20. I. Tkachev and A. Abate. On infinite-horizon probabilistic properties and stochastic bisimulation functions. In Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference, pages 526--531, Orlando, FL, December 2011.
21. I. Tkachev and A. Abate. Regularization of Bellman Equations for Infinite-Horizon Probabilistic Properties. In Proceedings of the 15th International Conference on Hybrid Systems: Computation and Control, pages 227--236, Beijing, PRC, April 2012.

Index Terms

• Mathematics of computing

  • Probability and statistics

    • Stochastic processes