The talk presents experiences in automatically verifying or exploring dynamic, asynchrnously communicating systems specified in operational UML. The BDD-based methods which have been successful for hardware and static, synchronous systems turn out to work badly in the presence of  asynchronous, buffered communication and dynamic object creation and deletion. Explicitly distinguishing discrete state components shows greater promise, as demonstrated via two different approaches. Extending such techniques with an efficient handling of arithmetical data remains a challenge, but constitutes a prerequisite for verifying data-intensive dynamic systems.