Uncertainty Propagation Using Probabilistic Affine Forms and Concentration of Measure Inequalities

详细信息    查看全文

• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：9636
• 期：1
• 页码：225-243
• 全文大小：479 KB
• 参考文献：1.Abate, A., Katoen, J., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. Eur. J. Control 6, 624–641 (2010)MathSciNet CrossRef MATH
  2.Adje, A., Bouissou, O., Goubault-Larrecq, J., Goubault, E., Putot, S.: Static analysis of programs with imprecise probabilistic inputs. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 22–47. Springer, Heidelberg (2014)CrossRef
  3.Auer, E., Luther, W., Rebner, G., Limbourg, P.: A verified matlab toolbox for the dempster-shafer theory. In: Workshop on the Theory of Belief Functions (2010)
  4.Borges, M., Filieri, A., d’Amorim, M., Păsăreanu, C.S., Visser, W.: Compositional solution space quantification for probabilistic software analysis (2014)
  5.Bornholt, J., Mytkowicz, T., McKinley, K.S.: Uncertain\({<\!{\rm T}\!>}\) : abstractions for uncertain hardware and software. IEEE Micro. 35(3), 132–143 (2015)CrossRef
  6.Bose, T., Trimper, S.: Stochastic model for tumor growth with immunization. Phys. Rev. E 79, 051903 (2009)MathSciNet CrossRef
  7.Bouissou, O., Goubault, E., Goubault-Larrecq, J., Putot, S.: A generalization of p-boxes to affine arithmetic. Computing 94(2–4), 189–201 (2012)MathSciNet CrossRef MATH
  8.Busaba, J., Suwan, S., Kosheleva, O.: A faster algorithm for computing the sum of p-boxes. J. Uncertain Syst. 4(4), 244–249 (2010)
  9.Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511–526. Springer, Heidelberg (2013)CrossRef
  10.Chistikov, D., Dimitrova, R., Majumdar, R.: Approximate counting in SMT and value estimation for probabilistic programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 320–334. Springer, Heidelberg (2015)
  11.Cousot, P., Monerau, M.: Probabilistic abstract interpretation. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 169–193. Springer, Heidelberg (2012)CrossRef
  12.De Loera, J., Dutra, B., Koeppe, M., Moreinis, S., Pinto, G., Wu, J.: Software for Exact Integration of Polynomials over Polyhedra. ArXiv e-prints, July 2011
  13.Dubhashi, D., Panconesi, A.: Concentration of Measure for the Analysis of Randomized Algorithms. Cambridge University Press, Cambridge (2009)CrossRef MATH
  14.Durrett, R.: Probability. Theory and Examples. Wadsworth & Brooks/Cole, Belmont (1991)MATH
  15.Enszer, J., Lin, Y., Ferson, S., Corliss, G., Stadtherr, M.: Probability bounds analysis for nonlinear dynamic process models. AIChE J. 57, 404–422 (2011)CrossRef
  16.Ferson, S.: RAMAS Risk Calc 4.0 Software: Risk Assessment with Uncertain Numbers. Lewis Publishers, Boca Raton (2002)
  17.Ferson, S., Kreinovich, V., Ginzburg, L., Myers, D., Sentz, K.: Constructing probability boxes and Dempster-Shafer structures. Technical report SAND2002-4015, Sandia National Laboratories (2003)
  18.Fuchs, M., Neumaier, A.: Potential based clouds in robust design optimization. J. Stat. Theo. Pract. 3, 225–238 (2009)MathSciNet CrossRef MATH
  19.Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: ISSTA, pp. 166–176. ACM (2012)
  20.Goubault, É., Putot, S.: Static analysis of numerical algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 18–34. Springer, Heidelberg (2006)CrossRef
  21.Goubault-Larrecq, J.: Continuous previsions. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 542–557. Springer, Heidelberg (2007)CrossRef
  22.Janson, S.: Large deviations for sums of partly dependent random variables. Random Struct. Algorithms 24(3), 234–248 (2004)MathSciNet CrossRef MATH
  23.Jegourel, C., Legay, A., Sedwards, S.: Cross-entropy optimisation of importance sampling parameters for statistical model checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 327–342. Springer, Heidelberg (2012)CrossRef
  24.Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218–234. Springer, Heidelberg (2009)CrossRef
  25.Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)CrossRef
  26.Lassaigne, R., Peyronnet, S.: Probabilistic verification and approximation. Ann. Pure Appl. Logic 152(1–3), 122–131 (2008)MathSciNet CrossRef MATH
  27.Lasserre, J.B.: Moments, Positive Polynomials and Their Applications. Imperial College Press Optimization Series, vol. 1. World Scientific, Singapore (2011)
  28.McClain, D.A., Hug, C.C.: Intravenous fentanyl kinetics. Clin. Pharmacol. Ther. 28(1), 106–114 (1980)CrossRef
  29.Monniaux, D.: Abstract interpretation of probabilistic semantics. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 322–339. Springer, Heidelberg (2000)CrossRef
  30.Neumaier, A.: Clouds, fuzzy sets and probability intervals. Reliable Comput. 10(4), 249–272 (2004)MathSciNet CrossRef MATH
  31.Rump, S.: INTLAB - INTerval LABoratory. In: Csendes, T. (ed.) Developments in Reliable Computing, pp. 77–104. Kluwer Academic Publishers, Berlin (1999)CrossRef
  32.Sankaranarayanan, S., Chakarov, A., Gulwani, S.: Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In: PLDI 2013, pp. 447–458. ACM Press (2013)
  33.Shafer, G.: A Mathematical Theory of Evidence. Princeton University Press, Princeton (1976)MATH
  34.Shafer, S.L., Siegel, L.C., Cooke, J.E., Scott, J.C.: Testing computer-controlled infusion pumps by simulation. Anesthesiology 68, 261–266 (1988)CrossRef
  35.Shmarov, F., Zuliani, P.: Probreach: verified probabilistic delta-reachability for stochastic hybrid systems. In: HSCC 2015, pp. 134–139 (2015)
  36.Steinhardt, J., Tedrake, R.: Finite-time regional verification of stochastic non-linear systems. Int. J. Robot. Res. 31(7), 901–923 (2012)CrossRef
  37.Sun, J., Huang, Y., Li, J., Wang, J.M.: Chebyshev affine arithmetic based parametric yield prediction under limited descriptions of uncertainty. In: ASP-DAC, pp. 531–536. IEEE Computer Society Press (2008)
  38.Terejanu, G., Singla, P., Singh, T., Scott, P.D.: Approximate interval method for epistemic uncertainty propagation using polynomial chaos and evidence theory. In: ACC 2010 (2010)
  39.Williamson, R.C., Downs, T.: Probabilistic arithmetic: numerical methods for calculating convolutions and dependency bounds. J. Approximate Reasoning 4(2), 89–158 (1990)MathSciNet CrossRef MATH
  40.Xiu, D.: Numerical Methods for Stochastic Computation: A Spectral Method Approach. Princeton University Press, Princeton (2010)MATH
  41.Younes, H.L.S., Simmons, R.G.: Statistical probabilitistic model checking with a focus on time-bounded properties. Inform. Comput. 204(9), 1368–1409 (2006)MathSciNet CrossRef MATH
  
• 作者单位：Olivier Bouissou (16)
  Eric Goubault (15)
  Sylvie Putot (15)
  Aleksandar Chakarov (17)
  Sriram Sankaranarayanan (17)
  
  16. CEA, LIST, Gif-sur-Yvette, France
  15. LIX, Ecole Polytechnique, CNRS, Université Paris-Saclay, Paris-Saclay, France
  17. University of Colorado, Boulder, USA
  
• 丛书名：Tools and Algorithms for the Construction and Analysis of Systems
• ISBN：978-3-662-49674-9
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

We consider the problem of reasoning about the probability of assertion violations in straight-line, nonlinear computations involving uncertain quantities modeled as random variables. Such computations are quite common in many areas such as cyber-physical systems and numerical computation. Our approach extends probabilistic affine forms, an interval-based calculus for precisely tracking how the distribution of a given program variable depends on uncertain inputs modeled as noise symbols. We extend probabilistic affine forms using the precise tracking of dependencies between noise symbols combined with the expectations and higher order moments of the noise symbols. Next, we show how to prove bounds on the probabilities that program variables take on specific values by using concentration of measure inequalities. Thus, we enable a new approach to this problem that explicitly avoids subdividing the domain of inputs, as is commonly done in the related work. We illustrate the approach in this paper on a variety of challenging benchmark examples, and thus study its applicability to uncertainty propagation.