## Synthesis of Uninitialized Systems

*
Thomas A. Henzinger,
Sriram C. Krishnan, Orna Kupferman, and Freddy Y.C. Mang*

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

*Proceedings of the
29th International Colloquium on Automata, Languages, and Programming*
(ICALP),
Lecture Notes in Computer Science 2380,
Springer, 2002, pp. 644-656.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2002 Springer.