  This paper deals with the problem of automatically and correctly controlling
infinite-state reactive programs to achieve LTL goals. Applications include
adapting a program to new requirements, or to repair bugs discovered in the
original specification or program code. Existing approaches are able to solve
this problem for safety and some reachability properties, but require an a
priori template of the solution for more general properties. Fully automated
approaches for full LTL exist, reducing the problem into successive finite LTL
reactive synthesis problems in an abstraction-refinement loop. However, they do
not terminate when the number of steps to be completed depends on unbounded
variables. Our main insight is that safety abstractions of the program are not
enough -- fairness properties are also essential to be able to decide many
interesting problems, something missed by existing automated approaches. We
thus go beyond the state-of-the-art to allow for automated reactive program
control for full LTL, with automated discovery of the knowledge, including
fairness, of the program needed to determine realisability. We further
implement the approach in a tool, with an associated DSL for reactive programs,
and illustrate the approach through several case studies.
