  In this paper, we investigate the problem of synthesizing strategies for
linear temporal logic (LTL) specifications that are interpreted over finite
traces -- a problem that is central to the automated construction of
controllers, robot programs, and business processes. We study a natural variant
of the finite LTL synthesis problem in which strategy guarantees are predicated
on specified environment behavior. We further explore a quantitative extension
of LTL that supports specification of quality measures, utilizing it to
synthesize high-quality strategies. We propose new notions of optimality and
associated algorithms that yield strategies that best satisfy specified quality
measures. Our algorithms utilize an automata-game approach, positioning them
well for future implementation via existing state-of-the-art techniques.
