\mu-calculus synthesis
----------------------

In system synthesis, we transform a specification into a system that
is guaranteed to satisfy the specification.  When the system is open,
it interacts with an environment via input and output signals and its
behavior depends on this interaction.  An open system should satisfy
its specification in all possible environments. In addition to the
input signals that the system can read, an environment can also have
internal signals that the system cannot read. In the above setting, of
{\em synthesis with incomplete information\/}, we should transform a
specification that refers to both readable and unreadable signals into
a system whose behavior depends only on the readable signals.  In this
work we solve the problem of synthesis with incomplete information for
specifications in $\mu$-calculus.  Since many properties of systems
are naturally specified by means of fixed points, the $\mu$-calculus
is an expressive and important specification language.  Our results
and technique generalize and simplify previous work on synthesis. In
particular, we prove that the problem of $\mu$-calculus synthesis with
incomplete information is EXPTIME-complete.  Thus, it is not harder
than the satisfiability or the synthesis problems for this logic.