Open Systems in Reactive Environments: Control and Synthesis
============================================================

We study the problems of synthesizing open systems as well as
controllers for open systems. We deal with specifications given as
formulas of the branching temporal logic CTL* and its sub-logic CTL.
A key aspect of our work is that we deal with {\em reactive}
environments. These are environments that can disable some of their
responses along the interaction with the system.

We show tight complexity bounds for the solutions to these problems
with the upper bounds being established using automata-theoretic
techniques.  When the answer to a problem is positive, it is possible
to synthesize the desired finite-state system or controller.  For CTL
specifications, the problem of synthesizing an open system as well as
that of synthesizing a controller are 2EXPTIME-complete in the size of
the specification. For CTL* specifications, both problems are
3EXPTIME-complete.  Thus, in a sense, reactive environments constitute
a provably harder setting for the synthesis of open systems and the
synthesis of controllers for them.