Efficiency through uncertainty: scalable formal synthesis for stochastic hybrid systems

ABSTRACT

This work targets the development of an efficient abstraction method for formal analysis and control synthesis of discrete-time stochastic hybrid systems (SHS) with linear dynamics. The focus is on temporal logic specifications over both finite- and infinite-time horizons. The framework constructs a finite abstraction as a class of uncertain Markov models known as interval Markov decision process (IMDP). Then, a strategy that maximizes the satisfaction probability of the given specification is synthesized over the IMDP and mapped to the underlying SHS. In contrast to existing formal approaches, which are by and large limited to finite-time properties and rely on conservative over-approximations, we show that the exact abstraction error can be computed as a solution of convex optimization problems and can be embedded into the IMDP abstraction. This is later used in the synthesis step over both bounded- and unbounded-time properties, mitigating the known state-space explosion problem. Our experimental validation of the new approach compared to existing abstraction-based approaches shows: (i) significant (orders of magnitude) reduction of the abstraction error; (ii) marked speed-ups; and (iii) boosted scalability, allowing in particular to verify models with more than 10 continuous variables.

References

1. Alessandro Abate, Maria Prandini, John Lygeros, and Shankar Sastry. 2008. Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44, 11 (2008), 2724--2734.
2. Alessandro Abate, Frank Redig, and Ilya Tkachev. 2014. On the effect of perturbation of conditional probabilities in total variation. Statistics & Probability Letters 88 (2014), 1--8.
3. Christel Baier, Joost-Pieter Katoen, et al. 2008. Principles of model checking. Vol. 26202649. MIT press Cambridge.
4. Dimitri P Bertsekas. 2014. Constrained optimization and Lagrange multiplier methods. Academic press.
5. H.A.P. Blom and J. Lygeros (Eds.). 2006. Stochastic Hybrid Systems: Theory and Safety Critical Applications. Number 337 in Lecture Notes in Control and Information Sciences. Springer Verlag, Berlin Heidelberg.
6. Luca Cardelli, Marta Kwiatkowska, and Luca Laurenti. 2016. A Stochastic Hybrid Approximation for Chemical Kinetics Based on the Linear Noise Approximation. In Int. Conf. on Computational Methods in Systems Biology. Springer, 147--167.
7. C.G. Cassandras and J. Lygeros (Eds.). 2006. Stochastic Hybrid Systems. Number 24 in Control Engineering. CRC Press, Boca Raton.
8. Sadegh Esmaeil Zadeh Soudjani and Alessandro Abate. 2013. Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM Journal on Applied Dynamical Systems 12, 2 (2013), 921--956.
9. Sadegh Esmaeil Zadeh Soudjani, Caspar Gevaerts, and Alessandro Abate. 2015. FAUST²: Formal Abstractions of Uncountable-STate STochastic Processes.. In TACAS, Vol. 15. 272--286.
10. Robert Givan, Sonia Leach, and Thomas Dean. 2000. Bounded-parameter Markov decision processes. Artificial Intelligence 122, 1--2 (2000), 71--109.
11. Branko Grünbaum, Victor Klee, Micha A Perles, and Geoffrey Colin Shephard. 1967. Convex polytopes. Vol. 16. Springer.
12. Ernst Moritz Hahn, Vahid Hashemi, Holger Hermanns, Morteza Lahijanian, and Andrea Turrini. 2017. Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes. In Int. Conf. on Quantitative Evaluation of SysTems (QEST). Springer, Berlin, Germany, 207--223.
13. Mohammad Hekmatnejad and Georgios Fainekos. 2018. Optimal Multi-Valued LTL Planning for Systems with Access Right Levels. In 2018 Annual American Control Conf. (ACC). IEEE, 2363--2370.
14. Sumit K Jha, Edmund M Clarke, Christopher J Langmead, Axel Legay, André Platzer, and Paolo Zuliani. 2009. A bayesian approach to model checking biological systems. In CMSB. Springer, 218--234.
15. Orna Kupferman and Moshe Y. Vardi. 2001. Model Checking of Safety Properties. Formal Methods in System Design 19 (2001), 291--314. Issue 3.
16. Morteza Lahijanian, Sean B Andersson, and Calin Belta. 2012. Approximate Markovian abstractions for linear stochastic systems. In IEEE Conf. on Decision and Control (CDC),. IEEE, 5966--5971.
17. Morteza Lahijanian, Sean B Andersson, and Calin Belta. 2015. Formal verification and synthesis for discrete-time stochastic systems. IEEE Trans. Automat. Control 60, 8 (2015), 2031--2045.
18. Luca Laurenti, Alessandro Abate, Luca Bortolussi, Luca Cardelli, Milan Ceska, and Marta Kwiatkowska. 2017. Reachability Computation for Switching Diffusions: Finite Abstractions with Certifiable and Tuneable Precision. In Proceedings of the 20th Int. Conf. on Hybrid Systems: Computation and Control. ACM, 55--64.
19. Ryan Luna, Morteza Lahijanian, Mark Moll, and Lydia E. Kavraki. 2014. Asymptotically Optimal Stochastic Motion Planning with Temporal Goals. In Int'l Workshop on the Algorithmic Foundations of Robotics (WAFR). Istanbul, Turkey, 335--352.
20. András Prékopa. 1971. Logarithmic concave measures with application to stochastic programming. Acta Scientiarum Mathematicarum 32 (1971), 301--316.
21. Abraham P Vinod, Baisravan Homchaudhuri, and Meeko MK Oishi. 2017. Forward stochastic reachability analysis for uncontrolled linear systems using Fourier transforms. In Proceedings of the 20th Int. Conf. on Hybrid Systems: Computation and Control. ACM, 35--44.
22. Di Wu and Xenofon Koutsoukos. 2008. Reachability analysis of uncertain systems using bounded-parameter Markov decision processes. Artificial Intelligence 172, 8--9 (2008), 945--954.
23. George Yin and Chao Zhu. 2010. Hybrid switching diffusions: properties and applications. Vol. 63. Springer New York.

Index Terms

• Computer systems organization

  • Embedded and cyber-physical systems

    • Embedded systems

• Mathematics of computing

  • Probability and statistics

    • Stochastic processes

      • Markov processes