Abstract:

Assume-Guarantee reasoning is an efficient means of synthetic verification of label transition systems. Recently, Assume-Guarantee reasoning has been used in verifying probabilistic systems. In the phase of reasoning, the learning of assume is accomplished by L start algorithm. In the paper, we propose a new method of Assume-Guarantee Reasoning for probabilistic systems. Firstly, a component of the composed system is abstracted directly to obtain an initial hypothesis. Secondly, by iterating with the AssumeGuarantee rule, the hypothesis is refined repeatedly. At last, a proper hypothesis is obtained to prove the correctness of the conclusion, or a counterexample is obtained to prove that the conclusion is incorrect.

Key words: assume-guarantee verification;abstraction refinement;probabilistic automata;probabilistic timed automata;compositional verification