Temporal Logic Verification of Stochastic Systems Using Barrier Certificates

  • Pushpak Jagtap
  • Sadegh SoudjaniEmail author
  • Majid Zamani
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)


This paper presents a methodology for temporal logic verification of discrete-time stochastic systems. Our goal is to find a lower bound on the probability that a complex temporal property is satisfied by finite traces of the system. Desired temporal properties of the system are expressed using a fragment of linear temporal logic, called safe LTL over finite traces. We propose to use barrier certificates for computations of such lower bounds, which is computationally much more efficient than the existing discretization-based approaches. The new approach is discretization-free and does not suffer from the curse of dimensionality caused by discretizing state sets. The proposed approach relies on decomposing the negation of the specification into a union of sequential reachabilities and then using barrier certificates to compute upper bounds for these reachability probabilities. We demonstrate the effectiveness of the proposed approach on case studies with linear and polynomial dynamics.


  1. 1.
    Abate, A., Katoen, J.P., Mereacre, A.: Quantitative automata model checking of autonomous stochastic hybrid systems. In: Proceedings of the 14th International Conference on Hybrid systems: Computation and Control, pp. 83–92. ACM (2011)Google Scholar
  2. 2.
    Ayala, A.I.M., Andersson, S.B., Belta, C.: Probabilistic control from time-bounded temporal logic specifications in dynamic environments. In: 2012 IEEE International Conference on Robotics and Automation, pp. 4705–4710 (2012)Google Scholar
  3. 3.
    Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT press, Cambridge (2008)Google Scholar
  4. 4.
    De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: International Joint Conference on Artificial Intelligence, vol. 13, pp. 854–860 (2013)Google Scholar
  5. 5.
    De Giacomo, G., Vardi, M.Y.: Synthesis for LTL and LDL on finite traces. In: International Joint Conference on Artificial Intelligence, vol. 15, pp. 1558–1564 (2015)Google Scholar
  6. 6.
    Dimitrova, R., Majumdar, R.: Deductive control synthesis for alternating-time logics. In: 2014 International Conference on Embedded Software (EMSOFT), pp. 1–10 (2014)Google Scholar
  7. 7.
    Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, É., Xu, L.: Spot 2.0 — a framework for LTL and \(\omega \)-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122–129. Springer, Cham (2016). Scholar
  8. 8.
    Henriksen, J.G., Jensen, J., Jørgensen, M., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: monadic second-order logic in practice. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89–110. Springer, Heidelberg (1995). Scholar
  9. 9.
    Huang, C., Chen, X., Lin, W., Yang, Z., Li, X.: Probabilistic safety verification of stochastic hybrid systems using barrier certificates. ACM Trans. Embed. Comput. Syst. 16(5s), 186 (2017)CrossRefGoogle Scholar
  10. 10.
    Jagtap, P., Zamani, M.: QUEST: a tool for state-space quantization-free synthesis of symbolic controllers. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 309–313. Springer, Cham (2017). Scholar
  11. 11.
    Klein, J., Baier, C.: Experiments with deterministic \(\omega \)-automata for formulas of linear temporal logic. Theor. Comput. Sci. 363(2), 182–195 (2006)Google Scholar
  12. 12.
    Kupferman, O., Vardi, M.: Model checking of safety properties. In: International Conference on Computer Aided Verification, pp. 172–183. Springer, Berlin (1999)CrossRefGoogle Scholar
  13. 13.
    Kushner, H.J.: On the stability of stochastic dynamical systems. Proc. Natl. Acad. Sci. 53(1), 8–12 (1965)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Lahijanian, M., Andersson, S.B., Belta, C.: Formal verification and synthesis for discrete-time stochastic systems. IEEE Trans. Autom. Control 60(8), 2031–2045 (2015)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Lavaei, A., Soudjani, S., Zamani, M.: From dissipativity theory to compositional construction of finite Markov decision processes. In: Hybrid Systems: Computation and Control (HSCC), pp. 21–30. ACM, New York (2018)Google Scholar
  16. 16.
    Maity, D., Baras, J.S.: Motion planning in dynamic environments with bounded time temporal logic specifications. In: 2015 23rd Mediterranean Conference on Control and Automation, pp. 940–946 (2015)Google Scholar
  17. 17.
    Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Postoyan, R., Nesic, D.: Time-triggered control of nonlinear discrete-time systems. In: 2016 IEEE 55th Conference on Decision and Control, pp. 6814–6819 (2016)Google Scholar
  19. 19.
    Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52(8), 1415–1428 (2007)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Prajna, S., Papachristodoulou, A., Parrilo, P.A.: Introducing SOSTOOLS: a general purpose sum of squares programming solver. In: Proceedings of the 41st IEEE Conference on Decision and Control, vol. 1, pp. 741–746 (2002).
  21. 21.
    Russell, S.J., Norvig, P.: Artificial Intelligence: A Modern Approach, 2nd edn. Pearson Education, London (2003)zbMATHGoogle Scholar
  22. 22.
    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. In: 2014 IEEE/RSJ International Conference on Intelligent Robots and Systems, pp. 1525–1532 (2014)Google Scholar
  23. 23.
    Esmaeil Zadeh Soudjani, S., Abate, A.: Precise approximations of the probability distribution of a Markov process in time: an application to probabilistic invariance. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 547–561. Springer, Heidelberg (2014). Scholar
  24. 24.
    Soudjani, S., Abate, A., Majumdar, R.: Dynamic Bayesian networks as formal abstractions of structured stochastic processes. In: 26th International Conference on Concurrency Theory, pp. 1–14. Dagstuhl Publishing, Madrid (2015)Google Scholar
  25. 25.
    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)MathSciNetCrossRefGoogle Scholar
  26. 26.
    Soudjani, S., Gevaerts, C., Abate, A.: FAUST\(^2\): formal abstractions of uncountable-state stochastic processes. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 272–286. Springer, Berlin (2015)Google Scholar
  27. 27.
    Steinhardt, J., Tedrake, R.: Finite-time regional verification of stochastic non-linear systems. Int. J. Robot. Res. 31(7), 901–923 (2012)CrossRefGoogle Scholar
  28. 28.
    Sturm, J.F.: Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optim. Methods Softw. 11(1–4), 625–653 (1999). Scholar
  29. 29.
    Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer Science & Business Media, Berlin (2009)CrossRefGoogle Scholar
  30. 30.
    Tkachev, I., Abate, A.: Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, pp. 283–292. ACM (2013)Google Scholar
  31. 31.
    Vincent, T.L., Yu, J.: Control of a chaotic system. Dyn. Control 1(1), 35–52 (1991)MathSciNetCrossRefGoogle Scholar
  32. 32.
    Wisniewski, R., Bujorianu, M.L.: Stochastic safety analysis of stochastic hybrid systems. In: 2017 IEEE 56th Annual Conference on Decision and Control, pp. 2390–2395 (2017)Google Scholar
  33. 33.
    Wongpiromsarn, T., Topcu, U., Lamperski, A.: Automata theory meets barrier certificates: temporal logic verification of nonlinear systems. IEEE Trans. Autom. Control 61(11), 3344–3355 (2016)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Technical University of MunichMunichGermany
  2. 2.Newcastle UniversityNewcastle upon TyneUnited Kingdom

Personalised recommendations