Temporal Synthesis for Bounded Systems and Environments
=======================================================
{\em Temporal synthesis} is the automated construction of a system
from its temporal specification. It is by now realized that requiring
the synthesized system to satisfy the specifications against all
possible environments may be too demanding, and, dually, allowing all
systems may be not demanding enough; systems and environments that are
too large may not be feasible in practice. In this work we study {\em
bounded temporal synthesis}, in which bounds on the sizes of the state
space of the system and the environment are additional parameters to
the synthesis problem. This study is motivated by the fact that such
bounds may indeed change the answer to the synthesis problem, as well
as the theoretical and computational aspects of the synthesis problem.
In particular, a finer analysis of synthesis, which takes system and
environment sizes into account, yields deeper insight into the
quantificational structure of the synthesis problem and the
relationship between strong synthesis -- there exists a system such
that for all environments, the specification holds, and weak synthesis
-- for all environments there exists a system such that the
specification holds.
We first show that unlike the unbounded setting, where determinacy of
regular games implies that strong and weak synthesis coincide, these
notions do not coincide in the bounded setting. We then turn to study
the complexity of deciding strong and weak synthesis. We show that
bounding the size of the system or both the system and the
environment, turns the synthesis problem into a search problem, and
one cannot expect to do better than brute-force search. In particular,
the synthesis problem for bounded systems and environment is
$\Sigma^P_2$-complete (in terms of the bounds, for a specification
given by a deterministic automaton). We also show that while bounding
the environment may lead to the synthesis of specifications that are
otherwise unrealizable, such relaxation of the problem comes at a high
price from a complexity-theoretic point of view.