  In the classical synthesis problem, we are given an LTL formula psi over sets
of input and output signals, and we synthesize a transducer that realizes psi.
One weakness of automated synthesis in practice is that it pays no attention to
the quality of the synthesized system. Indeed, the classical setting is
Boolean: a computation satisfies a specification or does not satisfy it.
Accordingly, while the synthesized system is correct, there is no guarantee
about its quality. In recent years, researchers have considered extensions of
the classical Boolean setting to a quantitative one. The logic LTL[F] is a
multi-valued logic that augments LTL with quality operators. The satisfaction
value of an LTL[F] formula is a real value in [0,1], where the higher the value
is, the higher is the quality in which the computation satisfies the
specification.
  Decision problems for LTL become search or optimization problems for LFL[F].
In particular, in the synthesis problem, the goal is to generate a transducer
that satisfies the specification in the highest possible quality.
  Previous work considered the worst-case setting, where the goal is to
maximize the quality of the computation with the minimal quality. We introduce
and solve the stochastic setting, where the goal is to generate a transducer
that maximizes the expected quality of a computation, subject to a given
distribution of the input signals. Thus, rather than being hostile, the
environment is assumed to be probabilistic, which corresponds to many realistic
settings. We show that the problem is 2EXPTIME-complete, like classical LTL
synthesis, and remains so in two extensions we consider: one that maximizes the
expected quality while guaranteeing that the minimal quality is, with
probability $1$, above a given threshold, and one that allows assumptions on
the environment.
