Some issues with nondeterminism could be handled by converting the system to a deterministic version, but with extra inputs representing the nondeterminism of the original system. I can well imagine this being difficult in practice.