This paper focuses on the so called controller synthesis problem, which addresses the question of how to limit the internal behavior of a given system implementation to meet its
specification, regardless of the behavior enforced by the environment. We consider this problem in the probabilistic setting,
where the underlying model has both probabilism and nondeterminism and the nondeterministic choices in some states are assumed
to be controllable while the others are under the control of an unpredictable environment. As for the specification, it is
defined by probabilistic computation tree logic. We show that under the restriction that the controller exploits only Markovian randomized strategy, the existence of such a controller is decidable, which is done by a reduction to the decidability of first-order theory
for reals. This also gives rise to an algorithm which can synthesize the controller if it does exist.