  Finite-state controllers (FSCs), such as plans with loops, are powerful and
compact representations of action selection widely used in robotics, video
games and logistics. There has been steady progress on synthesizing FSCs in
deterministic environments, but the algorithmic machinery needed for lifting
such techniques to stochastic environments is not yet fully understood. While
the derivation of FSCs has received some attention in the context of discounted
expected reward measures, they are often solved approximately and/or without
correctness guarantees. In essence, that makes it difficult to analyze
fundamental concerns such as: do all paths terminate, and do the majority of
paths reach a goal state?
  In this paper, we present new theoretical results on a generic technique for
synthesizing FSCs in stochastic environments, allowing for highly granular
specifications on termination and goal satisfaction.
