Abstract of Paper

$\mu$-calculus Synthesis
by Orna Kupferman and Moshe Y. Vardi


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 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.