Testing probabilistic equivalence through Reinforcement Learning

详细信息    查看全文

• 作者：José ; e Desharnais^a ; ^{Josee.Desharnais@ift.ulaval.ca} ; Franç ; ois Laviolette^a ; ^{Francois.laviolette@ift.ulaval.ca} ; Sami Zhioua^b ; ^{zhioua@kfupm.edu.sa}
• 关键词：Verification ; Stochastic systems ; Markov processes ; Distance ; Divergence ; Reinforcement Learning ; Testing ; Equivalence relations
• 刊名：Information and Computation
• 出版年：2013
• 出版时间：June, 2013
• 年：2013
• 卷：227
• 期：Complete
• 页码：21-57
• 全文大小：764 K

文摘

Checking if a given system implementation respects its specification is often done by proving that the two are ¡°equivalent¡±. The equivalence is chosen, in particular, for its computability and of course for its meaning, that is, for its adequacy with what is observable from the two systems (implementation and specification). Trace equivalence is easily testable (decidable from interaction), but often considered too weak; in contrast, bisimulation is accepted as the canonical equivalence for interaction, but it is not testable. Richer than an equivalence is a form of distance: it is zero between equivalent systems, and it provides an estimation of their difference if the systems are not equivalent. Our main contribution is to define such a distance in a context where (1) the two systems to be compared have a stochastic behavior; (2) the model of one of them (e.g., the implementation) is unknown, hence our only knowledge is obtained by interacting with it; (3) consequently the target equivalence (observed when distance is zero) must be testable. To overcome the problem that the model is unknown, we use a Reinforcement Learning approach that provides powerful stochastic algorithms that only need to interact with the model.

Our second main contribution is a new family of testable equivalences, called K-moment. The weakest of them, 1-moment equivalence, is trace equivalence; as K grows, K-moment equivalences become finer, all remaining, as well as their limit, weaker than bisimulation. We propose a framework to define (and test) a bigger class of testable equivalences: Test-Observation-Equivalences (TOEs), and we show how they can be made coarser or not, by tuning some parameters.