testb handles the test in [?Q]P by assuming the test succeeds with an implication Q→P, because test ?Q can only make a transition when formula Q holds true.
[?Q]P
Q→P
?Q
Q
Other tactics such as chase and unfold also use this axiom.