Generalized Craig Interpolation for Stochastic Satisfiability Modulo Theory Problems

  • Ahmed Mahdi
  • Martin Fränzle
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8762)

Abstract

Craig interpolation is widely used in solving reachability and model-checking problems by SAT or SMT techniques, as it permits the computation of invariants as well as discovery of meaningful predicates in CEGAR loops based on predicate abstraction. Extending such algorithms from the qualitative to the quantitative setting of probabilistic models seems desirable. In 2012, Teige et al. [1] succeeded to define an adequate notion of generalized, stochastic interpolants and to expose an algorithm for efficiently computing them for stochastic Boolean satisfiability problems, i.e., SSAT. In this work we present a notion of Generalized Craig Interpolant for the stochastic SAT modulo theories framework, i.e., SSMT, and introduce a mechanism to compute such stochastic interpolants for non-polynomial SSMT problems based on a sound and, w.r.t. the arithmetic reasoner, relatively complete resolution calculus. The algorithm computes interpolants in SAT, SMT, SSAT, and SSMT problems. As this extends the scope of SSMT-based model-checking of probabilistic hybrid automata from the bounded to the unbounded case, we demonstrate our interpolation principle on an unbounded probabilistic reachability problem in a probabilistic hybrid automaton.

Keywords

Linear Order Satisfying Assignment Reachability Problem Predicate Abstraction Safety Target 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Teige, T., Fränzle, M.: Generalized Craig interpolation. Logical Methods in Computer Science 8(2) (2012)Google Scholar
  2. 2.
    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.) HSCC 2008. LNCS, vol. 4981, pp. 172–186. Springer, Heidelberg (2008)Google Scholar
  3. 3.
    Papadimitriou, C.H.: Games against nature. J. Comput. Syst. Sci. 31(2), 288–301 (1985)MathSciNetCrossRefMATHGoogle Scholar
  4. 4.
    Teige, T.: Stochastic Satisfiability Modulo Theories: A Symbolic Technique for the Analysis of Probabilistic Hybrid Systems. PhD thesis, Dpt. of Computing Science, Carl von Ossietzky Universität, Oldenburg, Germany (August 2012)Google Scholar
  5. 5.
    Majercik, S.M., Littman, M.L.: Maxplan: A new approach to probabilistic planning. In: Simmons, R.G., Veloso, M.M., Smith, S.F. (eds.) AIPS, pp. 86–93. AAAI (1998)Google Scholar
  6. 6.
    Majercik, S.M., Littman, M.L.: Contingent planning under uncertainty via stochastic satisfiability. Artif. Intell. 147(1-2), 119–162 (2003)MathSciNetCrossRefMATHGoogle Scholar
  7. 7.
    Bacchus, F., Dalmao, S., Pitassi, T.: DPLL with caching: A new algorithm for #sat and Bayesian inference. Electronic Colloquium on Computational Complexity (ECCC) 10(003) (2003)Google Scholar
  8. 8.
    Freudenthal, E., Karamcheti, V.: QTM: Trust management with quantified stochastic attributes. Technical Report NYU Computer Science Technical Report TR2003-848, Courant Institute of Mathematical Sciences, New York University (2003)Google Scholar
  9. 9.
    Teige, T., Eggers, A., Fränzle, M.: Constraint-based analysis of concurrent probabilistic hybrid systems: An application to networked automation systems. Nonlinear Analysis: Hybrid Systems 5(2), 343–366 (2011)MathSciNetMATHGoogle Scholar
  10. 10.
    Mahdi, A., Fränzle, M.: Resolution for stochastic SAT modulo theories. Technical report, Dpt. of Computing Science, Carl von Ossietzky Universität Oldenburg, Germany (December 2013)Google Scholar
  11. 11.
    Benhamou, F., Granvilliers, L.: Combining local consistency, symbolic rewriting and interval methods. In: Pfalzgraf, J., Calmet, J., Campbell, J. (eds.) AISMC 1996. LNCS, vol. 1138, pp. 144–159. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  12. 12.
    Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log. 62(3), 981–998 (1997)CrossRefMATHGoogle Scholar
  13. 13.
    Kupferschmid, S., Becker, B.: Craig interpolation in the presence of non-linear constraints. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 240–255. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  14. 14.
    McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  15. 15.
    Christ, J., Hoenicke, J., Nutz, A.: Proof tree preserving interpolation. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 124–138. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  16. 16.
    Brillout, A., Kroening, D., Wahl, T.: Craig interpolation for quantifier-free Presburger arithmetic. CoRR abs/0811.3521 (2008)Google Scholar
  17. 17.
    Griggio, A., Le, T.T.H., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo linear integer arithmetic. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 143–157. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  18. 18.
    Goel, A., Krstić, S., Tinelli, C.: Ground interpolation for combined theories. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 183–198. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  19. 19.
    Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log. 12(1), 7 (2010)MathSciNetCrossRefGoogle Scholar
  20. 20.
    Lynch, C., Tang, Y.: Interpolants for linear arithmetic in SMT. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 156–170. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  21. 21.
    Vizel, Y., Ryvchin, V., Nadel, A.: Efficient generation of small interpolants in CNF. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 330–346. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  22. 22.
    Mahdi, A., Fränzle, M.: Generalized Craig interpolation for SSMT. Technical report, Dpt. of Comuting Sceince, Carl von Ossietzky Universität, Oldenburg, Germany (2014)Google Scholar
  23. 23.
    Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970, pp. 466–483. Springer, Heidelberg (1983)CrossRefGoogle Scholar
  24. 24.
    Fränzle, M., Herde, C., Ratschan, S., Schubert, T., Teige, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. Journal on Satisfiability, Boolean Modeling and Computation – Special Issue on SAT/CP Integration 1, 209–236 (2007)Google Scholar
  25. 25.
    Teige, T., Fränzle, M.: Resolution for stochastic boolean satisfiability. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 625–639. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  26. 26.
    Benhamou, F., McAllester, D.A., Van Hentenryck, P.: CLP(Intervals) revisited. In: ILPS, pp. 124–138. MIT Press (1994)Google Scholar
  27. 27.
    Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log. 22(3), 269–285 (1957)MathSciNetCrossRefMATHGoogle Scholar
  28. 28.
    Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with craig interpolation and symbolic pushdown systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 489–503. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  29. 29.
    Cooper, D.C.: Theorem proving in arithmetic without multiplication. Machine Intelligence 7, 91–99 (1972)MATHGoogle Scholar
  30. 30.
    Ferrante, J., Rackoff, C.: A decision procedure for the first order theory of real addition with order. SIAM J. Comput. 4(1), 69–76 (1975)MathSciNetCrossRefMATHGoogle Scholar
  31. 31.
    Tarski, A.: A decision method for elementary algebra and geometry. RAND Corporation, Santa Monica, Calif. (1948)Google Scholar
  32. 32.
    Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1/2), 29–35 (1988)MathSciNetCrossRefMATHGoogle Scholar
  33. 33.
    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.) ATVA 2008. LNCS, vol. 5311, pp. 171–185. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  34. 34.
    Zhang, L., She, Z., Ratschan, S., Hermanns, H., Hahn, E.M.: Safety verification for probabilistic hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 196–211. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  35. 35.
    Fränzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurability and safety verification for stochastic hybrid systems. In: HSCC, pp. 43–52. ACM (2011)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Ahmed Mahdi
    • 1
  • Martin Fränzle
    • 1
  1. 1.Carl von Ossietzky UniversitätOldenburgGermany

Personalised recommendations