Abstract. This work deals with Markov processes that are defined over an uncountable state space (possibly hybrid) and embedding non-determinism in the shape of a control structure. The contribution looks at the problem of optimization, over the set of allowed controls, of probabilistic specifications defined by automata -- in particular, the focus is on deterministic finite-state automata. This problem can be reformulated as an optimization of a probabilistic reachability property over a product process obtained by taking the cross product of the model for the specification and of the model of the system. Optimizing over automata-based specifications thus leads to maximal or minimal probabilistic reachability properties over finite and infinite horizons. For both setups, the contribution shows that these problems can be sufficiently tackled with memoryless (Markov) policies. This outcome has relevant computational repercussions: in particular, the work shows that a discretization procedure can be set up leading to optimization problems over Markov decision processes. Further, the discretization is associated with exact error bounds. The technique is experimentally tested on a case study.