Skip to main content
SpringerLink
Log in

Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs

  • Conference paper
Book cover Automated Deduction – CADE-23 (CADE 2011)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6803))

Included in the following conference series:

Abstract

Logic is a powerful tool for analyzing and verifying systems, including programs, discrete systems, real-time systems, hybrid systems, and distributed systems. Some applications also have a stochastic behavior, however, either because of fundamental properties of nature, uncertain environments, or simplifications to overcome complexity. Discrete probabilistic systems have been studied using logic. But logic has been chronically underdeveloped in the context of stochastic hybrid systems, i.e., systems with interacting discrete, continuous, and stochastic dynamics. We aim at overcoming this deficiency and introduce a dynamic logic for stochastic hybrid systems. Our results indicate that logic is a promising tool for understanding stochastic hybrid systems and can help taming some of their complexity. We introduce a compositional model for stochastic hybrid systems. We prove adaptivity, càdlàg, and Markov time properties, and prove that the semantics of our logic is measurable. We present compositional proof rules, including rules for stochastic differential equations, and prove soundness.

This material is based upon work supported by the National Science Foundation by NSF CAREER Award CNS-1054246, NSF EXPEDITION CNS-0926181, CNS-0931985, CNS-1035800, by ONR N00014-10-1-0188 and DARPA FA8650-10C-7077.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), 2724–2734 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  2. Bujorianu, M.L., Lygeros, J.: Towards a general theory of stochastic hybrid systems. In: Blom, H.A.P., Lygeros, J. (eds.) Stochastic Hybrid Systems: Theory and Safety Critical Applications. Lecture Notes Contr. Inf., vol. 337, pp. 3–30. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. Cassandras, C.G., Lygeros, J. (eds.): Stochastic Hybrid Systems. CRC, Boca Raton (2006)

    Google Scholar 

  4. Dutertre, B.: Complete proof systems for first order interval temporal logic. In: LICS, pp. 36–43. IEEE Computer Society, Los Alamitos (1995)

    Google Scholar 

  5. Dynkin, E.B.: Markov Processes. Springer, Heidelberg (1965)

    Book  MATH  Google Scholar 

  6. Feldman, Y.A., Harel, D.: A probabilistic dynamic logic. J. Comput. Syst. Sci. 28(2), 193–215 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  7. Fränzle, M., Teige, T., Eggers, A.: Engineering constraint solvers for automatic analysis of probabilistic hybrid automata. J. Log. Algebr. Program. 79(7), 436–466 (2010)

    Article  MATH  MathSciNet  Google Scholar 

  8. Ghosh, M.K., Arapostathis, A., Marcus, S.I.: Ergodic control of switching diffusions. SIAM J. Control Optim. 35(6), 1952–1988 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  9. Hu, J., Lygeros, J., Sastry, S.: Towards a theory of stochastic hybrid systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 160–173. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  10. Karatzas, I., Shreve, S.: Brownian Motion and Stochastic Calculus. Springer, Heidelberg (1991)

    MATH  Google Scholar 

  11. Kloeden, P.E., Platen, E.: Numerical Solution of Stochastic Differential Equations. Springer, New York (2010)

    MATH  Google Scholar 

  12. Koutsoukos, X.D., Riley, D.: Computational methods for verification of stochastic hybrid systems. IEEE T. Syst. Man, Cy. A 38(2), 385–396 (2008)

    Article  Google Scholar 

  13. Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328–350 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  14. Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162–178 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  15. Kushner, H.J. (ed.): Stochastic Stability and Control. Academic Press, New York (1967)

    MATH  Google Scholar 

  16. Kwiatkowska, M.Z., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 23–37. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  17. Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027–1077 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  18. Bevilacqua, V., Sharykin, R.: Specification and analysis of distributed object-based stochastic hybrid systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 460–475. Springer, Heidelberg (2006)

    Google Scholar 

  19. Øksendal, B.: Stochastic Differential Equations: An Introduction with Applications. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  20. Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309–352 (2010)

    Article  MATH  MathSciNet  Google Scholar 

  21. Platzer, A.: Quantified differential dynamic logic for distributed hybrid systems. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 469–483. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  22. Platzer, A.: Stochastic differential dynamic logic for stochastic hybrid systems. Tech. Rep. CMU-CS-11-111, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA (2011)

    Google Scholar 

  23. Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE T. Automat. Contr. 52(8), 1415–1429 (2007)

    Article  MathSciNet  Google Scholar 

  24. Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: FOCS, pp. 109–121. IEEE, Los Alamitos (1976)

    Google Scholar 

  25. Richardson, M., Domingos, P.: Markov logic networks. Machine Learning 62(1-2), 107–136 (2006)

    Article  Google Scholar 

  26. Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1951)

    MATH  Google Scholar 

  27. Younes, H.L.S., Kwiatkowska, M.Z., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. STTT 8(3), 216–228 (2006)

    Article  MATH  Google Scholar 

  28. Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Simulink/Stateflow verification. In: Johansson, K.H., Yi, W. (eds.) HSCC, pp. 243–252. ACM, New York (2010)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

    André Platzer

Authors
  1. André Platzer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research, One Microsoft Way, 98052-6399, Redmond, WA, USA

    Nikolaj Bjørner

  2. Max-Planck-Institut für Informatik, Campus E 1.4, 66123, Saarbrücken, Germany

    Viorica Sofronie-Stokkermans

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Platzer, A. (2011). Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs. In: Bjørner, N., Sofronie-Stokkermans, V. (eds) Automated Deduction – CADE-23. CADE 2011. Lecture Notes in Computer Science(), vol 6803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22438-6_34

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22438-6_34

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22437-9

  • Online ISBN: 978-3-642-22438-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation