What is RL-Div ?
RL-Div is a software tool that allows to compute the relative divergence (distance) between two systems (a Specification and an Implementation). This will be useful to answer the following question : to which degree an implementation (Software, telecommunication protocol, etc.) is conforming to its pre-established specification. And in case the systems are different, RL-Div returns the test (sequence of actions) witnessing the most this divergence.

RL-Div Features
- Unlike the majority of works in the formal verification literature, RL-Div does not suppose the knowledge of the two models (implementation and specification) to proceed. Only the model of the specification is required. For the implementation, only the possibility of interacting with it is necessary. 

- The tool is based on an efficient Reinforcement Learning algorithm. Reinforcement Learning is the branch of Artificial Intelligence which is particularly efficient in the presence of uncertainty.

- RL-Div supports several known equivalence notions : Trace equivalence, Ready equivalence, Failure equivalence, and Barb equivalence. In addition, it comes with a new family of equivalence notions, called k-moment, which can be a good compromise between Bisimulation (too strong) and Trace Equivalence (too weak).

- Thanks to Reinforcement Learning, the tool can consider huge systems with more than 10⁴⁰ states ! Note that classical verification algorithms cannot go beyond 10¹² sates.

Implementation
RL-Div has been implemented using Java programming language. The Reinforcement Learning algorithm we used is Q-Learning.

Snapshot of RL-Div

Demo
The following is a simple demo of RL-Div. The demo is an applet so you should install Java plugin into your browser in order to visualize the animation. When you press run, the applet shows how the algorithm runs. Actually, the algorithm tries to identify the difference between the two systems : implementation and specification. The red colour means that the algorithm is detecting big difference between the systems in the specified component. The white colour, however, indicates that the systems are very similar.