Learning-based symbolic assume-guarantee reasoning for Markov decision process by using interval Markov process |
| |
Authors: | Redouane Bouchekir Mohand Cherif Boukala |
| |
Affiliation: | 1.MOVEP, Computer Science Department,USTHB,Algiers,Algeria |
| |
Abstract: | Many real-life critical systems are described with large models and exhibit both probabilistic and non-deterministic behaviour. Verification of such systems requires techniques to avoid the state space explosion problem. Symbolic model checking and compositional verification such as assume-guarantee reasoning are two promising techniques to overcome this barrier. In this paper, we propose a probabilistic symbolic compositional verification approach (PSCV) to verify probabilistic systems where each component is a Markov decision process (MDP). PSCV starts by encoding implicitly the system components using compact data structures. To establish the symbolic compositional verification process, we propose a sound and complete symbolic assume-guarantee reasoning rule. To attain completeness of the symbolic assume-guarantee reasoning rule, we propose to model assumptions using interval MDP. In addition, we give a symbolic MTBDD-learning algorithm to generate automatically the symbolic assumptions. Moreover, we propose to use causality to generate small counterexamples in order to refine the conjecture assumptions. Experimental results suggest promising outlooks for our probabilistic symbolic compositional approach. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|