Proper:a Tool For Analyzing Termination And Assertions For Affine Probabilistic Programs

The concept of “Internet of things” promotes the development of science and technology in various intelligent scenarios such as smart city and smart home.Seamless experience of multi scenario application has become the cornerstone of smart life.Intelligent devices can not directly observe the relevant factors,but through network communication and other means to perceive environmental changes and user needs,and make decisions under uncertain conditions.In real life,uncertainty is also a common problem,which makes us need to use prerequisite knowledge and deductive reasoning combined with uncertain data to infer and estimate the possibility of events.Probability is an important tool for expressing imprecise and incomplete knowledge.Probability programming is an important method to infer under uncertain conditions.It is an important step from the research laboratory to the real world.It combines probabilistic reasoning model with Turing complete programming language,unifies the formal description of calculation and uncertain knowledge,and can effectively deal with complex relational models and uncertain problems.In this thesis,we present a tool for analyzing and verifying affine probability programs,namely,PROPER.First of all,under the semantic framework based on classical imperative programs,we define a clear and expressive probabilistic programming language that supports more than ten probability distributions,which is helpful for the construction of probabilistic reasoning models.In addition,in order to ensure that the probabilistic reasoning model has good reliability,correctness and stability,we analyze and verify it from two aspects.On the one hand,PROPER can analyze the termination of affine probability programs qualitatively and quantitatively.We extend the traditional linear rank supermartingale to polynomial rank supermartingale,and verify it by synthesizing polynomial rank supermartingales.Qualitative analysis aims to verify whether a probabilistic program terminates with probability 1(almost-sure termination).Quantitative analysis aims to calculate the upper bound of the expected termination time(expectation problem)and the number of steps that make the termination probability decline exponentially,namely concentration problem.On the other hand,PROPER can calculate the probability interval of an assertion.We use static analysis to explore as many different program paths as possible to analyze the probability that the assertion is correct at the end of each path.When the coverage of the explored program paths is high enough,it can be regarded as analyzing the whole program.It is helpful to analyze the influence of variable uncertainty on the results of probabilistic program,and has potential value in the field of artificial intelligence such as incomplete knowledge processing,meta-reasoning,risk analysis,cognitive search engines and so on.Our experiments show that PROPER is effective for analyzing various affine probability programs.