Refinement Sensitive Formal Semantics of State Machines With Persistent Choice

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 – μ-automata with a novel refinement relation – and a sound three-valued satisfaction relation for properties expressed in the μ-calculus.