Testing Probabilistic Equivalence Through Reinforcement Learning

We propose a new approach to verification of probabilistic processes for which the model may not be available. We use a technique from Reinforcement Learning to approximate how far apart two processes are by solving a Markov Decision Process. If two processes are equivalent, the algorithm will return zero, otherwise it will provide a number and a test that witness the non equivalence. We suggest a new family of equivalences, called K-moment, for which it is possible to do so. The weakest, 1-moment equivalence, is trace-equivalence. The others are weaker than bisimulation but stronger than trace-equivalence.

• Type: Conference
• Year: 2006
• Where: FSTTCS
• Authors: Josee Desharnais, François Laviolette, Sami Zhioua
• Keywords: FSTTCS 2006, Markov Decision Process, Probabilistic Processes, Reinforcement Learning, Software Engineering