Advertisement

Constraint-Solving Techniques for the Analysis of Stochastic Hybrid Systems

  • Martin FränzleEmail author
  • Yang Gao
  • Sebastian Gerwinn
Chapter
Part of the NASA Monographs in Systems and Software Engineering book series (NASA)

Abstract

The ProCoS project has been seminal in widening the perspective on verification of computer-based systems to a coverage of the detailed interaction and feedback dynamics between the embedded system and its environment. We have since then seen a steady increase both in expressiveness of the “hybrid” modeling paradigms adopting such an integrated perspective and in the power of automatic reasoning techniques addressing relevant fragments of logic and arithmetic. In this chapter we review definitions of stochastic hybrid automata and of parametric stochastic hybrid automata, both of which unify the hybrid view on system dynamics with stochastic modeling as pertinent to reliability evaluation, and we elaborate on automatic verification and synthesis methods based on arithmetic constraint solving. The procedures are able to solve step-bounded stochastic reachability problems and multi-objective parameter synthesis problems, respectively.

Keywords

Importance Sampling Markov Decision Process Constraint System Proposal Distribution Hybrid Automaton 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems. Lecture Notes in Computer Science, vol. 736, pp. 209–229. Springer, New York (1993)Google Scholar
  2. 2.
    Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138, 3–34 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Audemard, G., Bozzano, M., Cimatti, A., Sebastiani, R.: Verifying industrial hybrid systems with MathSAT. ENTCS 89(4) (2004)Google Scholar
  4. 4.
    Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere et al. [7], chap. 26, pp. 825–885Google Scholar
  5. 5.
    Bellman, R.: A Markovian decision process. J. Math. Mech. 6, 679–684 (1957)MathSciNetzbMATHGoogle Scholar
  6. 6.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: TACAS’99. Lecture Notes in Computer Science, vol. 1579, pp. 193–207. Springer, New York (1999)Google Scholar
  7. 7.
    Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)Google Scholar
  8. 8.
    Bousquet, O., Boucheron, S., Lugosi, G.: Introduction to statistical learning theory. Advanced Lectures on Machine Learning, pp. 169–207. Springer, New York (2004)Google Scholar
  9. 9.
    Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Chaochen, Z., Ravn, A.P., Hansen, M.R.: An extended duration calculus for hybrid real-time systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems. Lecture Notes in Computer Science, vol. 736, pp. 36–59. Springer, New York (1992)Google Scholar
  11. 11.
    Eggers, A., Fränzle, M., Herde, C.: SAT modulo ODE: a direct SAT approach to hybrid systems. In: Cha, S.S., Choi, J.Y., Kim, M., Lee, I., Viswanathan, M. (eds.) Proceedings of the 6th International Symposium on Automated Technology for Verification and Analysis (ATVA’08). Lecture Notes in Computer Science, vol. 5311, pp. 171–185. Springer, New York (2008)Google Scholar
  12. 12.
    Fränzle, M., Herde, C.: Efficient proof engines for bounded model checking of hybrid systems. In: Ninth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 04), Electronic Notes in Theoretical Computer Science (ENTCS). Elsevier (2004)Google Scholar
  13. 13.
    Fränzle, M., Herde, C., Ratschan, S., Schubert, T., Teige, T.: Interval constraint solving using propositional SAT solving techniques. In: Proceedings of the CP 2006 First International Workshop on the Integration of SAT and CP Techniques, pp. 81–95 (2006)Google Scholar
  14. 14.
    Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. JSAT 1(3–4), 209–236 (2007)zbMATHGoogle Scholar
  15. 15.
    Fränzle, M., Hermanns, H., Teige, T.: Stochastic satisfiability modulo theory: a novel technique for the analysis of probabilistic hybrid systems. In: Egerstedt, M., Mishra, B. (eds.) Proceedings of the 11th International Conference on Hybrid Systems: Computation and Control (HSCC’08). Lecture Notes in Computer Science (LNCS), vol. 4981, pp. 172–186. Springer, New York (2008)Google Scholar
  16. 16.
    Fränzle, M., Teige, T., Eggers, A.: Engineering constraint solvers for automatic analysis of probabilistic hybrid automata. J. Logic Algebr. Program. 79, 436–466 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Fränzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurability and safety verification for stochastic hybrid systems. In: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, pp. 43–52. ACM (2011)Google Scholar
  18. 18.
    Fränzle, M., Gerwinn, S., Kröger, P., Abate, A., Katoen, J.: Multi-objective parameter synthesis in probabilistic hybrid systems. In: Sankaranarayanan, S., Vicario, E. (eds.) Formal Modeling and Analysis of Timed Systems - 13th International Conference, FORMATS 2015, Madrid, Spain, 2–4 September 2015, Proceedings. Lecture Notes in Computer Science, vol. 9268, pp. 93–107. Springer, New York (2015)Google Scholar
  19. 19.
    Gao, Y., Fränzle, M.: A solving procedure for stochastic satisfiability modulo theories with continuous domain. In: Campos, J., Haverkort, B.R. (eds.) Quantitative Evaluation of Systems, 12th International Conference, QEST 2015, Madrid, Spain, 1–3 September 2015, Proceedings. Lecture Notes in Computer Science, vol. 9259, pp. 295–311. Springer, New York (2015)Google Scholar
  20. 20.
    Granvilliers, L., Benhamou, F.: Realpaver: an interval solver using constraint satisfaction techniques. ACM Trans. Math. Softw. (TOMS) 32(1), 138–156 (2006)Google Scholar
  21. 21.
    Groote, J.F., Koorn, J.W.C., van Vlijmen, S.F.M.: The safety guaranteeing system at station Hoorn-Kersenboogerd. In: Conference on Computer Assurance, pp. 57–68. National Institute of Standards and Technology (1995)Google Scholar
  22. 22.
    Henzinger, T.A.: The theory of hybrid automata. In: Inan, M., Kurshan, R. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series F: Computer and Systems Sciences, vol. 170, pp. 265–292. Springer, New York (2000)Google Scholar
  23. 23.
    Herde, C., Eggers, A., Fränzle, M., Teige, T.: Analysis of hybrid systems using HySAT. In: The Third International Conference on Systems (ICONS 2008), pp. 196–201. IEEE Computer Society (2008)Google Scholar
  24. 24.
    Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58, 13–30 (1963)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Julius, A.A.: Approximate abstraction of stochastic hybrid automata. In: Hespanha, J.P., Tiwari, A. (eds.) Hybrid Systems: Computation and Control: 9th International Workshop, HSCC 2006, Santa Barbara, CA, USA, 29–31 March 2006. Proceedings. Lecture Notes in Computer Science, vol. 3927, pp. 318–332. Springer, New York (2006)Google Scholar
  26. 26.
    Lee, E.A., Zheng, H.: Operational semantics of hybrid systems. In: Morari, M., Thiele, L. (eds.) HSCC’05. Lecture Notes in Computer Science, vol. 3414. Springer, New York (2005)Google Scholar
  27. 27.
    Littman, M.L., Majercik, S.M., Pitassi, T.: Stochastic boolean satisfiability. J. Autom. Reason. 27(3), 251–296 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Majercik, S.M.: Stochastic boolean satisfiability. In: Biere et al. [7], chap. 27, pp. 887–925Google Scholar
  29. 29.
    Majercik, S.M., Littman, M.L.: Maxplan: a new approach to probabilistic planning. AIPS 98, 86–93 (1998)Google Scholar
  30. 30.
    Majercik, S.M., Littman, M.L.: Contingent planning under uncertainty via stochastic satisfiability. In: AAAI/IAAI, pp. 549–556 (1999)Google Scholar
  31. 31.
    McDiarmid, C.: On the method of bounded differences. Surv. Comb. 141(1), 148–188 (1989)MathSciNetzbMATHGoogle Scholar
  32. 32.
    Miller, R.G.: Simultaneous Statistical Inference. Springer, New York (1981)CrossRefzbMATHGoogle Scholar
  33. 33.
    Papadimitriou, C.H.: Games against nature. J. Comput. Syst. Sci. 31(2), 288–301 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  34. 34.
    Ravn, A.P., Rischel, H.: Requirements capture for embedded real-time systems. In: Proceedings of IMACS-MCTS’91 Symposium on Modelling and Control of Technological Systems, Villeneuve d’Ascq, France, 7–10 May, vol. 2, pp. 147–152. IMACS (1991)Google Scholar
  35. 35.
    Sproston, J.: Decidable model checking of probabilistic hybrid automata. In: Joseph, M. (ed.) Formal Techniques in Real-Time and Fault-Tolerant Systems. Lecture Notes in Computer Science, vol. 1926, pp. 31–45. Springer, New York (2000)Google Scholar
  36. 36.
    Sproston, J.: Model checking for probabilistic timed and hybrid systems. Ph.D. thesis, University of Birmingham (2001)Google Scholar
  37. 37.
    Teige, T.: Stochastic satisfiability modulo theories: a symbolic technique for the analysis of probabilistic hybrid systems. Ph.D. thesis, Universität Oldenburg (2012)Google Scholar
  38. 38.
    Teige, T., Fränzle, M.: Stochastic satisfiability modulo theories for non-linear arithmetic. Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, pp. 248–262. Springer, New York (2008)Google Scholar
  39. 39.
    Tokdar, S.T., Kass, R.E.: Importance sampling: a review. Wiley Interdiscip. Rev.: Comput. Stat. 2(1), 54–60 (2010)CrossRefGoogle Scholar
  40. 40.
    Tseitin, G.: On the complexity of derivations in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logics (1968)Google Scholar
  41. 41.
    Vapnik, V.N.: Statistical Learning Theory, vol. 1. Wiley, New York (1998)zbMATHGoogle Scholar
  42. 42.
    Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Computer Aided Verification, 14th International Conference, CAV 2002, Copenhagen, Denmark, 27–31 July 2002, Proceedings, pp. 223–235 (2002)Google Scholar
  43. 43.
    Zhang, L., She, Z., Ratschan, S., Hermanns, H., Hahn, E.M.: Safety verification for probabilistic hybrid systems. In: Proceedings of the 22nd International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 6174, pp. 196–211. Springer, New York (2010)Google Scholar
  44. 44.
    Zhang, Y., Sankaranarayanan, S., Somenzi, F.: Statistically sound verification and optimization for complex systems. In: Cassez, F., Raskin, J.F. (eds.) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 8837, pp. 411–427. Springer, New York (2014)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Department of Computing ScienceCarl von Ossietzky Universität OldenburgOldenburgGermany
  2. 2.OFFIS Institute for Information TechnologyOldenburgGermany

Personalised recommendations