Toward Implicit Learning for the Compositional Verification of Markov Decision Processes

In this paper, we propose an automated compositional verification using implicit learning to verify Markov Decision Process (MDP) against probabilistic safety properties. Our approach, denoted ACV uIL (Automatic Compositional Verification using Implicit Learning), starts by encoding implicitly the MDP components by using compact data structures. Then, we use a sound and complete symbolic assumeguarantee reasoning rule to establish the compositional verification process. This rule uses the CDNF learning algorithm to generate automatically the symbolic probabilistic assumptions. Experimental results suggest promising outlooks for our approach.