High-Quality Synthesis Against Stochastic Environments
======================================================

In the classical synthesis problem, we are given a linear temporal
logic (LTL) formula $\psi$ over sets of input and output signals, and
we synthesize a transducer that realizes $\psi$: with every sequence
of input signals, the transducer associates a sequence of output
signals so that the generated computation satisfies $\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 $\FLTL$ is a multi-valued
logic that augments LTL with quality operators.  The satisfaction
value of an $\FLTL$ 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
$\FLTL$. 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. The complexity stays 2EXPTIME also 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.