A nondeterministic program logic (Q1091387)

There exist different proofs that the deterministic dynamic logic is strictly less expressive than its nondeterministic version [cf., e.g., the paper of the reviewer and \textit{M. A. Taitslin}, Inf. Control 57, 48- 55 (1983; Zbl 0537.68037)]. In all proofs, a formula of nondeterministic dynamic logic which is proved to be intranslatable into any formula of deterministic dynamic logic, actually contains no test in its programs. M. Taitslin's question was: is every formula of nondeterministic dynamic logic translatable into a formula of the same logic such that every of its programs is either deterministic or contains no test? The paper answers that question negatively.