Modeling languages usually support two kinds of nondeterminism, an external one for interactions of a system with its environment, and one that stems from under-specification as familiar in models of behavioral requirements. Both forms of nondeterminism are resolvable by composing a system with an environment model and by refining under-specified behavior (respectively). Modeling languages usually donÆt support nondeterminism that is persistent in that neither the composition with an environment nor refinements of under-specification will resolve it. Persistent nondeterminism is used, e.g., for modeling faulty systems. We present a formal semantics for UML state machines enriched with an operator ôpersistent choiceö that models persistent nondeterminism. This semantics is based on abstract models (mu-automata with a novel refinement relation) and a sound three-valued satisfaction relation for properties expressed in the mu-calculus.\r\n