The figure below demonstrates the effect of systematic exploration along the live run while we have limited view of the system. The yellow part is the parts that we can manage to check. The other parts would be missed because we do not have snapshots from all the nodes.
The figure below, depicts the coverage rate of symbolic execution. As you can see the yellow part which are checked by SE, scattered along the model space and hence most of them are irrelative. On the other hand, the advantage is that we are totally prepared for the near future and we do not miss any spot.
Hence, although systematic modelchecking might be more useful for bug finding, symbolic execution fits more for the sake of execution steering.
In other words, we have two purpose of modelchecking by live run:
The normal model checker fulfill the first objective: it might not prepare us for all the events that are about to happen (because of in flight messages, missing snapshots that generate the message and so on), but all the state that are checked are relevant; they really can happen in the step.
On the other hand, symbolic execution fulfills the second objective: I would be prepared for any kind of message that could happen in near future. But, most of events that I am prepared for are totally irrelevant, because there precondition of them are not hold by the system. e.g. I am prepared by a join message from node i which is far far away, but the state of this node will never issue such a message.