Disproving Reachability in Probabilistic Term Rewriting
Authors: J.-C. Kassing, M. Leven Rosarius, H. Nagel, and J. Giesl
Reachability is a central question in term rewriting: can a given target term (e.g., an error state) be reached from a start term? It is also an important property in confluence analysis, and corresponding tools compete in the annual confluence competition. An interesting generalization of this problem is handling programs that can make random choices during execution. For such probabilistic programs, reachability becomes a quantitative property instead of a qualitative one: instead of asking whether the target is reachable, one asks with which probability it is reached. We lift reachability analysis from ordinary term rewriting to probabilistic term rewrite systems. To do so, we formalize the maximal probability of reaching a target term and adapt two techniques for analyzing reachability (based on symbol transition graphs and on term orderings) to compute upper bounds on this probability.