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.