Synthesis of uninitialized systems
==================================
The sequential synthesis problem, which is closely related to Church's
solvability problem, asks, given a specification in the form of a
binary relation between input and output streams, for the construction
of a finite-state stream transducer that converts inputs to
appropriate outputs. For efficiency reasons, practical sequential
hardware is often designed to operate without prior initialization.
Such hardware designs can be modeled by uninitialized state machines,
which are required to satisfy their specification if started from any
state.
In this paper we solve the sequential synthesis problem for
uninitialized systems, that is, we construct uninitialized
finite-state stream transducers. We consider specifications given by
LTL formulas, deterministic, nondeterministic, universal, and
alternating Buchi automata. We solve this uninitialized synthesis
problem by reducing it to the well-understood initialized synthesis
problem. While our solution is straightforward, it leads, for some
specification formalisms, to upper bounds that are exponentially worse
than the complexity of the corresponding initialized problems.
However, we prove lower bounds to show that our simple solutions are
optimal for all considered specification formalisms. We also study
the problem of deciding whether a given specification is
uninitialized, that is, if its uninitialized and initialized synthesis
problems coincide. We show that this problem has, for each
specification formalism, the same complexity as the equivalence
problem.