Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
DeepSafe: A Data-Driven Approach for Assessing Robustness of Neural Networks Read chapter Read first chapter

2018 | OriginalPaper | Chapter

Temporal Logic Verification of Stochastic Systems Using Barrier Certificates

Authors : Pushpak Jagtap, Sadegh Soudjani, Majid Zamani

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Synthesis in pMDPs: A Tale of 1001 Parameters
next chapter Bisimilarity Distances for Approximate Differential Privacy
Literature
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)
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)
3.
Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT press, Cambridge (2008)
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)
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)
6.
Dimitrova, R., Majumdar, R.: Deductive control synthesis for alternating-time logics. In: 2014 International Conference on Embedded Software (EMSOFT), pp. 1–10 (2014)
7.
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). https://​doi.​org/​10.​1007/​3-540-60630-0_​5CrossRef
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)CrossRef
10.
11.
Klein, J., Baier, C.: Experiments with deterministic \(\omega \)-automata for formulas of linear temporal logic. Theor. Comput. Sci. 363(2), 182–195 (2006)
12.
Kupferman, O., Vardi, M.: Model checking of safety properties. In: International Conference on Computer Aided Verification, pp. 172–183. Springer, Berlin (1999)CrossRef
13.
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)MathSciNetCrossRef
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)
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)
17.
Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003)MathSciNetCrossRef
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)
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)MathSciNetCrossRef
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). http://​www.​cds.​caltech.​edu/​sostools/​
21.
Russell, S.J., Norvig, P.: Artificial Intelligence: A Modern Approach, 2nd edn. Pearson Education, London (2003)MATH
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)
23.
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)
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)MathSciNetCrossRef
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)
27.
Steinhardt, J., Tedrake, R.: Finite-time regional verification of stochastic non-linear systems. Int. J. Robot. Res. 31(7), 901–923 (2012)CrossRef
28.
29.
Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer Science & Business Media, Berlin (2009)CrossRef
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)
31.
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)
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)MathSciNetCrossRef
Metadata
Title
Temporal Logic Verification of Stochastic Systems Using Barrier Certificates
Authors
Pushpak Jagtap
Sadegh Soudjani
Majid Zamani
Copyright Year
2018
Book
Automated Technology for Verification and Analysis

Print ISBN: 978-3-030-01089-8

Electronic ISBN: 978-3-030-01090-4

Copyright Year: 2018

DOI
https://doi.org/10.1007/978-3-030-01090-4_11

Premium Partner

    Image Credits