Program Verification using Reinforcement Learning

par/by Sami Zhioua
Université Laval

In this talk, we show how we successfully applied Reinforcement Learning on a program verification problem. In program verification, the goal is typically to check whether a system implementation (program, physical device, protocol, etc.) conforms to its pre-established specification. Generally, equivalence is expected between the two. Several equivalence notions with different levels of abstraction exist in the literature (e.g. trace, failure, bisimulation, etc.). However, in the verification of probabilistic systems, a more appropriate approach would be a notion of distance or divergence that quantifies how far apart the processes are. The algorithm we developed approximates the divergence between a system implementation (given as a black-box) and a specification by solving a Markov Decision Process (MDP). The key idea is to define correctly the MDP in such a way that the optimal value corresponds to the divergence between the systems. This optimal value can then be estimated by reinforcement learning methods. The algorithm can be tailored to several known equivalence notions: trace, ready, failure, etc. and a new one (K-moment equivalence) which is stronger than trace but weaker than bisimulation. Finally, we point out how the algorithm can be extended to approximate the divergence between MDPs which suggests an interesting contribution to a theory of approximations.