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.
- 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
Thanks to Reinforcement Learning, the tool can consider huge systems with
more than 1040 states ! Note that classical verification
algorithms cannot go beyond 1012 sates.
RL-Div has been implemented using Java programming language. The Reinforcement
Learning algorithm we used is Q-Learning.
Snapshot of RL-Div
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.